We have developed a new method for describing concurrent and asynchronous systems and successfully applied it to describing micro-architectures and cache coherence protocols.The method is based on term rewriting systems (TRS),in which system states are specficied by terms,and state transitions are efined by rewriting rules.Such descriptions are concise and amenable to both formal verification and hardware synthesis.(See,for example,Arvind and Xiaowei Shen,"Using Term Rewriting Systems to Design and Verify Processors",IEEE MICRO,May/June 1999).
展开▼