Dominant controllability check using QBF-solver and netlist optimizer

Abstract

This paper presents an application of formal methods to the verification of hardware power management modules. The property being verified is called Dominant Controllability and is a property of a netlist node and a subset of the inputs. The property holds if there exists an assignment to the subset of the inputs such that it sets the node to 0/1 regardless of the values at the rest of the inputs. Verification of power management modules in recent CPU and GPU designs includes hundreds of such properties. Two approaches are described for verifying such properties: netlist optmization and QBF solving. In the latter case, a QBF preprocessor is used, requiring partial model reconstruction. Each method can be used independently or combined into a third algorithm that heuristically selects a method based on its performance on a design. Experimental results for these methods are presented and discussed. © 2014 Springer International Publishing Switzerland.