DocumentCode :
710628
Title :
Signature oriented model pruning to facilitate multi-threaded processors debugging
Author :
Refan, Fatemeh ; Alizadeh, Bijan ; Navabi, Zainalabedin
Author_Institution :
Sch. of Electr. & Comput. Eng., Univ. of Tehran, Tehran, Iran
fYear :
2015
fDate :
27-29 April 2015
Firstpage :
1
Lastpage :
6
Abstract :
In this paper, we propose a signature based pruning technique to facilitate the debugging of multi-threaded processors. To accomplish this, a pipelined implementation of the multi-threaded processor model is checked for correspondence against the specification model based on flushing proof. Then, a two-stage signature oriented pruning method is proposed to avoid the space explosion problem caused by inserting debugging facilities in the model. The results show an average improvement of 47%, and 71% in the size of decision formula and CPU time for the DLX processor, respectively.
Keywords :
formal specification; formal verification; multi-threading; pipeline processing; program debugging; theorem proving; flushing proof; multithreaded processor debugging; pipelined implementation; signature oriented model pruning; space explosion problem; specification model; Data mining; Debugging; Instruction sets; Maintenance engineering; Pipelines; Registers; Correspondence Checking; Formal Debugging; Model Pruning; Multi-threaded Processors; State Space Explosion;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
VLSI Test Symposium (VTS), 2015 IEEE 33rd
Conference_Location :
Napa, CA
Type :
conf
DOI :
10.1109/VTS.2015.7116271
Filename :
7116271
Link To Document :
بازگشت