Partitioned model checking from software specifications

With the trends toward higher-level design, verification models written in software, and hardware/software codesign, it is increasingly important to verify that RTL hardware behaves correctly according to an executable software specification. In this paper, we propose a natural way to formalize a cycle-accurate software specification as an annotated control flow graph, and then we introduce a novel partitioned model-checking algorithm that exploits the annotated control flow graph. Preliminary experimental results show that our new method runs faster than standard model checking.