An Abstract Reachability Approach by Combining HOL Induction and Multiway Decision Graphs

In this paper, we provide a necessary infrastructure to define an abstract state exploration in the HOL theorem prover. Our infrastructure is based on a deep embedding of the Multiway Decision Graphs （MDGs） theory in HOL. MDGs generalize Reduced Ordered Binary Decision Diagrams （ROBDDs） to represent and manipulate a subset of first-order logic formulae. The MDGs embedding is based on the logical formulation of an MDG as Directed Formulae （DF）. Then, the MDGs operations are defined and the correctness proof of each operation is provided. The MDG teachability algorithm is then defined as a conversion that uses our MDG theory within HOL. Finally, a set of experimentations over benchmark circuits has been conducted to ensure the applicability and to measure the performance of our approach.

NuMDG:A New Tool for Multiway Decision Graphs Construction

Multiway Decision Graphs （MDGs） are a canonical representation of a subset of many-sorted first-order logic. This subset generalizes the logic of equality with abstract types and uninterpreted function symbols. The distinction between abstract and concrete sorts mirrors the hardware distinction between data path and control. Here we consider ways to improve MDGs construction. Efficiency is achieved through the use of the Generalized-If-Then-Else （GITE） commonly operator in Binary Decision Diagram packages. Consequently, we review the main algorithms used for MDGs verification techniques. In particular, Relational Product and Pruning by Subsumption are algorithms defined uniformly through this single CITE operator which will lead to a more efficient implementation. Moreover, we provide their correctness proof. This work can be viewed as a way to accommodate the ROBBD algorithms to the realm of abstract sorts and uninterpreted functions. The new tool, called NuMDG, accepts an extended SMV language, supporting abstract data sorts. Finally, we present experimental results demonstrating the efficiency of the NuMDG tool and evaluating its performance using a set of benchmarks from the SMV package.

Enhancing SAT-Based Test Pattern Generation

This paper presents modeling tools based on Boolean satisfiability (SAT) to solve problems of test generation for combinational circuits. It exploits an added layer to maintain circuit-related information and value justification relations to a generic SAT algorithm. It dovetails binary decision graphs (BDD) and SAT techniques to improve the efficiency of automatic test pattern generation (ATPG). More specifically, it first exploits inexpensive reconvergent fanout analysis of circuit to gather information on the local signal correlation by using BDD learning, then uses the above learned information to restrict and focus the overall search space of SAT-based ATPG. Its learning technique is effective and lightweight. The experimental results demonstrate the effectiveness of the approach.