Underapproximation for model-checking based on universal circuits

For two naturals m, n such that m < n, we show how to construct a circuit C with m inputs and n outputs, that has the following property: for some 0 ≤ k ≤ m, the circuit defines a k-universal function. This means, informally, that for every subset K of k outputs, every possible valuation of the variables in K is reachable. Now consider a circuit M with n inputs that we wish to model-check. Connecting the inputs of M to the outputs of C gives us a new circuit M with m inputs, that its original inputs have freedom defined by k. This is a very attractive feature for underapproximation in model-checking: on one hand the combined circuit has a smaller number of inputs, and on the other hand it is expected to find an error state fast if there is one. We show a random construction of a k-universal circuit that guarantees that k is very close to m, with an arbitrarily high probability. We also present a deterministic construction of such a circuit, but here the value of k is smaller ...

• Type: Journal
• Year: 2010
• Where: IANDC
• Authors: Arie Matsliah, Ofer Strichman
• Keywords: IANDC 2010, K-universal Function, Original Inputs, Possible Valuation