Token-Aware Completion Functions for Elastic Processor Verification
Joint Authors
Sarker, Koushik
Katti, Rajendra S.
Srinivasan, Sudarshan K.
Source
Research Letters in Electronics
Issue
Vol. 2009, Issue 2009 (31 Dec. 2009), pp.1-5, 5 p.
Publisher
Hindawi Publishing Corporation
Publication Date
2009-09-06
Country of Publication
Egypt
No. of Pages
5
Main Subjects
Abstract EN
We develop a formal verification procedure to check that elastic pipelined processor designs correctly implement their instruction set architecture (ISA) specifications.
The notion of correctness we use is based on refinement.
Refinement proofs are based on refinement maps, which—in the context of this problem—are functions that map elastic processor states to states of the ISA specification model.
Data flow in elastic architectures is complicated by the insertion of any number of buffers in any place in the design, making it hard to construct refinement maps for elastic systems in a systematic manner.
We introduce token-aware completion functions, which incorporate a mechanism to track the flow of data in elastic pipelines, as a highly automated and systematic approach to construct refinement maps.
We demonstrate the efficiency of the overall verification procedure based on token-aware completion functions using six elastic pipelined processor models based on the DLX architecture.
American Psychological Association (APA)
Srinivasan, Sudarshan K.& Sarker, Koushik& Katti, Rajendra S.. 2009. Token-Aware Completion Functions for Elastic Processor Verification. Research Letters in Electronics،Vol. 2009, no. 2009, pp.1-5.
https://search.emarefa.net/detail/BIM-474935
Modern Language Association (MLA)
Srinivasan, Sudarshan K.…[et al.]. Token-Aware Completion Functions for Elastic Processor Verification. Research Letters in Electronics No. 2009 (2009), pp.1-5.
https://search.emarefa.net/detail/BIM-474935
American Medical Association (AMA)
Srinivasan, Sudarshan K.& Sarker, Koushik& Katti, Rajendra S.. Token-Aware Completion Functions for Elastic Processor Verification. Research Letters in Electronics. 2009. Vol. 2009, no. 2009, pp.1-5.
https://search.emarefa.net/detail/BIM-474935
Data Type
Journal Articles
Language
English
Notes
Includes bibliographical references
Record ID
BIM-474935