|
Data read is eventually written
vmode default
{
var xx(0..1) : boolean;
assign next(xx(0..1)) := xx(0..1);
define data_x_is_written :=
((fell(BtoR_REQ(0)) | fell(BtoR_REQ(1))) & (DO(0..1)=xx(0..1)));
%for i in 0..3 do
define data_x_is_read_from_%{i} :=
( rose(BtoS_ACK(i)) & (DI(%{i}*32..%{i}*32+1)=xx(0..1)));
/* Note : We "cheat" on this point. The bus is read by GenBuf one cycle
before the rise of BtoS_ACK(i). However, since the sender
does not release the bus until later - this will do for the
tutorial. */
%end
define data_x_is_read := ( data_x_is_read_from_0 | data_x_is_read_from_1
| data_x_is_read_from_2 | data_x_is_read_from_3);
}
vunit data_read_is_eventually_written
{
"Every data word read by GenBuf will be eventually sent out to a receiver"
%for i in 0..3 do
assert "if sender %{i} is read and has data then data is eventually written"
always (data_x_is_read_from_%{i} -> eventually!( data_x_is_written));
%end
}
Results
| 
