Paper Info
Title
Hardware Modeling Using Function Encapsulation
Abstract
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.
Year
DOI
Venue
2000
10.1007/3-540-40922-X_15
FMCAD
Keywords
Field
DocType
hardware modeling,high-level design,microprocessor verification project,abstract function,abstract specification,low-level design,hardware detail,reference model,microarchitectural design,executable behavioral model,function encapsulation,acl2 encapsulation,behavior modeling,speculative execution
Computer architecture,Reference model,Computer science,Speculative execution,Microprocessor,Behavioral modeling,Formal specification,Real-time computing,ACL2,Computer hardware,Branch predictor,Executable
Conference
Volume
ISSN
ISBN
1954
0302-9743
3-540-41219-0
Citations 
PageRank 
References 
2
0.40
7
Authors
2
Name
Order
Citations
PageRank
Jun Sawada132521.16
Warren A. Hunt, Jr.252059.18