Academic Journals Database
Disseminating quality controlled scientific knowledge

Probabilistic Verification over GF(2m) Using Mod2-OBDDs

Author(s): J.L. Imana

Journal: Intelligent Information Management
ISSN 2160-5912

Volume: 02;
Issue: 02;
Start page: 95;
Date: 2010;
Original page

Keywords: Verification | Probabilistic | OBDD | Mod2-OBDD | Galois Field GF(2m)

Formal verification is fundamental in many phases of digital systems design. The most successful verification procedures employ Ordered Binary Decision Diagrams (OBDDs) as canonical representation for both Boolean circuit specifications and logic designs, but these methods require a large amount of memory and time. Due to these limitations, several models of Decision Diagrams have been studied and other verification techniques have been proposed. In this paper, we have used probabilistic verification with Galois (or finite) field GF(2m) modifying the CUDD package for the computation of signatures in classical OBDDs, and for the construction of Mod2-OBDDs (also known as ?-OBDDs). Mod2-OBDDs have been constructed with a two-level layer of ?-nodes using a positive Davio expansion (pDE) for a given variable. The sizes of the Mod2-OBDDs obtained with our method are lower than the Mod2-OBDDs sizes obtained with other similar methods.
Save time & money - Smart Internet Solutions      Why do you need a reservation system?