I am modeling an up-down counter and plan to use a set of assertions to check the correctness of its behaviour. The up-down counter is coded like so:
====================================================================
module updncounter (
input clk,
input rstn,
input ld,
input en,
input updn,
input [7:0] ldc,
output [7:0] q
);
logic [7:0] cnt;
always @(posedge clk or rstn) begin
if (!rstn) begin
cnt <= 'h0;
end
else begin
if (ld) begin
cnt <= ldc;
end
else begin
if (en) begin
if (updn) begin
cnt <= cnt + 8'h1;
end
else begin
cnt <= cnt - 8'h1;
end
end
end
end
end
assign q = cnt;
endmodule : updncounter
===================================================================
and its corresponding basic stimulus and assertions as follows:
The immediate (deferred) assertion on the negedge of reset fails at the simulation time when rstn changes from 1 to 0 (that is, at 1ns). I assume that the cause of the failure is that the assertion samples the “q” output from the counter as “X” although the counter’s asynchronous reset block is changing it to “0” at the same timestep.
Any suggestions on what is going wrong and how to get the assertion working by coding it correctly. (I do not want to change the sampling edge of the assertion to “@(posedge rstn)”.)
In reply to verificator:
You can use the final.
Deferred assertions use #0 (for an Observed deferred assertion) or final (for a final deferred assertion in the Postponed region) after the verification directive.
Corrections
upcnt : assert property (
disable iff (!rstn)
@(posedge clk)
(!ld && en && updn) // |-> q == $past(q) + 8'h1 // ERROR
|=> q == $past(q) + 8'h1
);
always @(negedge rstn)
rst_val : assert final (q == 'h0) // <------------------
$display("reset value check passed in %m");
else
$error("reset value check failed in %m");
The change from “#0” to “final” does not work. I would like to understand in what ways is using “final” different from using “#0”.
Also, on the concurrent assertion, my idea of using the overlapping implication operator was that the increment operation is expected to work on any posedge that:
ld is sampled low, and,
en is sampled high, and,
updn is sampled high
Request you to elaborate on why we should use a non-overlapping implication operator.
In reply to verificator:
OOPS! We don’t discuss specific tools (delete the specific tool name and replace it with something like “a simulation tool”.
I modified your code a bit (put everything in one module, added some data and timing info)
assign q = cent; // line 27
always @(negedge rstn)
rst_val : assert final (q == 'h0) // line 56
** Error: 0 CNT reset value check failed in updncounter.rst_cnt q=xxxxxxxx
# Time: 0 ns Scope: updncounter.rst_cnt File: testbench.sv Line: 65
# 1 CNT reset value check passed in updncounter.rst_cnt q=00000000
# ** Error: 1 q reset value check failed in updncounter.rst_val q=xxxxxxxx
// So the q is not seen as updated in the assertion (though final).
// Am not sure why because the final is in the Postponed region ????
Consider Edit code - EDA Playground where I comment always @(negedge rstn)
Immediate assertions can be inside or outside procedural statements. That fixes the problem
// always @(negedge rstn)
rst_val : assert final (q == 'h0)
$display("%t q reset value check passed in %m q=%b", $realtime, q);
else
$error("%t q reset value check failed in %m q=%b", $realtime, q);
// -----------------
rst_cnt : assert final (cnt == 'h0)
$display("%t CNT reset value check passed in %m q=%b", $realtime, cnt);
else
$error("%t CNT reset value check failed in %m q=%b", $realtime, cnt);
# ** Error: 0 q reset value check failed in updncounter.rst_val q=xxxxxxxx
# Time: 0 ns Scope: updncounter.rst_val File: testbench.sv Line: 60
# ** Error: 0 CNT reset value check failed in updncounter.rst_cnt q=xxxxxxxx
# Time: 0 ns Scope: updncounter.rst_cnt File: testbench.sv Line: 65
# 1 CNT reset value check passed in updncounter.rst_cnt q=00000000
# 1 q reset value check passed in updncounter.rst_val q=00000000
If antecedent is true thenat the next cycle q should be equal to the previous value of q + 1’b1.
With the overlapping implication, you are saying:
If antecedent is true then in the SAME cycle q should be equal to the previous value of q + 1’b1. That is not what you want.
Ben Cohen http://www.systemverilog.us/ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home
On the overlapping/non-overlapping implication operator, yes, I now understand that the increment/decrement will start only on the edge that samples the ld to be low (which is the next edge after ld is high in our case).
As for the reset value check, I see that the assertion passes at time t=1ns. However, I am unable to understand:
Can we add such an assertion outside of an procedural block? (After all, we want to check that the q value is 0 only when reset is asserted.)
When will such an assertion be evaluated? I see that the assertions you have coded are evaluated at 0, 1 and 11ns. On what basis have these points of evaluation been chosen by the simulator?
The assertion fails at 0 and 11ns. How do we get a clean assertion at all time stamps?
Any particular reason why you have chosen to add an assertion on cnt (in addition to q)?
OK, here is what is happening and why the assert fails at 1 ns
// You have
always @(posedge clk or rstn) begin
if (!rstn) begin
cnt <= 'h0;
//...
end
always @(negedge rstn) begin
rst_val : assert final (q == 'h0); // ignoring the action block for now
// If inline, it works butassertion is evaluated at every change
rst_inline : assert final (q == 'h0)
$display("%t inline q reset value check passed in %m q=%b", $realtime, q);
else
$error("%t inline q reset value check failed in %m q=%b", $realtime, q);
# 1 inline q reset value check passed in updncounter.rst_inline q=00000000
# 2 CNT reset value check passed in updncounter.rst_cnt q=00000000
# 2 q reset value check passed in updncounter.rst_val q=00000000
# ** Error: 11 inline q reset value check failed in updncounter.rst_inline q=00000001
cnt gets updated in the NBA region.
The assert fina gets evaluated in the ACTIVE region, before the update of cnt and q. Thus, the assert sees the XXXX and it does not see the update (in the NBA region).
In that case, you would need
always @(negedge rstn) begin
#1; assert(...)
The final stuff is really more in the display of the action block.
From my book:
4.6.2.1 Deferred assertion reporting
[1] When a deferred assertion declared with assert #0 passes or fails, the action block is not executed immediately. Instead, the action block subroutine call (or $error, if an assert or assume fails and no action_block is present) and the current values of its input arguments are placed in a deferred assertion report queue associated with the currently executing process. Such a call is said to be a pending assertion report. See Figure 4.6.2.1 for a view of the queue for the deferred action block.
If a deferred assertion flush point (see below and Appendix B) is reached in a process, its deferred assertion report queue is cleared. Any pending assertion reports will not be executed. In the Observed region (for deferred assertion), or Postponed region (for final assertion) of each simulation time step, each pending assertion report that has not been flushed from its queue shall mature, or be confirmed for reporting. Once a report matures, it may no longer be flushed. Then the associated subroutine call (or $error, if the assertion fails and no action block is present (see 4.1.3) is executed in the Observed region for deferred assertion, or in the Postponed region for the final assertion, and the pending assertion report is cleared from the appropriate process’s deferred assertion report queue.
Figure
flush point: (see 4.3.4, 4.6.2.1) [1] A process is defined to have reached a deferred assertion flush point if any of the following occur:
The process, having been suspended earlier due to reaching an event control or wait statement, resumes execution.
The process was declared by an always_comb or always_latch, and its execution is resumed due to a transition on one of its dependent signals.
The outermost scope of the process is disabled by a disable statement.