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 does not send when the queue is empty

vunit genbuf_does_not_send_when_queue_empty
{
"non of BtoS_ACK will assert when queue is full"

inherit Queue;

%for i in 0..1 do
    assert "GenBuf does not request receivers when the queue is empty"
      always (rose(BtoR_REQ(%{i})) -> prev( Q_counter > 0 ));

%end
}
Results



 
 





    About IBMPrivacyContact