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)

Data read is eventually written

vmode default
{
  var xx(0..1) : boolean;
  assign next(xx(0..1)) := xx(0..1);

  define data_x_is_written :=
       ((fell(BtoR_REQ(0)) | fell(BtoR_REQ(1))) & (DO(0..1)=xx(0..1)));

%for i in 0..3 do
    define  data_x_is_read_from_%{i} :=
        ( rose(BtoS_ACK(i)) & (DI(%{i}*32..%{i}*32+1)=xx(0..1)));

    /* Note : We "cheat" on this point. The bus is read by GenBuf one cycle
              before the rise of BtoS_ACK(i). However, since the sender
              does not release the bus until later - this will do for the
              tutorial. */
%end

  define data_x_is_read :=  ( data_x_is_read_from_0 |  data_x_is_read_from_1
                            | data_x_is_read_from_2 |  data_x_is_read_from_3);
}

vunit data_read_is_eventually_written
{
"Every data word read by GenBuf will be eventually sent out to a receiver"
%for i in 0..3 do
    assert "if sender %{i}  is read and has data then data is eventually written"
      always (data_x_is_read_from_%{i} -> eventually!( data_x_is_written));
%end
}
Results



 
 





    About IBMPrivacyContact