Verification and diagnosis of digital systems by ternary reasoning

  • Ayman M. Wahba
  • Einar J. Aas
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 683)


Ternary vectors {0,1,X} may be used to simulate binary systems more efficiently than binary vectors. It has recently been shown by R.E. Bryant that formal verification by ternary simulation is feasible. In this paper, we demonstrate that complete verification of Finite State Machines is possible by ternary simulation. The verification vectors are derived from AND/OR trees. We also show how design error diagnosis can be performed by utilizing the difference vector set. Algorithms for the diagnosis of single inverter errors, and wrong gate type, are presented, together with illustrative examples.


  1. [AAS92]
    E.J. Aas, K.A. Klingsheim and T. Steen, “Quantifying Design Quality: A Model and Design Experiments”, Proc. EuroASIC'92, IEEE Comp. Soc., 1992, pp. 172–177.Google Scholar
  2. [BOR92]
    D.D. Borrione, L.V. Pierre and A.M. Salem, “Formal Verification of VHDL Descriptions in the Prevail Environment”, IEEE Design and Test, Vol. 9, No. 2, June 1992, pp. 42–56.Google Scholar
  3. [BRY86]
    R.E. Bryant, “Graph-Based Algorithms for Boolean Function Manipulation”, IEEE Trans. on Comp., Vol. C-35, No. 8, Aug. 1986, pp. 677–691.Google Scholar
  4. [BRY91a]
    R.E. Bryant, “A Methodology for Hardware Verification Based on Logic Simulation”, Journ. of the ACM, Vol. 38, No. 2, April 1991, pp. 299–328.Google Scholar
  5. [BRY91b]
    R.E. Bryant, D.L. Beatty and C.J.H. Seger, “Formal Hardware Verification by Symbolic Ternary Trajectory Evaluation”, Proc.28th DAC, 1991, pp. 397–402.Google Scholar
  6. [CLA91]
    L.J.M. Claesen, F. Proesmans, E. Verlind and H. De Man, “SFG-Tracing: a Methodology for the Automatic Verification of MOS Transistor Level Implementations from High Level Behavioral Specifications”, Proc. ACM/SIGDA Int. Workshop on Formal Methods in VLSI Design, Miami, January 1991.Google Scholar
  7. [GUP92]
    A. Gupta, “Formal Hardware Verification Methods: A Survey”, Journ. of Formal Methods in System Design”, Vol. 1,1992, pp. 151–238.Google Scholar
  8. [HWA85]
    K.S. Hwang and M.R. Mercer, “Derivation and Refinement of Fanout Constraints to Generate Tests in Combinational Logic Circuits”, Proc. ICCAD-85, 1985.Google Scholar
  9. [KUO92]
    S.Y. Kuo, “Locating Logic Design Errors via Test Generation and Don't Care Propagation”, Proc. Euro-DAC, 1992, pp. 466–471.Google Scholar
  10. [MAD88]
    J.C. Madre and J.P. Billon, Proving Circuit Correctness using Formal Comparison between Expected and Extracted Behaviour”, Proc. 25th DAC, 1988.Google Scholar
  11. [MAD89]
    J.C. Madre, O. Coudert and J.P. Billon, “Automating the Diagnosis and the Rectification of Design Errors with PRIAM”, Proc ICCAD, 1989, pp. 30–33.Google Scholar
  12. [SEL68]
    F.F. Sellers, M.Y. Hsiao and L.W. Bearnson, “Analyzing Errors with the Boolean Difference”, IEEE Trans. Comp., Vol. EC-17, July 1968, pp. 676–683.Google Scholar
  13. [TAM89]
    K.A. Tamura, “Locating Functional Errors in Logic Circuits”, Proc. 26th DAC, 1989, pp. 185–191.Google Scholar
  14. [TOM90]
    M. Tomita and H.H. Jiang, “An Algorithm for Locating Logic Design Errors”, Proc ICCAD, 1990, pp. 463–471.Google Scholar
  15. [WEI85]
    R.S. Wei and A. Sangiovanni-Vincentelli, “PLATYPUS: A PLA Test Pattern Tool”, Proc. 22nd DAC, 1985, pp. 197–203.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  • Ayman M. Wahba
    • 1
  • Einar J. Aas
    • 1
  1. 1.IMAG-ARTEMIS LaboratoryJoseph Fourier UniversityGrenobleFrance

Personalised recommendations