RE: [sv-ac] blocking assignments

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
>>>> 
>>>>
>>>>      
>>>>
>