Dominant Controllability Check Using QBF-Solver and Netlist Optimizer

ABSTRACT. This paper presents an application of formal methods to the verification of power management modules in hardware designs. This paper identifies a distinct property of power management module and names it Dominant Controllability. This 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 of the rest of the inputs. Verification of power management modules in recent CPU and GPU designs includes hundreds of such properties. Dominant Controllability is different than controllability or random controllability which require only that the node is set to 0/1 by an assignment or random assignment to the inputs. The new application verifies Dominant Controllability using two formal methods: QBF-solver and netlist optimizer. Each method can be use independently or combined by a third algorithm that heuristically selects a method based on their performance in a specific design. The experimental results show that using QBF-solver is significantly faster when Dominant Controllability fails to hold (there is a bug in the design). Dominant Controllability fails when no assignment sets the node to 0/1, or when each such assignment is not dominant over other assignments to the rest of the inputs. In this case QBF-solver is faster because it concludes if Dominant Controllability fails without enumerating the large number of assignments. If the QBF-solver concludes that Dominant Controllability holds, netlist optimizer is used to verify the result, with a linear cost. Our experimental results show that even though using the netlist optimizer is incomplete, it is often successful when the power management module is very simple. The results also show that the third algorithm named Alternating selects the faster method successfully.