Interfacing System Description Languages to
State-Space Exploration-Based Verification
Using the Non-Deterministic Abstract Machine Representation
This work identifies two techniques usable in a design verification
system based on language-containment. They allow for the predictable
treatment of synchronous systems with large state-spaces in the
context of the reachable-states computation and language-containment
check. The first technique is a restriction on the synchronous system
description along two axes: the patterns of inter-process
communication and the variety of intra-process transition relations
allowed. This restriction is embodied in the Non-Deterministic
Abstract Machine (NDAM) architecture and notation. The second of the two
techniques is cofactor tuples which
take advantage of the structure imposed by first restriction and allow
for larger system descriptions to be processed faster in the
reachable-states computation.
The contribution of this work is that design verification queries for
arbitrary synchronous systems may be formulated for more efficient
solution in terms of communications and operations on a known system
architecture rather than in terms of a direct analogy with a digital
circuit. In particular the intent is to be able to provide faster
results for larger systems by mapping an arbitrarily-structured
synchronous system description onto a larger but more well-structured
synchronous architecture. That architecture being well-structured in
the sense of being known to have good properties for the two main
computations of concern in language-containment based design
verification: the reachable states computation and the transition
relation transitive closure computation. The goal of this mapping is
to offer a more stable base upon which design verification queries can
be formulated.
Non-Deterministic Abstract Machine (NDAM)
The virtual system architecture of proposed has much the same form as
that of a clock-cycle based simulator or a synchronous software
program. Examples of such architectures in real-world systems include
programs written in a the Synchronous VHDL subset
[Baker93] or any
Esterel program
[BerryGonthier88].
The virtual architecture consists of
a number
of processes each of which has its own local memory that can only be
manipulated by it. Processes communicate with each other and with the
system environment by means of valued signals which are available to
all other processes as a broadcast medium. Signals are statically
allocated resources and maintain a notion of event occurrence. Time is
discrete and is marked off by instants between which nothing else of
interest occurs in the system. For any signal an event may or may not
have occurred in the current instant and a process may await events on
one or more signals.
Cofactor Tuples
Cofactor tuples are used to speed up the next-state computation for
well-characterized transition relations such as those corresponding to
certain operations in an instruction set processor. The cofactor
tuples are a method for hardcoding these transition relations using
tuples of integers to represent the nodes of a transition relation
BDD. This representation is possible because these transition
relations are only used in the and_smooth portion of the next-state
computation and in that context, only the cofactor operation is needed
on the representation. The integer tuple representation is significant
for it allows very large but highly-regular transition relations to be
represented compactly outside the BDD system yet to operate
consistently with a BDD-based symbolic and_smooth computation. The
savings of this representation can be quite significant in both space
and time. For example, the worst case size of a BDD representation for
a single-register writeback to a register file is . Quite a number of
the transition relations in the NDAM architecture have the necessary
highly-regular properties.
- [Baker93]
-
``An Application of the Synchronous/Reactive Semantics to
the VHDL Language,'' UCB/ERL Memo 93/10, 1993. Also available by
ftp.
- [BerryGonthier88]
-
``The Esterel Synchronous Programmign Language:
Design, Semantics, Implementation,'' Rapport de Recherche 842,
INRIA, 1988.
Last Updated 5/13/94.
service entrance.