Subject: CBV DEFENSE, REVISED POINTS ONLY
From: John Havlicek (havlicek@adttx.sps.mot.com)
Date: Tue Nov 20 2001 - 08:37:29 PST
Dear VFV:
I have been requested to post just the revised comments of the
CBV defense so that committee members do not have to sift through
all defense points in looking for the revisions.
Below are the revised comments that differ from the corresponding
comments in the original defense.
Regards,
John Havlicek
===============================================================================
R1e The language must define more than one language binding.
Not fulfilled by CBV. CBV defines only a binding to Verilog expressions.
CBV can be modified to accept VHDL expressions or other similarly
expressive expressions.
R25a The language must allow arbitrary composition of formulae and temporal
operators.
Not fulfilled by CBV.
The temporal operators of CBV are "+(n)", "+(n to m)", "+(n to *)",
and "eventually". These operators are discussed individually below.
1. +(n). This operator can be applied to any CBV statement:
+(n) : <statement>
2. +(n to m). This operator can be applied to CBV expression
statements:
+(n to m) : <expression> ;
Application of "+(n to m)" to a general CBV statement is
syntactically illegal, but the desired meaning can be expressed
by
if +(n to *) : (STAR =< m)
<statement>
3. +(n to *). Application of "+(n to *)" to a CBV statement is
syntactically illegal, but the desired meaning can be expressed
by
if +(n to *) : (1)
<statement>
4. eventually. Application of "eventually" to a CBV statement is
syntactically illegal.
CBV can be modified to allow application of "eventually" to
any CBV statement. Doing so will disrupt the current coding
paradigm and intuitive semantics of CBV. Also, the meaning of
a CBV module may no longer be captured by a dual-run omega
automaton whose size is linear in the product of the size of
the text of the CBV module and the size of the state space of
its global and local variables.
The omega language of
eventually <statement>
is the union of the omega languages of
+(n) : <statement>
where n ranges over the non-negative integers. An implementor
of this feature can choose a convenient representation for a
specification that applies "eventually" to statements. One
possibility is to use a non-deterministic alternating omega
automaton, in which case a node for an "eventually" statement
should be existential and have a self loop.
R27a The language must be defined such that properties are closed under
negation.
Not fulfilled by CBV. CBV can be modified to be able to express
all omega-regular properties (see R71d), in which case its properties
will be closed under negation.
R34a The language must support description/use of level-sensitive clocks.
Not fulfilled by CBV. We doubt that modification of CBV to support
level-sensitive clocks is a serious issue, but we still do not
understand enough about level-sensitive clocks to give a proposal.
For example, to define the meaning of "+(n to m)" for a level-sensitive
clock, we need to understand the meaning of the period of the
clock.
CBV allows triggering and capture based on level-sensitive conditions,
such as
if (~a)
$a_low_check() ;
However, the sampling points for testing these conditions are
determined by edge events of other clocks or by the finest granularity
of transition of the formal model.
R46a The language must support user-defined parameterized macro
definition and expansion.
Not fulfilled by CBV. CBV provides the `define, `ifdef, and
`include preprocessing directives. But CBV does not provide
a more expressive macro language. Other text processing
macro expansion tools can be run over CBV files before compiling
the CBV.
CBV can be modified to support richer macro definitions and
expansion.
R52a The language must support specification that a signal is constant
between successive events (e.g., clock edges).
Fulfilled by CBV. For formal verification, the design is
converted to a model that is a discrete transition system.
CBV can sample at the granularity of transitions of this
model and therefore can express constancy of signals sampled
at this granularity.
R55a The language semantics for formal verification must be well-defined.
Fulfilled by CBV. A CBV specification module defines a
non-deterministic, dual-run (a.k.a., forall) omega automaton
whose acceptance conditions is defined in terms of finitely many
LTL formulas of the forms
(Ga), (G(b -> Fc))
where a,b,c are sets of states of the automaton. The various
assertions of the CBV specification give rise to the (Ga) formulas,
and the eventualities give rise to the (G(b -> Fc)) formulas.
The temporal preconditions for the assertions and eventualities
determine the finite state machine underlying the automaton. The
automaton accepts an omega string if and only if all its runs over
the omega string satisfy all the LTL formulas.
The complement of the specification automaton is a B\"uchi automaton
with the same underlying FSM. The CBV specification can be formally
verified by checking emptiness of the language of the product of the
model with this B\"uchi automaton.
If CBV is expanded as described under R71d, then an additional
form of acceptance condition,
(G(d -> FGe))
will be added.
R56a The language semantics for simulation must be well-defined.
Fulfilled by CBV. In terms of the comment for R55a, the
specification passes a finite simulation if and only if all
finite runs of the specification automaton over the finite
simulation string satisfy the LTL formulas of the form (Ga)
and (G(b -> Fc)). The eventuality obligations are required
to be fulfilled within the the finite simulation.
R65a The language must support efficient negation/complementation of
properties. (Subjective)
Not fulfilled by CBV. CBV does not have a negation operator.
CBV can be modified to include a negation operator "not",
applicable to CBV statements. The "not" operator provides a
syntactically efficient negation. The overall efficiency
of static and dynamic verification for CBV with "not" will
depend on choices of representation and algorithm by the
implementor.
Adding "not" will disrupt the current coding paradigm and intuitive
semantics of CBV. Also, the meaning of a CBV module may no longer
be captured by a dual-run omega automaton whose size is linear in
the product of the size of the text of the CBV module and the size
of the state space of its global and local variables.
The omega language of
not <statement>
is the complement of the omega language of
<statement>
An implementor of this feature can choose a convenient representation
for a specification that uses the "not" operator. The following
equivalence rules may be useful in coalescing instances of the "not"
operator. In these rules, "E" is an expression and "S" and "T" are
CBV statements.
0. not not S
<->
S
1. not E ;
<->
!(E) ;
2. not +(n to m) : E ;
<->
if +(n to m) : (E) 0 ;
3. not +(n) : S
<->
+(n) : not S
4. not if +(n to m) : (E) S
<->
begin
+(n to m) : E ;
+(m) : not S
end
5. not if +(n) : (E) S else T
<->
if +(n) : (E) not S else not T
6. not
begin
loc_1 <= <expression_1>;
...
loc_k <= <expression_k>;
S
end
<->
begin
loc_1 <= <expression_1>;
...
loc_k <= <expression_k>;
not S
end
Pushing "not" through a non-recursive task call can be
accomplished by first inlining the task body. The cost of
all such inlinings is at most a squaring of the size of
the CBV text.
One possible representation is an alternating automaton. If "not"
is applied to a "begin-end" statement, the node for the "begin-end"
can be made existential together with application of the "not"
to each of the constituent statements of the "begin-end". It
may be convenient to make one positive and one negated version
of each task that is defined. The resulting alternating automaton
should satisfy the bound given under (R64a) for the original
dual-run automaton.
Alternatively, one can complement the appropriate sub-automata
of the dual-run automaton described under (R55a). In general,
the complementation may result in an exponential blowup. The
complementation should be achievable on the automaton that
represents the CBV module stripped of its variables--in other
words, the FSM for the global variables and the state space of
the local variables of the CBV module should not be involved
in the complementation.
R71b The language must support assumptions with no proof obligation
(e.g., for case splitting).
Not fulfilled by CBV. CBV can be modified to support case splitting
based on additional constraints. The case splitting conditions
can be checked easily for logical exhaustiveness by comparing the
BDD for their disjunction to logical 1.
R71c The language must support formulae (to be assumed) that can specify
any omega-regular language.
Not fulfilled by CBV. CBV can be modified to fulfill R71d and
R71f, in which case fulfillment of R71c follows.
R71d The language must support formulae (to be checked) that can specify
any omega-regular language.
Not fulfilled by CBV. More accurately, the question of whether
CBV, as submitted to Accellera, can express every omega-regular
property is not resolved. CBV can easily be modified, however,
to achieve so-called "omega-regular power". One can add the
following statement:
limit_task_set(<task1>, <task2>, ... ) ;
The limit_task_set statement is placed in any begin-end statement
and activates a limit task obligation for each of the statements
in the body of the begin-end.
The meaning is that an omega sequence is accepted if and only if
all runs of the CBV specification automaton over the sequence
satisfy the old CBV acceptance criteria and, additionally, satisfy
the LTL formula
G(activate_limit_task_set -> FG(task1_active | task2_active | ... ))
With the limit_task_set statement, it is straightforward to encode
any omega-regular property using a B\"uchi automaton for the
complement of the property. One defines a task for each state of the
B\"uchi automaton. The next-state relation is encoded within these
tasks using begin-end statements to achieve non-deterministic
branching. There are variables
var not_init[0:0] = 1 ;
assign init[0:0] = ~not_init ;
to detect the first cycle. If G1,...,Gm are the tasks for the
non-final states of the B\"uchi automaton and if I1,...,Ik are
the tasks of the initial states of the B\"uchi automaton, then
the following top-level CBV statement accepts the original property:
if (init)
begin
limit_task_set(G1,...,Gm) ;
I1 ;
...
Ik ;
end
R71f The language must support assuming every assertion.
Not fulfilled by CBV. CBV can be modified to support this
requirement by adding an "assume" directive of the form
assume <statement>
The "assume" directive indicates that the property represented
by <statement> is to be treated as an assumption. Only top-level
statements can be conditioned by the "assume" directive. As an
equivalent alternative to applying "assume" to every top-level
statement of a module, the user can condition the module itself
as follows:
assume module <prefix> ;
This archive was generated by hypermail 2b28 : Tue Nov 20 2001 - 08:57:13 PST