Formal Verification Tools for VHDL Based Systems

Abstract

This talk will present the formal verification techniques, based on VHDL, developped at LIP6 (University of Paris VI) and more specificly by ANP (Numerical Algorithms and Parallelism) team comprised of R. K Bawa, E Encrenaz,F Rahim, headed by Prof. M Minoux.

The verification methodology described here aims at providing the designers with automatic tools integrated in the VHDL environment. The development of automatic verification techniques for VHDL systems requires a formal model of the VHDL semantics on which automated formal verification tools are based. We restrict the analysis of the systems to their observable points, called stable states, and the semantics of a subset of VHDL is defined in terms of interpreted and timed Petri nets (ITPN). Firstly we will describe the VPN tool which translates the VHDL descriptions into ITPN (Interpreted Timed Petri Net). An on the fly reduction algorithm, exploiting the structure of VHDL programs, reduces the size of the Petri net while preserving its semantics. A transition system representing the behaviour of the VHDL program is extracted from this formal model. It is used to perform the symbolic model checking of temporal properties described in an overlanguage of CTL, and to check the behavioral equivalence of two Finite State Machines described either at the same or at different levels of VHDL. An application controlled dynamic reordering strategy for containing the BDD explosion is used and experimental results has proved its effeceincy on various examples.

The VMC tool is implemented to perform symbolic model checking and abstraction on VHDL descriptions. The PSM tool is used to prove behavioral equivalence of FSMs described in VHDL at different level of abstration. The results of symbolic model checking (an 8-request bus arbiter and now an abstracted 32 bit pipelined RISC processor) and of equivalence of FSMs (the DLX and MIPSR4000 control automaton), considering the VHDL simulation semantics, were among the first to be published on non-trivial examples.

An original approach for the recognition of memorizing elements from a VHDL decription is proposed for behavioral synthesis. This approach does not depend on description as it is presently the case with both academic and industrial tools. This later work is being extended with a behavioral synthesis tool which will overcome the portability problems encountered using different tools

Transparencies

Relevant Papers