Formal Methods in Computer Aided Design
San Jose, CA, USA
November 12 - 16
```Paper Abstracts

---------------------------------------------------------------------------
Model checking with SAT

Edmund M. Clarke

Symbolic model checking with binary decision diagrams was a major
breakthrough and led to the use of this model checking for hardware
verification by semiconductor companies. However, because binary
decision diagrams are a canonical form for Boolean functions and
variables must occur in the same order on each path from the root to a
leaf, the number of state variables that can be handled by this means
is limited.

The development of powerful programs for determining if a Boolean
function is satisfiable promises to have an equally dramatic effect on
the success of model checking.  Bounded model checking for linear
temporal logic was the first technique to exploit the power of SAT
solvers. While this approach is useful for finding counterexamples, it
cannot in general be used to show that a formula is true in a model. A
number of methods have been proposed for making bounded model checking
complete or extending traditional fix-point algorithms for model
checking to use SAT solvers instead of binary decision diagrams. These
techniques include bounding the diameter of the model, induction,
efficient image computation using cube enlargement or circuit
co-factoring, and Craig interpolation.

My tutorial will describe how bounded model checking for linear
temporal logic works, including new linear translations into SAT and
explain the complete algorithms for SAT-based model checking and
discuss the advantages and disadvantages of each approach.

---------------------------------------------------------------------------
Theorem Proving in Verification: The ACL2 System

J. Strother Moore

I plan to mention syntax, axioms, rules of inference, the basic idea
of symbol manipulation to transform formulas, mechanization, the
cooperative roles of heuristics and decision procedures, and
user-interface issues.  I will show how you use a formal logic to
formalize different kinds of computing systems including a netlist
language, a simple compiler, a JVM.  I will do a variety of simple
proofs, first just in the functional setting (e.g., append and
reverse) and then about computational models, like a multiplier
netlist and properties of JVM bytecode programs.  Along the way I will
mention, but not dwell on, some ACL2 industrial applications just so
they know this is real.  The applications will include the AMD Athlon
FPU, a microcoded operating system kernel, and the JVM.

---------------------------------------------------------------------------
SMT Solvers: Theory & Practice

Leonardo de Moura

Decision procedures for checking satisfiability of logical formulas
are crucial for many verification applications. Of particular recent
interest are solvers for Satisfiability Modulo Theories (SMT). SMT
solvers decide logical satisfiability (or dually, validity) of
formulas in classical multi-sorted first-order logic with equality,
with respect to a background theory. The success of SMT for
verification applications is largely due to the suitability of
supported background theories for expressing verification
conditions. These theories include: the empty theory, which gives rise
to the so-called logic of equality and uninterpreted functions (EUF);
real or integer arithmetic; and theories of program or hardware
structures such as bitvectors and arrays.

In this talk we will discuss how modern SMT solvers work, the theory
behind them, and the SAT extensions required for SMT. I will also
focus in some specific (and important) theories such as: linear
arithmetic and bitvectors. I will also describe how SMT solvers are
used in industry and Microsoft in particular.

---------------------------------------------------------------------------
Integrating FV Into Main-Stream Verification: The IBM Experience

Jason Baumgartner

In this talk we discuss the evolving role of the (semi-)formal
SixthSense project at IBM. IBM has a long history of successful FV
deployment, which has secured the role of a dedicated model checking
team on virtually all IBM hardware products. However, that team is
invariably too small to impact the majority of the design logic,
resulting in FV being treated as a prioritized fire-fighting technique
peripheral to the main-stream design and (simulation-based)
verification methodology. To bring formal methods to the masses, the
SixthSense philosophy has been that of: (1) adopting reusable
specification across FV and simulation frameworks, and (2) scaling
automated formal algorithms to the size of testbenches common in
simulation frameworks.  This paradigm has resulted in substantially
wider-scale usage of SixthSense, often by users who are not versed in
formal methods, and on problems whose size and complexity far exceed
those thought amenable to automated formal analysis.

We discuss the impact this need for scalability has placed on
SixthSense technologies and implementation. In particular, we discuss
the core technologies implemented within the SixthSense system, from
semi-formal and proof algorithms to the novel transformation-based
verification framework interconnecting these with a variety of
reduction and abstraction engines. This overall framework leverages
the synergy between these algorithms to bring large testbenches within
the capacity of the core automated solver engines. In many cases, this
scalability enables bugs to be identified semi-formally, and even
proofs to be completed, without a need for any manual decomposition or
attributing of large-scale testbenches.

We lastly discuss the impact that this technical solution has had on
design and verification methodologies within IBM. We discuss numerous
applications of this technology, including designer-level verification
and design optimization, sequential equivalence checking,
reference-model style verification, and hardware-failure recreation
efforts. These include cases where the entire SixthSense testbench is
reused with main-stream simulation and emulation, and cases where
large-scale simulation-based verification tasks have been outright
replaced by SixthSense.

---------------------------------------------------------------------------
What can the SAT experience teach us about abstraction?

Ken McMillan

---------------------------------------------------------------------------
Enabling Large-Scale Pervasive Logic Verification through
Multi-Algorithmic Formal Reasoning

Jason Baumgartner, Tilman Gloekler, Devi Shanmugam, Rick Seigler, Gary
Van Huben, Hari Mony, Paul Roessler, and Barinjato Ramanandray

Pervasive Logic is a broad term applied to the variety of logic
present in hardware designs, yet not a part of their primary
functionality. Examples of pervasive logic include initialization and
self-test logic. Because pervasive logic is intertwined with the func-
tionality of chips, the verification of such logic tends to require
very deep sequential analysis of very large slices of the design. For
this reason, pervasive logic verification has hitherto been a task for
which formal algorithms were not considered applicable.

In this paper, we discuss several pervasive logic verification tasks
for which we have found the proper combination of algorithms to enable
formal analysis. We describe the nature of these verification tasks,
and the testbenches used in the verification process. We furthermore
discuss the types of algorithms needed to solve these verification
tasks, and the type of tuning we performed on these algorithms to
enable this analysis.

---------------------------------------------------------------------------
Post-reboot Equivalence and Compositional Verification of Hardware

Zurab Khasidashvili, Marcelo Skaba, Daher Kaiss, and Ziyad Hanna

We introduce a finer concept of a Hardware Machine, where the set of
post-reboot operation states is explicitly a part of the FSM
definition. We formalize an ad-hoc flow of combinational equivalence
verification of hardware, the way it was performed over the years in
the industry. We define a concept of post-reboot bisimulation, which
better suits the Hardware Machines, and show that a right form of
combinational equivalence is in fact a form of post-reboot
bisimulation. Further, we show that alignability equivalence is a form
of post-reboot bisimulation, too, and the latter is a refinement of
alignability in the context of compositional hardware verification. We
find that post-reboot bisimulation has important advantages over
alignability also in the wider context of formal hardware
verification, where equivalence verification is combined with formal
property verification and with validation of a reboot sequence. As a
result, we propose a more comprehensive, compositional, and fully-
formal framework for hardware verification. Our results are extendible
to other forms of labeled transition systems and adaptable to other
forms of bisimulation used to model and verify complex hardware and
software systems.

---------------------------------------------------------------------------
Synchronous Elastic Networks

Sava Krstic, Jordi Cortadella, Mike Kishinevsky, and John O'Leary

We formally define--at the stream transformer level--a class of
synchronous circuits that tolerate any variability in the latency of
their environment. We study behavioral properties of networks of such
circuits and prove fundamental compositionality results. The paper
contributes to bridging the gap between the theory of
latency-insensitive systems and the correct implementation of
efficient control structures for them.

---------------------------------------------------------------------------
Finite Instantiations for Integer Difference Logic

Hyondeuk Kim and Fabio Somenzi

The last few years have seen the advent of a new breed of decision
procedures for various fragments of first-order logic based on
propositional abstraction. A lazy satisfiability checker for a given
fragment of first-order logic invokes a theory-specific decision pro-
cedure (a theory solver) on (partial) satisfying assignments for the
abstraction. If the assignment is found to be consistent in the given
theory, then a model for the original formula has been found. Oth-
erwise, a refinement of the propositional abstraction is extracted
from the proof of inconsistency and the search is resumed. We de-
scribe a theory solver for integer difference logic that is effective
when the formula to be decided contains equality and disequality
(negated equality) constraints so that the decision problem partakes
of the nature of the pigeonhole problem. We propose a reduction of the
problem to propositional satisfiability by computing bounds on a
sufficient subset of solutions, and present experimental evidence for
the efficiency of this approach.

---------------------------------------------------------------------------
Tracking MUSes and Strict Inconsistent Covers

Eric Gregoire, Bertrand Mazure, and Cedric Piette

In this paper, a new heuristic-based approach is in-
troduced to extract minimal ly unsatisfiable subformulas
(in short, MUSes) of SAT instances. It is shown that
it often outperforms current competing methods. Then,
the focus is on inconsistent covers, which represent sets
of MUSes that cover enough independent sources of in-
feasibility for the instance to regain satisfiability if they
were repaired. As the number of MUSes can be expo-
nential with respect to the size of the instance, it is
shown that such a concept is often a viable trade-off
since it does not require us to compute al l MUSes but
provides us with enough mutual ly independent infeasi-
bility causes that need to be addressed in order to restore
satisfiability.

---------------------------------------------------------------------------
Ario: A Linear Integer Arithmetic Logic Solver

Hossein Sheini and Karem Sakallah

In this paper we describe our solver for systems
of linear integer arithmetic logic. Such systems are commonly
used in design verification applications and are classified under
Satisfiability Modulo Theories (SMT) problems. Recognizing the
fact that in many such applications the majority of atoms are
equalities or integer unit-two-variable inequalities (UTVPIs), we
present a framework that integrates specialized theory solvers
for those atoms within a SAT solver. The unique feature of our
strategy is its simultaneous adoption of both a congruence-closure
equality solver and a transitive-closure UTVPI solver to find a
satisfiable set of those atoms. A full-scale ILP solver is then
utilized to check the consistency of all integer constraints within
the solution. Other notable features of our solver include its
combined deduction and learning schemes that collectively make
our solver distinct among similar solvers.

---------------------------------------------------------------------------
Understanding the Dynamic Behaviour of Modern DPLL SAT Solvers
through Visual Analysis

Cameron Brien and Sharad Malik

Despite the many recent improvements in the speed and robustness of
DPLL-based SAT solvers, we still lack a thorough understanding of the
working mechanisms and dynamic behaviour of these solvers at
run-time. In this paper, we present TIGERDISP, a tool designed to
allow researchers to visualize the dynamic behaviour of modern DPLL
solvers in terms of time-dependent metrics such as decision depth,
implications and learned conflict clauses. It is our belief that
inferences about dynamic behaviour can be drawn more easily by vi-
sual analysis than by purely aggregate post-execution metrics such as
total number of decisions/implications/conflicts. These inferences can
then be validated through detailed quantitative analysis on larger
sets of data. To this end, we have used TIGERDISP with the HAIFASAT
and MINISAT solvers and have generated a few specific inferences about
their relatively efficient and inefficient solving runs. We have then
tested one of these inferences through quantitative analysis on a
larger data set and have presented our findings in this paper. An
important application of TIGERDISP would be in the development of a
solver that employs adaptive algorithms. This is an area that has
intrigued researchers in the past, but has not seen significant
results for lack of a clear understanding as to what constitutes good
progress during the run of a SAT solver. With better knowledge of
dynamic behaviour, it is conceivable that an adaptive solver could be
designed such that it switches between several competitive heuristics
at runtime based on a quantitative analysis of its own dynamic
behaviour.

---------------------------------------------------------------------------
Over-Approximating Boolean Programs with Unbounded Thread Creation

Byron Cook, Daniel Kroening and Natasha Sharygina

This paper describes a symbolic algorithm for overapproximating
reachability in Boolean programs with unbounded thread creation. The
fix-point is detected by projecting the state of the threads to the
globally visible parts, which are finite. Our algorithm models
recursion by over-approximating the call stack that contains the
return locations of recursive function calls, as reachability is
undecidable in this case. The algorithm may obtain spurious
counterexamples, which are removed iteratively by means of an
abstraction refinement loop. Experiments show that the symbolic
algorithm for unbounded thread creation scales to large abstract
models.

---------------------------------------------------------------------------
An Improved Distance Heuristic Function for Directed Software
Model Checking

Neha Rungta and Eric Mercer

State exploration in directed software model check-
ing is guided using a heuristic function to move states near
errors to the front of the search queue. Distance heuristic
functions rank states based on the number of transitions needed
to move the current program state into an error location. Lack
of calling context information causes the heuristic function to
underestimate the true distance to the error; however, inlining
functions at call sites in the control flow graph to capture calling
context leads to an exponential growth in the computation. This
paper presents a new algorithm that implicitly inlines functions
at call sites to compute distance data with unbounded calling
context that is polynomial in the number of nodes in the control
flow graph. The new algorithm propagates distance data through
call sites during a depth-first traversal of the program. We show
in a series of benchmark examples that the new heuristic function
with unbounded distance data is more efficient than the same
heuristic function that inlines functions at their call sites up to
a certain depth.

---------------------------------------------------------------------------
Liveness and Boundedness of Synchronous Data Flow Graph

Amir Hossein Ghamarian, Marc Geilen, Twan Basten, Bart Theelen,
Mohammad Reza Mousavi, and Sander Stuijk

Synchronous Data Flow Graphs (SDFGs) have proven to be suitable for
specifying and analyzing streaming applications that run on single- or
multi-processor platforms. Streaming applications essentially
continue their execution indefinitely. Therefore, one of the key
properties of an SDFG is liveness, i.e., whether all parts of the SDFG
can run infinitely often. Another elementary requirement is whether an
implementation of an SDFG is feasible using a limited amount of
memory. In this paper, we study two interpretations of this property,
called boundedness and strict boundedness, that were either already
introduced in the SDFG literature or studied for other models. A
third and new definition is introduced, namely self-timed boundedness,
which is very important to SDFGs, because self-timed execution
results in the maximal throughput of an SDFG. Necessary and
sufficient conditions for liveness in combination with all variants of
boundedness are given, as well as algorithms for checking those
conditions. As a by-product, we obtain an algorithm to compute the
maximal achievable throughput of an SDFG that relaxes the requirement
of strong connectedness in earlier work on throughput analysis.

---------------------------------------------------------------------------
Model Checking Data-Dependent Real-Time Properties of the European
Train Control System

Johannes Faber and Roland Meyer

The behavior of embedded hardware and software systems is determined
by at least three dimensions: control flow, data aspects, and
real-time requirements. To specify the different dimensions of a
system with the best-suited techniques, the formal language CSP-OZ-DC
[1] integrates Communicating Sequential Processes (CSP) [2], Object-Z
(OZ) [3], and Duration Calculus (DC) [4] into a declarative
formalism equipped with a unified and compositional semantics. In this
paper, we provide evidence that CSP-OZ-DC is a convenient language for
modeling systems of industrial relevance. To this end, we examine the
emergency message handling in the European Train Control System (ETCS)
[5] as a case study with uninterpreted constants and infinite data
domains. We automatically verify that our model ensures real-time
safety properties, which crucially depend on the system's data
handling.

Related work on ETCS case studies focuses on stochastic examinations
of the communication reliability [6], [7]. The components' data
aspects are neglected, though.

---------------------------------------------------------------------------
The design of a distributed model checking algorithm for Spin

Gerard Holzmann

For as long as many of us can remember, PC speeds and memory
sizes have been increasing, following a roughly exponential trend
that is known as Moore's curve. With it, the speed and scope of
formal methods tools has also steadily improved. It is as if the
formal methods community has been getting a free ride for many
years. But, this trend has ended. Instead of continuing to
increase clock speeds, the chips makers are now focusing on the
development of multi-core systems: doubling the number of cores
on a single chip at regular intervals, while keeping clock speeds
constant. Designers of logic model checkers must now switch
strategies as well if they want to continue the free ride.  We
report on early work on the design and implementation of a
multi-core version of the Spin model checker. In this talk I will
explain the rationale for the chosen approach, and present the
first experimental results.

---------------------------------------------------------------------------
Reducing Verification Complexity of a Multicore
Coherence Protocol Using Assume/Guarantee

Xiaofang Chen, Yu Yang, Ganesh Gopalakrishnan, and Ching-Tsun Chou

We illustrate how to employ metacircular assume/guarantee reasoning
to reduce the verification complexity of finite instances of protocols
for safety, using nothing more than an explicit state model
checker. The formal underpinnings of our method are based on
establishing a simulation relation between the given protocol M, and
several overapproximations thereof, M1, . . . , Mk. Each Mi simulates
M , and represents one "view" of it. The Mis depend on each other both
to define the abstractions as well as to justify them. We show that in
case of our hierarchical coherence protocol, its designer could easily
construct each of the Mi in a counterexample guided manner. This
approach is practical, considerably reduces the verification
complexity, and has been successfully applied to a complex
hierarchical multicore cache coherence protocol which could not be
verified through traditional model checking.

---------------------------------------------------------------------------
Advanced Unbounded Model Checking Based on AIGs, BDD Sweeping, and
Quantifier Scheduling

Florian Pigorsch, Christoph Scholl, and Stefan Disch

In this paper we present a complete method for verifying properties
expressed in the temporal logic CTL. In contrast to the majority of
verification methods presented in recent years, we support unbounded
model checking based on symbolic representations of characteristic
functions. Among others, our method is based on an advanced
And-Inverter Graph (AIG) implementation, quantifier scheduling, and
BDD sweeping. For several examples, our method outperforms BDD based
symbolic model checking by orders of magnitude. However, our approach
is also able to produce competitive results for cases where BDD are
known to perform well.

---------------------------------------------------------------------------
Symmetry reduction for STE model checking

Ashish Darbari

In spite of the tremendous success of STE model checking one cannot
verify circuits with arbitrary large number of state holding
elements. In this paper we present a methodology of symmetry reduction
for STE model checking, using a novel set of STE inference rules. For
symmetric circuit models these rules provide a very effective
reduction strategy. When used as tactics, rules help decompose a given
STE property to a set containing several classes of equivalent STE
properties. A representative from each equivalence class is picked and
verified using an STE simulator, and the correctness of the entire
class of assertions is deduced, using a theorem that we
provide. Finally inference rules are used in the forward direction to
deduce the overall statement of correctness. Our experiments on
verifying arbitrarily large CAMs and circuits with multiple CAMs, show
that these can be verified using a fixed, small number of BDD
variables.

---------------------------------------------------------------------------
Thorough Checking Revisited

Shiva Nejati, Mihaela Gheorghiu, and Marsha Chechik

Recent years have seen a proliferation of 3-valued models for
capturing abstractions of systems, since these enable verifying both
universal and existential properties. Reasoning about such systems is
either inexpensive and imprecise (compositional checking), or
expensive and precise (thorough checking). In this paper, we prove
that thorough and compositional checks for temporal formulas in their
disjunctive forms coincide, which leads to an effective procedure for
thorough checking of a variety of abstract models and the entire
calculus.

---------------------------------------------------------------------------
Life in the Jungle: Simulation vs. Verification

Robert Jones

---------------------------------------------------------------------------
Ecological Niche or Survival Gear? - Improving an
industrial simulation methodology with Formal methods

Wolfgang Roesner

---------------------------------------------------------------------------
Giving the Gorilla some Brains: How can Formal complement Simulation?

Andreas Kuehlmann

Despite much progress in the area of formal methods, simulation-based
techniques are still the main workhorse for functional verification
and will remain so for the foreseeable future.  However, contrary to
this practical reality, most research efforts in functional
verification are devoted to formal methods.  On the other hand,
current techniques applied in random-biased simulation for testing
functional correctness are mostly ad-hoc and may greatly benefit from
a more formal approach.  Examples are algorithms for efficient
constraint solving, coverage analysis, and systematic coverage
maximization.  During this panel we will discuss the pros and cons of
the various approaches to functional verification and attempt to
outline a possible synergy between them.  The goal is to increase the
awareness of large-scale verification requirements and trade-offs and
to start a discussion that might broaden the scope of current
verification research.

For introducing the topic, two industry experts will first give an
overview lecture describing requirements for large scale verification
projects and then join a larger panel to discuss the various
trade-offs and opportunities.

---------------------------------------------------------------------------
Synthesis of Designs from Property Specifications

Amir Pnueli

---------------------------------------------------------------------------
Optimizations for LTL Synthesis

Barbara Jobstmann and Roderick Bloem

We present an approach to automatic synthesis of specifications given
in Linear Time Logic. The approach is based on a translation through
universal co-Buchi tree automata and alternating weak tree automata
[1]. By careful optimization of all intermediate automata, we achieve
a major improvement in performance.

We present several optimization techniques for alternating tree
automata, including a game-based approximation to language emptiness
and a simulation-based optimization. Furthermore, we use an
incremental algorithm to compute the emptiness of nondeterministic BuĻ
chi tree automata. All our optimizations are computed in time
polynomial in the size of the automaton on which they are computed.

We have applied our implementation to several examples and show a
significant improvement over the straightforward
implementation. Although our examples are still small, this work
constitutes the first implementation of a synthesis algorithm for full
LTL. We believe that the optimizations discussed here form an
important step towards making LTL synthesis practical.

---------------------------------------------------------------------------
From PSL to NBA: A Modular Symbolic Encoding.

Alessandro Cimatti, Marco Roveri, Simone Semprini and Stefano Tonetta

The IEEE standard Property Specification Language (PSL) allows to
express all ω-regular properties mixing Linear Temporal Logic (LTL)
with Sequential Extended Regular Expressions (SEREs), and is
increasingly used in many phases of the hardware design cycle, from
specification to veri cation.

Many verification engines are able to manipulate Nondeterministic
Buchi Automata (NBA), that can represent ω-regular
properties. Thus, the ability to convert PSL into NBA is an important
enabling factor for the reuse of a large wealth of verification tools.

Recent works propose a two-step conversion from PSL to NBA: first, the
PSL property is encoded into an Alternating Buchi Automaton (ABA);
then, the ABA is converted into an NBA with variants of
Miyano-Hayashi's construction. These approaches are problematic in
practice: in fact, they are often unable to carry out the conversion
in acceptable time, even for PSL specifications of moderate size.

In this paper, we propose a modular encoding of PSL into symbolically
represented NBA. We convert a PSL property into a normal form that
separates the LTL and the SERE components. Each of these components
can be processed separately, so that the NBA corresponding to the
original PSL property is presented in the form of an implicit product,
delaying composition until search time.

Our approach has two other advantages: first, we can leverage mature
techniques for the LTL components; second, we leverage the particular
form of the PSL components that appear in the normal form to improve
over the general translation.

The transformation is proved correct. A thorough experimental analysis
over large sets of paradigmatic properties (from patterns of
properties commonly used in practice) shows that our approach
drastically reduces the construction time of the symbolic NBA, and
positively affects the overall verification time.

---------------------------------------------------------------------------
Assume-Guarantee Reasoning for Deadlock

Sagar Chaki and Nishant Sinha

We extend the learning-based automated assume guarantee paradigm to
perform compositional deadlock detection. We define Failure
Automata, a generalization of finite automata that accept regular
failure sets. We develop a learning algorithm LF that constructs the
minimal deterministic failure automaton accepting any unknown regular
failure set using a minimally adequate teacher. We show how LF can be
used for compositional regular failure language containment, and
deadlock detection, using non-circular and circular assume guarantee
rules. We present an implementation of our techniques and encouraging
experimental results on several non-trivial benchmarks.

---------------------------------------------------------------------------
A Refinement Method for Validity Checking of Quantified First-Order
Formulas in Hardware Verification

Husam Abu-Haimed, David Dill, and Sergey Berezin

We introduce a heuristic for automatically check- ing the validity of
first-order formulas of the form ∀αm ∃βn.ψ(αm, βn) that are encountered in
inductive proofs of hardware correctness. The heuristic introduced in
this paper is used to automatically check the validity of k-step
induction formulas needed to verify hardware designs. The heuristic
works on word-level designs that can have data and address buses of
arbitrary widths. Our refinement heuristic relies on the idea of
predicate instantiation introduced in [2]. The heuristic proves
quantified formulas by the use of a validity checker, CVC [21], and a
first-order theorem prover, Otter [16]. Our heuristic can be used as a
stand-alone technique to verify word-level designs or as a component
in an interactive theorem prover. We show the effectiveness of this
heuristic for hardware verification by ver- ifying a number of
hardware designs completely automatically.  The large size of the
quantified formulas encountered in these examples shows the
effectiveness of our heuristic as a component of a theorem prover.

---------------------------------------------------------------------------
An Integration of HOL and ACL2.

Michael Gordon, Warren Hunt, Matt Kaufmann, and James Reynolds

A link between the ACL2 and HOL4 proof assistants is described. This
allows each system to be deployed smoothly within a single formal
development. Several applications are being considered: using ACL2's
execution environment for simulating HOL models; using ACL2's proof
automation to discharge HOL proof obligations; and using HOL to
specify and verify properties of ACL2 functions that cannot easily be
stated in the first-order ACL2 logic.

Care has been taken to ensure sound translations between the logics
supported by HOL and ACL2. The initial ACL2 theory has been defined
inside HOL, so that it is possible to prove mechanically that
first-order ACL2 functions on S-expressions correspond to higher-order
functions operating on a variety of types. The translation between
the two systems operates at the level of S-expressions and is intended
to handle large hardware and software models.

---------------------------------------------------------------------------
ACL2SIX : A Hint used to Integrate a Theorem Prover and an Automated
Verification Tool

Jun Sawada and Erik Reeber

We present a hardware verification environment that integrates the
ACL2 theorem prover and SixthSense, an IBM internal formal
verification tool. In this environment, SixthSense is invoked through
an ACL2 function acl2six that makes use of a general-purpose external
interface added to the ACL2 theorem prover. This interface allows
decision procedures and modelcheckers to be connected to ACL2 by
simply writing ACL2 functions. Our environment also exploits a unique
approach to connect the logic of a general-purpose theorem prover with
machine designs in VHDL without a language embedding.  With an example
of a pipelined multiplier, we show how our environment can be used to
divide a large verification problem into a number of simpler problems,
which can be verified using automated verification engines.

---------------------------------------------------------------------------
Automatic Generation of Schedulings for Improving the
Test Coverage of Systems-on-a-Chip

Claude Helmstetter, Florence Maraninchi, Laurent Maillet-Contoz, and
Matthieu Moy

SystemC is becoming a de-facto standard for the early simulation of
Systems-on-a-chip (SoCs). It is a parallel language with a
scheduler. Testing a SoC written in SystemC implies that we execute
it, for some well chosen data. We are bound to use a particular
deterministic implementation of the scheduler, whose specification is
non-deterministic. Consequently, we may fail to discover bugs that
would have appeared using another valid implementation of the
scheduler. Current methods for testings SoCs concentrate on the
generation of the inputs, and do not address this problem at all. We
assume that the selection of relevant data is already done, and we
generate several schedulings allowed by the scheduler
specification. We use dynamic partial-order reduction techniques to
avoid the generation of two schedulings that have the same effect on
the system's behavior. Exploring alternative schedulings during
testing is a way of guaranteeing that the SoC description, and in
particular the embedded software, is scheduler-independent, hence more
robust. The technique extends to the exploration of other non-fully
specified aspects of SoC descriptions, like timing.

---------------------------------------------------------------------------
Simulation Bounds for Equivalence Verification of Arithmetic Datapaths with
Finite Word-Length Operands

Namrata Shekhar, Priyank Kalla, M. Brandon Meredith, and Florian Enescu

This paper addresses simulation-based verification of highlevel
descriptions of arithmetic datapaths. Instances of such designs are
commonly found in DSP for audio, video and multimedia applications,
where the word-lengths of input/output bit-vectors are fixed according
to the desired precision. Initial descriptions of such systems are
usually specified as Matlab/C code. These are then automatically
translated into behavioural/RTL descriptions (HDL) for subsequent
hardware synthesis.

In order to verify that the initial Matlab/C model is bit-true
equivalent to the translated RTL, how many simulation vectors need to
be applied?  This paper explores results from number theory and
commutative algebra to show that exhaustive simulation is not
necessary for testing their equivalence. In particular, we derive an
upper bound on the number of simulation vectors required to prove
equivalence or identify bugs. These vectors cannot be arbitrarily
generated; we determine exactly those vectors that need to be
simulated. Extensive experiments are performed within practical CAD
settings to demonstrate the validity and applicability of these
results.

---------------------------------------------------------------------------
Design for Verification of the PCI-X Bus.

Ali Habibi, Haja Moinudeen, and Sofiene Tahar

The importance of re-usable Intellectual Properties (IPs) cores is
increasing due to the growing complexity of today's system-on-chip and
the need for rapid prototyping. In this paper, we provide a design for
verification approach of a PCI-X bus model, which is the fastest and
latest extension of PCI technologies. We use two different modeling
levels, namely UML and AsmL. We integrate the verification within the
design phases where we use model checking and model based testing,
respectively at the AsmL and SystemC levels. This case study presents
an illustration of the integration of formal methods and simulations
for the purpose of providing better verification results of SystemC
IPs.

---------------------------------------------------------------------------
Formal Analysis and Verification of an OFDM Modem Design using HOL

Abu Nasser Mohammed Abdullah, Behzad Akbarpour, and Sofiene Tahar

In this paper we formally specify and verify an implementation of the
IEEE802.11a standard physical layer based OFDM (Orthogonal Frequency
Division Multiplexing) modem using the HOL (Higher Order Logic)
theorem prover. The versatile expressive power of HOL helped model the
original design at all abstraction levels starting from a
floating-point model to the fixed-point design and then synthesized
and implemented in FPGA technology. The paper also investigates the
rounding error accumulated during ideal real to floating-point and
fixedpoint transitions at the algorithmic level.

---------------------------------------------------------------------------
A Formal Model of Lower System Layers

Julien Schmaltz

We present a formal model of the bit transmission between
registers with arbitrary clock periods. Our model considers precise
timing parameters, as well as metastability. We formally de ne the
behavior of registers over time. From that de nition, we prove, under
certain conditions, that data are properly transmitted. We discuss how
to incorporate the model in a purely digital model. The hypotheses of
our main theorem de ne conditions that must be satis ed by the purely
digital part of the system to preserve correctness.

---------------------------------------------------------------------------
Formal Verification in Industry -- Current State and Future Directions

Christian Jacobi

Recent years have shown a dramatic increase in the capabilities
of formal and semi-formal verification methods. Despite those
improvements, the main verification work-horse in industry
remains random simulation. In this talk we will summarize the
verification approaches applied in large-scale microprocessor
development projects, and will describe where and how formal
verification is already being applied. We then describe some
obstacles that prevent a wider range of FV usage, and discuss
some ideas on how the research community could help to overcome
those obstacles. One of those ideas is the development of
"verification templates": blue-prints for how to verify certain
types of logic. For example, there are well known and proven
strategies for arithmetic circuits, but there is little
experience on the automatic verification of complex cache
controllers at the RTL level. Another obstacle is lacking synergy
between simulation and FV techniques, which could be improved
with synthesizable testbenches that can run in simulation, formal
verifcation, and also on hardware accelerators.

---------------------------------------------------------------------------
Balancing Formal and Dynamic Techniques in Validation of Industrial
Arithmetic Designs

Roope Kaivola

Formal verification of microprocessor components has been pursued
in various forms for roughly a decade now in Intel. One of the
most successful target areas has been the verification of
floating-point arithmetic units against IEEE floating-point
standard. In this area, formal verification has become an
established practice applied in most recent processor designs. I
will describe our verification framework for the task, combining
symbolic simulation and BDD analysis with theorem-proving, inside
a general-purpose functional programming language.  I will also
discuss the tradeoffs between dynamic testing and formal
verification in a product development project setting.

---------------------------------------------------------------------------
Perils of Post-Silicon Validation

Piyush Desai

Efficient and timely post-si validation of contemporary general
purpose CPUs is a daunting task due to three formidable obstacles.

1. Explosion of configuration, state, and data space that must be
validated to warrant production quality coverage.

2. Lack of necessary and sufficient control (stimuli) to accelerate
validation and debug.

3. Lack of necessary and sufficient visibility for coverage
measurements and failure debug.

The explosion of the coverage space that must be targeted for
necessary and sufficient post-si validation is the most fundamental
barrier that deserves immediate attention. The problem is rooted in
the fact that there are no formal and deterministic methods to specify
a necessary and sufficient coverage sub-space (N+S sub-space) from the
virtually infinite coverage space of a typical CPU
implementation. Once a formal specification paradigm is available to
capture the total coverage space, algorithms can be developed to prune
the space to identify inherent redundancies, factor in user specified
constraints, and deduce the N+S sub-space.  Tools based on such
coverage pruning algorithms can be directed to generate test cases to
exercise the N+S sub-space, and/or sweep through run-time execution
traces to gather coverage data and even recognize functional
anomalies. Such approaches have been applied with limited success to
specific functional domains such as the instruction-set architecture
and the architecturally defined memory ordering. More general
techniques and algorithms must be developed however to specify and
prune large state machines, and data and configuration spaces.

A critical variation of the coverage theme is sustained stress testing
around design corners. As opposed to testing for functional coverage,
sustained stress testing of complex control logic and datapths tends
to expose rare functional failures and circuit marginalities that
almost always involve intricate sequence of unpredictable events and
data patterns. Staging sustained stress scenarios require precise
analytical or queuing models in order to characterize the optimal
instruction and data flows that will saturate the underlying control
logic and datapath structures with maximal achievable throughput
rate. Applicable random events are introduced in such instruction/data
flows at different rates to stress the design. A framework for
building formal stochastic models for major control and datapaths in a
CPU implementation would significantly accelerate stress testing and
the discovery of the gnarly design errata that are usually associated
with such testing.

These are just couple of examples of the challenges we face and need
to address in the industry. Given that the realm of post-si functional
validation has remained relatively unexplored in the academia, while
the architecture of general purpose CPUs has been evolving rapidly to
satisfy a myriad of demanding workloads of multimedia, database, and
networking/communication tasks, significant challenges and
opportunities exist for researching breakthrough solutions for the
aforementioned barriers. In this talk I will give a prelude to more of
these challenges and opportunities.

---------------------------------------------------------------------------
Sequential Equivalence Checking across Arbitrary Design Transformations:
Technologies and Applications

Viresh Paruthi

High-end hardware design flows mandate a variety of sequential
transformations to address needs such as performance, power,
post-silicon debug and test. Furthermore, it is often the case that
functional design modifications are required to preserve
backward-compatibility of specific aspects and modes of design
behavior. The industrial demand for robust sequential equivalence
checking (SEC) solutions capable of efficiently and exhaustively
proving the required equivalence criteria between two designs is thus
becoming increasingly prevalent. In this talk, we discuss the role of
SEC within IBM. We motivate the need for a highly-automated scalable
solution, which is robust against a variety of design transformations
- including those that alter initialization sequences, and preserve
equivalence only conditionally. This motivation has caused us to
embrace the paradigm of SEC with respect to designated initial states.

We next describe the unique technologies comprised within our SEC
framework, embodied in the SixthSense toolset. To achieve the
necessary degree of scalability, we leverage a diverse set of
synergistic transformation and verification algorithms within our SEC
framework, which we have found necessary for the automated solution of
the most complex SEC problems. Lastly, we discuss numerous types of
applications of this SEC solution in an industrial setting, and its
significance in reshaping design and verification methodologies.

---------------------------------------------------------------------------
On-Chip Instrumentation as a Verification Tool

Rick Leatherman

On Chip Instrumentation or OCI, the addition of IP to perform in
silicon analysis and optimization of complex systems been widely used
for processor subsystems that are not amenable to purely software
oriented verification approaches. First Silicon Solutions is extending
this approach to address larger portions of the architecture and more
global instrumentation of the SoC. We will discuss approaches to OCI
in current use as well as work being done by related ongoing standards
groups and activities with regards to open problems in this area.

```