In reply to hisingh:
By doing the cover to address the increment of the now_serving also increments the ticket
thru the inc_ticket()
Thus, your ticket counter went something like 2, 4, 6, 8 instead of 1, 2, 3, …
You don’t need the cover statement, the assert st does that anyway.
And why split the increment of those counters in 2 places?
property reqack_unique;
int v_serving_ticket;
@(posedge clk) ( $rose(rdy), v_serving_ticket = ticket , inc_ticket() ) |->
strong( (( now_serving == v_serving_ticket ) && ack ) [ ->1 ]) ;
// ================================================================
endproperty
a_property : assert property ( reqack_unique )
now_serving =now_serving+1; else begin // pass or fail, need to increment now_serving
now_serving = now_serving + 1 ; // Increment for Each Pass / Fail
$display(" TIME : %0t AB FAIL " , $time ) ;
end
/* Doing the cover to increment the now serving also increments the ticket
thru the inc_ticket()
c_property : cover property ( reqack_unique )
begin
now_serving = now_serving + 1 ; // Increment for Each Pass / Fail
$display(" TIME : %0t AB PASS " , $time ) ;
end */