Subject: ForSpec's rigid variables
From: Armoni, Roy (roy.armoni@intel.com)
Date: Mon Nov 19 2001 - 11:59:22 PST
Hi Bernard,
Let me try to explain again why the rigid variables work for data checking.
Let me just
emphasize right at the beginning that all said in the rest of this note is
from the definition
point of view. It has nothing to do with the actual implementation, so
please, do not try
to conclude anything about the efficiency from this note. It addresses only
the correctness
side.
Suppose that we have as part of our spec the following declaration:
rigid bit[10] tag;
then, every infinite trace t is spawned into 1024 traces t_0,...,t_1023, all
of them are
exactly the same. Each of them is later extended with the tag variable,
holding a different
value, say, t_i is having the value i for the tag. The important point, is
that throughout the
trace, tag does not change its value. In t_i, the variable tag will have
the value i all the time.
This is BTW the source for the name rigid.
Now, let's try to see what happens with the assertion
assert p := always (datain=tag) -> next (dataout=tag);
p is being checked against all traces. Suppose that at some point j, datain
has the value k.
For all traces t_i where i!=k, the antecedent (datain=tag) will fail,
causing the consequent
next (dataout=tag) not to be checked. However, exactly on t_k, the
antecedent succeeds,
making sure that if in the next cycle dataout is different than k, an error
will be flaged.
The nice thing is that for every different value of the datain, there is
exactly one i s.t. in
t_i (or t_datain if you like), the antecedent succeeds, causing the
consequence to be
checked.
Let me also note that the above is a "mathematical" trick that takes
advantage of the
universal path quantifier of linear time logics. Their are other,
deterministic ways, to achieve
the same thing, but then one pays in efficiency. Actually, efficiency is
the only reason to
use this particular method.
Hope that this clarifies things. Please let me know if I left anything not
clear enough.
Regards,
Roy
-----Original Message-----
From: Bernard Deadman [mailto:bdeadman@sdvinc.com]
Sent: Monday, November 19, 2001 12:41 AM
To: vardi@cs.rice.edu
Cc: vfv@eda.org
Subject: Re: sugar: case-by-case analysis of accellera requirements
At 04:06 PM 11/18/2001 -0600, Moshe Vardi wrote:
> > the "rigid bit" variable semantics and scope.
> >
>
>Bernard, let me try once more to explain rigid bits. Let's start with
>regular bits. When you declare in ForSpec "bit x", you are simply adding
>a new virtual signal. This signal is initially unconstrained so it can
>take arbitary values at any cycle. Now, "rigid x" is simply an
>abbreviation for "bit x; model always x=x'", which means that x is
>constrained to have a constant value.
Moshe,
Thanks. That much I understood. The problem I'm having is to see how
"rigid bit" variables support multiple, concurrent 'tags' in Property
20. If I visualize the variable as taking on the first value with which it
is "touched" then I can see the first split transaction works, but I just
can't get my mind around how a single "rigid bit" variable supports
multiple tags at different times during a simulation? Worse still I can't
see where multiple concurrent tags are stored?
As I remember saying before, either the "rigid bit" variable has to hold a
number of simultaneous tags which seems intuitively counter to the idea of
"rigid", or I have to assume the variables are "local" to each instance of
the property which I don't think is explained in the ForSpec documentation,
and in which event I can't see when a regular variable isn't adequate in
this example.
I'm prepared to believe the Forspec for Property 20 is correct, but it
seems part of the explanation is missing. Could someone humor me and
explain it at the "rigid bits for dummies" level? Or with diagrams?
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 : Mon Nov 19 2001 - 12:00:25 PST