SYMBOLIC MODEL CHECKING FOR SEQUENTIAL-CIRCUIT VERIFICATION

The temporal logic model checking algorithm of Clarke, Emerson, and Si stla [17] is modified to represent state graphs using binary decision diagrams (BDD's) [7] and partitioned transition relations [10], [11]. Because this representation captures some of the regularity in the sta te space of circuits with data path logic, we are able to verify circu its with an extremely large number of states. We demonstrate this new technique on a synchronous pipelined design with approximately 5 x 10( 120) states. Our model checking algorithm handles full CTL with fairne ss constraints. Consequently, we are able to express a number of impor tant liveness and fairness properties, which would otherwise not be ex pressible in CTL. We give empirical results on the performance of the algorithm applied to both synchronous and asynchronous circuits with d ata path logic.