With the success of the CounterDataFlow Pipeline microarchitecture developed by Oregon State University, there is increasing demand for a highly flexible high-level simulator modeling tool to support the further expansions and studies of the Counterflow pipeline processors family. This work examines the implementation of a Java-based execution-driven simulator modeling tool, bBlocks, which gains flexibility by identifying the independent parts in a micro system and partitioning them into reusable blocks. Two simulators have been constructed to demonstrate the possibility of bBlocks. / Graduation date: 2001

Thesis (Ph. D.)--University of Texas at Austin, 1999. / Vita. Includes bibliographical references (leaves 1103-1112). Available also in a digital version from Dissertation Abstracts.

Thesis (M.S.)--Ohio University, June, 1990. / Title from PDF t.p.

Thesis (M.S. in Electrical Engineering)--Washington State University. / Includes bibliographical references.

Thesis (Ph. D.)--Washington State University, May 2006. / Includes bibliographical references (p. 94-96).

Thesis (M.S.)--Ohio University, November, 1987. / Title from PDF t.p.

Thesis (Ph. D.)--University of Texas at Austin, 2008. / Vita. Includes bibliographical references.

Revision of thesis (Ph. D.)--Auburn University, 1979. / Includes index. Bibliography: p. 149-150.

Thesis (Ph.D.)--University of Delaware, 2006. / Principal faculty advisor: Guang R. Gao, Dept. of Electrical and Computer Engineering. Includes bibliographical references.

Functional verification is a critical problem facing the semiconductor industry: hardware designs are extremely complex and highly optimized, and even a single bug in deployed systems can cost more than $10 billion. We focus on the verification of pipelining, a key optimization that appears extensively in hardware systems such as microprocessors, multicore systems, and cache coherence protocols. Existing techniques for verifying pipelined machines either consume excessive amounts of time, effort, and resources, or are not applicable at the bit-level, the level of abstraction at which commercial systems are designed and functionally verified. We present a highly automated, efficient, compositional, and scalable refinement-based approach for the verification of bit-level pipelined machines. Our contributions include: (1) A complete compositional reasoning framework based on refinement. Our notion of refinement guarantees that pipelined machines satisfy the same safety and liveness properties as their instruction set architectures. In addition, our compositional framework can be used to decompose correctness proofs into smaller, more manageable pieces, leading to drastic reductions in verification times and a high-degree of scalability. (2) The development of ACL2-SMT, a verification system that integrates the popular ACL2 theorem prover (winner of the 2005 ACM Software System Award) with decision procedures. ACL2-SMT allows us to seamlessly take advantage of the two main approaches to hardware verification: theorem proving and decision procedures. (3) A proof methodology based on our compositional reasoning framework and ACL2-SMT that allows us to reduce the bit-level verification problem to a sequence of highly automated proof steps. (4) A collection of general-purpose refinement maps, functions that relate pipelined machine states to instruction set architecture states. These refinement maps provide more flexibility and lead to increased verification efficiency. The effectiveness of our approach is demonstrated by verifying various pipelined machine models, including a bit-level, Intel XScale inspired processor that implements 593 instructions and includes features such as branch prediction, precise exceptions, and predicated instruction execution.