Title :
Formal verification of a pipelined microprocessor
Author :
Srivas, Mandayam ; Bickford, Mark
Author_Institution :
Odyssey Res. Associates, Ithaca, NY, USA
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;
Journal_Title :
Software, IEEE
