The Programmable Logic Array (PLA) has been widely used in the design of VLSI circuits and systems because of its regularity, flexibility, and simplicity. The equivalence problem is typically to verify that the final description of a circuit is functionally equivalent to its initial description. Verifying the functional equivalence of two descriptions is equivalent to proving their logical equivalence. This problem of pure logic is essential to circuit design. The most widely used technique to solve the problem is based on Binary Decision Diagram or BDD, proposed by Bryant in 1986. Unfortunately, BDD requires too much time and space to represent moderately large circuits for equivalence testing. We design and implement a new algorithm called the Cover-Merge Algorithm for the equivalence problem based on a divide-and-conquer strategy using the concept of cover and a derivational method. We prove that the algorithm is sound and complete. Because of the NP-completeness of the problem, we emphasize simplifications to reduce the search space or to avoid redundant computations. Simplification techniques are incorporated into the algorithm as an essential part to speed up the the derivation process. Two different sets of heuristics are developed for two opposite goals: one for the proof of equivalence and the other for its disproof. Experiments on a large scale of data have shown that big speed-ups can be achieved by prioritizing the heuristics and by choosing the most favorable one at each iteration of the Algorithm. Results are compared with those for BDD on standard benchmark problems as well as on random PLAs to perform an unbiased way of testing algorithms. It has been shown that the Cover-Merge Algorithm outperforms BDD in nearly all problem instances in terms of time and space. The algorithm has demonstrated fairly stabilized and practical performances especially for big PLAs under a wide range of conditions, while BDD shows poor performance because of its memory greedy representation scheme without adequate simplification.
| Identifer | oai:union.ndltd.org:unt.edu/info:ark/67531/metadc278922 |
| Date | 12 1900 |
| Creators | Moon, Gyo Sik |
| Contributors | Vlach, Frank, Jacob, Roy Thomas, Yang, Chao-Chih, Wong, Benedict D. |
| Publisher | University of North Texas |
| Source Sets | University of North Texas |
| Language | English |
| Detected Language | English |
| Type | Thesis or Dissertation |
| Format | vi, 118 leaves, Text |
| Rights | Public, Copyright, Copyright is held by the author, unless otherwise noted. All rights reserved., Moon, Gyo Sik |
Page generated in 0.0017 seconds