Logic Verification and Synthesis with Temporal Logic

By Masahiro Fujita

We discuss about logic verification and synthesis approaches from
temporal logic specifications. We consider logic verification and
synthesis problems under the following situations:

(1) Design is given as a FSM and specification is given as temporal
logic formulae

(2) Both design and specification are given as temporal logic formulae

In the case of logic synthesis, the problem becomes an Engineering
Change problem, since we have to rectify the given design in order to
meet the given specification.

The method we use is a kind of automata theoretic approach. We first
translate given temporal logic formulae into state transition
representations. Then we do synthesis or verification by reachable
analysis. We use two types of temporal logic, Linear Time Temporal
Logic (LTTL) and Interval Temporal Logic (ITL). Since ITL is based on
intervals and their sequences, we can easily describe both concurrent
and serial behaviors by specifying behaviors inside intervals and
sequences among them.  Although ITL is more powerful in this sense,
full set of ITL does not have a decision procedure. So, we define a
reasonable subset and use it for synthesis and verification.  Both
LTTL and ITL formulas are expanded into the ones for the present state
and those for the next states, which can be easily converted into
state machines, by tabulated rules for temporal operators.  The
generated state machines can be further processed by logic
synthesizer, such as SIS, and transformed into
synchronous/asynchronous sequential circuits.

We show some implementation results. Although our implementations use
explicit representation of states (no use of BDD), we can solve some
realistic problems.