Re: [sv-ac] "solve before" of free variables in checker?

From: ben cohen <hdlcohen@gmail.com>
Date: Sat Dec 04 2010 - 14:53:33 PST

LRM 17.7.2 "When a solution attempt is made on an assume set, values shall
be sought for all active checker variables
such that, together with the inactive variables and state, none of the
assumptions will fail in that time step"
Thar means that there is an implicit "solve before" in order for the
assumptions ot be met.
Ben

On Sat, Dec 4, 2010 at 2:43 PM, ben cohen <hdlcohen@gmail.com> wrote:

> In a checker with free variables , is there a concept of the "solve
> before" as done in a class?
> Below is an example with a class. This is followed by a checker model.
> Are the two equivalent?
> Are the positions of the "assume" properties relevant? In other words, if
> m_cy is declared before m_before, would it make a difference?
> In the example below, if *m_cy* is solved before *m_before*, then y could
> take the value 8.
> *class *SolveBefore;
> *rand bit *x[15:0]; //
> *rand bit *[15:0] y; //
> *constraint *c_x { x <=7;}
> *constraint *c_xy {
> (x==0) -> y==0;
> (x>0 && x<=2) -> y==1;
> (x >15) -> y==8;
> *solve *x *before *y;
> }
> *endclass *: SolveBefore
>
> *checker *SolveBefore_chk (*event* clk);
> *rand *bit x[15:0]; //
> *rand *bit [15:0] y; //
> m_before: *assume property*(@(clk) x <=7);
> m_cy: *assume* *property *(@(clk) if(x==0) y==0
> *else if* (x>0 && x<=2) y==1
> *else if *(x>15) y==8);
> *endchecker *: SolveBefore_chk
>
> Ben *SystemVerilog.us*
>

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.
Received on Sat Dec 4 14:54:26 2010

This archive was generated by hypermail 2.1.8 : Sat Dec 04 2010 - 14:54:39 PST