TRS as an HDL
Clean, expressive, precise and concise
- speculative & superscalar microarchitectures
- memory models & cache coherence protocols [ISCA99, ICS99]
Supports parallel and non-deterministic specifications
The correctness of a TRS can be verified against a reference TRS specification
Some pipelining can be done automatically as a source-to-source transformation on TRS’s
Superscalar versions of TRS’s can be derived mechanically from pipelined TRS’s.