Predicting Formal Verification Resource Needs (Computation Time and Memory) through Machine Learning

Abstract

This paper presents an application of Machine Learning (ML) for estimating the resource requirements (time and memory) for formal verification of digital systems. Formal Verification has become the main bottleneck in the digital design process. As designs grow in size, the verification cost exponentially increases. Some verification efforts fail when the cost of the verification is too large. The most common failures are due to state explosion problem when memory runs out or when verification does not meet time constraints and cannot complete within the given time. For this reason, having an estimation of the computation resources beforehand can be valuable. In this work, a neural network is used to predict the formal verification cost for a diverse collection of designs. Experiments with a large variety of Verilog benchmarks have been conducted. In each experiment, the specific features of a given design are extracted, the design is synthesized and formally verified, and the verification time and memory usage are recorded. The neural network then uses this data to learn the correlation between design features and verification cost. A genetic algorithm experimented with different neural network designs to determine an appropriate framework. The experimental results confirm that the developed neural network can predict the resource requirements and memory usage with reasonable accuracy.