Formal verification of a pipelined microprocessor

Author

Srivas, Mandayam ; Bickford, Mark

Author_Institution

Odyssey Res. Associates, Ithaca, NY, USA

Volume

7

Issue

5

fYear

1990

Firstpage

52

Lastpage

64

Abstract

The application of modern functional languages and supporting verification technology to a scaled-down but realistic microprocessor is described. The model is of an infinite stream of machine instructions consuming an infinite stream of interrupt signals and is specified at two levels: instruction and hardware design. A correctness criterion is stated for an appropriate sense of equivalent behavior of these levels and proved using a mechanically supported induction argument. The functional-language-based verification system Clio and the Mini Cayuga microprocessor are described. The formal specification and verification process are examined in detail.<>

Keywords

functional programming; microprocessor chips; parallel architectures; parallel machines; program verification; Mini Cayuga microprocessor; correctness criterion; formal specification; functional-language-based verification system Clio; hardware design; infinite stream; interrupt signals; machine instructions; mechanically supported induction argument; modern functional languages; pipelined microprocessor; verification process; verification technology; Application software; Clocks; Formal verification; Hardware; Mathematical model; Microprocessors; Pipeline processing; Reduced instruction set computing; Registers; Writing;

fLanguage

English

Journal_Title

Software, IEEE

Publisher

ieee

ISSN

0740-7459

Type

jour

DOI

10.1109/52.57892

Filename

57892