Formal Design of a Class of Computers
Li-Guo Wang and Michael MendlerAbstract: We present a novel construction model of hardware and demonstrate how to use it in the entire process of formally designing a class of computers involving their specification, construction and verification. In this report we focus on the high stages of the design: the refinement from the behaviour specification at machine instruction level to the abstract microprogram at the term transition level. The concept of term transition introduced in this work establishes a new generic high-level design stage which is common for computer architecture and design. Our approach is based on formal syntax and formal proof and constitutes a framework for the rigorous specification and verification of hardware synthesis systems.
ECS-LFCS-95-333, September 1995.
This report is available in the following formats:
Previous | Index | Next