Hi Doron, I agree that the non-determinism is a problem, but it is a different problem. The Verilog simulation algorithm is non-deterministic by its nature, and very little may be done here. In FV modeling proposal the simulation algorithm is completely deterministic, but it is impossible to extend it to entire Verilog RTL. You can sometimes avoid the reporting of a glitch assertion violation by a smarter simulation algorithm, e.g., trying to sort the signals topologically. From the user point of view it is not important how it has been achieved: using the topological sorting or by suppressing the intermediate reports. Thanks, Dmitry -----Original Message----- From: dbustan [mailto:dbustan@freescale.com] Sent: Sunday, November 12, 2006 11:58 PM To: Korchemny, Dmitry Cc: sv-ac@eda.org Subject: RE: [sv-ac] blocking assignments Hi Dmitry, In Matt's example, there is a nondeterministic scheduling, for which the values of the wires at the end of the time step are deterministic. For such examples, you solution makes sense. But what if the final result is non-deterministic? In this case your solution may miss bugs from different scheduling. You may say that non-deterministic final results are indications for bad coding style, but that could be one of the reasons you put the assertions there at the first place. I think that what you really want is some order of the scheduling of combinatorial assignments and maybe latches as well. In Matt's example, the always_comb should have scheduled last because no combinational assignments depend on "o". Doron -----Original Message----- From: Korchemny, Dmitry [mailto:dmitry.korchemny@intel.com] Sent: א 12 נובמבר 2006 07:53 To: Doron Bustan Cc: sv-ac@eda.org Subject: RE: [sv-ac] blocking assignments Hi Doron, I suggest the following solution: Follow the execution of the immediate assertion instance, but don't execute its action block. When entering the Observed region for the first time, check the status of the assertion: if it passed at the last check - execute the pass statement in the Reactive region, if it failed - execute the fail statement in the Reactive region. When I am talking about the instances, I mean that when the assertion appears within the statically computable for-loop, it should be unrolled: E.g., for (int i = 0; i < 3; i++) assert a[i]; should be treated as: assert a[0]; assert a[1]; assert a[2]; Thanks, Dmitry -----Original Message----- From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On Behalf Of Doron Bustan Sent: Thursday, November 09, 2006 12:28 AM Cc: sv-ac@server.eda.org Subject: Re: [sv-ac] blocking assignments Ok, this makes sense. Correct me if I am wrong but at timestep 3, first the simulator goes to the NBA region, moves the assignments ff1 <= i_ff1; ff2 <= i_ff2; to the active region, then there is a race condition between : "ff1 <= i_ff1" and "ff2 <= i_ff2" in your case "ff1 <= i_ff1" is scheduled first then there is a race condition between always_comb begin assert(m==ff1); case({m,ff1}) 2'b00: o = 1'b0; 2'b11: o = 1'b1; endcase $display("%t m:%b ff1:%b",$time,m,ff1); end and "ff2 <= i_ff2" in your case the assertion is scheduled first (and fires) then "ff2 <= i_ff2" is scheduled, after which "n = ff2", after which "m = n && tmp" and finally the assertion again (does not fire). for a different legal scheduling we could have "ff2 <= i_ff2" schedule before the assertion and then if "n = ff2" and "m = n && tmp" also get scheduled before the assertion, it will only be evaluated once with m = 1, ff1 = 1. So, although there are many different possible schedules, which may result in different evaluations of the assertion, the last evaluation of the assertion will always be true. I think I understand the problem, but still not the solution. Doron Maidment, Matthew R wrote: >Time 0: > >{m,ff1} == 2'b00 > >Time 3: > >{m,ff1} == 2'b01 >{m,ff1} == 2'b11 > >And, no, the clock does not toggle between X and Z. T > >I used 'bit' for all data types for simplicity, so all >vars are 0 at time 0. > >Time 1: >Clock rises and i_ff* are assigned 1. >Time 3: >Clock rises and ff* get i_ff* >Because ff1 changes from 0->1, the always_comb block with >the assertion evaluates and the assertion fires. >Meanwhile ff2 changes from 0->1, triggers the assignment >of "n", which triggers the assignment of "m" which triggers >the always_comb block with the assertion. This time, >the inputs to the assertion are 2'b11 and the assertion >does NOT file. > >So the assertion is evaluated 2X at time 3. > >Matt >-- >Matt Maidment >mmaidmen@ichips.intel.com > > > > >>-----Original Message----- >>From: Doron Bustan [mailto:dbustan@freescale.com] >>Sent: Wednesday, November 08, 2006 1:37 PM >>To: Maidment, Matthew R >>Cc: sv-ac@eda.org >>Subject: Re: [sv-ac] blocking assignments >> >>Hi Matt, >> >>please give more detailes >> >>what happen at timestep 0? At timestep 1? At the rest of the >>timesteps >>(if any) >> >>Are there more than one evaluation in a single time step? >> >>BTW doesn't the clk flip between x and z ? >> >>thanks >> >>Doron >> >>Maidment, Matthew R wrote: >> >> >> >>>Here's a more interesting example. >>> >>>module bar(); >>> >>>bit clk; >>>bit m,n,o; >>>bit ff1,ff2; >>>bit i_ff1,i_ff2; >>>always_comb begin >>> assert(m==ff1); >>> case({m,ff1}) >>> 2'b00: o = 1'b0; >>> 2'b11: o = 1'b1; >>> endcase >>> $display("%t m:%b ff1:%b",$time,m,ff1); >>>end >>> >>>bit tmp; >>>always_comb >>>tmp = 1; >>>always_comb >>> n = ff2; >>>always_comb >>> m = n && tmp; >>>always_ff@(posedge clk) >>> ff1 <= i_ff1; >>>always_ff@(posedge clk) >>> ff2 <= i_ff2; >>> >>>initial >>>forever begin >>> #1; >>> clk = ~clk; >>>end >>>initial begin >>>@(clk) begin >>> i_ff1 <=1; >>> i_ff2 <=1; >>>end >>>#1000; >>>$finish; >>>end >>>endmodule >>> >>>This assertion fires on 2 simulators that I tried. >>>The order of evaluation is: >>> >>>{m,ff1} == 01 //Fire >>>{m,ff1} == 11 //Does not fire >>> >>>This assertion is an explicit form of the implicit unique case >>>check. I believe unique and priority checks should also be >>>addressed by your work. >>> >>> >>>Matt >>>-- >>>Matt Maidment >>>mmaidmen@ichips.intel.com >>> >>> >>> >>> >>> >>> >>>>-----Original Message----- >>>>From: owner-sv-ac@server.eda.org >>>>[mailto:owner-sv-ac@server.eda.org] On Behalf Of Doron Bustan >>>>Sent: Wednesday, November 08, 2006 11:20 AM >>>>Cc: sv-ac@server.eda.org >>>>Subject: Re: [sv-ac] blocking assignments >>>> >>>>Hi Dmitry, >>>> >>>>I guess that illustrates the problem, but it does not >>>>make sens, does it? >>>> >>>>we need a reasonable example that is deterministic, >>>>and in which the assertion is being evaluated at least >>>>twice without leaving the active region. >>>> >>>>Doron >>>> >>>>Korchemny, Dmitry wrote: >>>> >>>> >>>> >>>> >>>> >>>>>Hi Doron, >>>>> >>>>>You are right. @(posedge clk) is a typo, should be @(*) (or >>>>> >>>>> >>>>> >>>>> >>>>@(b), but it >>>> >>>> >>>> >>>> >>>>>is not synthesizable). >>>>> >>>>>always @* begin >>>>> if (cond) begin >>>>> a = b; >>>>> assert (a == c) ; >>>>> b = c; >>>>> end >>>>>end >>>>> >>>>>Is it correct now? >>>>> >>>>>I'll try to get a real life example in addition to this >>>>> >>>>> >>>>> >>>>> >>>>artificial one. >>>> >>>> >>>> >>>> >>>>>I think, we should define simulation semantics that would be >>>>> >>>>> >>>>> >>>>> >>>>consistent >>>> >>>> >>>> >>>> >>>>>with FV in the synthesizable case. Two candidates are >>>>>- taking the latest signal value from the active region before the >>>>>first entry to the observed region, and >>>>>- "sampling" the signal values at the first entry to the observed >>>>>region. As for non-synthesizable or "difficult" for >>>>> >>>>> >>synthesis example, >> >> >>>>>it is important only that the algorithm is well defined: >>>>> >>>>> >>for "exotic" >> >> >>>>>cases it is difficult to invent something better than immediate >>>>>assertions. >>>>> >>>>>Thanks, >>>>>Dmitry >>>>> >>>>>-----Original Message----- >>>>>From: owner-sv-ac@server.eda.org >>>>> >>>>> >>>>> >>>>> >>>>[mailto:owner-sv-ac@server.eda.org] On >>>> >>>> >>>> >>>> >>>>>Behalf Of Doron Bustan >>>>>Sent: Wednesday, November 08, 2006 12:26 AM >>>>>To: sv-ac@server.eda.org >>>>>Subject: [sv-ac] blocking assignments >>>>> >>>>>Just to make sure that I don't miss something important... >>>>> >>>>>In the example: >>>>> >>>>>always @(posedge clk) begin >>>>> if (cond) begin >>>>> a = b; >>>>> assert (a == c) ; >>>>> b = c; >>>>> end >>>>>end >>>>> >>>>>the assertion is being evaluated at most once in every "clk" cycle. >>>>> >>>>> >>>>>I think that we need more than one always block to cause >>>>> >>>>> >>the assertion >> >> >>>>>to >>>>>execute more than once, something like: >>>>> >>>>>always @(b) begin >>>>> if (cond) begin >>>>> a = b; >>>>> assert (a == c) ; >>>>> end >>>>>end >>>>> >>>>>always @(c) begin >>>>> b = c; >>>>>end >>>>> >>>>>this will cause the assert to possibly fire twice at the same >>>>> >>>>> >>>>> >>>>> >>>>time step >>>> >>>> >>>> >>>> >>>>>without >>>>>exiting the active region. We should also consider the >>>>> >>>>> >>following case: >> >> >>>>>always @(b) begin >>>>> if (cond) begin >>>>> a = b; >>>>> assert (a == c) ; >>>>> end >>>>>end >>>>> >>>>>always @(c) begin >>>>> b <= c; >>>>>end >>>>> >>>>>Here the assert is being triggered twice, but the simulator >>>>> >>>>> >>>>> >>>>> >>>>goes to the >>>> >>>> >>>> >>>> >>>>>NBA >>>>>region between the two triggers. >>>>> >>>>> >>>>>is this right? >>>>> >>>>>Doron >>>>> >>>>> >>>>> >>>>> >>>>> >>>>>Received on Sun Nov 12 23:08:53 2006
This archive was generated by hypermail 2.1.8 : Sun Nov 12 2006 - 23:09:08 PST