Simplifying the design and automating the verification of pipelines with structural hazards
Jason T. Higgins, Mark D. Aagaard · ACM Transactions on Design Automation of Electronic Systems · 2005
This article describes a technique that simplifies the design of pipelined circuits automates the specification and verification of structural-hazard and datapath correctness properties for pipelined circuits. The technique is based upon a template for pipeline stages, a control-circuit cell library, a decomposition of structural hazard and datapath correctness into a collection of simple properties, and a prototype design tool that generates verification scripts for use by external tools. Our case studies include scalar and superscalar implementations of a 32-bit OpenRISC integer microprocessor.