From programs to transistors: Verifying hardware synthesis tools

Abstract

We describe a project for synthesizing circuits from a high-level language description. The aims of this project are to guarantee the correctness of the resulting designs while allowing the designer flexibility in interacting with the system. In this paper we discuss two components of the project. The first starts with a state transition system and generates a specification of a datapath and an implementation of a controller as a microcode ROM. The second generates correct CMOS implementations of boolean expressions. This component produces highly optimized circuits which contain transmission gates as well as series and parallel networks of transistors. These two components are part of a larger goal: to go from programs to transistors with a flexible, yet guaranteed correct system.