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)

Receiver properties

vmode default
{
  define B2R_REQ := BtoR_REQ(0) | BtoR_REQ(1) ; 
}

vunit receiver_ack 
{
"Several receivers acknowledge properties"

%for i in 0..1 do
    assert "GenBuf will deassert its request to receiver %{i} a cycle after receiver %{i} acknowledged the request"
      always (RtoB_ACK(%{i}) -> next(!BtoR_REQ(%{i})));
%end

  assert "GenBuf does not request both receivers at the same time"
    always !(BtoR_REQ(0) & BtoR_REQ(1));

  assert "GenBuf will not make two consecutive requests to receiver 0"
    always (rose(BtoR_REQ(0)) -> next next_event(rose(B2R_REQ))( BtoR_REQ(1)));

  assert "GenBuf will not make two consecutive requests to receiver 1"
    always (rose(BtoR_REQ(1)) -> next next_event(rose(B2R_REQ))( BtoR_REQ(0)));

  assert "GenBuf deasserts BtoR_REQ in the cycle it puts the data on bus"
    always (rose(DO(0..31)!= 0) -> fell(B2R_REQ));
}
Results



 
 


 


    About IBMPrivacyContact