Probabilistic Analysis for Sequential Circuits Verification Using Markov Chains

Random testing is used extensively in functional verification of hardware systems. In practice, testing stops when a certain coverage criterion is achieved. However, testing has the inherent problem of being only able to expose bugs, not prove their absence. Thus, proving whether a potential bug exists or not under current verification efforts would be helpful to measure the completeness of testing. This brief proposes a probabilistic coverage analysis method to quantify the probability of bug existence for sequential circuit verification under random testing. The proposed method consists of an effective formula for computing the probability of a bug (assuming it exists) being detected in a sequential circuit. The formula is time complexity cubic to the number of coverage bins and linear to the number of test cycles. To validate the proposed method, it was implemented in MATLAB to calculate the probability of a bug being detected. Experimental results on 20,116 random instances indicate that, using Monte Carlo simulation, the proposed analysis method has an average absolute relative error of approximately 0.027%, comparing to 7.38% in existing work.