Certified Software for Designing Asynchronous Circuits

Abstract

Correctness and trust in a piece of software is important, especially for complex and/or critical systems like medical devices, computerized weapons, or any management of private data. Certified software aims to evidence correctness and establish trust in software by pairing executable instructions with mechanically-verifiable proofs that certain properties of the instructions are upheld. In this dissertation, we build certified software that is used to design asynchronous circuits. These circuits differ from synchronous circuits by coordinating communication via local message-passing channels rather than a global clock signal. Asynchronous circuits improve upon the time- and power-efficiency of synchronous circuits, but also introduce the complexity challenges of decentralized circuit communication. Communicating Hardware Processes (CHP) is a language used to write high-level asynchronous circuit designs. We use the Coq Proof Assistant to build a mechanical formalization of CHP language semantics and a certified CHP program simulator. The semantics formalization is novel in the combination of its mechanization, its comprehensive expression of the CHP language, and its precise abstraction of lower-level circuit design decisions. The simulator is novel in its certification, which mechanically verifies that it simulates a CHP program correctly, and it serves as a model for future Coq-built CHP software tools that can be certified against the mechanical language semantics.