Architectural Specification and Simulation Through Rewriting-Logic

In recent years Arvind’s Group at MIT has shown the usefulness of term rewriting theory for the specification of processor architectures. In their approach processors spec-ified by term rewriting systems are translated into a stan-dard hardware description language for simulation pur-poses. In this work we present our current investigation on the use of Rewriting-Logic, which is a more powerful theo-retical framework than pure rewriting, for specification and verification of processor architectures at a higher abstrac-tion level. We adopt the rewriting-logic environment ELAN to specify and verify architectures without the need to resort to the details of hardware description languages for simu-lation purposes. Our investigation shows that simulation at rewriting-logic level may provide useful insights to guide the architectural design