loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
First IEEE International Conference on Engineering of Complex Computer Systems (ICECCS'95)
A formal method for provably correct composition of a real-life processor out of basic components. (The APE100 Reverse Engineering Study)
Ft. Lauderdale, Florida
November 06-November 10
ISBN: 0-8186-7123-8
ASCII Text
x 
 
E. Borger, G. Del Castillo, "A formal method for provably correct composition of a real-life processor out of basic components. (The APE100 Reverse Engineering Study)," Engineering of Complex Computer Systems, IEEE International Conference on, pp. 145, First IEEE International Conference on Engineering of Complex Computer Systems (ICECCS'95), 1995.
 
 
BibTex
x
 
@article{ 10.1109/ICECCS.1995.479320,
author = {E. Borger and G. Del Castillo},
title = {A formal method for provably correct composition of a real-life processor out of basic components. (The APE100 Reverse Engineering Study)},
journal ={Engineering of Complex Computer Systems, IEEE International Conference on},
volume = {0},
year = {1995},
isbn = {0-8186-7123-8},
pages = {145},
doi = {http://doi.ieeecomputersociety.org/10.1109/ICECCS.1995.479320},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Engineering of Complex Computer Systems, IEEE International Conference on
TI - A formal method for provably correct composition of a real-life processor out of basic components. (The APE100 Reverse Engineering Study)
SN - 0-8186-7123-8
SP
EP
A1 - E. Borger,
A1 - G. Del Castillo,
PY - 1995
KW - reverse engineering; parallel architectures; formal specification; real-life processor; APE100 Reverse Engineering; modular structuring; microprocessor zCPU; APE100 massively parallel machine; provably correct composition; formal method
VL - 0
JA - Engineering of Complex Computer Systems, IEEE International Conference on
ER -
 
E. Borger, Dipartimento di Inf., Pisa Univ., Italy
G. Del Castillo, Dipartimento di Inf., Pisa Univ., Italy
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.
Index Terms:
reverse engineering; parallel architectures; formal specification; real-life processor; APE100 Reverse Engineering; modular structuring; microprocessor zCPU; APE100 massively parallel machine; provably correct composition; formal method
Citation:
E. Borger, G. Del Castillo, "A formal method for provably correct composition of a real-life processor out of basic components. (The APE100 Reverse Engineering Study)," iceccs, pp.145, First IEEE International Conference on Engineering of Complex Computer Systems (ICECCS'95), 1995
Usage of this product signifies your acceptance of the Terms of Use.