# An Algorithm for the PLA Equivalence Problem

### Description

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 ... continued below

vi, 118 leaves

### Creation Information

Moon, Gyo Sik December 1995.

### Context

This dissertation is part of the collection entitled: UNT Theses and Dissertations and was provided by UNT Libraries to Digital Library, a digital repository hosted by the UNT Libraries. It has been viewed 37 times , with 4 in the last month . More information about this dissertation can be viewed below.

## Who

People and organizations associated with either the creation of this dissertation or its content.

### Rights Holder

For guidance see Citations, Rights, Re-Use.

• Moon, Gyo Sik

### Provided By

#### UNT Libraries

The UNT Libraries serve the university and community by providing access to physical and online collections, fostering information literacy, supporting academic research, and much, much more.

## What

Descriptive information to help identify this dissertation. Follow the links below to find similar items on the Digital Library.

### Description

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.

vi, 118 leaves

### Identifier

Unique identifying numbers for this dissertation in the Digital Library or other systems.

### Collections

This dissertation is part of the following collection of related materials.

#### UNT Theses and Dissertations

Theses and dissertations represent a wealth of scholarly and artistic content created by masters and doctoral students in the degree-seeking process. Some ETDs in this collection are restricted to use by the UNT community.

What responsibilities do I have when using this dissertation?

## When

Dates and time periods associated with this dissertation.

### Creation Date

• December 1995

### Added to The UNT Digital Library

• March 26, 2014, 9:30 a.m.

### Description Last Updated

• March 25, 2015, 2:57 p.m.

Yesterday: 0
Past 30 days: 4
Total Uses: 37

## Interact With This Dissertation

Here are some suggestions for what to do next.