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!
This is exciting to see! The typed s-expression approach with distinct types for booleans, sequences, and temporal properties is a much cleaner foundation than the current flattening to AIGER.
I recently contributed the itp engine to sby (interpolation-based model checking, PR #353) and one thing I’ve been thinking about is how Property IR could eventually benefit engines like this. Right now the engine only sees a bad output literal and all property structure is already gone by the time AIGER reaches the checker. Keeping that structure alive longer in the pipeline through the $property cell is interesting, especially for how A/B partitioning could be done more intelligently in the future.
A couple of questions as this develops:
For recursive properties like always_a: what does the synthesized checker circuit look like, and will sby engines eventually see something richer than a bad output?
Is there a planned pattern for how engines report back per-assertion results tied to specific Property IR declarations?
I think the transparency goal here resonates and proof producing approaches like interpolation work best when the full pipeline is open and inspectable. Looking forward to following this!
Regarding your first question, there is no one definite answer as to how exactly the resulting checker circuit will look like, because we want so support several modes (like weak/strong satisfaction) that will lead to different results. We are still working on the intermediate steps and automata representations that come before the circuit translation, so at the current stage it is difficult to answer.
At the moment we have no concrete plans for changing what the model checker sees, but the new IR certainly lays the foundation for this. There is no reason you couldn’t add metadata to aiger/btor in SBY’s backend-specific prep script, for example to distinguish between property-internal signals and design signals, assuming that suitable Property IR and/or backend passes for Yosys are written.
We will use the existing infrastructure for reporting results, and there will be no changes to it by introducing Property IR. Does your question refer to more specific information than the current reporting of pass/fail statuses of properties and counterexample traces? It would certainly be interesting to have more detailed information, for example for subproperties, but we have no specific plans for that.
Our primary goal at the moment is to reach a state where Property IR can serve as a replacement for the current SVA flow without changing the overall usage and surrounding infrastructure, but doing so in clean way that makes it easier to extend and maintain.
We are planning to have a working implementation of Property IR in Yosys by the end of 2026. (That does not mean that all SVA features that can be expressed in Property IR will necessarily be supported by then, but we want to support at least everything that is supported now.)
Thanks for the detailed response. The metadata suggestion for aiger/btor is interesting and something I’ll explore in the context of the itp engine. Looking forward to seeing Property IR develop.