EECS 298-11: CAD Seminar
Wednesday, February 19, 1997, 5pm
Cory Hall--Hogan Room


		Validity Checking for Combinations of Theories with Equality
					David Dill
		   		Stanford University

SVC is a decision procedure for a fragment of first-order logic with
equality, uninterpreted functions, array operations, and linear
arithmetic.  SVC allows automatic reasoning about infinite sets
of values.  Even when reasoning about finite-size values, SVC
can work at the word level rather than the bit level, and unlike
BDDs, does not require a (potentially large) canonical representation
of the logical formula.  SVC is currently being used in an effort
to verify a microprocessor formally at the RTL level, in addition to
other applications.

I will describe some of the capabilities, issues, and algorithms used
in SVC.