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 keeps FIFO order

vunit genbuf_keeps_fifo_order
{
"GenBuf is queue keeps order i.e. GenBuf is indeed FIFO"

  inherit Queue;
  define some_data_is_written := (fell(BtoR_REQ(0)) | fell(BtoR_REQ(1)));

  %for j in 1..4 do
    assert "If data is read when the queue is at depth %{j} then the data will be written in %{j} write operations"
      always (data_x_is_read & (Q_counter = j)
                        -> next(next_event( some_data_is_written )[j](DO(0..1)=xx(0..1))));
%end
}
Results



 
 


 


    About IBMPrivacyContact