mwang@watmath.UUCP (mwang) (10/29/85)
DEPARTMENT OF COMPUTER SCIENCE
UNIVERSITY OF WATERLOO
COMPUTER SCIENCE COLLOQUIUM
- Wednesday, November 6, 1985.
Prof. Randal E. Bryant of Carnegie-Mellon University
will speak on ``Formal Verification of Digital Circuits
by Logic Simulation''.
TIME: 3:30 PM
ROOM: MC 5158
ABSTRACT
A logic simulator can prove the correctness of a digi-
tal circuit if it can be shown that only circuits
implementing the system specification will produce a
particular response to a sequence of simulation com-
mands. This style of verification has advantages over
other proof methods in being readily automated and
requiring less attention to the low-level details of
the design, as well as advantages over other approaches
to simulation in providing more reliable results, often
at a lower cost.
This talk explores two methods for verifying circuits
by logic simulation. The first, called ``black-box''
simulation, involves simply observing the output pro-
duced by the simulator in response to a sequence of
inputs with no consideration of the internal circuit
structure. In contrast to the classical machine iden-
tification problem, however, the simulator is assumed
capable of modeling a signal as having an unknown or X
value, where the simulator must produce responses that
are monotonic for the partial ordering X < 0 and X < 1.
In addition to supplying input sequences, the user can
command the simulator to set all internal signals to X.
It is shown that a circuit can be verified by black-box
simulation if and only if the specified behavior is
that of a definite system, i.e. the output of the sys-
tem at any time depends only on the most recent k
inputs for some constant k. The second method, called
``inductive'' simulation, involves using the simulator
October 24, 1985
- 2 -
to prove a series of assertions about the circuit
behavior from which it can be inferred that the circuit
will operate correctly for all possible input
sequences. This method can be used to verify arbitrary
circuits, but requires the user to introduce informa-
tion about the internal structure of the circuit.
In general the circuit verification problem is NP-hard.
However, for a variety of different types of memory
circuits the ability of the simulator to model unknown
signals can be exploited to verify the circuit with a
simulation sequence that is linear or near-linear in
the memory size.
Refreshments will be served at 3:00pm.
October 24, 1985