Constructive Verification Of Quasi Delay-Insensitive Circuits

Abstract

Self-timed circuits have recently regained active interest as their abilities in avoiding timing and voltage margins, disconnecting pipeline depth from occupancy, and achieving average-case performance can help mitigate the challenges of very deep sub-micron design. However, there has been limited industrial adoption of these techniques, significantly due to the lack of commercial Computer Aided Design (CAD) support for synthesis and verification. This thesis presents a novel verification technique for the Quasi Delay-Insensitive (QDI) family of self-timed circuits leveraging properties of these circuits to reconstruct specifications from their implementations, using very little designer effort. The technique is presented in three stages: first, how to extract synchronization information from the gatelevel description, second, a type-and-effect system for ensuring stability and noninterference in the synchronization protocols, and lastly, a method for removing concurrency while maintaining the implementation relation of interest.