A Digital Version of Green's Theorem for Formal Verification

Title: A Digital Version of Green's Theorem for Formal Verification

Research Question: How can we quantify the interaction between a block and its environment in formal verification to improve coverage and reduce redundancy?

Methodology: The researchers propose a novel scheme to the coverage problem by setting a discrete version of Green's Theorem, specifically adapted for Model Checking-based verification. This method is best suited for the coverage problem as it allows for the quantification of incompleteness or redundancy of a set of rules describing the model under verification. It can be done continuously throughout the verification process, enabling the user to identify stages with incompleteness or redundancy.

Results: The researchers present a local example on a small hardware model to demonstrate their method. They also show its possibility for large-scale systems, comparing it to other methods by applying it to the same test cases.

Implications: This method provides a quantitative way to estimate the interaction between a block and its environment, improving the coverage problem in formal verification. It enables verifiers to easily quantify the correctness of neighboring units, making it a valuable tool in industrial implementation of verification methods. The method's ability to be extended globally to large-scale units makes it even more beneficial, as it allows for a unified development process from architect to designer to verifier.

Link to Article: https://arxiv.org/abs/0309008v1 Authors: arXiv ID: 0309008v1