Subject: Re: ForSpec's rigid variables
From: Anthony Mcisaac (Anthony.Mcisaac@st.com)
Date: Tue Nov 20 2001 - 12:02:41 PST
On Nov 19, 2:39pm, bdeadman@sdvinc.com wrote:
> Subject: Re: ForSpec's rigid variables
> I would also comment that I don't think the term "rigid bit variable" is
> intuitive for a user migrating from an HDL simulation background, where
> variables have quite a different interpretation in sequential logic
> design. Dare I therefore suggest "forall" or some other term that implies
> loops is more appropriate?
Bernard,
I shall attempt to offer a simulation-style account. Please note that this
is a conceptual account, which may be unrelated to the way the check is
implemented in simulation.
The rigid variable is an extra input, under the control of the test writer.
She can give it a specific value, or a random value, at the start of the
simulation,
but it is then constrained to keep the same value throughout the simulation.
On any occasion when the simulator sees a tag value that happens
to be equal to this rigid variable, it activates a checker.
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)
I hope this has at least added a different viewpoint.
Anthony
-- 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 : Tue Nov 20 2001 - 12:18:08 PST