|
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
| 
