I am writing an assertion to check the value of a signal from the DUT against a value I calculated in my assertions module.
On the waveform I see that both the signals do have similar values.
My problem is that the assertions aren’t even triggering!
The code that I have is :
act_vfy is a flag, upon its negedge is when the assertion should trigger!
Similarly I have 16 assertions each to check for 16 values from the DUT which arrives as different signals.
[Ben] Your issue seems to be the sampling regions and when the signals are sampled.
From your description, I believe that you are using something like the following code:
always_ff @(posedge clk)
if(some_condition) act_vfy <= 1'b0;
else act_vfy <= 1'b1;
// act_vfy changes in the NBA region, see below for regions
always_ff @(posedge clk)
if(some_situation) enc_sva <= some_value;
// BAD STYLE because of triggering and sampling regions
// ****
cmd_10_chk_VERY_BAD_STYLE: assert property (@(negedge act_vfy)(1) |->
(enc_sva[8] == enc_dut_8[3:0]) );
// The sampling value for enc_sva[8] is one delta time (i.e., just before)
// act_vfy is falling (i.e., when it was ==1'b1.
// I believe that what you want to express is that
// * When act_vfy went to a zero, then after enc_sva[8] settles,
// (enc_sva[8] == enc_dut_8[3:0])
// Your correct should should then look like this:
always_ff @(posedge clk)
if(some_condition) act_vfy <= 1'b0;
else act_vfy <= 1'b1;
always_ff @(posedge clk)
if(some_situation) enc_sva <= some_value;
// *****************************************
cmd_10_chk_better: assert property (@(posedge clk) $fell(act_vfy) |->
(enc_sva[8] == enc_dut_8[3:0]))
else $error ("Error: encode failed for SVA, %d != %d", enc_sva[8], enc_dut_8 );
// *****************************************
// On a separate note, properties of the type
1'b1 |-> consequent // can be reduced to:
consequent // The 1'b1 antecedent is not needed.
// Similarly I have 16 assertions each to check for 16 values
// from the DUT which arrives as different signals.
// [Ben] Consider using the generate statement if it fits your needs.
// Below is an example of a generate statement, from my SVA Handbook 4th Edition, 2016
generate for (genvar g_i=0; (g_i<8); g_i++) begin
if (g_i >= N)
ap_range_gen: assert property (v==g_i && $rose(a) |-> ##[N:g_i] b);
end endgenerate
However, I can’t use clk in my assertions module as it is a system clock and I am just checking the functionality of a an individual module of the DUT…
The DUT runs on the system clock, and assertions are written in a separate module and is bound to the DUT using the “bind” construct.
So, I would have to approach this issue differently and help is much appreciated.
In reply to ben@SystemVerilog.us:
However, I can’t use clk in my assertions module as it is a system clock and I am just checking the functionality of a an individual module of the DUT…
The DUT runs on the system clock, and assertions are written in a separate module and is bound to the DUT using the “bind” construct.
I fail to understand why you can’t use the DUT clk in the bind. The bind is like instantiating a module (or a checker) inside the DUT; thus, the clock can be passed as an actual argument.
So, I would have to approach this issue differently and help is much appreciated.
See if you can get access to the clock with the bind.
If you still can’t, and you must use a signal as the clocking event, then in your verification module you need to generate a secondary clock based on that event. For example:
bit a, b, c, a_chk;
// a, b, c, are clocked at posedge clk.
// clk period > 5 (in this example)
always @(a) begin
#5 a_chk <= a;
end
apa_b: assert property(
@(negedge a) |-> @(negedge a_chk) b );
// b is sampled delta time before negedge a_chk,
// but b has now settled in value
In reply to ben@SystemVerilog.us:
I have another similar module which is working fine without the system clock!
That’s playing with fire as you’re monkeying around sampling regions.
If you have a situation where it worked, that’s possibly because you’re model has gate-level delays such that your trigger clocking event occurs at a later time than the sampling of your signals.
Advice: Stay clean! Those sampling regions can be tricky!
Ben Cohen http://www.systemverilog.us/ben@systemverilog.us
