Introduction

Multiway Decision Graphs (MDGs) represent and manipulate a subset of first-order logic formulas suitable for high-level hardware verification With MDGs, a data value is represented by a single variable of abstract type and a data operation is represented by an uninterpreted function symbol. For more information, please refer to our publications.

The MDG operators and verification procedures are packaged as MDG tools and implemented in Prolog. They currently run under Quintus Prolog Version 3.2. MDG provides the following features: 1) Verification of combinational circuits, 2) Safety property checking, 3) State enumeration 4) Equivalence checking of two state machines 5) Model checking.

MDG Tools for the Verification of RTL Designs presents an overview of the MDG tools. The MDG tools contain three sub-directories: documents, examples and programs. The document sub-directory contains manuals ( user's manual and developer's manual) and algorithms( basic set and extended set). The example sub-directory provides several illustrative examples for combinational and sequential verification. There is a README file for each example. The program sub-directory includes all the Prolog source files.

---

Please contact:

Sofiene Tahar, Associate Professor/Graduate Program Director (Ph.D.)
Concordia University
Electrical and Computer Engineering
1455 de Maisonneuve, West, S-H-961-15
Montreal, Quebec H3G 1M8
CANADA
(514) 848-3114 (voice)
(514) 848-2802 (fax)
Email: tahar@ece.concordia.ca.