Partitioned Model Checking from Software Specifications Xiushan Feng, Alan J. Hu, and Jin Yang IEEE Asia South Pacific Design Automation Conference, IEEE Press, 2005, pp. 583-587. 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.