A Tool for Translation of VHDL Descriptions into a Formal Model and Its Application to Formal Verification and Synthesis

摘要

This paper presents the VPN tool (VHDL to Petri Nets) for translating a subset of VHDL'87 into a formal model based on Interpreted and Timed Petri Nets (ITPN). This formal model finds its application to different kind of analysis such as symbolic model checking, behavioral equivalence and behavioral synthesis of the VHDL descriptions.