Synthesis of Digital Designs from Recursive Equations (ACM Distinguished Dissertation)

0.0

Applicative languages provide a fully abstract, mathematically natural notation for specifying algorithms. This book develops a new approach to digital circuit design that is founded on the tenets of applicative programming style and which sheds light on functional programming disciplines by exploring their use in a novel realm of implementation. The book defines a circuit description language that uses systems equations to state connectivity-systems that are, in fact, applicative programs that compute the logical behavior of the circuit described. An interpreter is then presented through which both specifications and target descriptions can be executed, allowing engineers to experiment directly with the design notation without having to translate into a simulation language or construct a physical prototype. This greatly facilitates informal verification of design refinements and the implementation of benchmark tests. Moreover, the target language stands alone as a vehicle for rapid prototyping when more traditional design methods are used. An introduction to program synthesis through transformation is included. The techniques discussed are later adapted to digital design synthesis. A formal model of digital behavior is defined and a connection established between functional specifications and digital descriptions. A central theorem gives the characterization needed to serve as a goal for transformation. Several short examples illustrate the basic approach from the formal and experimental points of view. A complex exercise in language-driven design shows how advanced programming techniques can be brought to bear on larger design efforts. And finally, the book defines a specialized transformation system to address data flow. This book is included in the ACM Distinguished Dissertation Series.