An Automatic Design Flow from Formal Models to FPGA
Judson S. Santiago · 2000
SMV [McM93] is a language suitable for integrated circuit design and optimized for formal verification. VHDL [IEE93] is a design format suitable for simulation and synthesis, but poorly designed for formal verification purposes. The contribution of this paper is the integration of the two approaches through the definition of systematic rules to translate SMV programs into VHDL descriptions, providing thus an important component for an automated circuit design environment making efficient use of formal methods. Moreover, our translation process targets a synthesis-specific subset of VHDL language. Consequently, the produced VHDL descriptions may be automatically mapped to standard FPGA devices using commercial synthesis tools. Keywords Formal methods, Circuit design automation, FPGA 1 Introduction In the last 30 years, the size of digital circuits has sustained an exponential growth. The task of designing hardware systems has become incredibly complex and, consequently, is now ...