Automated pipeline design

ABSTRACT

The interlock and forwarding logic is considered the tricky part of fully-featured piplined microprocessor and especially debugging these parts delays the hardware design process considerably. It is therefore desirable to automate the design of both interlock and forwarding logic. The hardware design engineer begins with a sequential implementation without any interlock and forwarding logic. A tool then adds the forwarding and interlock logic required for pipelining. This paper describes the algorithm for such a tool and the correctness is formally verified. We use a standard DLX RISC processor as an example.

REFERENCES

• 1: Clark W. Barrett , David L. Dill , Jeremy R. Levitt, A decision procedure for bit-vector arithmetic, Proceedings of the 35th annual conference on Design automation, p.522-527, June 15-19, 1998, San Francisco, California, United States [doi>10.1145/277044.277186]
• 2: Mark Bickford , Mandayam Srivas, Verification of a pipelined microprocessor using Clio, Proceedings of the Mathematical Sciences Institute workshop on Hardware specification, verification and synthesis: mathematical aspects, p.307-332, February 1990, Ithaca, New York, United States
• 3: Armin Biere , Edmund M. Clarke , Richard Raimi , Yunshan Zhu, Verifiying Safety Properties of a Power PC Microprocessor Using Symbolic Model Checking without BDDs, Proceedings of the 11th International Conference on Computer Aided Verification, p.60-71, July 06-10, 1999
• 4: Randal E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, Aug. 1986 [doi>10.1109/TC.1986.1676819]
• 5: A. Camilleri, M. Gordon, and T. Melham. Hardware verification using higher order logic. In From HDL Descriptions to Guaranteed Correct Circuit Designs, pages 41-66. North-Holland, 1986.
• 6: Edmund M. Clarke , E. Allen Emerson, Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic, Logic of Programs, Workshop, p.52-71, May 01, 1981
• 7: E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
• 8: David Cyrluk , S. Rajan , Natarajan Shankar , Mandayam K. Srivas, Effective Theorem Proving for Hardware Verification, Proceedings of the Second International Conference on Theorem Provers in Circuit Design - Theory, Practice and Experience, p.203-222, September 26-28, 1994
• 9: Michael J. Flynn, Computer Architecture: Pipelined and Parallel Processor Design, Jones and Bartlett Publishers, Inc., 1995
• 10: John L. Hennessy , David A. Patterson, Computer architecture (2nd ed.): a quantitative approach, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1996
• 11: Ravi Hosabettu , Ganesh Gopalakrishnan , Mandayam K. Srivas, A Proof of Correctness of a Processor Implementing Tomasulo's Algorithm without a Reorder Buffer, Proceedings of the 10th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, p.8-22, September 27-29, 1999
• 12: C. Jacobi and D. Kroening. Proving the correctness of a complete microprocessor. In Proc. of 30. Jahrestagung der Gesellschaft f. ur Informatik. Springer, 2000.
• 13: M. Kaufmann and J. Moore. ACL2: An industrial strength version of nqthm. In In Proc. of the Eleventh Annual Conference on Computer Assurance, pages 23-34. IEEE, 1996.
• 14: D. Kroening, W. Paul, and S. Mueller. Proving the correctness of pipelined micro-architectures. In Proc. of the ITG/GI/GMM-Workshop "Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen", pages 89-98. VDE, 2000.
• 15: Jeremy Levitt , Kunle Olukotun, A scalable formal verification methodology for pipelined microprocessors, Proceedings of the 33rd annual conference on Design automation, p.558-563, June 03-07, 1996, Las Vegas, Nevada, United States [doi>10.1145/240518.240624]
• 16: M. McFarland. Formal verification of sequential hardware: A tutorial. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 12(5):633-654, 1993.
• 17: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 18: Kenneth L. McMillan, Verification of an Implementation of Tomasulo's Algorithm by Compositional Model Checking, Proceedings of the 10th International Conference on Computer Aided Verification, p.110-121, June 28-July 02, 1998
• 19: Kenneth L. McMillan, Verification of Infinite State Systems by Compositional Model Checking, Proceedings of the 10th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, p.219-234, September 27-29, 1999
• 20: Silvia M. Muller , Wolfgang Paul, Computer Architecture: Complexity and Correctness, Springer-Verlag New York, Inc., Secaucus, NJ, 2000
• 21: David A. Patterson , John L. Hennessy, Computer organization & design: the hardware/software interface, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1993
• 22: Jun Sawada , Warren A. Hunt, Jr., Results of the Verification of a Complex Pipelined Machine Model, Proceedings of the 10th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, p.313-316, September 27-29, 1999
• 23: James E. Smith , Andrew R. Pleszkun, Implementing Precise Interrupts in Pipelined Processors, IEEE Transactions on Computers, v.37 n.5, p.562-573, May 1988 [doi>10.1109/12.4607]
• 24: Miroslav N. Velev , Randal E. Bryant, Formal verification of superscale microprocessors with multicycle functional units, exception, and branch prediction, Proceedings of the 37th conference on Design automation, p.112-117, June 05-09, 2000, Los Angeles, California, United States [doi>10.1145/337292.337331]
• 25: Phillip J. Windley, Formal Modeling and Verification of Microprocessors, IEEE Transactions on Computers, v.44 n.1, p.54-72, January 1995 [doi>10.1109/12.368009]

INDEX TERMS

Primary Classification:
  C. Computer Systems Organization
  C.1 PROCESSOR ARCHITECTURES
      C.1.3 Other Architecture Styles
          Subjects: Pipeline processors

Additional Classification:
  C. Computer Systems Organization

  J. Computer Applications
  J.2 PHYSICAL SCIENCES AND ENGINEERING
      Subjects: Electronics

General Terms:
Design, Measurement, Performance, Theory, Verification

Keywords:
forwarding, interlock, pipeline