Randal E. Bryant Carnegie Mellon University

Symbolic Simulation and its Connection to Formal Verification

Symbolic simulation can efficiently evaluate the behavior of a circuit over many different combinations of state and input. Like other forms of simulation, it can be performed at different levels of abstraction, ranging from simplified transistor-level to very abstract term-level models. Symbolic encoding can be used to compress the representation of data, time, and even the circuit structure. In application, it can be used to simply speed up conventional simulation or to perform formal verification.

This is a preview of an invited talk that will be presented at Formal Methods in Computer-Aided Design, November 6, 2002, in Portland Oregon.

Bio
Randal E. Bryant has been on the faculty of Carnegie Mellon University since 1984. He is currently the President's Professor of Computer Science in the Computer Science Department, is the head of this department, and holds a courtesy appointment in Electrical and Computer Engineering. He has been doing research on symbolic simulation and formal hardware verification since 1985.