RE: [sv-ac] Nondeterministic free variables

Hi Dmitry,
 
yes this is the modeling style I was thinking of.
 
best...
ed


________________________________

	From: Korchemny, Dmitry [mailto:dmitry.korchemny@intel.com] 
	Sent: Thursday, October 25, 2007 12:24 PM
	To: Eduard Cerny
	Cc: sv-ac@eda.org
	Subject: 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.

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


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