Verification of Sequential Circuits by Tests-As-Proofs Paradigm

TL;DR

This paper presents an incomplete, scalable algorithm for bug detection in sequential circuits using the Tests-As-Proofs paradigm, which constructs counterexamples from proof-based state sequences to improve bug detection probability.

Contribution

It introduces a novel TAP-based algorithm for bug detection in sequential circuits, enhancing effectiveness of incomplete methods through proof-guided test generation.

Findings

Algorithm demonstrates preliminary effectiveness in bug detection

Counterexamples are constructed from proof-derived state sequences

Scales better than complete verification methods

Abstract

We introduce an algorithm for detection of bugs in sequential circuits. This algorithm is incomplete i.e. its failure to find a bug breaking a property P does not imply that P holds. The appeal of incomplete algorithms is that they scale better than their complete counterparts. However, to make an incomplete algorithm effective one needs to guarantee that the probability of finding a bug is reasonably high. We try to achieve such effectiveness by employing the Test-As-Proofs (TAP) paradigm. In our TAP based approach, a counterexample is built as a sequence of states extracted from proofs that some local variations of property P hold. This increases the probability that a) a representative set of states is examined and that b) the considered states are relevant to property P. We describe an algorithm of test generation based on the TAP paradigm and give preliminary experimental results.