Representing and modeling digital circuits
Tomas Rokicki · 1994
A computer-aided circuit design tool can be described as a set of algorithms applied to an internal representation of a circuit design or specification in order to answer specific questions or perform certain operations. The representation directly limits the operations that can be performed as well as the accuracy of the resulting answers. This dissertation concerns the development and exploration of one such design representation and shows how it is appropriate for a wide range of circuit design tasks. Along the way, we discover some new techniques for specification, modeling, simulation, and verification of circuits. We especially consider real-time aspects of circuit behavior, and we present some significant enhancements to existing real-time verification algorithms. We present a rich and expressive formalism, called orbital nets, that precisely describes control, timing, and data flow aspects of circuit behavior. We develop the concepts of synchronization, composition, and receptiveness for this formalism, and illustrate how it can be used to specify, model, simulate, and verify digital circuits. We present a textual description language that provides convenient access to orbital nets through parameterization, partial evaluation, and structural and functional decomposition. We present efficient hierarchical real-time simulation and verification algorithms. We prove the equivalence of continuous time and discrete time semantics for orbital nets, and develop some new geometric timing algorithms that exploit concurrency to efficiently verify real-time safety properties.