Formal implementation verification of the bus interface unit for the Alpha 21264 microprocessor

Posted at 1:00 am on 10/12/1997 by Dr. Rahul Razdan


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.

Full Article in  Proceedings., 1997 IEEE International Conference on Computer Design: VLSI in Computers and Processors, 1997. ICCD'97.


Total Views: 152