2003/09/07 by Eli Appleboim, Appleboim, Eli, Emil Saucan +1
Computer Science · #B.6.3 #FOS: Computer and information sciences #Formal Methods in Verification #Logic, programming, and type systems #Software Reliability and Analysis Research #Symbolic Computation (cs.SC) #cs.SC
paper · pdf · doi:10.48550/arxiv.cs/0309008
13 Pages, 6 figures. Submitted to the IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
arxiv created 2003/09/07 · openalex publication_date 2003/09/07 · arxiv updated 2009/12/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.