Title :
Report on the formal specification and partial verification of the VIPER microprocessor
Author :
Brock, Bishop ; Hunt, Warren A., Jr.
Author_Institution :
Comput. Logic, Austin, TX, USA
Abstract :
VIPER (verifiable integrated processor for enhanced reliability) is a 32-b microprocessor architecture. The claim that the gate level of the VIPER microprocessor is mathematically verified is examined. Although a great deal of effort has been expended on the formal specification and verification of VIPER, there is not sufficient evidence to substantiate the claim that the VIPER gate-level specification (the implementation netlist) has been proven to implement its top-level specification (the instruction interpreter). Some of the broader issues in managing formal hardware verification projects are discussed, using the VIPER projects as an example. The specification and verification approach used for VIPER is also contrasted with that used during the specification and verification of the FM8502 microprocessor
Keywords :
formal logic; formal specification; microprocessor chips; program verification; FM8502 microprocessor; VIPER gate-level specification; VIPER microprocessor; enhanced reliability; formal hardware verification projects; formal specification; gate level; implementation netlist; instruction interpreter; microprocessor architecture; top-level specification; verifiable integrated processor; Automotive engineering; Formal specifications; Hardware; Humans; Logic; Microprocessor chips; Military computing; NASA; Process design; Radar;
Conference_Titel :
Computer Assurance, 1991. COMPASS '91, Systems Integrity, Software Safety and Process Security. Proceedings of the Sixth Annual Conference on
Conference_Location :
Gaithersburg, MD
Print_ISBN :
0-7803-0126-9
DOI :
10.1109/CMPASS.1991.161048
