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 Wed Nov 8 17:22:56 2006
This archive was generated by hypermail 2.1.8 : Wed Nov 08 2006 - 17:23:10 PST