UC Irvine

Verification of modern digital systems can consume up to 70% of the design cycle. Verification engineers must create formal properties which reflect correct operation from design specifications or other documents. This process of creating formal correctness properties from textual descriptions is a laborious task which is difficult to automate.

In this work I investigate the creation of formal verification properties from textual descriptions written in natural language. I present two approaches that utilize natural language processing (NLP) and machine learning techniques for the automatic generation of verification properties. In the first approach a set of correctness properties expressed in natural language, called natural language assertions (NLAs), is divided into subsets of structurally similar sentences. A generalized formal property template for each subset is used to provide a mapping from each sentence to a well specified verification property. Experimental results show that this methodology reduces the number of formal properties which must be manually created by up to an order of magnitude.

In the second approach I create a custom attributed formal grammar which captures the English semantics of a temporal tree logic. A translation system is implemented which uses this attribute grammar to perform a semantic parsing of NLAs. Attributes for each grammatical production in the parse tree are then used to build a fully specified formal property for each NLA. Experimental results show that valid formal properties are generated from English NLAs in over 90% of test cases.

In evaluating the translation system it was observed that translation rates for NLAs are strongly dependent on the quality of the formal grammar used. High translation rates require a finely tuned custom grammar. To facilitate the creation of such a grammar I propose a new learning algorithm which automatically generates custom attribute grammars from a small set of NLAs and formal properties. This machine generated grammar is used in the NLA translation system to create formal properties from NLAs taken from two design documents for designs in the same product family. Experimental results show that the learned attribute grammar is of sufficient quality to successfully translate up to 88% of NLAs.