A Formal Framework for Modular Synchronous System Design

We present the formal framework for a novel approach for specifying and automatically implementing systems such as digital circuits and network protocols. The goal is to reduce the design time and effort required to build correct, efficient, complex systems and to eliminate the need for the designer to deal directly with global synchronization and concurrency issues. Our compiler automatically transforms modular and asynchronous specifications of circuits written in our specification language, into tightly coupled, fully synchronous implementations in synthesizable Verilog. We formally state the correctness theorems and give an outline of the correctness proofs for two of the three main techniques that our compiler implements.

• Type: Conference
• Year: 2003
• Where: FM
• Authors: Maria-Cristina V. Marinescu, Martin C. Rinard
• Keywords: Correctness Proofs, Correctness Theorems, Digital Circuits, FM 2003