| Existing hardware development methods continue to struggle in the face of on-going advances in implementation technology. While computer-aided design tools have made impressive gains at the lowest levels of abstraction, methods to develop designs against abstract notions of correctness continue to lag far behind. This is especially problematic for fault-tolerant systems targeted to critical applications, both because of the greater complexity of these systems and because of the catastrophic consequences of an undetected design flaw. The work described in this dissertation addresses this problem by contributing a number of improved methods to: (i) model, (ii) verify, and (iii) compose hardware systems at the high levels of abstraction poorly served by existing methods.;In this dissertation we present a new state machine-based methodology for specifying hardware systems at high levels of abstraction. New methods for behavioral decomposition, early abstraction, and interclocked composition are described that support the practical modeling of large distributed hardware systems and several levels of fault-tolerant behavior. A highly-expressive and accessible interface logic is presented that supports the flexible abstraction mappings required by abstract state machines. Our specification methods are quite general, having demonstrated applications in both theorem proving and simulation-based modeling.;We describe a number of improved methods to verify abstract interpreters in this dissertation. Two new approaches are developed within a theorem proving environment that offer faster execution speeds and easier proof constructions in many applications. Both methods, called interval matching and signal rewriting, gain their efficiency through the reuse of complex behavior preproved for the individual components of a circuit. We also describe a new simulation environment with enhanced rigor and automation that adopts many of the concepts developed in a theorem proving environment. We present a novel proof-of-concept tool that automatically generates simulation test bench models for use in this new environment.;Finally, we present new methods to compose hardware subsystems represented at high levels of abstraction. The methods are rigorously sound, in the sense that the interconnections defined by such compositions are proved from the implementation structure. Compositions over point-to-point interconnects are supported by our methods. |
