Authors: Khaza Anuarul Hoque; Otmane Ait Mohamed; Sa'ed Abed; Mounir Boukadoum
Addresses: Department of Electrical and Computer Engineering, Concordia University, 1455 de Maisooneve Blvd. W, Montreal, Quebec H3G 1M8, Canada. ' Department of Electrical and Computer Engineering, Concordia University, 1455 de Maisooneve Blvd. W, Montreal, Quebec H3G 1M8, Canada. ' Department of Computer Engineering, Hashemite University, P.O. Box 150459, Zarqa 13115, Jordan. ' Department of Computer Science, University of Quebec at Montreal, CP. 8888, Succ. Centre-Ville, Montreal, QC H3P 3P8, Canada
Abstract: Multiway decision graph (MDG) is a canonical representation of a subset of many-sorted first-order logic. It generalises the logic of equality with abstract types and uninterpreted function symbols. The area of satisfiability (SAT) has been the subject of intensive research in recent years, with significant theoretical and practical contributions. In this paper, we propose a new design verification tool integrating MDG and SAT, to check the safety of a design by invariant checking. Using MDG to encode the set of states provides a powerful mean of abstraction. We use a SAT solver to search for paths of reachable states violating the property under certain encoding constraints. In addition, we introduce an automated conversion-verification methodology to convert a directed formula (DF) into a conjunctive normal form (CNF) formula that can be fed to a SAT solver. The formal verification of this conversion is conducted within the HOL theorem prover. Finally, we present experimental results and a case study to show the correctness and the efficiency of our proposed methodology.
Keywords: satisfiability; SAT; invariant checking; model checking; multiway decision graphs; MDG; conjunctive normal form; CNF conversion; safety checking; design verification; design safety.
International Journal of Critical Computer-Based Systems, 2012 Vol.3 No.1/2, pp.4 - 25
Received: 08 May 2021
Accepted: 12 May 2021
Published online: 24 Jan 2012 *