Deterministic dynamic monitors for linear-time assertions

Abstract

We describe a framework for dynamic verification of temporal assertions based on assertion compilation into deterministic automata. The novelty of our approach is that it allows efficient dynamic verification of general linear temporal formulas written in formal property specification languages such as LTL, ForSpec, PSL, and SVA, while the existing approaches are applicable to limited subsets only. We also show an advantage of the described framework over industrial simulators, which typically use transaction-based verification. Another advantage of our approach is its ability to use deterministic checkers directly for hardware emulation. Finally, we compare the deterministic compilation with the OBDD-based on-the-fly simulation of deterministic automata. We show that although the OBDD-based simulation method is much slower, the two methods may be efficiently combined for hybrid simulation, when the RTL signals in assertions are mixed with symbolic variables. © 2006 Springer-Verlag Berlin/Heidelberg.