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 ;

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) );


    About IBMPrivacyContact