straction reduces the number of states necessary to perform formal verification while maintaining the functionality of the original model with respect to ifications 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 ng VHDL semantics for model abstraction to improve the performance of formal verification tools such as COSPAN.
Yee-Wing Hsieh, Steven P. Levitan