|
Sender 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 : {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 designed 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}*32..%{i+1}*32-1));
%end
| 
