abstraction, modular verification, timed circuits
The major barrier that prevents the application of formal verification to large designs is state explosion. This paper presents a new approach for verification of timed circuits using automatic abstraction. This approach partitions the design into modules, each with constrained complexity. Before verification is applied to each individual module, irrelevant information to the behavior of the selected module is abstracted away. This approach converts a verification problem with big exponential complexity to a set of subproblems, each with small exponential complexity. Experimental results are promising in that they indicate that our approach has the potential of completing much faster while using less memory than traditional flat analysis.
Original Publication Citation
Q. Zheng, E. G. Mercer, and C. J. Myers, "Modular Verification of Timed Circuits Using Automatic Abstraction," IEEE Transactions on Computer-Aided Design of Integrated Circuits, 22(9):1138-1153, September, 23.
BYU ScholarsArchive Citation
Mercer, Eric G.; Myers, Chris; and Zheng, Hao, "Modular Verification of Timed Circuits Using Automatic Abstraction" (2003). All Faculty Publications. 477.
Physical and Mathematical Sciences
© 2003 Institute of Electrical and Electronics Engineers
Copyright Use Information