Subject: RE: simulation interpretation of ForSpec's rigid variables
From: Armoni, Roy (roy.armoni@intel.com)
Date: Tue Dec 04 2001 - 04:30:36 PST
Hi Bernard,
It seems that again there is confusion here between the language definition,
and the tool
implementation. So actually, to make it clear, the semantics of ForSpec
both for simulation
and for FV clearly say that option (a) below is the one. Since a rigid
variable is part of the
spec - not of the design - there is no need to generate stimuli for it. One
need to compile
the spec such that the resulting automaton will check for every possible
value.
Also, in an earlier note you wrote:
"... How many Formal tools have been proven to support this at the scale
(74 bits) that
the application demands? ... "
I would like to say that data consistency checking is very easy for model
checkers because
there is no dependency between the bits in the word. For what it worth, I
wrote the following
code in ForSpec:
/* ------------------------------------------------------------------ */
/* data in - data out modeling */
/* ------------------------------------------------------------------ */
bit[128] datain;
bit SOT, c1; // SOT - start of transaction. c1 - clock.
/* ------------------------------------------------------------------ */
/* c1 is initialized to low, and then, toggles forever. */
/* ------------------------------------------------------------------ */
init c1=false;
assign c1'=!c1;
/* ------------------------------------------------------------------ */
/* dataout implement a pipe of length 5. */
/* ------------------------------------------------------------------ */
dataout := past(datain,5,c1);
/* ------------------------------------------------------------------ */
/* Transactions may begin only after cycle 5. */
/* ------------------------------------------------------------------ */
restrict always SOT -> past(true,5,c1);
/* ------------------------------------------------------------------ */
/* Check data consistency using rigid variables. */
/* ------------------------------------------------------------------ */
rigid bit[128] datasave;
assert dataCheck := change_if (c1)
always (SOT & datasave=datain) -> wnext[5] (dataout=datasave);
The first part (above the last comment) models a simple pipeline with data
path of width
128 bits and 6 stages (datain and additional 5 stages in the past operator).
Altogether,
the model contains 128*6 bits of data, one bit of clock and 1 bit for SOT
(770 bits).
The spec contributes 128 bits for the rigid variable and a few extra bits
for the tableau
construction. So a total of ~900 variables were fed to the model checker.
It took 9 seconds
of elapsed time to verify the spec on a Pentium/Linux machine, consuming
only 500K of
memory in 21 iterations.
I also inserted an error into the spec by writing:
assert dataCheck := change_if (c1)
always (SOT & datasave=datain) -> wnext[4] (dataout=datasave);
And got a counter example, again after 9 seconds, this time with 900K of
memory and
19 iterations.
To summarize, I believe that the above example shows that the rigid
variables do not add
any meaningful overhead to model checking. They can also be implemented in
checkers
with the exact semantics as set in the language definition.
Regards,
Roy
-----Original Message-----
From: Bernard Deadman [mailto:bdeadman@attglobal.net]
Sent: Thursday, November 29, 2001 5:31 PM
To: Anthony Mcisaac
Cc: bdeadman@sdvinc.com; roy.armoni@intel.com; vfv@eda.org
Subject: Re: simulation interpretation of ForSpec's rigid variables
At 03:19 PM 11/29/2001 +0000, Anthony Mcisaac wrote:
>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?
Anthony,
I have to say I'm glad it's not just me that can't work this out! I was
beginning to feel like the dumbest person in the World!
A "rigid" variable is really counter intuitive during simulation and none
of the possibilities you raise are explained in the self proclaimed
semantics description.
In particular I don't see how the property could be checked over all values
during simulation, because the property is used as a monitor rather than to
control the stimulus for the simulation. My best guess therefore is option
b) which certainly implies the semantics are different between Formal and
simulation-based verification.
Regards
Bernard
This archive was generated by hypermail 2b28 : Tue Dec 04 2001 - 04:32:13 PST