DocumentCode
3296153
Title
Modeling and verification of a pipelined CPU
Author
Ivanov, Lubomir
Author_Institution
Dept. of Comput. Sci., Iona Coll., New Rochelle, NY, USA
Volume
3
fYear
2002
fDate
4-7 Aug. 2002
Abstract
In this paper, we present a formal model of a pipelined version of the DLX processor, and verify the correct operation of the pipeline using a formal verification approach based series-parallel posets. We illustrate how the method can be used to detect pipeline hazards and other problems. The full verification was carried out automatically with the help of a verification tool, based on algorithms with low time- and space complexity.
Keywords
formal verification; integrated circuit design; integrated circuit modelling; logic design; microprocessor chips; pipeline processing; DLX processor; automatic verification tool; formal verification software tool; low complexity algorithms; pipeline hazards; pipelined CPU modeling; series-parallel poset verification; Computer industry; Educational institutions; Formal verification; Hazards; Pipelines; Protocols; Registers; Software standards; Software tools; Standards development;
fLanguage
English
Publisher
ieee
Conference_Titel
Circuits and Systems, 2002. MWSCAS-2002. The 2002 45th Midwest Symposium on
Print_ISBN
0-7803-7523-8
Type
conf
DOI
10.1109/MWSCAS.2002.1187062
Filename
1187062
Link To Document