Capturing assertions from natural language descriptions

We present a technique to automatically generate formal, executable assertions from natural language assertion descriptions written in English. Assertions are program invariants which are commonly used for result checking in the hardware verification process. We present an attribute grammar which captures the semantics of a subset of English language assertion descriptions. Using the attribute grammar, we parse assertion descriptions and generate semantically equivalent formal models. We have evaluated our technique using a large set of industrial assertion descriptions. We present the successful assertion generation results, as well as the limitations of our approach and methods to address those limitations in the future.