First-Order theories for the verification of complex FSMs

T. Margaria

	   A formal framework for efficient verification of Finite State
	   Machines with data path and control unit is presented. A
	   homogeneous incremental approach to the definition of gate
	   level and Register Transfer level semantics allows to build a
	   unique compositional semantics that encompasses both design
	   levels.  In particular, criteria for axiomatizing Register
	   Transfer behavioural and structural descriptions in the ART*
	   language allow to express their intended functionality within
	   a uniform {\em semantic framework} based on First-Order
	   Logic, in a {\em formal verification system}.  Proving the
	   correctness of a circuit with respect to its specifi- cations
	   is then amenable to a proof of logic equivalence between
	   the respective semantic formulae. Within this framework,
	   the proposed verification methodology allows efficient
	   hierarchical, mixed-mode verifications. Proofs are performed
	   automatically by means of the OTTER general-purpose theorem
	   prover. Experimental results show a performance improvement
	   of a factor 10 over the known RT-level verification techniques.