RE: [sv-ac] blocking assignments

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