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 - sender handshake

vunit genbuf_to_sender_handshake
{
"GenBuf to sender handshake"
 
%for i in 0..3 do   

  assert "In case the sender deasserts its request GenBuf will eventually deassert its acknowledgement"
    always ( !StoB_REQ(%{i}) -> eventually! ( !BtoS_ACK(%{i})));

  assert "GenBuf will not deassert its acknowledgement unless the sender first deasserted its request" 
    always ( BtoS_ACK(%{i}) -> ( BtoS_ACK(i) until_ (!StoB_REQ(%{i}))));
%end
}
Results



 
 


 


    About IBMPrivacyContact