Subject: Re: [sv-ac] False firing of assertions examples.
From: Ambar Sarkar (ambar.sarkar@paradigm-works.com)
Date: Thu Sep 05 2002 - 04:33:23 PDT
Adam:
My coffee wasn 't that strong this morning...so I forgot to specify what my
questions are!
> I have two questions and some comments regarding the proposed methodology:
So the questions are:
Q1. Why not use assert_strobe always? This would take care of any false
firing due to simulator timestep.
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?
Regards, and a good morning to all.
-Ambar
----- Original Message -----
From: "Ambar Sarkar" <ambar.sarkar@paradigm-works.com>
To: "Adam Krolnik" <krolnik@lsil.com>; <sv-ac@eda.org>
Cc: "Adam Krolnik" <krolnik@lsil.com>
Sent: Thursday, September 05, 2002 7:10 AM
Subject: Re: [sv-ac] False firing of assertions examples.
> Adam,
>
> Excellent examples.
>
> I have two questions and some comments regarding the proposed methodology:
>
> C1. Instead of if (s1) assert (!s2), I would expect:
>
> assert_strobe(!s1 | !s2);.
>
> would take care of false firing due to simulator time-steps (not #delays).
>
> C2. If we are only interested in the assertion at clock edges, a cleaner
> approach (IMHO) would be to associate the clock with the named assertion
> *outside* the combinational block. For example, if we had a mechanism in
> SystemVerilog to specify the following:
>
> evaluate <named_assertion> at <clock_edge>
>
> C2 is especially important since acombinational module may be used in
> multiple instantiations, and each instantiation may be associated with a
> different clock. Specifying the clock with the assertion would mean we
would
> have to rewrite the assertion for every clock or use automatic clock
> inferencing. Unambiguous automatic clock inferencing may not be feasible
in
> all circumstances.
>
> So, the methodology I am suggesting is as follows:
>
> M1. Specify all combinational block assertions as named assert_strobes.
This
> takes care of simulation timestep issues.
> M2. If the signals to this block change due to #delays, associate the
> relevant clock signal with the named assertion separately from the
> assertion, preferably outside the combinational block.
> In other words, specify any applicable clock(there need not be one)
> separately from the assertion.
>
> The advantages of this methodology are
> 1. Not have to worry about how to figure out what the relevant clock is
for
> a combinational block when writing the assertion.
> 2. Promote reuse of assertions. A combinational module can now be used in
10
> different places with 10 different clocks, and we would not have to change
> the assertion code.
> 3. Be able to actually check for cases where any unintended #delay effect
> needs to be caught.
> 4. Not have to deal with these extra disables and checkit steps. Let's the
> designer directly specify exactly what combinational property she is
> interested in, and no more.
>
> Just throwing in my thoughts.
> Regards,
> -Ambar
> ----- Original Message -----
> From: "Adam Krolnik" <krolnik@lsil.com>
> To: <sv-ac@eda.org>
> Cc: "Adam Krolnik" <krolnik@lsil.com>
> Sent: Wednesday, September 04, 2002 7:23 PM
> Subject: [sv-ac] False firing of assertions examples.
>
>
> >
> >
> > Good afternoon all;
> >
> > Here is an example of a false firing of an assertion in a
> > combinatorial block.
> >
> > The heart of the example looks like this:
> >
> > always @(s1 or s2 or d1 or d2)
> > begin
> > ...
> > // We can't have s1 and s2 on otherwise we give bad data.
> > if (s1) assert (! s2);
> >
> > do = s1 & d1 | s2 & d2;
> > end
> >
> > If you ran this on your favorite SystemVerilog simulator, there
> > may be a possibility of this assert statement reporting an error
> > that is false.
> >
> > Here we see the output of $monitor and the assertion error message.
> > 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
> >
> > But wait, time 20 does not show the selects (s1, s2) in that state -
> > whoa!!
> > This is due to intra-timestep value changes inherent in the simulator.
> >
> > Okay, how do we fix this?
> > [ Don't use procedural assertions - use declarative!]
> >
> > On a lighter note there is a way to trade this problem for another,
> > but this other problem is an annoyance to designers.
> >
> > We need to add this statement:
> >
> > disable checkit;
> >
> > This statement will disable the assertion if it was started due to
> > a previous value change (either in the same timestep or a previous
> > step.) This will prevent an assertion from firing if the antecedent
> > path (in our case, s1) changes value such that the assertion is no
> > longer going to be evaluated. A designer will need to add a disable
> > statement for each assertion that they write in a combinatorial
> > block. Failure to add this mandatory disable may result in a false
> > failure of the assertion.
> >
> > In addition to this extra statement (at the beginning of the block)
> > the designer will need to use assert_strobe instead of an immediate
> > assertion. This is because the immediate assertion would have already
> > generated the error message. Use of the strobed assertion will delay
> > the evaluation of the assertion until we know the values are stable.
> >
> > Thus our simple example is now (more complex):
> >
> > always @(s1 or s2 or d1 or d2)
> > begin
> > disable checkit; // disable the assertion ??!! :(
> > ...
> >
> > // We can't have s1 and s2 on otherwise we give bad data.
> > if (s1) checkit: assert_strobe (! s2);
> >
> > // Our functionality that we are preventing.
> > do = s1 & d1 | s2 & d2;
> > end
> >
> > Thus, we should now recommend the following:
> >
> > 1. Use a disable statement FOR EACH assertion in a combinatorial
> > block. Make sure you name your assertion too! This disable
> > shall be placed at the beginning of the block.
> > 2. Use a named (always) assert_strobe statement in combinatorial
> > blocks to allow prevention of false firings.
> >
> > Okay great...
> >
> > Let's hook this up to some other code we have here....
> > Okay, let's run it...
> >
> > 0 s1 = 0, s2=0
> > 10 s1 = 1, s2=0
> > Error(2) at time 20 - s1 and s2 are true.
> > 20 s1 = 1, s2=1
> > 21 s1 = 0, s2=1
> > 30 s1 = 0, s2=0
> > $finish at simulation time 80
> >
> >
> > Hey -- what's the deal!!!! I get an error at time 20 and the $monitor
> > says the selects are both on - this must be real...
> >
> > Wait!! At time 21 (#1 later), the selects are okay - argggh!
> > My other code has a different coding style and it uses # delays,
> > or the IO's have some gate delays within them...
> >
> > Okay, now we have inter-timestep delays that must be accounted for in
> > our assertion methodology...
> >
> >
> > Okay, let's modify our assertion a little bit more to this somewhat
> > strange form.
> >
> > always @(s1 or s2 or d1 or d2)
> > begin
> > disable checkit; // Methodology recommendation #1
> >
> > // We can't have s1 and s2 on otherwise we give bad data.
> > // Check s2 at the end of the cycle - before the registers update to
> > // their new values. Wierd - yes!
> > if (s1) checkit: assert (1;!s2) @@(posedge clk);
> >
> > // Our functionality that we are preventing.
> > do = s1 & d1 | s2 & d2;
> > end
> >
> > So we use the disable (to disable previously evaluated assertions), then
> > we use a immediate assert statement?! Wait that violates methodology #2.
> > Okay, so what - does it work? YES! But it's wierd, I have to now check
> > my expressions in the next timestep (but before the new values arrive?!)
> > Ohhhh, is this going to work? Yes it should...
> >
> > Alright, what's our methodology.
> >
> > 1. Use a disable statement FOR EACH assertion in a combinatorial
> > block. Make sure you name your assertion too! This disable
> > shall be placed at the beginning of the block.
> >
> > 2. Always use the form "<name>: assert (1;<expr>) @@(posedge clk)"
> > statement in combinatorial blocks to allow prevention of
> > false firings.
> >
> > One caution is this note in the SystemVerilog 3.0 draft (pg 46)
> >
> > "Note that to avoid races, the variables read in clocked immediate
> > assertions
> > should be written by nonblocking assignments."
> >
> > This conflicts with out proposed methodology, we'll have to see what
> > should
> > happen.
> >
> > This is for combinatorial blocks - for sequential blocks, what should we
> > do.
> >
> > 3. For sequential blocks, one may use immediate assertion statements
> > to check for correct values. Since the assertion is executed in a
> > sequential block, there will be no unstable signal values.
> >
> > The only drawback to use of the immediate assertions is that they are
> > evaluating the signals "at the end of the cycle". By this I mean that
> > the signals will receive a new value at the end of the current timestep
> > (through nonblocking, continuous assignment or procedural assignments.)
> > An error message will report this current time as the time of faiure.
> > Debugging tools will show the new signal values at this time, causing
> > a little bit of confusion. One will have to step back to the previous
> > cycle to see the (in)correct values to debug from.
> >
> > I am including 4 attachments that show these examples. They are:
> >
> > intra.v - example with intra-timestep problems.
> > inter.v - example with inter-timestep problems.
> > intra.sv - system verilog version (hopefully)
> > inter.sv - system verilog version
> >
> > You can see (not see) the problem by running these on your simulator
> > and including the +define statements listed in the file to prevent
> > the problems.
> >
> > Maybe we should consider extracting procedural assertions and their
> > context and simulating them as declarative assertions.
> >
> > Thanks.
> >
> > Adam Krolnik
> > Verification Mgr.
> > LSI Logic Corp.
> > Plano TX. 75074
>
>
> --------------------------------------------------------------------------
--
> ----
>
>
> >
> >
> > // This is a testcase that shows false assertion firing,
> > // due to intra-timestep value fluxuations.
> > // Run this on your favorite verilog simulator.
> > // To model strobe semantics (which have the same problem) use
> > // the argument +define+STROBE
> >
> > // To prevent the problem, use +define+STROBE+PREVENT to disable any
> > // previously started assertions (from the same timestep.)
> >
> > module intra;
> >
> > reg rs1, rs1a, s2, s3;
> >
> > reg do, d1, d2;
> >
> > reg tmp, s1a;
> >
> > reg clk;
> > initial
> > begin
> > clk = 1'b1;
> > forever clk = #5 ~clk;
> > end
> >
> > wire s1 = rs1 | s1a;
> >
> > initial $monitor($stime,, "s1 = %b, s2=%b", s1, s2);
> >
> > initial begin
> > rs1 = 1'b0;
> > rs1a = 1'b1;
> > s2 = 1'b0;
> >
> > @(posedge clk);
> > rs1a = 1'b0; // Turn on s1.
> >
> > @(posedge clk);
> > s2 = 1'b1; // Oops, we have both selects set...
> > rs1a = 1'b1; // Because of the always block below.
> >
> > @(posedge clk);
> >
> > s2 = 1'b0;
> >
> > repeat (5) @(posedge clk);
> > $finish;
> > end
> >
> >
> >
> > event docheck;
> > // Block with out assertion (modeled with a display statement.)
> > always @(s1 or s2 or d1 or d2)
> > begin
> > // This is how one prevents false firings due to intra-timestep
> > // value changes. By disabling a previously started assertion
> > // it will not fail. NOTE: requiring this kills overlapping
> > // assertions, because disable stops all running blocks/assertions!
> > `ifdef PREVENT
> > disable checkit; // disable any (ALL) previous assertions.
> > `endif
> >
> > // This is our model of the antecedent in more complex
> > // assertions. This may have been several nested if()'s or
> > // a case item, etc.
> > if (s1)
> >
> > // Model our assertion - file://assert never (s1 & s2);
> > if (s2)
> > begin
> > `ifdef STROBE
> > // This part models assert_strobe semantics.
> > -> docheck;
> > `else
> > // This part models immediate assert semantics.
> > $display("Error at time %0d - s1 and s2 are true.", $stime);
> > `endif
> > end
> >
> >
> > // Our functionality that we are preventing.
> > do = s1 & d1 | s2 & d2;
> > end
> >
> > // Assert_Strobe model version.
> > always @(docheck)
> > begin :checkit
> > #0 $display("Error at time %0d - s1 and s2 are true.", $stime);
> > file://#0 $display("Error again - was this still running?.");
> > end
> >
> > // Model of another combinatorial block of equations.
> > always @(rs1a)
> > s1a = ~rs1a;
> >
> >
> >
> > endmodule
> >
> >
>
>
> --------------------------------------------------------------------------
--
> ----
>
>
> >
> >
> > // This is a testcase that shows false assertion firing,
> > // due to intra-timestep value fluxuations.
> > // Run this on your favorite SystemVerilog simulator.
> > module intra;
> >
> > reg rs1, rs1a, s2, s3;
> >
> > reg do, d1, d2;
> >
> > reg tmp, s1a;
> >
> > reg clk;
> > initial
> > begin
> > clk = 1'b1;
> > forever clk = #5 ~clk;
> > end
> >
> > wire s1 = rs1 | s1a;
> >
> > initial $monitor($stime,, "s1 = %b, s2=%b", s1, s2);
> >
> > initial begin
> > rs1 = 1'b0;
> > rs1a = 1'b1;
> > s2 = 1'b0;
> >
> > @(posedge clk);
> > rs1a = 1'b0; // Turn on s1.
> >
> > @(posedge clk);
> > s2 = 1'b1; // Oops, we have both selects set...
> > rs1a = 1'b1; // Because of the always block below.
> >
> > @(posedge clk);
> >
> > s2 = 1'b0;
> >
> > repeat (5) @(posedge clk);
> > $finish;
> > end
> >
> >
> > // Block with out assertion (modeled with a display statement.)
> > always @(s1 or s2 or d1 or d2)
> > begin
> > disable checkit; // disable any (ALL) previous assertions.
> >
> > // This is our model of the antecedent in more complex
> > // assertions. This may have been several nested if()'s or
> > // a case item, etc.
> > // We need assert_strobe to delay the evaluation until all values
> > // settle and we need the disable above in case s1 settles to
> > // the value 0 (meaning that we shouldn't have run the assertion.
> > if (s1) checkit: assert_strobe (! s2);
> >
> > // Our functionality that we are preventing.
> > do = s1 & d1 | s2 & d2;
> > end
> >
> > // Model of another combinatorial block of equations.
> > always @(rs1a)
> > s1a = ~rs1a;
> >
> >
> >
> > endmodule
> >
> >
>
>
> --------------------------------------------------------------------------
--
> ----
>
>
> >
> >
> > // This is a testcase that shows false assertion firing,
> > // due to inter-timestep value fluxuations.
> > // Run this on your favorite verilog simulator.
> >
> > // To prevent the problem, use +define+PREVENT to disable any
> > // previously started assertions. This will kill any erroneously
> > // started ones.
> >
> > module inter;
> >
> > reg rs1, rs1a, s2, s3;
> >
> > reg do, d1, d2;
> >
> > reg tmp, s1a;
> >
> > reg clk;
> > initial
> > begin
> > clk = 1'b1;
> > forever clk = #5 ~clk;
> > end
> >
> > wire s1 = rs1 | ~s1a;
> >
> > initial $monitor($stime,, "s1 = %b, s2=%b", s1, s2);
> >
> > initial begin
> > rs1 <= 1'b0;
> > s1a <= 1'b1;
> > s2 <= 1'b0;
> >
> > @(posedge clk);
> > s1a <= 1'b0; // Turn on s1.
> >
> > @(posedge clk);
> > s2 <= 1'b1; // Oops, we have both selects set...
> > s1a <= #1 1'b1; // Model input delay (from different coding style
> block.)
> >
> > @(posedge clk);
> >
> > s2 <= 1'b0;
> >
> > repeat (5) @(posedge clk);
> > $finish;
> > end
> >
> >
> >
> > event docheck;
> > // Block with out assertion (modeled with a display statement.)
> > always @(s1 or s2 or d1 or d2)
> > begin
> > // This is how one prevents false firings due to inter-timestep
> > // value changes. By disabling a previously started assertion
> > // it will not fail. NOTE: requiring this kills overlapping
> > // assertions, because disable stops all running blocks/assertions!
> > `ifdef PREVENT
> > disable checkit; // disable any (ALL) previous assertions.
> > `endif
> >
> > `ifdef INTER
> > // This is our model of the antecedent in more complex
> > // assertions. This may have been several nested if()'s or
> > // a case item, etc.
> > if (s1)
> >
> > // Model our assertion - file://assert never (s1 & s2);
> > // This part uses assert (immediate) semantics by checking at the
> > // end of the cycle.
> > -> docheck;
> > `else
> > if (s1)
> > // Model our assertion - file://assert never (s1 & s2);
> > if (s2)
> > begin
> > // This part models assert_strobe semantics.
> > -> docheck;
> > end
> > `endif
> >
> >
> > // Our functionality that we are preventing.
> > do = s1 & d1 | s2 & d2;
> > end
> >
> > `ifdef INTER
> > // Assert_Strobe model version.
> > always @(docheck)
> > begin :checkit
> > @(posedge clk);
> > if (s2)
> > $display("Error(1) at time %0d - s1 and s2 are true.", $stime);
> > end
> >
> > `else
> >
> > // Assert_Strobe model version.
> > always @(docheck)
> > begin :checkit
> > #0 $display("Error(2) at time %0d - s1 and s2 are true.", $stime);
> > file://#0 $display("Error again - was this still running?.");
> > end
> > `endif
> >
> > endmodule
> >
> >
>
>
> --------------------------------------------------------------------------
--
> ----
>
>
> >
> >
> > // This is a testcase that shows false assertion firing,
> > // due to inter-timestep value fluxuations.
> > // Run this on your favorite SystemVerilog simulator.
> >
> > module inter;
> >
> > reg rs1, rs1a, s2, s3;
> >
> > reg do, d1, d2;
> >
> > reg tmp, s1a;
> >
> > reg clk;
> > initial
> > begin
> > clk = 1'b1;
> > forever clk = #5 ~clk;
> > end
> >
> > wire s1 = rs1 | ~s1a;
> >
> > initial $monitor($stime,, "s1 = %b, s2=%b", s1, s2);
> >
> > initial begin
> > rs1 <= 1'b0;
> > s1a <= 1'b1;
> > s2 <= 1'b0;
> >
> > @(posedge clk);
> > s1a <= 1'b0; // Turn on s1.
> >
> > @(posedge clk);
> > s2 <= 1'b1; // Oops, we have both selects set...
> > s1a <= #1 1'b1; // Model input delay (from different coding style
> block.)
> >
> > @(posedge clk);
> >
> > s2 <= 1'b0;
> >
> > repeat (5) @(posedge clk);
> > $finish;
> > end
> >
> >
> > always @(s1 or s2 or d1 or d2)
> > begin
> > // This is how one prevents false firings due to
intra/inter-timestep
> > // value changes. By disabling a previously started assertion
> > // it will not fail. NOTE: requiring this kills overlapping
> > // assertions, because disable stops all running blocks/assertions!
> >
> > disable checkit; // disable any (ALL) previous assertions.
> >
> > // This is our model of the antecedent in more complex
> > // assertions. This may have been several nested if()'s or
> > // a case item, etc.
> > // Check s2 at the end of the cycle - before the registers update to
> > // their new values. Wierd - yes!
> > if (s1) checkit: assert (1;!s2) @@(posedge clk);
> >
> > // Our functionality that we are preventing.
> > do = s1 & d1 | s2 & d2;
> > end
> >
> > endmodule
> >
> >
>
This archive was generated by hypermail 2b28 : Thu Sep 05 2002 - 04:36:28 PDT