RE: [sv-ac] Nondeterministic free variables

Hi Ed,

 

Even if we allow using $nondet in blocking assignments, there will still
be an important semantic difference between two definitions:

 

freevar bit x = $nondet(x); // Never assigned elsewhere

 

defines a rigid variable - its value never changes

 

Using current definition:

 

freevar bit x; // Never assigned elsewhere

 

the value of x is free, its value may change arbitrarily at any time.

 

To model this behavior in the $nodet approach one should write:

 

freevar bit x = $nondet(x);

always_check @$global_clock x <= $nondet(x);

 

This is also error prone: the people will likely forget to write this
and will get rigid variables instead of free variables in their
verification code. Such mistakes are difficult to catch, and they may
lead to false positives in verification.

 

Thanks,

Dmitry

 

________________________________

From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On
Behalf Of Eduard Cerny
Sent: Thursday, October 25, 2007 5:48 PM
To: Korchemny, Dmitry; Eduard Cerny
Cc: sv-ac@server.eda.org
Subject: RE: [sv-ac] Nondeterministic free variables

 

Hi Dmitry,

 

I think that in simulation $nondet would have to be handled by one of
the 3 possibilities you listed, possibly a random value. false
negaive... might... but if used as constraint it might work in
simulation.

For VIS, even if it is limited to cont asssigns, does it have to be? Why
not in synchronous assignments in our case? 

In any case, I do not insist on this solution, just thought that it
could get us out of what seemed to be an impass.

 

Best regards,

ed

	 

	
________________________________


	From: Korchemny, Dmitry [mailto:dmitry.korchemny@intel.com] 
	Sent: Thursday, October 25, 2007 11:30 AM
	To: Eduard Cerny
	Cc: sv-ac@eda.org
	Subject: [sv-ac] Nondeterministic free variables

	Hi Ed,

	 

	I would like to address our discussion at the last meeting
concerning non-deterministic free variables. You suggested to follow VIS
convention and to use a special function $nondet for non-deterministic
free variables.

	 

	My general comment is that $nondet is just a different notation,
and I don't see how this notation may solve the problem of simulating
non-deterministic free variables. One could use a default value for the
variable type instead of $nondet in simulation, etc, but the same thing
may be implemented using the syntax suggested in the proposal; both
implementations will likely result in false negatives.

	 

	Now I would like to address the problems I see when using VIS
$nondet function.

	 

	Citing VIS documentation:

	"... a nondeterministic construct, $ND, has been added to
Verilog to specify nondeterminism on wire variables and is the only
legal way to introduce nondeterminism in VIS. For example, to require
that the output at a particular state is nondeterministically GO or
NOGO, one can introduce a new variable, r, and write the following
Verilog fragment. 

	assign r=$ND{GO,NOGO};
	.
	.
	always@(posedge clk) begin
	.
	.
	state = r;
	.
	.
	end

	"

	In VIS a non-deterministic value may be assigned using
continuous assignment only, and therefore the non-determinism in
sequential variables will have to be coded explicitly:

	 

	freevar bit r1, x1 = r1;

	freevar bit r2, x2 = r2;

	assign r1 = $nondet(r1);

	assign r2 = $nondet(r2);

	always_check @clk begin

	x1 <= x1 && something_else;

	x2 <= x2 && something_else;

	end

	 

	// Values of x1 and x2 are different in this example

	 

	instead of

	 

	freevar x1, x2;

	always_check @clk begin

	x1 <= x1 && something_else;

	x2 <= x2 && something_else;

	end

	 

	// Values of x1 and x2 are different in this example

	 

	as now.

	 

	Note that creating one non-determinitsic variable for all cases
instead of creating individual copy for each case will be a common bug,
and this bug will be very hard to catch. Compare:

	 

	freevar bit r, x1 = r, x2 = r; // One non-deterministic variable
is used

	assign r = $nondet(r);

	always_check @clk begin

	x1 <= x1 && something_else;

	x2 <= x2 && something_else;

	end

	 

	// Values of x1 and x2 are identical in this example

	 

	Thanks,

	Dmitry

	
---------------------------------------------------------------------
	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 <http://www.mailscanner.info/> , and is

believed to be clean. 
---------------------------------------------------------------------
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.