@inProceedings{becker-et-al-iccd-2008,
author = "Bernd Becker
and Marc Herbstritt
and Natalia Kalinnik
and Matthew Lewis
and Juri Lichtner
and Tobias Nopper
and Ralf Wimmer",
title = "Propositional Approximations for Bounded
Model Checking of Partial Circuit Designs",
booktitle = "Proceedings of the 26\textsuperscript{th} IEEE International Conference
on Computer Design",
address = "Resort at Squaw Creek, Lake Tahoe, CA, USA",
month = oct,
year = "2008",
publisher = "IEEE Computer Society Press",
isbn = "978-1-4244-2658-4",
pages = "52--59",
abstract = "Bounded model checking of partial circuit designs enables
the detection of errors even when the implementation of the
design is not finished. The behavior of the missing parts
can be modeled by a conservative extension of propositional
logic, called 01X-logic. Then the transitions of the
underlying (incomplete) sequential circuit under verification
have to be represented adequately. In this work, we investigate
the difference between a relation-oriented and a function-oriented
approach for this issue. Experimental results on a large
set of examples show that the function-oriented representation
is most often superior w.\,r.\,t. (1) CPU runtime and (2)
accuracy regarding the ability to find a counterexample, such that
by using the function-oriented approach an increase of
accuracy up to 210\% and a speed-up of the CPU runtime up to
390\% compared to the relation-oriented approach are achieved. But
there are also relevant examples, e.\,g. a VLIW-ALU, for which the
relation-oriented approach outperforms the function-oriented one
by 300\% in terms of CPU-time,
showing that both approaches are efficient for different scenarios.",
}