[sv-ac] RE: continuous assignment example

Hi Dimitry,

So, now we have all of the following that have to execute in Observed
region:

1. evaluatiion of free vars based on assumes
2. assertion execution
3. cont assigns
4. deferred assertions

Now, thinking about another mantis where you have always_comb in
checkers. Take the following example:

always_comb
  w = v & x;
Will this always_comb also execute in Observed region after v gets
updated ? Will this always_comb use sampled values or current values of
'x'.

One thing I want to understand is what is the use of 'w' in the example
below. Isn't it enough to just put the RHS of the assignment wherever
'w' is to be used ? Or use 'let' to do the substitution ? From the
functionality it looks like you are really looking for something like
'let' instead of an independent process ? Is there a case where 'let'
can not be used ?

Thanks.
Manisha

-----Original Message-----
From: Korchemny, Dmitry [mailto:dmitry.korchemny@intel.com]
Sent: Wednesday, December 08, 2010 2:32 PM
To: Kulshrestha, Manisha; sv-ac@eda.org
Subject: RE: continuous assignment example

Hi Manisha,

Please, see my comments below.

Thanks,
Dmitry

-----Original Message-----
From: Kulshrestha, Manisha [mailto:Manisha_Kulshrestha@mentor.com]
Sent: Tuesday, December 07, 2010 8:23 PM
To: Korchemny, Dmitry; sv-ac@eda.org
Subject: continuous assignment example

Hi Dimitry,

Here is the example we were discussing at the end of today's meeting:

randomization modifies the sampled value
continuous assignment modifies the sampled value
NBA does not modify the sampled value

checker c(a);
rand bit v;
bit x;
bit w;
always @clk x <= a;

assume property (@(clk) a == v);

assign w = $sampled(v & x) = v & $sampled(x);

assert property (@clk a == w);
assert property (@clk a == v);

endchecker

Just a followup on this example: when does the sampled value of x
changes ?
[Korchemny, Dmitry] It changes in the Preponed region of the next time
step, as regular design variables (since the LRM does not define where
the sampled values change, it would be safer to say that in the Preponed
region of the next tick the sampled value of x have a new value if a has
changed).

If it changes in Preponed region of next time step, then will this
continuous assignment evaluate again at next simulation tick ?
[Korchemny, Dmitry] According to the definition of continuous assignment
it should.

But perhaps there is no need to do that as value of 'w' will not be used
till next clock event.
[Korchemny, Dmitry] Indeed, there is no need to do that till the next
clock event in this case. This is also the case unless the continuously
assigned variables are used in a deferred assertion.

So, these continuous assignments are more like blocking assignments
which happen between freevar update and assertion evaluation. Is that
correct ?
[Korchemny, Dmitry] See my previous comment.

Manisha

---------------------------------------------------------------------
Intel Israel (74) Limited

This e-mail and any attachments may contain confidential material for
the sole use of the intended recipient(s). Any review or distribution
by others is strictly prohibited. If you are not the intended
recipient, please contact the sender and delete all copies.

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.