非表示:
キーワード:
-
要旨:
We present a new approach to hardware verification based on describing
circuits in Monadic Second-order Logic (MSL). We show how to use
this logic to represent generic designs like $n$-bit adders, which are
parameterized in space, and sequential circuits, where time is an
unbounded parameter. MSL admits a decision procedure, implemented in
the MONA tool, which reduces formulas to canonical automata.
The decision problem for MSL is non-elementary decidable and
thus unlikely to be usable in practice. However, we have used
MONA to automatically verify, or find errors in, a number of
circuits studied in the literature. Previously published machine
proofs of the same circuits are based on deduction and may involve
substantial interaction with the user. Moreover, our approach is
orders of magnitude faster for the examples considered. We show why
the underlying computations are feasible and how our use of
MONA generalizes standard BDD-based hardware reasoning.
