Title :
Modeling and verification of a pipelined CPU
Author_Institution :
Dept. of Comput. Sci., Iona Coll., New Rochelle, NY, USA
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;
Conference_Titel :
Circuits and Systems, 2002. MWSCAS-2002. The 2002 45th Midwest Symposium on
Print_ISBN :
0-7803-7523-8
DOI :
10.1109/MWSCAS.2002.1187062
