RE: [sv-ac] blocking assignments

I don't agree that the non-deterministic scheduling is a problem. It is simply reflecting the physical reality. Design methodologies are created which ensure that the final result is in fact deterministic. If your design is indeed glitch-sensitive, then you have a real problem and you want to detect it.

Shalom

> -----Original Message-----
> From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On
> Behalf Of Korchemny, Dmitry
> Sent: Monday, November 13, 2006 9:08 AM
> To: dbustan
> Cc: sv-ac@server.eda.org
> Subject: RE: [sv-ac] blocking assignments
> 
> 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
> >>>>>
> >>>>>
> >>>>>
> >>>>>
> >>>>>
> >>>>>