IBM®
Skip to main content
    Israel [change]    Terms of use
 
 
 
    Home    Products    Services & solutions    Support & downloads    My account    
IBM Research

RuleBase Parallel Edition

Formal Verification


Generalized Buffer (PSL/Sugar version)

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



 
 





    About IBMPrivacyContact