Open computation tree logic with fairness

Abstract

One of the main concerns of the designer of a circuit module is to guarantee that the interface of the module conforms to specific protocols (such as PCI Bus, AMBA bus or Ethernet) by which it interacts with its environment. The computational complexity of verifying such open systems under all possible environments has been shown to be very hard (EXPTIME complete). On the other hand, designers are typically required to guarantee correct behavior only for specific valid behaviors of the environment (such as a valid PCI Bus environment). Open Computation Tree Logic (Open-CTL) provides the designer the ability to model the environment constraints and the correctness property in a unified way, and has been shown to be useful for checking protocol compliance of modules. In this paper, we introduce the notion of fairness constraints on the environment. We show that the use of fairness constraints allows us to model the designer's intent in a meaningful way that conforms with the protocol being checked. We present a symbolic model checking algorithm for verifying Open-CTL properties under given fairness constraints.