Identification of non-redundant memorizing elements in VHDL synchronous designs for formal verification tools

International audienceFormal tools for the verification of HDL synchronous descriptions are currently in development for both the Verilog [2,3] and VHDL languages [1], but little work has been done on tools able to handle both languages [8]. The well known reason is that VHDL and Verilog's simulation semantics are quite different. So, the task of deciding formally whether two synchronous descriptions written in the two languages are equivalent is not obvious. We are working on establishing a link between two formal verification systems : Prevail, developed in our team, and VIS, developed at UC Berkeley. PREVAIL takes VHDL as input language, and offers access to several verification tools [9,14]. The VIS system takes Verilog as input to its equivalence checker, model checker and synthesis tools [4,7]. Both systems interpret synchronous descriptions in terms of Finite States Machines (FSM) [5]. The approach we adopt to settle the bridge between the two system is to translate VHDL into Blif-mv, the intermediate format recognised by Berkeley's tools, and to translate Verilog in PIF, the language recognised by Prevail's tools. In this paper, we only discuss the first link, i.e. translating VHDL into Blif-mv code. A prototype has already been written to establish the validity of the approach. An important aspect that was pointed out in this work is the problem of memorizing elements, because each supplementary flip-flop introduced in the code doubles the number of states of the resulting Finite State Machine. Contrary to Verilog's wires and regs that define precisely which elements are memorizing and which ones are not, VHDL memorizing elements are not explicitly declared by the designer. They have to be inferred by the tools. General rules were already given in [8]. In this paper we describe those rules more precisely. We extend the rules to handle if/then/else constructions and we explicit rules that permit to suppress redundant memorizing elements. Those rules are implemented in vhdl2mv, our compiler from VHDL to Blif-mv