Property IR is a new intermediate representation for temporal properties as specified by SystemVerilog Assertions (SVA). The goal is to support formal verification flows, while decoupling front-end tasks (parsing, name resolution, etc.) from checker circuit synthesis and optimization. This is achieved by providing a unified representation for assertions, automata, and circuits, allowing us to lift several limitations of the current SVA implementation (which is Tabby CAD / Verific only). We plan to reach feature parity throughout 2026.
This effort is part of the OSVISE project, and it will be integrated with MLIR/CIRCT. The OSVISE project is funded by the German Federal Ministry of Research, Technology and Space (BMFTR) and is led by the AEMY Lab at Hochschule München. Property IR is specifically intended as a suitable target for third-party frontends, and we’re interested in coordinating with interested parties.
The first version of the Property IR specification is available here.
Comments and questions are welcome!