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

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

The wakeup logic in out-of-order superscalar microprocessors is responsible for resolving the data dependency hazard between instructions. Its performance is critical because it may prevent the processor to have deeper pipelines or to achieve the highest IPC (Instructions Per Cycle) possible. In this thesis, we implemented the circuit and layout for two types of wakeup logic (CAM-type and RAM-type) used in the modem microprocessors. These two implementations are simulated extensively using a circuit level simulator - HSPICE, with full parasitic loads. We, then, made comparison between the CAM-type and RAM-type wakeup circuits. From the simulation results, the CAM-type wakeup logic has a better performance than the RAM-type wakeup logic if a larger number of physical registers is employed by the processor. The performance impacts caused by varying the other superscalar design parameters, such as instruction window size and issue width, are not much different for both types of wakeup logic implementations. / Graduation date: 2003

Thesis (Ph. D.)--Ohio State University, 2005. / Title from first page of PDF file. Document formatted into pages; contains xix, 183 p.; also includes graphics (some col.). Includes bibliographical references (p. 170-183). Available online via OhioLINK's ETD Center

Thesis (M.S.)--University of Delaware, 2009. / Principal faculty advisor: Guang R. Gao, Dept. of Electrical & Computer Engineering. Includes bibliographical references.

Tang, Tin-Yau. / Thesis (M.Phil.)--Chinese University of Hong Kong, 2000. / Includes bibliographical references (leaves 122-123). / Abstracts in English and Chinese. / Table of Content --- p.2 / List of Figures --- p.4 / List of Tables --- p.6 / Acknowledgements --- p.7 / Abstract --- p.8 / Chapter I. --- Introduction --- p.11 / Chapter 1.1 --- Asynchronous Design --- p.12 / Chapter 1.1.1 --- What is asynchronous design? --- p.12 / Chapter 1.1.2 --- Potential advantages of asynchronous design --- p.12 / Chapter 1.1.3 --- Design methodology for asynchronous circuit --- p.15 / Chapter 1.1.4 --- Difficulty and limitation of asynchronous design --- p.19 / Chapter 1.2 --- Pipeline and Asynchronous Pipeline --- p.21 / Chapter 1.2.1 --- What is pipeline? --- p.21 / Chapter 1.2.2 --- Property of pipeline system --- p.21 / Chapter 1.2.3 --- Asynchronous pipeline --- p.23 / Chapter 1.3 --- Design Motivation --- p.26 / Chapter II. --- Design Theory --- p.27 / Chapter 2.1 --- A Novel Asynchronous Pipeline Architecture --- p.28 / Chapter 2.1.1 --- The problem of classical asynchronous pipeline --- p.28 / Chapter 2.1.2 --- The new handshake cell --- p.28 / Chapter 2.1.3 --- The modified asynchronous pipeline architecture --- p.29 / Chapter 2.2 --- Design of the ALU --- p.36 / Chapter 2.2.1 --- The functionality of ALU --- p.36 / Chapter 2.2.2 --- The choice of the adder and the BLC adder --- p.37 / Chapter III. --- Implementation --- p.41 / Chapter 3.1 --- ALU Detail --- p.42 / Chapter 3.1.1 --- Global arrangement --- p.42 / Chapter 3.1.2 --- Shift and Rotate --- p.46 / Chapter 3.1.3 --- Flags generation --- p.49 / Chapter 3.2 --- Application of the Pipeline Architecture --- p.53 / Chapter 3.2.1 --- The reset network for the pipeline architecture --- p.53 / Chapter 3.2.2 --- Handshake simplification for splitting and joining of datapath. --- p.55 / Chapter IV. --- Result --- p.59 / Chapter 4.1 --- Measurement and Simulation Result --- p.60 / Chapter 4.2 --- Global Routing Parasites --- p.63 / Chapter 4.3 --- Low Power Application --- p.65 / Chapter V. --- Conclusion --- p.67 / Chapter VI. --- Appendixes --- p.69 / Chapter 6.1 --- The Small Micro-coded Processor --- p.69 / Chapter 6.2 --- The Instruction Table of the ALU --- p.70 / Chapter 6.3 --- Measurement and Simulation Result --- p.71 / Chapter 6.4 --- "VHDLs, Schematics and Layout" --- p.87 / Chapter 6.5 --- Pinout of the Test Chip --- p.120 / Chapter 6.6 --- The Chip Photo --- p.121 / Chapter VII. --- Reference --- p.122

Thesis (M.S.)--Oregon State University, 2006. / Printout. Includes bibliographical references (leaves 104-107). Also available on the World Wide Web.

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

Due to the rapidly increasing complexity in hardware designs and competitive time to market trends in the industry, there is an inherent need to move designs to a higher level of abstraction. Behavioral Synthesis is the process of automatically compiling such Electronic System Level (ESL) designs written in high-level languages such as C, C++ or SystemC into Register-Transfer Level (RTL) implementation in hardware description languages such as Verilog or VHDL. However, the adoption of this flow is dependent on designers' faith in the correctness of behavioral synthesis tools. Loop pipelining is a critical transformation employed in behavioral synthesis process, and ubiquitous in commercial and academic behavioral synthesis tools. It improves the throughput and reduces the latency of the synthesized hardware. It is complex and error-prone, and a small bug can result in faulty hardware with expensive ramifications. Therefore, it is critical to certify the loop pipelining transformation so that designers can trust the behaviorally synthesized pipelined designs. Certifying a loop pipelining transformation is however, a major research challenge because there is a huge semantic gap between the input sequential design and the output pipelined implementation, making it infeasible to verify their equivalence with automated sequential equivalence checking (SEC) techniques. Complex loop pipelining transformations can be certified by a combination of theorem proving and SEC: (1) creating a certified pipelining algorithm which generates a reference pipeline model by exploiting pipeline generation information from the synthesis flow (e.g. the iteration interval of a generated pipeline) and (2) conduct SEC between the synthesized pipeline and this reference model. However, a key and arguably, the most complex component of this approach is the development of a formal, mechanically verifiable loop pipelining algorithm. We show how to systematically construct such an algorithm, and carry out its verification using the ACL2 theorem prover. We propose a framework of certified pipelining primitives which are essential for designing pipelining algorithms. Using our framework, we build a certified loop pipelining algorithm. We also propose a key invariant in certifying this algorithm, which links sequential loops with their pipelined counterparts. This is unlike other invariants that have been used in proofs of microprocessor pipelines so far. This dissertation provides a framework for creating certified pipelining algorithms utilizing a mechanical theorem prover. Using this framework, we have developed a certified loop pipelining algorithm. This certified algorithm is essential in the overall approach to certify behaviorally synthesized pipelined designs. We demonstrate the scalability and robustness of our algorithm on several ESL designs across various domains.

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.