[sv-ac] RE: continuous assignment example

Hi Manisha,

Please, see my comments below.

Thanks,
Dmitry

-----Original Message-----
From: Kulshrestha, Manisha [mailto:Manisha_Kulshrestha@mentor.com]
Sent: Thursday, December 09, 2010 6:37 AM
To: Korchemny, Dmitry; sv-ac@eda.org
Subject: 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

[Korchemny, Dmitry] I am not sure about deferred assertions. Unfortunately, my proposal is not deferred-assertion friendly. Though I realize that deferred assertions are an issue, I suggest to consider them separately when we understand the remaining stuff should work.

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

[Korchemny, Dmitry] Yes, blocking assignments should also execute in the Observed region taking into account that a continuous or a blocking assignment changes the sampled value of its LHS.

Consider the following example:

bit v, w;
always_comb begin
  v = x; // x is a design or a TB variable, its preponed value is used here
         // The new sampled value of v is $sampled(x)
  w = v; // w is assigned a sampled value of v = $sampled(x)
         // Now both v, w, and x have the same sampled value

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 ?

[Korchemny, Dmitry] Unfortunately there are several situations where let cannot be used or its usage is tedious:
* Assigning values to output checker arguments
* Dealing with aggregate data types.

Two following examples illustrate the last point.

1)

checker check(bit[3:0] a, event clk, ...);
  let e(i) = f(i, ...);
  assert property (@clk {e(0),e(1),e(2),e(3)} > 1);
endchecker : check

against

checker check(bit[3:0] a, event clk, ...);
  bit [3:0] x;
  always_comb
   for (int i = 0; i < 4; i++)
     x[i] = f(i, ...);
  assert property (x > 1);
endchecker : check

2)

let a = very.long.hierarchical.name;
... a[5] // Illegal

type(very.long.hierarchical.name) a;
assign a = very.long.hierarchical.name;
...a[5] // legal

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.

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