›› 2011, Vol. 26 ›› Issue (1): 139-152.doi: 10.1007/s11390-011-1117-8

• Algorithm and Complexity • Previous Articles     Next Articles

NuMDG: A New Tool for Multiway Decision Graphs Construction

Sa'ed Abed1, Member, ACM, IEEE, Yassine Mokhtari2, Otmane Ait-Mohamed2, Member, ACM, IEEE, and Sofiène Tahar2, Senior Member, IEEE, Member, ACM   

  1. 1. Department of Computer Engineering, Hashemite University, Zarqa, Jordan;
    2. Department of Electrical and Computer Engineering, Concordia University, Montreal, Canada
  • Received:2009-07-29 Revised:2010-11-13 Online:2011-01-01 Published:2011-01-01
  • About author:Sa'ed Abed received a B.Sc. degree in electrical engineering in 1994 and an M.Sc. degree in computer engineering in 1996, both from Jordan University of Science and Technology, Jordan. In 2008, he received his Ph.D. degree in computer engineering from Concordia University, Montreal, Canada. He has previously worked as lecturer in the Department of Computer Science at King Faisal University in Saudi Arabia from 1997 until 2003. In 2008, Dr. Abed joined the Department of Computer Engineering of Hashemite University, Zarqa, Jordan, as assistant professor. His research interests include formal methods, theorem proving, model checking, SAT-solvers, VLSI design, high level synthesis, computer architecture and fault tolerance. Dr. Abed also served as a reviewer for various international conferences and journals. He is member of IEEE, ACM and the Jordanian Engineers Association.
    Yassine Mokhtari received the B.Sc., M.Sc. and Ph.D. degrees in computer science from University Henri Poincare Nancy I, France, in 1994, 1995 and 2000, respectively. He then worked as a postdoctoral fellow in the Department of Electrical and Computer Engineering of Concordia University, Montreal, Canada between 2000 and 2001. He was appointed adjunct professor in the same department of Concordia University between 2001 and 2003. Currently, he is a senior verification engineer, AMD, Toronto, Canada. His main research interests include automatic verification of hardware and software, object-oriented concepts, and semantics and type systems. Before that he worked from 1996?1997 as expert engineer in telecommunication at CNRS, France, and in 2002?2003 as ASIC design verification engineer at Silicon Access Networks, Ottawa, Canada.
    Otmane Ait-Mohamed received M.Sc. and Ph.D. degrees in computer science from University Henri Poincare Nancy I, France, in 1992 and 1996, respectively. Currently, he is an associate professor in the Department of Electrical and Computer Engineering, Concordia University, Montreal, Canada. Before that he worked with Cistel Technology, then Nortel Networks where he introduced the use of formal method techniques in the hardware design flow. His main research areas include software model checking, assertion based verification, automatic test generations, and FPGA-based design and verification. Dr. Ait Mohamed served as track chair of NEWCAS for several years. In 2008, he was the program chair for the TPHOLs conference held in Montreal. He is also reviewer for several related conferences and journals. Dr. Ait Mohamed is member of the Executive Committee of RESMIQ. He is a professional engineer in the Province of Quebec (OIQ). He is member of IEEE, ACM and the IEEE Computer Society.
    Sofiène Tahar received the Diploma degree in computer engineering from the University of Darmstadt, Germany, in 1990, and the Ph.D. degree with distinction in computer science from the University of Karlsruhe, Germany, in 1994. Currently, he is a professor and research chair in formal verification of systemon-chip at the Department of Electrical and Computer Engineering, Concordia University, Montreal, Canada. His research interests are in the areas of formal hardware verification, system-on-chip verification, analog and mixed signal circuits verification, and probabilistic, statistical and reliability analysis of systems. Dr. Tahar, a professional engineer in the Province of Quebec, is the founder and director of the Hardware Verification Group at Concordia University. In 2007, he was named University Research Fellow upon receiving Concordia University's Senior Research Award. Dr. Tahar is senior member of IEEE, member of ACM, IEEE Computer Society and IEEE Communications Society.

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 GITE 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.

[1] Bryant R E. Graph-based algorithms for Boolean function anipulation. IEEE Transactions on Computers, Aug. 1986, 5(8): 677-691.
[2] Corella F, Zhou Z, Song X, Langevin M, Cerny E. Multiway ecision graphs for automated hardware verification. Formal ethods in System Design, Feb. 1997, 10(1): 7-46.
[3] Tahar S, Song X, Cerny E, Zhou Z, Langevin M, Ait Mohamed . Modelling and automatic verification of the fairisle ATM witch fabric using MDGs. IEEE Transactions on CAD of ntegrated Circuits and Systems, Jul. 1999, 18(17): 955-972.
[4] Xu Y, Song X, Cerny E, Ait Mohamed O. Model checking for first-order temporal logic using multiway decision graphs MDGs). The Computer Journal, 2004, 47(1): 71-84.
[5] Zhou Z. Multiway decision graphs and their applications in utomatic formal verification of RTL designs [Ph.D. Disseration]. Universite de Montreal, Canada, 1997.
[6] Mokhtari Y, Abed S, Ait Mohamed O, Tahar S, Song X. new approach for the construction of multiway decision raphs. In Proc. the 5th International Colloquium on Theretical Aspects of Computing, Istanbul, Turkey, Sept. 1-3, 2008, pp.228-242.
[7] Fontaine P, Gribomont E P. Using BDDs with combinations f theories. In Proc. the 9th International Conference on ogic for Programming and Automated Reasoning (LPAR), bilisi, Geogia, Oct. 14-18, 2002, pp.190-201.
[8] Goel A, Sajid K, Zhou H, Aziz A, Singhal V. BDD based proedures for a theory of equality with uninterpreted functions. orm. Methods Syst. Des., 2003, 22(3): 205-224.
[9] Burch J R, Dill D L. Automatic verification of pipelined miroprocessor control. In Proc. Int. Conf. Computer-Aided erification, Stanford, USA, Jan. 21-23, 1994, pp.68-80.
[10] Damm W, Pnueli A, Ruah S. Herbrand automata for hardare verification. In Proc. the 9th International Confernce on Concurrency Theory (CONCUR1998), Nice, France, ept. 8-11, 1998, pp.67-83.
[11] Berezin S, Biere A, Clarke E, Zhu Y. Combining symbolic odel checking with uninterpreted functions for out-of-order rocessor verification. In Proc. the Second International onference on Formal Methods in Computer-Aided Design FMCAD1998), Palo Alto, USA, Nov. 4-6, 1998, pp.369-386.
[12] Hojati R, Dill D L, Brayton R K. Verifying linear temporal roperties of data insensitive controllers using finite instantitions. In Proc. the IFIP TC10 WG10.5 International Conerence on Hardware Description Languages and Their Appliations : Specification, Modelling, Verification and Synthesis f Microelectronic Systems (CHDL1997), London, UK, 1997, p.60-73.
[13] Bryant R, German S, Velev M. Processor verification using efficient reductions of the logic of uninterpreted functions to ropositional logic. ACM Trans. Comput. Logic, 2001, 2(1): 3-134.
[14] Velev M N, Bryant R E. Effective use of Boolean satisfiability rocedures in the formal verification of superscalar and VLIW icroprocessors. J. Symb. Comput., 2003, 35(2): pp.73-106.
[15] Velev M. Using automatic case splits and efficient CNF transation to guide a SAT-solver when formally verifying out-ofrder processors. In Proc. Artificial Intelligence and Matheatics (AI&MATH), Fort Lauderdale, USA, Jan. 4-6, 2004, p.242-254.
[16] Ackermann W. Solvable Cases of the Decision Problem. North-Holland Pub. Co., 1954.
[17] Pnueli A, Rodeh Y, Shtrichman O, Siegel M. Deciding equalty formulas by small domains instantiations. In Proc. the 1th International Conference on Computer Aided Verificaion (CAV1999), Trento, Italy, Jul. 6-10, 1999, pp.455-469.
[18] Rodeh Y, Shtrichman O. Finite instantiations in equivaence logic with uninterpreted functions. In Proc. the 13th nternational Conference on Computer Aided Verification (CAV2001), Paris, France, Jul. 18-22, 2001, pp.144-154.
[19] Bryant R E, German S M, Velev M N. Exploiting positive quality in a logic of equality with uninterpreted functions. In Proc. the 11th International Conference on Computer ided Verification (CAV 1999), Trento, Italy, Jul. 6-10, 1999, p.470-482.
[20] Lahiri S K, Bryant R E, Bryant A E, Goel A, Talupur M. Reisiting positive equality. In Proc. Tools and Algorithms for he Construction and Analysis of Systems, Barcelona, Spain, ar. 29-Apr. 2, 2004, pp.1-15.
[21] Peled D. Combining partial order reductions with on-the-fly odel-checking. In Proc. the 6th International Conference n Computer Aided Verification (CAV1994), Stanford, USA, un. 1-23, 1994, pp.377-390.
[22] Kurshan R P, Levin V, Minea M, Peled D, Yenigün, H. Static artial order reduction. In Proc. the 4th International Conerence on Tools and Algorithms for Construction and Analsis of Systems (TACAS 1998), Lisbon, Portugal, Mar. 28- pr. 4, 1998, pp.345-357.
[23] Velev M. Using rewriting rules and positive equality to forally verify wide-issue out-of-order microprocessors with a eorder buffer. In Proc. The Conference on Design, Auomation and Test in Europe (DATE2002), Paris, France, ar. 4-8, 2002, p.28.
[24] Clocksin W, Mellish C. Programming in Prolog. Springer erlag, 1987,
[25] Bahar R, Frohm E, Gaona C, Hachtel G, Macii E, Pardo , Somenzi F. Algebraic decision diagrams and their appliations. In Proc. IEEE/ACM International Conference on omputer Aided Design, Santa Clara, California, Nov. 7-11, 993, pp.188-191.
[26] Cimatti A, Clarke E M, Giunchiglia E, Giunchiglia F, Pisore M, Roveri M, Sebastiani R, Tacchella A. NuSMV 2: An pensource tool for symbolic model checking. In Proc. the 4th International Conference on Computer Aided Verificaion (CAV2002), Copenhagen, Denmark, Jul. 27-31, 2002, pp.359-364.
[27] Ait-Mohamed O, Song X, Cerny E. On the non-termination of MDG-based abstract state enumeration. Theoretical Comuter Science, 2003, 300(1-3): 161-179.
[28] Zhou Z, Song X, Tahar S, Cerny E, Corella F, Langevin M. Formal verification of the island tunnel controller using ultiway decision graphs. In Proc. the First International onference on Formal Methods in Computer-Aided Design FMCAD1996), Palo Alto, USA, Nov. 6-8, 1996, pp.233-247.
[29] Ait-Mohamed O, Cerny E, Song X. MDG-based verification y retiming and combinational transformations. In Proc. he 8th Great Lakes Symposium on VLSI, Lafayette, USA, Feb. 1998, pp.356-361.
[30] Chen H, Hsiang J. Recurrence domains: Their unification and pplication to logic programming. Inform. and Comput., 995, 122(1): 45-69.

No related articles found!
Full text



[1] Li Renwei;. Soundness and Completeness of Kung s Reasoning Procedure[J]. , 1988, 3(1): 7 -15 .
[2] Cai Shijie; Zhang Fuyan;. A Fast Algorithm for Polygon Operations[J]. , 1991, 6(1): 91 -96 .
[3] Andrew I. Adamatzky;. Identification of Nonstationary Cellular Automata[J]. , 1992, 7(4): 379 -382 .
[4] Farid Mheir-ELSaadi; Bozena Kaminska;. An Automatic Hierarchical Delay Analysis Tool[J]. , 1994, 9(4): 349 -364 .
[5] Zhou Jianqiang; Xie Li; Dai Fei; Sun Zhongxiu;. Adaptive Memory Coherence Algorithms in DSVM[J]. , 1994, 9(4): 365 -372 .
[6] LIN Hua; LU Mi; Jesse Z.FANG;. A Direct Approach for Finding Loop Transformation Matrices[J]. , 1996, 11(3): 237 -256 .
[7] Xu Meihe; Tang Zesheng;. A Boundary Element Method for Simulation of Deformable Objects[J]. , 1996, 11(5): 497 -506 .
[8] Chen Yangjun;. Magic Sets Revisited[J]. , 1997, 12(4): 346 -365 .
[9] Tian Zengping; Wang Yujun; Qu Yunyao; Shi Baile;. On the Expressive Power of F-Logic Language[J]. , 1997, 12(6): 510 -519 .
[10] Hao Ruibing; Wu Jianping;. A Formal Approach to Protocol Interoperability Testing[J]. , 1998, 13(1): 79 -90 .

ISSN 1000-9000(Print)

CN 11-2296/TP

Editorial Board
Author Guidelines
Journal of Computer Science and Technology
Institute of Computing Technology, Chinese Academy of Sciences
P.O. Box 2704, Beijing 100190 P.R. China
E-mail: jcst@ict.ac.cn
  Copyright ©2015 JCST, All Rights Reserved