Towards Formal Verification of ASIP Based on HDPN

Verification is one of the most complex and expensive tasks in current application specific instruction-set processor (ASIP) design process. Many existing approaches utilize a multi-level strategy to efficiently design and verify ASIP aiming to discover the flaws earlier. This paper presents a verification approach based on HDPN (hardware design based-on Petri net) and NuSMV. The validation of static properties, viz. structural and functional description of ASIP architecture, implements with HDPN, and the verification of dynamic properties, viz. logic design, implements with NuSMV. In order to check the dynamic properties of HDPN-based models, a scheme of translating from a HDPN description into SMV is discussed in this paper. In addition, a DLX pipelined processor is presented to demonstrate the verification approach.