Digital Version of Green`s Theorem and its Application to The Coverage Problem in Formal Verification

TL;DR

This paper introduces a discrete Green's theorem-based method for quantifying coverage in model checking of integrated circuits, allowing continuous assessment of rule completeness and redundancy during verification.

Contribution

It develops a novel quantitative approach for coverage analysis using a discrete Green's theorem tailored for formal verification, applicable to large-scale systems.

Findings

Enables continuous coverage estimation during verification

Provides precise quantification of rule redundancy and incompleteness

Demonstrates effectiveness on both small and large hardware examples

Abstract

We present a novel scheme to the coverage problem, introducing a quantitative way to estimate the interaction between a block and its enviroment.This is achieved by setting a discrete version of Green`s theorem, specially adapted for Model Checking based verification of integrated circuits.This method is best suited for the coverage problem since it enables one to quantify the incompleteness or, on the other hand, the redundancy of a set of rules, describing the model under verification.Moreover this can be done continuously throughout the verification process, thus enabling the user to pinpoint the stages at which incompleteness/redundancy occurs. Although the method is presented locally on a small hardware example, we additionally show its possibility to provide precise coverage estimation also for large scale systems. We compare this method to others by checking it on the same test-cases.