Auxiliary state machines + context-triggered properties in verification

Banerjee, Ansuman ; Dasgupta, Pallab ; Chakrabarti, P. P. (2008) Auxiliary state machines + context-triggered properties in verification ACM Transactions on Design Automation of Electronic Systems, 13 (4). pp. 1-31. ISSN 1084-4309

Full text not available from this repository.

Official URL: http://doi.org/10.1145/1391962.1391970

Related URL: http://dx.doi.org/10.1145/1391962.1391970

Abstract

Formal specifications of interface protocols between a design-under-test and its environment mostly consist of two types of correctness requirements, namely (a) a set of invariants that applies throughout the protocol execution and (b) a set of context-triggered properties that applies only when the protocol state belongs to a specific set of contexts. To model such requirements, an increasingly popular design choice in the assertion IP design community has been the use of abstract context state machines and state-oriented properties. In this paper, we formalize this modeling style and present algorithms for verifying such specifications. Specifically, we present a purely formal approach and a semi-formal approach for verifying such specifications. We demonstrate the use of this design style in modeling some of the industry standard protocol descriptions and present encouraging results.

Item Type:Article
Source:Copyright of this article belongs to Association for Computing Machinery
ID Code:129701
Deposited On:18 Nov 2022 09:40
Last Modified:18 Nov 2022 09:40

Repository Staff Only: item control page