This paper presents a method for automatic diagnosis and correction of design bugs in processors. Given a golden sequential instruction-set architecture model of a processor and its erroneous detailed cycle-accurate model at micro-architecture level, we employ a symbolic simulator and a property checker in an iterative process to formally find the candidate buggy locations and their corresponding fixes, without requiring an error model. We have shown the effectiveness of our method on a complex out-of-order super scalar processors supporting atomic execution.
展开▼
