This research is on symbolic simulation as a basis for formally verifying complex IC designs. Symbolic simulation differs from classical simulation in that during simulator operation the user can set inputs not only to 0 or 1 but also to Boolean variables. The research exploits existing simulation technology by taking a behavioral approach to circuit verification. In this, the verifier applies logic simulation to compute the circuit's response to a series of stimuli chosen to detect all possible design errors. Research tasks include: selecting a set of simulation patterns which can defeat a malicious adversary attempting to foil the verifier; determining structures and algorithms, based on binary decision diagrams, for manipulating Boolean formulas; and investigating the use of the simulation system as an aid to debugging and design.
