On The Integration of Decision Diagrams in High Order Logic Based Theorem Provers: a Survey <s> Fig.1: Theorem Proving and Model Checking Interface <s> The Voss system is a formal verification system aimed primarily at hardware verification. In particular, verification using symbolic trajectory evaluation is strongly supported. The Voss system consists of a set of programs. The main one is called fl and is the core of the verification system. Since the metalanguage in fl is a fully general functional language in which Ordered Binary Decision Diagrams (OBDDs) have been built in, the verification system is not only useful for carrying out trajectory evaluation, but also for experimenting with various verification (formal and informal) techniques that require the use of OBDDs. This document is intended as both a user''s guide and (to some extent) a reference guide. For the Voss alpha release, this document is still quite incomplete, but work is underway to remedy this. <s> BIB001 </s> On The Integration of Decision Diagrams in High Order Logic Based Theorem Provers: a Survey <s> Fig.1: Theorem Proving and Model Checking Interface <s> Although automated proof checking tools for general-purpose logics have been successfully employed in the verification of digital systems, there are inherent limits to the efficient automation of expressive logics. If the expressiveness is constrained, there are useful logic fragments for which efficient decision procedures can be found. The model checking paradigm yields an important class of decision procedures for establishing temporal properties of finite-state systems. Model checking is remarkably effective for automatically verifying finite automata with relatively small state spaces, but is inadequate when the state spaces are either too large or unbounded. For this reason, it is useful to integrate the complementary technologies of model checking and proof checking. Such an integration has to be carried out in a delicate manner in order to be more than just the sum of the techniques. We describe an approach for such an integration where a BDD-based model checker for the propositional mu-calculus has been used as a decision procedure within the framework of the PVS proof checker. We argue that our approach fits in nicely with the design philosophy of PVS of providing highly effective mechanical reasoning capability by using efficient decision procedures as the workhorses of an interactive proof checker. <s> BIB002 </s> On The Integration of Decision Diagrams in High Order Logic Based Theorem Provers: a Survey <s> Fig.1: Theorem Proving and Model Checking Interface <s> We claim that no single technique such as rewriting, BDDs, or model checking is effective for all aspects of hardware verification. Many examples need the careful integration of these techniques. We have shown some simple examples to illustrate the integration available in PVS. This combination of techniques has been applied to some larger examples such as an SRT divider and Rockwell-Collins AAMP series of processors. The automation available in PVS on these examples can be further improved through the use of more decision procedures (e.g., bit vectors) and better verification methodologies (e.g., abstraction, induction). <s> BIB003 </s> On The Integration of Decision Diagrams in High Order Logic Based Theorem Provers: a Survey <s> Fig.1: Theorem Proving and Model Checking Interface <s> Traditional ROBDD-based methods of automated verification suffer from the drawback that they require a binary representation of the circuit. To overcome this limitation we propose a broader class of decision graphs, called {\em Multiway Decision Graphs} (MDGs), of which ROBDDs are a special case. With MDGs, a data value is represented by a single variable of abstract type, rather than by 32 or 64 boolean variables, and a data operation is represented by an uninterpreted function symbol. MDGs are thus much more compact than ROBDDs, and this greatly increases the range of circuits that can be verified. We give algorithms for MDG manipulation, and for implicit state enumeration using MDGs. We have implemented an MDG package and provide experimental results. <s> BIB004 </s> On The Integration of Decision Diagrams in High Order Logic Based Theorem Provers: a Survey <s> Fig.1: Theorem Proving and Model Checking Interface <s> We describe the verification of the IM: a large, complex (12000 gates and 1100 latches) circuit that detects and marks the boundaries between Intel architecture (IA-32) instructions. We verified a gate-level model of the IM against an implementation-independent specification of IA-32 instruction lengths. We used theorem proving to to derive 56 model-checking runs and to verify that the model-checking runs imply that the IM meets the specification for all possible sequences of IA-32 instructions. Our verification discovered eight previously unknown bugs. <s> BIB005 </s> On The Integration of Decision Diagrams in High Order Logic Based Theorem Provers: a Survey <s> Fig.1: Theorem Proving and Model Checking Interface <s> Contemporary microprocessors implement many iterative algorithms. For example, the front-end of a microprocessor repeatedly fetches and decodes instructions while updating internal state such as the program counter; floating-point circuits perform divide and square root computations iteratively. Iterative algorithms often have complex implementations because of performance optimizations like result speculation, re-timing and circuit redundancies. Verifying these iterative circuits against high-level specifications requires two steps: reasoning about the algorithm itself and verifying the implementation against the algorithm. In this paper we discuss the verification of four iterative circuits from Intel microprocessor designs. These verifications were performed using Forte, a custom-built verification system; we discuss the Forte features necessary for our approach. Finally, we discuss how we maintained these proofs in the face of evolving design implementations. <s> BIB006 </s> On The Integration of Decision Diagrams in High Order Logic Based Theorem Provers: a Survey <s> Fig.1: Theorem Proving and Model Checking Interface <s> Forte is a formal verification system developed by Intel's Strategic CAD Labs for applications in hardware design and verification. Forte integrates model checking and theorem proving within a functional programming language, which both serves as an extensible specification language and allows the system to be scripted and customized. The latest version of this language, called reFL ect , has quotation and antiquotation constructs that build and decompose expressions in the language itself. This provides combination of pattern-matching and reflection features tailored especially for the Forte approach to verification. This short paper is an abstract of an invited presentation given at the International Conference on Integrated Formal Methods in 2004, in which the philosophy and architecture of the Forte system are described and an account is given of the role of reFL ect in the system. <s> BIB007
The hybrid approach implement a tool linking model checking and theorem proving. During the verification procedure, the user deals mainly with the theorem proving tool. Verification using hybrid approach proceeds as shown in (Fig.1) . The user starts by providing the theorem proving with the design (specification or implementation), the property and the goal to be proven. If the goal fits the required pattern, the theorem proving tool generates the required model checking files (sub-goals). The latter are sent to the model checking tool for verification. If the property holds, a theorem is created. Otherwise, the proof is performed interactively. There are many examples of integration tools such as integrating the HOL system (HOL88) and Voss. Voss system BIB001 , an implementation of Symbolic Trajectory Evaluation (STE), was implemented in a lazy Functional Language (FL). In  Voss was interfaced to HOL and the verification using a combination of deduction and STE was demonstrated. The HOL-Voss system integrates HOL88 deduction with BDDs computations. The BDDs tools are programmed in FL as a builtin datatype. The assertion language of Voss was formalized in HOL and a tactic, which can make an external call to the Voss system, checks whether an assertion is true. Then the proved assertion was returned as a HOL theorem. A system based on this idea, called Voss-ThmTac, was later developed by Aagaard et al. BIB005 , which combines the ThmTac theorem prover with the Voss system. Then the development of HOL-Voss evolved into a new system called Forte BIB006 . The idea comes from the very tight integration of the two provers, using a single language, FL, as both the theorem prover's meta-language and its object language. Thus lifted FL programs could evaluate FL expressions directly instead of having to translate back and forth, achieving the goal of efficiently unifying the model checker and theorem prover's specification languages. More recently, with industrial take-up at Intel, Forte BIB007 has become one of the most mature formal verification environments based on tool integration. Rajan et al. BIB002 BIB003 described an approach where a BDD-based model checker for the propositional µ -calculus has been used as a decision procedure within the framework of PVS. An extension of the µ -calculus, consists of Quantified Boolean Formulae (QFB), is defined using PVS higher-order logic. The temporal operators are then defined using the µ -calculus. These temporal operators apply to arbitrary state spaces. In the case where the state type is constructed in a hereditarily finite manner, µ -calculus expressions are translated into input acceptable by a µ -calculus model checker. This model checker can then be used as a decision procedure to prove certain subgoals. The model checker accepts the translated input from µ -calculus expression. The generated subgoals are verified by the model checker and the results are used in the proof process of PVS. Schneider et al.  used higher order hardware formulae to express the safety and liveness properties hierarchically. They proposed an approach of invoking model checking within HOL where properties are translated from HOL to temporal logic. A new class of higher-order formulae was presented, which allows a unified description of hardware structure and behavior at different levels of abstraction. Datapath oriented verification goals involving abstract data types can be expressed by these formula as well as control dominated verification goals with irregular structure. To ease the proof of the goals in HOL, a translation procedure was presented which converts the goals into several Computational Tree Logic (CTL) model checking problems, which are then solved outside HOL. Schneider and Hoffmann  linked the SMV model checker to HOL using PROSPER. It provides an open proof architecture for the integration of different verification tools in a uniform higher-order logic environment. They embedded the linear time temporal logic (LTL) in HOL and translated LTL formulae into ω -Automata, a form that can be reasoned about within SMV. The translation is completely implemented by means of HOL rules. HOL terms are exported to SMV through the PROSPER plug-in interface. On successful model checking, the results are returned to HOL and turned to theorems. This integration tool allows SMV to be used as a HOL decision procedure. The deep embedding of the SMV specification language in HOL allows LTL specifications to be manipulated in HOL. MDGs BIB004 are decision diagrams based verification tool, primarily designed for hardware verification. It is based on Multiway Decision Graphs which extend ROBDDs  with abstract sorts and uninterpreted function symbols. MDGs are canonical representations of a certain class of quantifier-free formulae of the logic called Directed Formulae (DFs)  . DFs can represent the transition and output relations of a state of machine, as well as the set of states. The MDG-HOL system  is a hybrid system which links the HOL interactive proof system and the MDGs automated hardware verification system. It supports a hierarchical verification approach and fits the use of MDGs verification naturally within the HOL framework for a compositional hierarchical verification. The HOL system is used to manage the proof. The MDGs system is called to verify the submodules of a design. When the MDG-HOL system is used to verify a design, the design is modeled as a hierarchy structure with modules divided into submodules. An extension of the above work was presented in  to link HOL and the MDGs model checker. The interface between the two tools is implemented using ML. Haiyan et al.  verified formally the linkage between a simplified version of MDG tool and the HOL theorem prover. The verification is based on the importing of MDGs results to HOL theorems. Then, they combined translator correctness theorems with the linkage theorems in order to allow low level MDGs verification results to be imported into HOL in terms of the semantics of MDG-HDL. The work was concerned with ways of increasing trust in the linked systems.