EECS 298-11: CAD Seminar Wednesday, February 28, 1995, 5pm 531 Cory Hall, Hogan Room Datapath Abstraction in Hardware Systems Ramin Hojati UC Berkeley The biggest stumbling block to make formal verification widely acceptable is the state space explosion problem. Abstraction is used to simplify a design so that the number of reachable states is reduced. Integer combinational/sequential (ICS) is a concurrency model capable of describing hardware systems at high and low levels of abstractions. ICS uses finite relations, interpreted and uninterpreted integer functions and predicates, interpreted memory functions, and supports non-determinism and fairness constraints. As a subset, it includes finite-state systems with general fairness constraints. Verification in this framework is performed using language containment as follows. 1. For a subclass of control-intensive ICS models, we prove that finite small instantiations can be used to decide the properties, sometimes with and sometimes without sacrificing accuracy. These results also hold for the standard finite-state systems and, thus provide some generic methods for automatic datapath abstraction for such systems. 2. For verifying properties of circuits with complex datapaths, the model can be executed symbolically to find the reachable states. This set of reachable states, which is not always finite, can then be used for property verification. In this talk, I present an introduction to the theory of ICS models, present some basic abstraction results, and give applications of these results to microprocessor and hardware verification. Upcoming Seminars: 3/6/96: Steve McGeady, Intel Internet Technology Lab 3/13/96: Yogen Dalal, Mayfield Fund 3/20/96: Thomas A. Henzinger, UC Berkeley