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


    About IBMPrivacyContact