ACL2 seminar, May 16, 2007

		Circuit Specification,
	 Abstraction, and Reverse Engineering

	      ***  Work In Progress  ***

		  Warren A. Hunt, Jr.

We are developing analysis and verification mechanisms for models
composed of hierarchically specified, cooperating finite-state
machines.  Our specification approach permits not only functional
properties, but also delay and dependency properties to be verified
using the ACL2 theorem-proving system.  We have used this system to
represent and compare a number of flawed adder specifications to a
reference adder specification in an effort to determine the usefulness
our tools to analyze flawed-circuit models; this determination is
still in progress.

We discuss a mechanism to count the number of different behaviors
between two circuits.  We present two different kinds of flawed adder
specifications, and we count the number of different behaviors between
these adders and our reference adder.  We are attempting to determine
if the number of different behaviors can be a useful metric when
attempting to discover subtle, possibly induced, flaws.  We also
investigate the use of dependency information as another means to
determine whether a circuit might have been inadvertently or
maliciously altered.  The novelty, if any, of our approach lies in our
ability to exactly count the number of cases where two Boolean
functions differ.