Property Checking By Logic Relaxation

TL;DR

This paper presents a novel property checking framework for sequential circuits using Logic Relaxation, which simplifies the transition system to efficiently identify safety violations by analyzing relaxed models.

Contribution

It introduces a new Logic Relaxation method for property checking that reduces complexity by focusing on relaxed systems close to the original, enabling more efficient verification.

Findings

The LoR method effectively identifies unsafe states in relaxed systems.

Relaxed models can simplify property verification by focusing on approximate reachable states.

The approach can significantly reduce verification complexity compared to traditional methods.

Abstract

We introduce a new framework for Property Checking (PC) of sequential circuits. It is based on a method called Lo-gic Relaxation (LoR). Given a safety property, the LoR method relaxes the transition system at hand, which leads to expanding the set of reachable states. For j-th time frame, the LoR method computes a superset A_j of the set of bad states reachable in j transitions only by the relaxed system. Set A_j is constructed by a technique called partial quantifier elimination. If A_j does not contain a bad state and this state is reachable in j transitions in the relaxed system, it is also reachable in the original system. Hence the property in question does not hold. The appeal of PC by LoR is as follows. An inductive invariant (or a counterexample) generated by LoR is a result of computing the states reachable only in the relaxed system. So, the complexity of PC can be drastically reduced by finding a "faulty" relaxation that is close to the original system. This is analogous to equivalence checking whose complexity strongly depends on how similar the designs to be compared are.