Design validation currently consumes a significant percentage of the design team and takes months of simulation time. This validation strain is bound to increase as the complexity of designs increases; simulation alone cannot be expected to keep up with the verification problem. Purely formal techniques for verification have made considerable progress over the last decade but still fall short of providing the breadth and depth of verification required for most integrated circuits, and require considerable investment of time and energy on the designer's part.

We have developed a validation approach that lies between simulation and formal verification, and uses a single specification model. The approach consists of a "golden" deterministic behavior description model, and a validation procedure to verify the equivalence between this golden model and any valid implementation of it. In this paper we present our approach where Linear Temporal Logic (LTL) with bounded future-time operators is used for behavioral property specification. Simulation monitoring and assertion checking is used in a state-of-the-art mixed Verilog/VHDL simulator (Mentor's ModelSim) in order to validate the design implementation against the desired properties.

Bio

Bassam Tabbara is a Ph.D. Candidate in EECS at the University of California at Berkeley. He received his B.S. in Electrical Engineering (summa cum laude) from UC Riverside in 1994, and his M.S. in Electrical Engineering from Berkeley in 1998. He is a fellow of the SRC, member of IEEE, and the CAD for VLSI group at Berkeley. His research interests include specification, validation, synthesis, and optimization of embedded systems.

Abdallah Tabbara is a Ph.D. Candidate in EECS at the University of California at Berkeley. He received his B.S. in Chemistry (magna cum laude) from UC Riverside in 1993, M.S. in Physical Chemistry from UC Riverside in 1994, and his M.S. in Electrical Engineering from Berkeley in 1999. He is a member of ACM, and the CAD for VLSI group at Berkeley. His research interests include design specification, and synthesis and physical design for DSM.