J. C. Madre and J. P. Billón, “Proving Circuit correctness using formal comparison between expected and extracted behaviour,” Proceedings of 25th ACM/IEEE Design Automation Conference, pp. 308–313, 1988.

has been cited by the following article:

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

  AUTHORS: J.L. Imana

  KEYWORDS: Verification, Probabilistic, OBDD, Mod2-OBDD, Galois Field GF(2m)

  JOURNAL NAME: Intelligent Information Management, Vol.2 No.2, March 16, 2010

  ABSTRACT: 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.