Unified Property Specification for Hardware/Software Co-Verification

Hardware/software co-verification is becoming an indispensable tool for building highly trustworthy embedded systems. A stumbling block to effective co-verification using model checking is the lack of support to unified property specification for hardware, software, and entire embedded systems. In this paper, we develop xPSL, a unified property specification language for co-verification. xPSL extends the IEEE Property Specification Language (PSL) to support specification of temporal assertions over both hardware and software events. The semantics of hardware and software events and their temporal correlations are formalized based on translation of both hardware and software semantics to a common formal semantic basis. xPSL has been applied in co-verification to specify properties of hardware and software components, and furthermore entire embedded systems. Case studies have shown that xPSL is very effective in enabling co-verification of system-level properties and facilitating compositional reasoning.