JavaScript is disabled for your browser. Some features of this site may not work without it.
Certified Software for Designing Asynchronous Circuits

Author
Nkounkou, Brittany
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.
Description
83 pages Supplemental file(s) description: Coq Code.
Date Issued
2020-08Subject
asynchronous circuits; certified software; communicating hardware processes; coq proof assistant; formal methods; programming languages
Committee Chair
Tate, Ross Everett
Committee Member
Manohar, Rajit; Weatherspoon, Hakim; Constable, Bob
Degree Discipline
Computer Science
Degree Name
Ph. D., Computer Science
Degree Level
Doctor of Philosophy
Rights
Attribution-ShareAlike 4.0 International
Type
dissertation or thesis
Except where otherwise noted, this item's license is described as Attribution-ShareAlike 4.0 International