Hardware Modeling Using Function Encapsulation
We describe how to specify an executable behavioral model of hardware without specifying the hardware detail using ACL2 encapsulation. ACL2 encapsulation is a mechanism to introduce abstract functions with constraints. It can be used to specify a microarchitectural design of hardware, which can be used for early simulation and for verification. Such a high-level design can also be used as a reference model when implementing low-level designs in RTL. This paper examines two abstract specifications from a microprocessor verification project. One example is a branch predictor for a processor with speculative execution and the other is a pipelined multiplier.
KeywordsAbstract Design Speculative Execution Branch Prediction Branch Instruction Hardware Modeling
Unable to display preview. Download preview PDF.
- BD94.Jerry R. Burch and David L. Dill. Automatic verification of pipelined microprocessor control. In Computer-Aided Verification (CAV’ 94), volume 818 of LNCS, pages 68–80. Springer Verlag, 1994.Google Scholar
- HS99.Warren A. Hunt, Jr. and Jun Sawada. The FM9801 microprocessor verification. IEEE Micro, 19(3):47–55, May/June 1999.Google Scholar
- KM96.Matt Kaufmann and J Strother Moore. ACL2: An industrial strength version of nqthm. In Eleventh Annual Conference on Computer Assurance (COMPASS-96), pages 23–34. IEEE Computer Society Press, June 1996.Google Scholar
- KM99.Matt Kaufmann and J Strother Moore. ACL2: A Computational Logic for Applicative Common Lisp, The User’s Manual. 1999. URL: http://www.cs.utexas.edu/users/moore/acl2/acl2-doc.html #User’s-Manual. KMM00. M. Kaufmann, P. Manolios, and J S. Moore. Computer-Aided Reasoning: An Approach. Kluwer Academic Press, 2000.
- Saw99a.Jun Sawada. Formal Verification of an Advanced Pipelined Machine. PhD thesis, University of Texas at Austin, December 1999. Also available from http://www.cs.utexas.edu/users/sawada/dissertation/diss.html
- Saw99b.Jun Sawada. Verification scripts for FM9801 pipelined microprocessor design, 1999. http://www.cs.utexas.edu/users/sawada/FM9801/
- SCV+99.Patrick Schaumont, Radim Cmar, Serge Vernalde, Marc Engels, and Ivo Bolsens. Hardware reuse at the behavioral level. In Design Automation Conference (DAC’ 99), pages 552–557. ACM Press, June 1999.Google Scholar
- Sho84.Robert E. Shostak. Deciding combinations of theories. Journal of the ACM, 31(1):1–12, January 1984.Google Scholar
- VB99.Miroslav N. Velev and Randal E. Bryant. Superscalar processor verification using efficient reductions of the logic of equality with uninterpreted functions to propositional logic. In Laurence Pierre and Thomas Kropf, editors, Correct Hardware Design and Verification Methods, (CHARME’ 99), volume 1703 of LNCS, pages 37–53. Springer Verlag, 1999.Google Scholar
- WH99.Dyson Wilkes and M.M. Kamal Hashmi. Application of high level interfacebased design to telecommunications system hardware. In Design Automation Conference (DAC’ 99), pages 552–557. ACM Press, June 1999.Google Scholar
- Win90.Phillip J. Windley. The Formal Verification of Generic Interpreters. PhD thesis, University of California, Davis, jun 1990.Google Scholar