A formal method for provably correct composition of a real-life processor out of basic components. (The APE100 Reverse Engineering Study)

Author

Börger, Egon ; Del Castillo, Giuseppe

Author_Institution

Dipartimento di Inf., Pisa Univ., Italy

fYear

1995

fDate

6-10 Nov 1995

Firstpage

145

Lastpage

148

Abstract

We present a design approach which allows us to formally specify a real-life processor as composed out of its basic architectural (formally specified) components. The methodology provides means to rely upon hierarchical refinements and modular structuring of the specifications as a discipline to control the behaviour of complex units in terms of the behaviour of their components. In particular this enables us to prove interesting dynamic properties about the processor in terms of properties of its basic architectural components. We have developed the method to accomplish a reverse engineering project for the VLSI implemented microprocessor zCPU, the controller of the successful APE100 massively parallel machine

Keywords

formal specification; parallel architectures; reverse engineering; APE100 Reverse Engineering; APE100 massively parallel machine; formal method; microprocessor zCPU; modular structuring; provably correct composition; real-life processor; Algebra; Assembly; Hardware; Lattices; Load modeling; Microprocessors; Numerical simulation; Pipeline processing; Reverse engineering; Very large scale integration;

fLanguage

English

Publisher

ieee

Conference_Titel

Engineering of Complex Computer Systems, 1995. Held jointly with 5th CSESAW, 3rd IEEE RTAW and 20th IFAC/IFIP WRTP, Proceedings., First IEEE International Conference on

Conference_Location

Ft. Lauderdale, FL

Print_ISBN

0-8186-7123-8

Type

conf

DOI

10.1109/ICECCS.1995.479320

Filename

479320