On-line assertion-based verification with proven correct monitors

In the context of embedded systems design, the authors developed an original method for generating hardware that monitors signals whose behavior is specified by logical and temporal properties written in PSL. The method is based on a library of primitive digital components, and a technique to interconnect them, both formally proven correct with respect to the mathematical semantics of PSL. The resulting digital module can be properly connected to the signals of the design under scrutiny. Monitoring runs concurrently with the observed signals, and notifies its environment whether the property checking is terminated or is still pending. A prototype implementation on a FPGA platform provides enough execution efficiency to allow the verification of a system on a chip running its own software. In this method, on-line monitoring imposes a circuit overhead that increases gracefully with the number of nested PSL operators, and the upper bound of the temporal observation window after property triggering.