#include "rules" 

--------------------- Errors found (for Tutorial) ------------------

define ERROR_FOUND(1) := 0;
define ERROR_FOUND(2) := 0;
define ERROR_FOUND(3) := 0;
define ERROR_FOUND(4) := 0;
define ERROR_FOUND(5) := 0;
define ERROR_FOUND(6) := 0; 

---------------------- Clock and Reset definitions -----------------

define clk := 1;

var RST : boolean;
assign
  init(RST) := 1;
  next(RST) := 0;

---------------------- Receivers definition -------------------------

module receiver_module( RST, BtoR_REQ, DO(0..31) )( RtoB_ACK ) 
{
    
    var RtoB_ACK : boolean;

  assign
    init(RtoB_ACK) := 0;
    next(RtoB_ACK) := case
        RST  : 0;
        else : BtoR_REQ; /* RtoB_ACK must be asserted a cycle after
                            the assertion of BtoR_REQ and deasserted 
                            a cycle after the deassertion of BtoR_REQ
                            this unusually simple specification was
                            made to keep this tutorial simple */ 
    esac;

}

%for i in 0..1 do
    instance receiver_%{i} : receiver_module( RST, BtoR_REQ(%{i}), DO(0..31) )
                                            ( RtoB_ACK( %{i}) );
%end
 
---------------------- Senders definition  -------------------------

module sender_module( RST, BtoS_ACK )( StoB_REQ, DI(0..31) )
{
  var StoB_REQ  : boolean;
  var DI(0..1) : boolean;

  assign
    init(StoB_REQ) := 0;
    next(StoB_REQ) := case
        RST        : 0;
        !StoB_REQ & 
            !BtoS_ACK & !prev(BtoS_ACK) : {0,1}; /* If not asserted
                                                         and not at the end 
                                                         of a transaction
                                                         then a request can
                                                         be made */ 

        StoB_REQ & BtoS_ACK             : 0;          /* If asserted
                                                         and acknowledged 
                                                         deassert */
        else       : StoB_REQ; 
    esac;


/* Note : we use only two bits of the data bus to symbolize data
          while the rest of the bits will be fixed to 0. 
          This is a technique to "save variables" and avoid explosion */

  assign
    init(DI(0..1)) := 0;
    next(DI(0..1)) := case
        RST                 : 0;
        rose(StoB_REQ)      : nondets(2); /* We assert (non deterministic) 
                                             data one cycle after the 
                                             request */
        StoB_REQ & BtoS_ACK : 0;          /* If buffer acknowledged our  
                                             request then invalidate 
                                             the data */  
        else           : DI(0..1);        
    esac;

    define DI(2..31) := 0;

}


%for i in 0..3 do
    instance sender_%{i} : sender_module( RST, BtoS_ACK( %{i} ))
                                        ( StoB_REQ( %{i} ), DI_%{i}_(0..31));
%end