Proceedings 10th IEEE Conference on:
Logic in Computer Science,
June 1995, San Diego, CA, 
IEEE Computer Society Press


Title:
Hardware Verification, Boolean Logic Programming,
Boolean Functional Programming.


Author:
Enrico Tronci
Univ. di L'Aquila
tronci@univaq.it
http://univaq.it/~tronci



Abstract

One of the main obstacles to automatic verification
of Finite State Systems (FSS) is state explosion.

In this respect automatic verification of an FSS M
using Model Checking and Binary Decision Diagrams 
(BDDs) has an intrinsic limitation: no automatic
global optimization of the verification task is possible
until a BDD representation for M is generated.
This is because systems ans specifications are defined
using different languages.

To perform global optimization before generating
a BDD representation for M we propose to use the same 
language to define systems and specifications.

We show that First Order Logic on a Boolean Domain
yields an efficient functional programming language
that can be used to represent, specify and automatically
verify FSS.

We show practical usefulness of our techniques
by giving experimental results on the automatic
verification of a commercial 64 bit multiplier
based on the Motorola MC14554B 2 bit multiplier.