This demo implements the timed past eventuality operator example in Table 2 on page 7 in "Online Monitoring of Metric Temporal Logic using Sequential Networks" by Doğan Ulus.

To see how the example is implemented, you can look at the code in tb.sv, TimedPastEventualityFormula.sv, and DisjunctionFormula.sv.

• Icarus Verilog

To run:

  ./run.sh

and compare to the result in Table 3 on page 7.