MDGs Tools. 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. 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
Keywords for this software
References in zbMATH (referenced in 3 articles )
Showing results 1 to 3 of 3.
- Abed, Sa’ed; Mohamed, Otmane Ait; Al Sammane, Ghiath: Automatic verification of reduction techniques in higher order logic (2013)
- Abed, Sa’ed; Mohamed, Otmane Ait: LCF-style platform based on multiway decision graphs (2009)
- Abed, Sa’ed; Mohamed, Otmane Ait; Al-Sammane, Ghiath: An abstract reachability approach by combining HOL induction and multiway decision graphs (2009)