Control/Data-flow Analysis for VHDL Semantic Extraction
Yee-Wing Hsieh, Steven P. Levitan · 1998
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. 1 Introduction Validating a design using formal verification methods is inherently computationally intensive, and, as a result, only small designs can be verified. To handle large designs, model abstraction is necessary. Model abstraction takes a model and replaces it with a highlevel description of non-deterministic automata that encapsulates the behavior of the model it replaces. Using this high-level abstract representation, model abstraction reduces the number of states necessary to perform formal verification and thus reduces the st...