2007 | OriginalPaper | Chapter
Underapproximation for Model-Checking Based on Random Cryptographic Constructions
Authors : Arie Matsliah, Ofer Strichman
Published in: Computer Aided Verification
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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 (we prove that
k
is very close to
m
with an arbitrarily high probability). 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 report initial experimental results with bounded model checking of industrial designs (the method is equally applicable to unbounded model checking and to simulation), which shows mixed results. An interesting observation, however, is that in 13 out of 17 designs, setting
m
to be
n
/5 is sufficient to detect the bug. This is in contrast to other underapproximation that are based on reducing the number of inputs, which in most cases cannot detect the bug even with
m
=
n
/2.