DocumentCode
1118309
Title
Some Problems in Certifying Microprograms
Author
Leeman, George B., Jr.
Author_Institution
Department of Computer Science, IBM Thomas J. Watson Research Center
Issue
5
fYear
1975
fDate
5/1/1975 12:00:00 AM
Firstpage
545
Lastpage
553
Abstract
A hypothetical computer is described, and procedures are indicated for showing the correctness of its microprogram. The underlying method used is that of Birman [1]. However, the computer discussed has some realistic characteristics not shared by the machine treated in [1], and the details of the microcode validation are complicated by this fact. A formal technique for partitioning the proof is presented and illustrated with examples.
Keywords
Program correctness, algebraic simulation, abstract program, microprogramming, commutative diagram, theorem proving.; Certification; Commutation; Computational modeling; Computer simulation; Data flow computing; Emulation; Manuals; Microprogramming; Programming profession; Read-write memory; Program correctness, algebraic simulation, abstract program, microprogramming, commutative diagram, theorem proving.;
fLanguage
English
Journal_Title
Computers, IEEE Transactions on
Publisher
ieee
ISSN
0018-9340
Type
jour
DOI
10.1109/T-C.1975.224258
Filename
1672851
Link To Document