RFC: SVA / PSL implementation ideas

Developers
1

Hey there,

I find myself with some motivation to implement support for synthesis of temporal logics (e.g. SVA/PSL), at the beginning focusing on FV uses.

The algorithm I have selected after some research is the one proposed in [1]. It would allow simple addition of more operators later and provide a basis to expand from. Furthermore, it allows to push most of the hard verification algorithms (construction of automata) into the model checker.

My proposed structure for this implementation is:

  • dedicated $temporal cell to store the formula
    • formula stored as cell parameter in appropriate format (polish notation string of AST)
    • → simple implementation/generation of temporal logic for frontends
  • passes to prepare $temporal cells
    • transformations of formulas (e.g. LTL’s NNF)
    • marking of formulas for assert or assume as some algorithms might like to handle these internally, attaching assert/assume cells to the appropriate structures
    • → reusability of code
  • a single pass to perform the desired construction (temporal logic → circuit/transition system)
    • easy expandability by simple addition of an algorithm as a new pass
    • configurability
    • different algorithms for different uses (e.g. alg A for FV, alg B for quick and dirty control circuit generation, …)

What are your thoughts on this structure?

The implementation of the selected algorithm I am very confident to be able to. However, I have not yet worked extensively with the yosys codebase (a small temporary tweak here and there to get something working, until I found a better way) and am still how to get a new cell into yosys (but i’m sure that it cannot possibly be that hard…).

The commit structure I have in mind would involve one PR for the $temporal cell, some preparation passes and the algorithm in [1] for basic LTL. A later PR’s would than add PLTL- and SERE-support to this algorithm respectively.

Any input/thoughts/pointers are greatly appreciated.

General overview LTL (I cannot give the exact equivalence for SVA/PSL operators):

  • basic boolean operation
    • and
    • or
    • not
    • implication (a -> b = !a | b)
    • equivalence
  • temporal operators
    • X (next; X a holds iff a holds in the next cycle)
    • G (global; G a holds iff a holds this and all following cycles)
    • F (future; F a holds iff a holds now or some time in the future)
    • U (until; a U b holds iff a holds up until the cycle b holds and F a holds)
    • some other versions of these which I will not get into detail

PLTL being LTL with additional temporal operators, which look into the past.

SERE covers the parts of SVA/PSL not covered by PLTL.

[1] Claessen, Koen, Niklas Een, and Baruch Sterin. “A circuit approach to LTL model checking.” 2013 Formal Methods in Computer-Aided Design. IEEE, 2013.

2

Thanks a lot for sharing your thoughts and ideas on the implementation of temporal logic synthesis! (And sorry for the late reply!)
We (the YosysHQ team) are actually currently working on a project with the goal to design/implement a new intermediate representation for SVA properties (“Property IR”) and replace Yosys’s current SVA implementation (which is Tabby CAD / Verific only), with implementing the translation from LTL/SERE to circuits being a part of that.

Our plan very much coincides with the structure you proposed, with a new $property cell to store SVA properties in a textual form with a syntax based on s-expressions. Different from the paper you shared, we want to use an automaton representation as an intermediate step before translating to circuits.

I am currently working on the specification of Property IR and on a prototype. We plan to finish the (preliminary) specification of Property IR by April 2026, and implement the new flow by the end of 2026. (Although it is not yet entirely clear what features of SVA we will be able to support by then.)

We intend to share more information on the new Property IR soon.

3

Additionally, this is done as part of the OSVISE project, and we’ll be integrating it with MLIR

4

Nice to hear, that my thoughts and ideas are not that far from those of someone familiar with the codebase.

As you are already working on this, I will postpone my research and maybe contribute the described pass at a later date. I can also think of prototyping usecases for another algorithm I came across, which I might implement once the Property IR is tied down.