Subject: RE: Clarification on 'rigid bit'
From: Armoni, Roy (roy.armoni@intel.com)
Date: Wed Sep 19 2001 - 23:37:53 PDT
Hi Bernard,
You are correct in your last sentence that rigid variables of ForSpec under
assertions are
similar to the variables with "forall" quantification in Sugar. This is
because every ForSpec assertion is being checked against all possible traces
(and non-deterministic choices).
As for the FV/simulation orientation, I am trying to keep my explanations
not oriented to any
side. ForSpec is a formal specification language that can be used for both
FV and
simulation. However, nothing in its semantics is biased to any side. Yet,
for the
implementation, you are correct that it is possible to spawn a new copy of
the variable or a new
checker for every tag value, but that would be an inefficient way. The most
efficient way to go
is through the automata theoretic approach. More details about it may be
found in Vardi's
work [An Automata-Theoretic Approach to Linear Temporal Logic,
http://www.cs.rice.edu/~vardi].
Regards, Roy
-----Original Message-----
From: Bernard Deadman [mailto:bdeadman@sdvinc.com]
Sent: Thursday, September 20, 2001 12:44 AM
To: Armoni, Roy
Cc: vfv@eda.org
Subject: RE: Clarification on 'rigid bit'
Roy,
Thanks for the explanation, which certainly helps. I think one level of
confusion is I always start from my experience with simulation whereas your
description seems to focus on Formal Verification.
I'm afraid I'm feeling stupid, but I'm still not certain how this works in
a dynamic environment. Can I visualize one option as being that the
implementation is responsible for allocating a new variable (or even a new
checker?) every time a different tag value is encountered, and that the
language places no constraints on the way this is achieved or the number of
concurrent tag variables that can exist? If this is indeed the case, then
I can visualize it as semantically similar to "forall" in Sugar in a
dynamic environment?
Thanks,
Bernard
At 09:34 PM 9/19/2001 +0300, Armoni, Roy wrote:
>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.
====================================================================
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 - 23:39:02 PDT