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



    About IBMPrivacyContact