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)

Only one sender at a time

vunit only_one_sender_at_a_time
{
  "Only one sender can send data at any given time."

  %for i in 0..3 do
     %for j in 0..3 do
        %if i != j %then
           assert "The %{i} th and %{j} th senders do not send together"
           always ( !(BtoS_ACK(%{i}) & BtoS_ACK(%{j})));
        %end
     %end
  %end
}
Results



 
 





    About IBMPrivacyContact