In this paper we present our method of formal verification of the transistor implementation of the Bus Interface Unit (BIU) of the Alpha 21264 microprocessor. We compare the logical description compiled from the Register Transfer Level (RTL) against that extracted from the custom-designed transistor-level schematics. BOVE, our BDD-based verification tool, does not require latch-to-latch correspondence, thus allowing the RTL to be more stable during the design process and giving the schematic designers freedom to implement race and timing optimizations. A unique "retiming" comparison algorithm efficiently compares partitions that include multiple pipeline stages, retiming optimizations and precharge logic. BOVE also verifies small finite-state machines that have different state encodings in the RTL and schematic.

Programmable reduced instruction set computers (PRISC) are a new class of computers which can offer a programmable functional unit (PFU) in the context of a RISC datapath. PRISC create application-specific instructions to accelerate the performance for a particular application. Our previous work has demonstrated that peephole optimizations in a compiler can utilize PFU resources to accelerate the performance of general purpose programs. However these compiler optimizations are limited by the structure of the input source code. This work generalizes on our previous work, and demonstrates that the performance of general abstract data types such as short-set vectors, hash tables, and finite state machines is significantly accelerated (250%-500%) by using PFU resources. Thus, a wide variety of end-user applications can be specifically designed to use PFU resources to accelerate performance. Results from applications in the domain of computer-aided design (CAD) are presented to demonstrate the usefulness of our techniques.>

Efficient manipulation of Boolean functions is an important component of many computer-aided design tasks. This paper describes a package for manipulating Boolean functions based on the reduced, ordered, binary decision diagram (ROBDD) representation. The package is based on an efficient implementation of the if-then-else (ITE) operator. A hash table is used to maintain a strong canonical form in the ROBDD, and memory use is improved by merging the hash table and the ROBDD into a hybrid data structure. A memory function for the recursive ITE algorithm is implemented using a hash-based cache to decrease memory use. Memory function efficiency is improved by using rules that detect when equivalent functions are computed. The usefulness of the package is enhanced by an automatic and low-cost scheme for recycling memory. Experimental results are given to demonstrate why various implementation trade-offs were made. These results indicate that the package described here is significantly faster and more memory-efficient than other ROBDD implementations described in the literature.

The COSMOS simulator provides fast and accurate switch-level modeling of MOS digital circuits. It attains high performance by preprocessing the transistor network into a functionally equivalent Boolean representation. This description, produced by the symbolic analyzer ANAMOS, captures all aspects of switch-level networks including bidirectional transistors, stored charge, different signal strengths, and indeterminate (X) logic values. The LGCC program translates the Boolean representation into a set of machine language evaluation procedures and initialized data structures. These procedures and data structures are compiled along with code implementing the simulation kernel and user interface to produce the simulation program. The simulation program runs an order of magnitude faster than our previous simulator MOSSIM II.