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