[AIGERImporter] Add lowering for justice and fairness properties

[okekayode]

Currently the AIGER parser handles bad state and invariant constraints by lowering to both verif.assert and verif.assume respectively, but justice and fairness properties are currently not supported.

Lowering Idea

As per https://fmv.jku.at/papers/BiereHeljankoWieringa-FMV-TR-11-2.pdf we can see that a fairness constraint is semantically something that is described to happen as "infinitely often f" (GF f).
Noted in the LTL dialect docs https://circt.llvm.org/docs/Dialects/LTL/ , always is described conceptually but unfortunately there is no ltl.always operation, only ltl.eventually is implemented thus allowing that G can be represented as $\neg F \neg $:

// global fairness is shared across all justice properties
%ff_f = ltl.eventually %f_lit
%gf_f = ltl.not(ltl.eventually(ltl.not(%ff_f))) 

Moreover a justice property is just a conjunction of fairness constraints:

// local fairness properties for ith justice property
%ff_j = ltl.eventually %j_lit
%gf_j = ltl.not(ltl.eventually(ltl.not(%ff_j))) 

%justice = ltl.and %gf_f %gf_j
verif.assert %justice

I am open and would love to hear any alternative approaches as I feel this lowering idea I have is quite verbose and may cause issues (dependent on backends). I am sure the lowering semantically makes sense according to the spec provided above, but surely there is a cleaner way to express liveness.

[uenoku]

The proposed lowering makes sense, and I think the verbosity aligns well with the LTL dialect's design. However, I’m not an expert on LTL, so I’d appreciate some feedback from @dobios

[dobios]

@okekayode Your comment makes sense and shows a potential mistake we made when designing the IR.

The reason there is no ltl.always is that, as with SVA if my understanding is correct, it is the default interpretation of any ltl op. So your implementation, while correct, is not explicitly necessary and I would like to avoid something that verbose in the lowerings as it would just end up making the outputs harder to analyse (and ltl is already hard enough to work with as is). I am open to revisiting the design of ltl in general and this is something I'm sure @fabianschuiki (who first introduced the dialect) agrees with? Not sure if this answers your question (I'm sure you meant to say fairness at the end and not liveness, as liveness is expressed with ltl.eventually).

[okekayode]

Cheers @dobios! Indeed i did mean fairness instead of liveness at the end there (oops). Since you mentioned being open to revisiting the design of ltl out of curiosity what do you think that would look like in the context of the lowerings and also in general? Moreover, reading the dialect docs a bit more I do see yes that ltl main goal is to "capture the core formalism underpinning SystemVerilog Assertions", so i even wonder if ltl is even the right place for AIGER fairness/justice at all now.

[dobios]

@okekayode I think that the main thing I would want to do when redesigning this is to decouple it entirely from SVA and have it actually encode LTL. This would mean that we could have a separate SVA dialect that acts as an AST for property assertions directly, but I don't think that should be part of the "core specification representation" that the ltl dialect is currently handling. In practice we'd move the ops like ltl.<x>_repeat, ltl.concat, ltl.sequence, and ltl.delay to a separate sva dialect, and instead explicitly encode things like ltl.next, ltl.always, ltl.weak_until, ltl.weak_release, and ltl.strong_release. Then we could have conversions to and from ltl and sva. The benefit of this is that it would make it easy to properly convert these operations to automata for model checking and such. That would be my idea for a proper ltl redesign.

I think that a proper LTL dialect is a missing abstraction level in our pipelines.

We could then have more experimental designs that encode büchi automata and stuff live in other dialects rather than trying to fit everything to ltl (which is the current approach).