Table of Contents

Mohamad Noureddine, Fadi A. Zaraket, American University of Beirut

Ali S. Elzein, IBM Systems and Technology, elzein@us.ibm.com

Synthesis techniques take realizable Linear Temporal Logic specifications
and produce correct circuits that implement the specifications.
The generated circuits can be used directly in logic designs,
and can also be used as miters that check the correctness of a design.
Typically, those techniques generate a non-deterministic finite state
automata and translate it into a finite state automata resulting in
an exponential blowup in the number of state elements.
In this paper, we focus on the problem of generating an And-Inverted-Graph
sequential circuit *C* out of an LTL specification *F*,
expressed in sequential extended regular expressions,
for the goal of using
*C* in symbolic and bounded model checkers to validate the
correctness of *S*; an existing circuit implementation of *F*.
We directly encode the non-determinism in *F* using free input
variables resulting in a sequential circuit *C* with a number of states
linear in the size of the formula *F*.
While our technique does not reduce the size of the symbolic
and bounded model checking problem, it succeeds to generate the input
to the model checker where other techniques fail, and in most
cases the model checker succeeds to either find defects in the design
that was otherwise uncheckable, or validates the design.
We evaluated our technique against existing synthesis techniques
with several benchmarks generated
from existing LTL synthesis tools and industrial benchmarks including
the IBM arbiter, a load balancer, and a traffic light system.
Our method found defects and validated systems that we were unable to model
check using NUSMV because LTL synthesis failed.

Except where otherwise noted, content on this wiki is licensed under the following license:CC Attribution-Noncommercial-Share Alike 3.0 Unported