Mike Gordon (Cambridge)
ABSTRACT Experiments to `execute' the formal semantics of the Accellera Property Specification Language (PSL) will be described. 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 an interpreter that evaluates whether a finite trace w (which may be generated by a simulator) satisfies a PSL formula f, i.e. computes the truth of "w |= f". Inspired by the IBM FoCs tool, we are in the process of implementing a compiler that applies the semantics to PSL properties to create checkers than can be added to simulation models. Although our tools are slow compared with hand coded implementations, they are not ludicrously slow and we believe that they might be capable of being made fast enough for some applications. They are also novel prototypes and can provide a reference for more efficient implementations. This is joint work with Joe Hurd and Konrad Slind