Formal verification of module interfaces against real time specifications

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 Ether net) 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). Designers attempt to model these behaviors through an appropriate test bench for the module. In this paper we present a module verifier tool based on a proposed real time temporal logic called Open-RTCTL, which allows combined specification of the correctness properties and the input environments. The tool accepts the design in a subset of Verilog. By making the designer specify the environment constraints, we are able to verify a module in isolation, and thereby avoid the state explosion problem due to composition of modules. We present experimental results on modules from the Texas-97 Benchmark circuits to demonstrate the space/time efficiency of the tool.