[Fwd: Re: [sv-ac] blocking assignments]

attached mail follows:

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