RE: [sv-ac] blocking assignments

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