Bluenose II: Towards Faster Design and Verification of Pipelined Circuits

pipelined circuits;design automation;formal design verification;Electrical and Computer Engineering

Chan, Ca Bol

University of Waterloo

关键词: pipelined circuits;    design automation;    formal design verification;    Electrical and Computer Engineering;   

Others  :  https://uwspace.uwaterloo.ca/bitstream/10012/3939/1/thesis.pdf

瑞士|英语

来源: UWSPACE Waterloo Institutional Repository

【 摘 要 】

The huge demand for electronic devices has driven semiconductor companies to create better products in terms of area, speed, power etc. and to deliver them to market faster. Delay to market can result in lost opportunities. The length of the design cycle directly affects the time to market. However, inadequate time for design and verification can cause bugs that will cause further delays to market and correcting the error after manufacturing is very expensive. A bug in an ASIC found after fabrication requires respinning the mask at a cost of several million dollars. Even as the pressure to reduce the length of the design cycles grows, the size and complexity of digital hardware circuits have increased, which puts even greater pressure on design and verification productivity. Pipelining is one optimization technique which has contributed to the increased complexity in hardware design. Pipeline increases throughput by overlapping the execution of instructions. It is a challenge to design and verify pipelines because the specification is written to describe how instructions are executed in sequence while there can be multiple instructions being executed in a pipeline at one time. The overlapping of instructions adds further complexity to the hardware in the form of hazards which arise from resource conflicts, data dependencies or speculation of parcels due to branch instructions. To address these issues, we present PipeNet, a metamodel for describing hardware design at a higher level of abstraction and Bluenose II, a graphical tool for manipulating a PipeNet model. PipeNet is based on a pipeline model in a formal pipeline verification framework. The pipeline model contains arbiters, flow-control state machines, datapath and data-routing. The designer describes the pipeline design using PipeNet. Based on the PipeNet model, Bluenose II generates synthesizable VHDL code and a HOL verification script. Bluenose II;;s ability to generate HOL scripts turns the HOL theorem prover into Bluenose II;;s external verification environment. A direct connection to HOL is implemented in the form of a console to display results from HOL directly in Bluenose II. The data structures that represent PipeNet are evaluated for their extensibility to accommodate future changes. Finally, a case study based on an implementation of a two-wide superscalar 32-bit RISC integer pipeline is conducted to examine the quality of the generated codes and the entire design process in Bluenose II. The generation of VHDL code is improved over that provided in Bluenose I, Bluenose II;;s predecessor.