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)

No acknowledge without a request

vunit no_ack_without_a_req 
{
"GenBuf does not acknowledge senders unless requested"
%for i in 0..3 do
    assert 
      always ((BtoS_ACK(%{i})) -> prev(StoB_REQ(%{i})));
%end

%for j in 0..1 do
    assert 
      always ((RtoB_ACK(%{j})) -> prev(BtoR_REQ(%{j})));
%end
}
These assertions mean that an acknowledge signal can only be on if the appropriate request signal was also on during the previous cycle.

Results



 
 





    About IBMPrivacyContact