Title :
Formal verification of an Intel XScale processor model with scoreboarding, specialized execution pipelines, and impress data-memory exceptions
Author :
Srinivasan, Sudharshan K. ; Velev, Miroslav N.
Author_Institution :
Sch. of Electr. & Comput. Eng., Georgia Inst. of Technol., Atlanta, GA, USA
Abstract :
We present the formal verification of an Intel Xscale processor model. The Xscale is a superpipelined RISC processor with 7-stage integer, 8-stage memory, and variable-latency multiply-and-accumulate execution pipelines. The processor uses scoreboarding to track data dependencies, and implements both precise and imprecise exceptions. Such set of features had not been modeled and formally verified previously. The formal verification was done with an automatic tool flow that consists of the term-level symbolic simulator TLSim, the decision procedure EVC, and an efficient SAT-checker.
Keywords :
computer testing; formal verification; microprocessor chips; performance evaluation; pipeline processing; reduced instruction set computing; 7-stage integer; 8-stage memory; EVC decision procedure; Intel XScale processor model; SAT-checker; TLSim simulator; automatic tool flow; data dependency tracking; formal verification; impress data-memory exception; multiply-and-accumulate execution pipeline; scoreboarding; specialized execution pipeline; superpipelined RISC processor; term-level symbolic simulator; variable-latency; Formal verification; Pipelines;
Conference_Titel :
Formal Methods and Models for Co-Design, 2003. MEMOCODE '03. Proceedings. First ACM and IEEE International Conference on
Conference_Location :
Mont Saint Michel, France
Print_ISBN :
0-7695-1923-7
DOI :
10.1109/MEMCOD.2003.1210090