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 does not receive when the queue is full

vmode Queue 
{
-- This is a mode keeping track of buffers queue (which is of depth 4)


  define rose_B2S_ACK := rose(BtoS_ACK(0)) | rose(BtoS_ACK(1))
			             | rose(BtoS_ACK(2)) | rose(BtoS_ACK(3)) ;

  define rose_R2B_ACK := rose(RtoB_ACK(0)) | rose(RtoB_ACK(1)) ;

  define rose_B2R_REQ := rose(BtoR_REQ(0)) | rose(BtoR_REQ(1)) ;
	 
  var old_QC : -1..5 ;
  var Q_counter : -1..5 ;

  assign
	 init(old_QC) := 0 ;
	 next(old_QC) := Q_counter ;

  assign
	 Q_counter := /* Note : Q_counter is assigned NOT next( Q_counter ) */
		case
		  RST :0 ;
		  old_QC=-1                         :-1 ; /* Underflow */
		  old_QC=5                          : 5 ;  /* Overflow */
		  rose_B2S_ACK & prev(rose_R2B_ACK) : old_QC ; /* Both read & write */ 
		  rose_B2S_ACK                      : old_QC + 1 ; 
		  prev(rose_R2B_ACK)                : old_QC-1 ;
		  else                              : old_QC ;
		esac ;
} 

vunit genbuf_does_not_receive_when_queue_full
{
"GenBuf does not receive when the queue is full"

inherit Queue;

%for i in 0..3 do
    assert "GenBuf does not acknowledge sender %{i} when the queue is full"
      always( rose( BtoS_ACK(%{i}) ) -> prev(Q_counter <=3));
%end
}
Results



 
 





    About IBMPrivacyContact