Executing the formal semantics of the Accellera Property Specification Language by mechanised theorem proving

The Accellera Property Specification Language (PSL) is designed for the formal specification of hardware. The Reference Manual contains a formal semantics, which we previously encoded in a machine readable version of higher order logic. In this paper, we describe how to `execute' the formal semantics using proof scripts coded in the HOL theorem prover's metalanguage ML. The goal is to see if it is feasible to implement useful tools that work directly from the official semantics by mechanised proof. Such tools will have a high assurance of conforming to the standard. We have implemented two experimental tools: an interpreter that evaluates whether a finite trace w (which may be generated by a simulator) satisfies a PSL formula f, and a compiler that converts PSL formulas to checkers in an intermediate format suitable for translation to HDL for inclusion in simulation testbenches. Although our tools use logical deduction and are thus slower than hand-crafted implementations, they may be speedy enough for some applications. They can also provide a reference for more efficient implementations.