Subject: RE: Clarification on 'rigid bit'
From: Armoni, Roy (roy.armoni@intel.com)
Date: Mon Oct 01 2001 - 00:20:38 PDT
Hi Bernard,
The automata theoretic approach shows that you will have to deal with only a
bounded
number of splits. By bounded I mean a number that is fixed during
compilation - independent
of how many transactions will exist in the trace.
You are correct that the automata theoretic approach allows the implementor
of the compiler
to optimize using all our knowledge gained in the past 40+ years. I object
however that this
is typical to ForSpec and Sugar vs. e and CBV. This is an implementation
issue. All of
ForSpec, e and CBV, and the linear fragment of Sugar, can be compiled into
automata.
What you call "the user intensive approach" is I believe a style in which
the user writes its
assumptions as automata (using the modeling power of the language) rather
than as formulas.
Am I correct? If so, that can be done in ForSpec, CBV and EDL. Temporal-e
does not have
this capability - for that, one should use e which I believe is not part of
Verisity's donation.
Verisity, please correct me if I'm wrong.
The other way around of using only formulas to describe properties is where
there is a
difference among the donations. As far as I know, ForSpec is the only
language for which we have a proof that every automaton can be compiled into
a formula (that is without using any
modeling features such as free or rigid bits and assignments). I believe
that CBV and Sugar
do not have the omega-regularity power because they lack the ability to nest
concatenation
and implication. I do not know about temporal e - I think that Verisity
said recently that they
believe they have omega regularity but they do not have a proof.
Regards, Roy
-----Original Message-----
From: Bernard Deadman [mailto:bdeadman@sdvinc.com]
Sent: Monday, September 24, 2001 2:13 AM
To: Armoni, Roy
Cc: vfv@eda.org
Subject: RE: Clarification on 'rigid bit'
At 09:37 AM 9/20/2001 +0300, Armoni, Roy wrote:
>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].
Roy,
Thanks for the pointer. I've read the paper a couple of times, though it
seems to be general in nature and I'm afraid it hasn't helped me understand
why the "automata theoretic approach" is more efficient in supporting
multiple concurrent variables. It could well be that I failed to make a
conceptual leap somewhere, but my present assumption is, in the context of
a dynamic verification implementation of property 20, that:
a) a "rigid bit" variable takes on every value with which it's 'touched'
b) the automaton (or perhaps multiple automata?) are evaluated for every
one of the multiple values encountered thus far in the simulation
c) you believe it is more efficient (or at least tolerable?) to use
standard automaton to evaluate the property rather than to make special
provisions for 'variable' values
d) and c) guarantees common semantics between Formal and Dynamic
verification
Is this broadly correct?
My first thought was to wonder if the efficiency of the implementation is
relevant in the selection of a language, and in general I think it's
important if the language enforces a particular implementation, in which
circumstances I strongly believe the choice should be an enlightened
one. I guess I'm arguing the ability to express a property is not in
itself sufficient for a viable solution, and that if my fears have
foundation, this is an issue that ought to be decided via the vote on the
requirements document.
If I look at the four donations, I see two broad styles.
1) the user intensive solution (temporal 'e') where:
i) more user skill is required because he has to figure out when and where
to spawn a new checker, therefore raising the potential for errors on the
part of the user
ii) the number of concurrent checkers is equal to the number of concurrent
un-resolved split transactions at any instant
2) the implementation intensive solution (ForSpec & Sugar) where:
i) the tool implementor has the responsibility and the user has a very much
simpler task
ii) there is a risk of a greater need for computing resources because the
solution is tougher to optimize
The conceptual problem I have is with my (probably flawed!) understanding
of the semantics of "rigid bit" variables, because it seems to me the
property has to be re-evaluated not just for every split transaction that
is un-reconciled at any instant, but, potentially for at least one or two
cycles using every tag value encountered thus far in the simulation. My
concern is this could consume a vast amount of resources since a simulation
running 4 or 5 order of magnitude slower than real time could easily
generate millions of unique tag values during several hours of simulation,
of which only a few tens at any instant may be un-reconciled split
transactions.
This does not sound a good bargain to me and I hope you can show me where
my understanding of "rigid bit" variables is fundamentally flawed!!!
Incidentally, I have always had the same probably with the Sugar 'forall'
construct. I can finally see how you can express the property but I have
little idea how to convert this is a viable implementation!
Thanks for your help,
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 Oct 01 2001 - 00:27:10 PDT