|
GenBuf writes only what it read before
-- We cheat to avoid explosion
vmode stuck_input_on_0
{
%for i in 0..3 do
define DI(%{i}*32..%{i+1}*32-1) := 0H ;
%end
}
vunit genbuf_is_not_creative
{
"all the data sent out of GenBuf was once read into GenBuf"
inherit stuck_input_on_0 ;
%for j in 0..1 do
assert "Data sent to receivier %{j} is not invented by GenBuf"
always (fell(BtoR_REQ(%{j})) -> (DO(0..31)=0H) );
%end
}
Results
| 
