Subject: simulation interpretation of ForSpec's rigid variables
From: Anthony Mcisaac (Anthony.Mcisaac@st.com)
Date: Thu Nov 29 2001 - 07:19:22 PST
Bernard,
Thank you for your reply.
Harry Foster will be providing me with the relevant documents. I have studied
the mailing list archive, and I did indeed have property #20 in mind. It's an
excellent example, raising several theoretical and practical issues.
Without going into more detail on these at this point, I would like to ask a
specific question of Intel, because, although the rigid variable approach is
equivalent to the natural interpretation of "forall" for model checking, I'm
not
sure that it is equivalent for simulation.
The question is: is the interpretation of the ForSpec solution for property 20
for simulation:
(a) The rigid variable is implicitly treated as a universally quantified
variable, so that the property must be checked for all possible tag values;
(b) The rigid variable is treated as a free variable, so that the property must
be checked for the value with which this variable is driven in the simulation;
(c) - Or does the semantics of ForSpec only define the intepretation of a
formula
on a trace, so that either of the above interpretations is possible (it depends
what set of traces you look at, when extra variables are added)?
In general, I would expect it to be easy to demonstrate an equivalence
between the semantics of any language for model checking and simulation, if
one only considers the interpretation on sets of traces. I'm not sure how far
beyond that one will want to go in practice - for example, does one make a
distinction in the language between specialization of an input as an
environment
constraint and as a selection of a test stimulus value?
On your general points about the potential for model checking of properties
like #20 , I am more optimistic than you - indeed we do check properties about
spilt transactions with tag matching. There are three reasons for optimism:
- The large state spaces in themselves are not an obstacle to successful
model checking. The way the approach naturally works can handle large
state spaces, without the need for specially clever tricks.
- In practice, on can often have very high confidence in the comprehensiveness
of a model-checking exercise, even if it is not exhaustive. For example, one
may check a property for a representative value of a tag.
- In principle, there are more sophisticated approaches one could take for
things like tags, which are only used for matching, and are not manipulated.
One could compile an "abstract interpretation" of an RTL design, in which a
tag type has three members: the value you're interested in; values
different from the one you're interested in; and any value. Properties passing
on this abstract interpretation would mean that similar properties were true
of the concrete model, for all values of the tag.
I would guess that in future we may want our property language to be
interpreted on a variety of abstract models.
Anthony
On Nov 20, 3:13pm, bdeadman@sdvinc.com wrote:
> Subject: Re: ForSpec's rigid variables
> Hi Anthony,
>
> Thanks for your comments. Before going deeply into this, have you seen the
> example properties document? If not I guess it would be appropriate for
> someone to forward a copy to you. Much of the comment on "rigid bit"
> variables has been triggered by properties such as #20, that we proposed
> because we want to write such things for protocol verification
> applications, including, as you comment split transaction reconciliation.
>
> IMHO todays model checkers have no hope of handling the number of states
> required to even scratch the surface of verifying multiple concurrent split
> transactions on, for example, a PCI bus. These properties can, however, be
> used beneficially in simulation, where they can replace substantial amounts
> of Object Oriented procedural code.
>
> I confess I'm still not sure how much ForSpec dictates about how a 74 bit
> "rigid bit" tag is treated by either a Formal Model checker or a
> simulation-based solution, except to say that I believe it should be
> treated in a very similar to the Sugar "forall" construct, ie the property
> must hold true for all possible values of the tag. Whether there is a
> short cut to avoid having to evaluate more than 2 ^ 74 possible tags * n
> levels of concurrency in a Formal checker is, I suppose, an implementation
> issue about which I don't know enough to comment, though it's somewhat
> irrelevant since no sane person would attempt this anyway!
>
> If you look at the examples offered for Property 20, the concept in
> simulation is there ought to be a number of concurrent instances of the
> property which is exactly equal to the number of un-reconciled split
> transactions at any instant. Once a split transaction is eventually
> reconciled, possibly after multiple re-tries (or it times out) the instance
> of the checker is satisfied and can be removed, as can the tag. Against
> this background I can see several possible implementations of IBM's
> "forall" or Intel's "rigid bit" structures that could be created so the
> number of values presently being considered is equal to the number of
> actual split transactions.
>
> The languages therefore express the intent just fine, though ForSpec and
> Sugar seem to impose a substantial load on the implementor to deliver a
> smart solution to stop the runtime memory requirement getting out of
> hand. In my opinion this is possible, and a simulation-based checker could
> be automatically built that will run virtually indefinitely, though the
> implementation is clearly not trivial!!! And there is also an obvious risk
> that a checker optimised for this application would have lousy performance
> in other applications!
>
> By contrast the CBV solution seems to be neat and tidy in that the approach
> will naturally limit simulation runtime memory requirements to a factor of
> the number of presently split transactions, while the temporal 'e' approach
> is to leave this in the hands of the user, though it operates in a similar
> manner.
>
> Thanks again for your comments,
>
> Bernard
>
> At 08:02 PM 11/20/2001 +0000, Anthony Mcisaac wrote:
>
>
> >If this really were the implementation, it probably wouldn't be very useful
> >without careful crafting of the test. One would probably have either a
rigid
> >variable that was never matched by any tag, or one that was matched so often
> >that it activated an unmanageable number of checkers. But it would be
> >possible to design a test so that the tag was matched on only a few
occasions,
> >and on some of these one was a long way into a pipeline of concurrent
> >split transactions.
> >
> >Formal verification is of course obliged to check properties for all values
of
> >the
> >inputs. The algorithm used for this will be very different from the account
> >above.
> >
> >I have no idea how these rigid bits in ForSpec are interpreted for
simulation,
> >but it would be interesting to know:
> >If rigid variables are introduced by the property writer, is the simulator
> >required
> >to flag any violation of the property for any value of the rigid variable,
or
> >can the
> >test writer control the value of the rigid variable?
> >Is the position different for other inputs introduced by the property
writer?
> >(if so, then I guess that
> >rigid bit x
> >and
> >bit x; model always x = x
> >aren't strictly equivalent)
>
>
>
>
> ====================================================================
> 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
>
>
>-- End of excerpt from bdeadman@sdvinc.com
-- Anthony McIsaacSTMicroelectronics Limited 1000 Aztec West Almondsbury Bristol BS32 4SQ
Tel: ++44 (0)1454 462466 Fax: ++44 (0)1454 617910
Email: Anthony.McIsaac@st.com
This archive was generated by hypermail 2b28 : Thu Nov 29 2001 - 07:20:39 PST