Predicting Formal Verification Resource Needs (Computation Time and Memory) through Machine Learning
Keywords:Formal Verification, Resource Requirements, Machine Learning, Computation Time, Memory, Estimation
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.
References or Bibliography
A. G. W. Eman M. Elmandouh, "Estimation of Formal Verification Cost Using Regressing Machine Learning," in IEEE International High Level Design Validation and Test Workshop (HLDVT), Santa Cruz, CA, 2016.
A. G. W. Eman M. Elmandouh, "Guiding Formal Verification Orchestration Using Machine Learning Methods," in ACM Transactions on Design Automation of Electronic Systems (TODAES), Volume 23 Issue 5, 2018.
M. T. M. M. D. R. D. J. G. a. D. E. S. C Richard Ho, "Early formal verification of conditional coverage points to indentify intrinsically hard-to-verify logic," in 45th Annual Design Automation Conference, 2008.
G. F. M. a. P. M. T. a. S. U. Hegde, "Designing Neural Networks using Genetic Algorithms," in International Conference on Genetic Algorithms, 1989.
"Synopsys Design Compiler: RTL Synthesis," in https://www.synopsys.com/support/training/rtl-synthesis/design-compiler-rtl-synthesis.html.
"Synopsys Formality," in https://www.synopsys.com/implementation-and-signoff/signoff/formality.html.
"Tensorflow: An Open Source Machine Learning Framework for Everyone," in https://www.tensorflow.org/.
"TFLearn: Deep learning library featuring a higher-level API for TensorFlow," in http://tflearn.org/.
T. Parr, "The Definitive ANTLR 4 Reference", Pragmatic Bookshelf, 2013.
D. K. D. a. R. Sanyal, "Semi-automatic generation of UML models from natural language requirements," in ISEC '11: Proceedings of the 4th India Software Engineering Conference, February 2011 .
B. T. a. R. K. Hammond Pearce, "DAVE: Deriving Automatically Verilog from English," in MLCAD '20: Proceedings of the 2020 ACM/IEEE Workshop on Machine Learning for CAD, November 2020.
C. B. H. a. I. G. Harris, "GLAsT: Learning formal grammars to translate natural language specifications into hardware assertions," in Design, Automation & Test in Europe Conference & Exhibition (DATE), 2016.
How to Cite
Copyright (c) 2022 Jason Twigg, Erik Torkelson; Nazanin Mansouri
This work is licensed under a Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International License.
Copyright holder(s) granted JSR a perpetual, non-exclusive license to distriute & display this article.