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). No pp. given. ISSN 1084-4309

Full text not available from this repository.

Related URL:


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:101411
Deposited On:09 Mar 2018 10:20
Last Modified:09 Mar 2018 10:20

Repository Staff Only: item control page