Paper: A Semantically-Derived Subset Of English For Hardware Verification

ACL ID P99-1058
Title A Semantically-Derived Subset Of English For Hardware Verification
Venue Annual Meeting of the Association of Computational Linguistics
Session Main Conference
Year 1999
Authors

To verify hardware designs by model checking, circuit specifications are commonly expressed in the temporal logic CTL. Automatic conversion of English to CTL requires the definition of an appropriately restricted subset of English. We show how the limited semantic expressibility of CTL can be exploited to derive a hierarchy of subsets. Our strategy avoids potential difficulties with approaches that take existing computational semantic analyses of English as their starting point--such as the need to ensure that all sentences in the subset possess a CTL translation. 1 Specifications in Natural Language Mechanised formal specification and verification tools can significantly aid system design in both software and hardware (Clarke and Wing, 1996). One well-established approach to verification,...