Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

20

WADT
2001
Springer

favoriteEmaildiscussreport

106views Software Engineering» more WADT 2001»

Verifying a Simple Pipelined Microprocessor Using Maude

13 years 9 months ago

Verifying a Simple Pipelined Microprocessor Using Maude

Download www-compsci.swan.ac.uk

Abstract. We consider the veriﬁcation of a simple pipelined microprocessor in Maude, by implementing an equational theoretical model of systems. Maude is an equationally-based language, with an eﬃcient term rewriting implementation, and eﬀective meta-level tools. Microprocessors and other systems are modelled as iterated maps operating in time e state-set, and are related by means of data and abstraction maps, and correctness is reduced to state exploration by the choice of an appropriate initialisation function, ensuring/enforcing consistency of the initial state.

Neal A. Harman

Real-time Traffic

Equational Theoretical Model | Simple Pipelined Microprocessor | Software Engineering | Term Rewriting Implementation | WADT 2001 |

claim paper

Related Content

» Automatic Verification of Pipelined Microprocessors

» Efficient Microprocessor Verification using Antecedent Conditioned Slicing

» A simple verified validator for software pipelining

» VerificationAware Microprocessor Design

» Automated Pipeline Design

» A Methodology for Validation of Microprocessors using Equivalence Checking

» A RefinementBased Compositional Reasoning Framework for Pipelined Machine Verification

» A Design Environment for Counterflow Pipeline Synthesis

» Tamper Evident Microprocessors

Post Info
More Details (n/a)

Added	30 Jul 2010
Updated	30 Jul 2010
Type	Conference
Year	2001
Where	WADT
Authors	Neal A. Harman

Comments (0)