Subject: Re: [sv-ac] False firing of assertions examples.
From: Adam Krolnik (krolnik@lsil.com)
Date: Thu Sep 05 2002 - 07:55:48 PDT
Hi Ambar;
>C1. Instead of if (s1) assert (!s2), I would expect:
>assert_strobe(!s1 | !s2);.
Remember, this is a model/example of larger things. I too would write
this simple assertion as you show. But there will be people who have to
write assertions like:
if (enable)
case (command)
C1: ...
C2: begin
if (inp1) out1 = inp1 + inp2;
if (inp4) out4 = inp4 - inp2;
case ({inp5,inp6})
assert ... // complex antecedent to this assert.
So the 'if (s1)' is a very simple model of possibly complex antecedents
like the above code fragment.
>would take care of false firing due to simulator time-steps
>(not #delays).
As the example shows (when you run it) that without the disable, use
of assert_strobe only fails to suppress the error. This can be shown
be running the example with the options +define+STROBE. The results
are:
0 s1 = 0, s2=0
10 s1 = 1, s2=0
Error at time 20 - s1 and s2 are true.
20 s1 = 0, s2=1
30 s1 = 0, s2=0
$finish at simulation time 80
It is only when you run with assert_strobe AND the disable that you
suppress the false firing (+define+STROBE+PREVENT). Try it, you'll
see.
>*outside* the combinational block. For example, if we had a
>mechanism in SystemVerilog to specify the following:
>evaluate <named_assertion> at <clock_edge>
I completely agree with you as I have proposed a method to assign
a global clock to all (some) assertions within a hierarchy.
Thus your methodology will not work as these examples show.
The point about #delays in a simulation is not something that can
be ignored. For example, we use assertions in our DSP core and verify
that with a core only testbench setup. We then instantiate the core
in our SOC testbench which contains #delays from IO pads, other
coding styles, etc. You can't make a recommendation as you have as
noone will then recode assertions because a different system now has
some delay.
To your questions:
>Q1. Why not use assert_strobe always? This would take care of
>any false firing due to simulator timestep.
See the examples, run them, test them. The examples show with a
running commentary why assert_strobe is not fully sufficient.
>Q2. How would be reuse the same combinational block assertion
>in multiple clock contexts? Are we required to change the assertion
>every-time we change the clock?
Let me extend this question with two examples. Note the question
remains - how do I write an assertion for these cases?
module dmux3 (o, i2, i1, i0, s);
// synopsys template
parameter WIDTH = 1;
output [WIDTH-1:0] o;
reg [WIDTH-1:0] o;
input [WIDTH-1:0] i2, i1, i0;
input [2:0] s; //solidify { 'X(onehot(s)) }
//expect:onehot(exactly1(s[2:0])) msg=("sel is %b", s);
//surefire lint_off CSEFUL
always @(i0 or i1 or i2 or s)
case (1'b1) //synopsys full_case parallel_case
s[0]: o = i0;
s[1]: o = i1;
s[2]: o = i2;
endcase // case(s)
//surefire lint_on CSEFUL
endmodule // dmux3
function [1:0] encode4;
input [3:0] onehot; //solidify assume oh {onehot(onehot)}
case (1'b1) //synopsys full_case parallel_case
onehot[0] : encode4 = 2'd0;
onehot[1] : encode4 = 2'd1;
onehot[2] : encode4 = 2'd2;
onehot[3] : encode4 = 2'd3;
endcase
endfunction
Here are two examples (fully real code, unadulterated for this email.)
Both are marked with proprietary solutions to check for illegal
stimulus. How should we write assertions for these components that
do not have a clock entering them. Note, the answer does not involve
adding a port for clock and reset to these nonclocked elements.
Formal tools, solve this by specifying a clock for all properties to
be operated on. We have a requirement to be able to specify a
clock for a hierarchy of properties, but this then makes the assertions
somewhat different from verilog since they require action somewhere else
to actually make them work. E.g.
assert ($onehot(select)) @@(); // Requires global clock to enable this.
This is somewhat strange verilog since there is no clock driving this.
It would be even more strange in this form:
always @(posedge clk)
begin
assert ($onehot(select)) @@(); // Another assertion needing global
clock.
These are important questions - I suggest that we have a discussion
about
them. In particular I don't like the disabling requirement. Anyone up
for proposing that assertions started more than once in the same
timestep
or more than once before the step control occurrs will disable previous
ones?
THanks.
Adam Krolnik
Verification Mgr.
LSI Logic Corp.
Plano TX. 75074
This archive was generated by hypermail 2b28 : Thu Sep 05 2002 - 07:59:02 PDT