Logic verification algorithms and their parallel implementation

ABSTRACT

LOVER incorporates a novel approach to combinational logic verification and obtains good results when compared to existing techniques. In this paper we describe a new verification algorithm, LOVER-PODEM, whose enumeration phase is based on PODEM. A variant of LOVER-PODEM, called PLOVER, is presented. We have developed, for the first time, parallel logic verification schemes. Issues in efficiently parallelizing both general and specific LOVER-based approaches to logic verification over a large number of processors are addressed. We discuss parallelism inherent in the LOVER framework regardless of what enumeration and simulation algorithms are used. Since the enumeration phase is the efficiency bottleneck in parallelizing LOVER-based approaches, we have developed parallel versions of PODEM-based enumeration algorithms. Experimental results are presented to show that high processor utilization can be achieved when these parallelisms are exploited. Speed-up factors of over 7.8 have been achieved with 8 processor configurations.

REFERENCES

• Bra84: Robert King Brayton , Alberto L. Sangiovanni-Vincentelli , Curtis T. McMullen , Gary D. Hachtel, Logic Minimization Algorithms for VLSI Synthesis, Kluwer Academic Publishers, Norwell, MA, 1984
• Brg85: F. Brglez and H. Fujiwara, "A neutral nettist of 10 combinational benchmark circuits and a target translator in FORTRAN," Special session on ATPG and fault simulation, Proc. 1985 IEEE Int. Syrup. Circuits and Systems, Kyoto, Japan, June 5-7, 1985.
• Bry85: R. E. Bryant, NSymbolic Manipulation of Boolean Functions', Chapel Hill Conference On VLSI, May 1985.
• Don76: W. E. Donath and H. Ofek, = Automatic Identification of Equivalence Points for Boolean Logic Verification', IBM Technical Disclosure Bulletin, vol. 18, No 8, Jan. 1976.
• Goe81: P. Goel. "An Implicit Enumeration Algorithm To Generate Tests for Combinational Logic Circuits" , IEEE Transactions on Computers, Vol C--30. Mar. 1981.
• Oda86: Gotaro Odawara , Masahiro Tomita , Osamu Okuzawa , Tomomichi Ohta , Zhen-quan Zhuang, A logic verifier based on Boolean comparison, Proceedings of the 23rd ACM/IEEE conference on Design automation, p.208-214, July 1986, Las Vegas, Nevada, United States
• Rot73: P. Roth, "VERIFY: An algorithm to verify a computer design," IBM Tech. Disclosure Bull. 15, 2646-2648(1973).
• Rot77: P. Roth. "Hardware Veritication'. IEEE Transactions on Computers, Vol C-26, 1977.
• Rot80: J. Paul Roth, Computer Logic, Testing and Verification, W. H. Freeman & Co., New York, NY, 1980
• Seq85: Sequent Computer Systems, Inc., ~Balance 8000 guide to parallel programming', Sequent Computer Systems, Inc., July 31 1985.
• Wei86: R.S. Wei and A. Sangiovanni-Vincentelli, "PROTEUS: A Logic Verification System for Combinational Logic Circurs', Proc. of International Testing Conference, Sept. 1986.

INDEX TERMS

Primary Classification:
  B. Hardware
  B.6 LOGIC DESIGN
      B.6.3 Design Aids
          Subjects: Verification

Additional Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.2 Modes of Computation
          Subjects: Parallelism and concurrency
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.2 Nonnumerical Algorithms and Problems
          Subjects: Sequencing and scheduling

General Terms:
Algorithms, Design, Theory, Verification