Yee-Wing Hsieh and Steven P. Levitan
Department of Electrical Engineering
University of Pittsburgh
Model abstraction reduces the number of states necessary to perform formal verification while maintaining the functionality of the original model with respect to the specifications to be verified. However, in order to perform model abstraction, we must extract the semantics of the model itself. In this paper, we describe a method for extracting VHDL semantics for model abstraction to improve the performance of formal verification tools such as COSPAN.
Keywords: VHDL semantics extraction, memory semantics extraction, control/data-flow analysis, model partitioning, model abstraction
Retrieve Word file (199809_02.doc : 3,411,968 bytes)
Received October 31, 1997; revised March 18, 1998.
Communicated by Jin-Yang Jou.
1 This work was supported, in part, by the National Science Foundation under MIP-9102721.