Subject: RE: Clarification on 'rigid bit'
From: Armoni, Roy (roy.armoni@intel.com)
Date: Wed Sep 19 2001 - 11:34:14 PDT
Hi Bernard,
A rigid variable is a variable that by definition chooses a
non-deterministic value, and later on, remains constant throughout the
trace. This is by definition, thus, you cannot see the explicit
initialization.
It is also possible to create a rigid variable by defining a free variable
and assign its next value to its current value, for instance,
bit[74] tag;
assign tag' = tag;
is equivalent in ForSpec to
rigid bit[74] tag;
In both cases there is no initialization, thus the variable is free at time
0, but later on it remains constant.
Since the semantics of ForSpec is that the property should be satisfied by
all traces (universal quantification), then the property is valid only if it
is satisfied with all possible values for tag.
Regards, Roy
-----Original Message-----
From: Bernard Deadman [mailto:bdeadman@sdvinc.com]
Sent: Wednesday, September 12, 2001 7:18 PM
To: roy.armoni@intel.com
Cc: vfv@eda.org
Subject: Clarification on 'rigid bit'
Roi,
I went back to look at how data & variables work in ForSpec. Property 20
is coded as:
rigid bit[74] tag;
tagmatch := tag = (address % address_parity % command % byte_enables %
REQ64#);
start := a_fall(frame), tagmatch;
wait := irdy_{0,7}, !irdy_ & trdy_ & stop_{1,8};
end := !irdy & (trdy_ & !stop_ | !trdy_ & stop_);
// transaction tries to complete
ALWAYS start TRIGGERS wait, end;
// transaction retry
ALWAYS start, wait, end \ !stop_ TRIGGERS (EVENTUALLY[1,31999] start) |
(EVENTUALLY[32000,32100] BridgeControlRegister[10];
The definition of rigid bit is "variables which don't change their value
after initialization", however I can't see where the initialization occurs
in this example. When does a tag get saved? What happens if there are
multiple concurrent split transactions with different tags? Can there be
multiple concurrent tag variables?
Thanks
Bernard
====================================================================
SDV Inc. 9111 Jollyville Rd, Suite 102, Austin, TX 78759 USA
Phone: (512) 231-9806 xt 101 FAX: (512) 231-9807 Mobile: (512)
431-5126
Email: bdeadman@sdvinc.com Website: www.sdvinc.com
This archive was generated by hypermail 2b28 : Wed Sep 19 2001 - 11:35:16 PDT