Title :
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
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;
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
DOI :
10.1109/ICECCS.1995.479320
