[LTL to Core] Add lowering for AssertProperty operations

[dobios]

In order to support the btor2 emission in Chisel, we need to have a good way to encode property assertions, as this should hopefully at some point be the default for formal verification.

This PR is a factored out version of #6649 that introduces a lowering pass for ltl and verif operations that are generated by the use of AssertProperty in Chisel, and encodes them using operations from the core dialects. This would allow for this assertion type to be used for Bounded Model Checking and is a first step for supported more SVA constructs in the formal backend.

[uenoku]

Thank you for working on this! Looks promising! A few highlevel comments:

1. I'm slightly nervous about having two lowering paths for hasBeenReset op in LTLToCore and VerifToSV. It is possible to unify them? I'm not sure the current two implementations are exactly same behavior in verilog though(LTLToCore lowers a reset value to power-on reset whereas LTLToVerif lowers it to initial statement).
2. I think SV doesn't belong to core dialects since SV is one of target dialects. So the name "LTLToCore" might not fit if we create SV always for verif assert? My impression was rather LTL and Verif are close to core dialect. The pass looks like legalization for btor emission so maybe "PrepareForBtor2Emission"? Sorry for bikeshedding but let me know what you think.

[uenoku]

What is this wire for?

[dobios]

Not sure, but it's getting generated somewhere outside of my pipeline

[fabianschuiki]

I would delete the hw.wire lines from the test, since your conversion doesn't explicitly do anything with them, so they don't add anything to the test.

[uenoku]

Why does the pass add a symbol?

[dobios]

Because the current build API doesn't allow me to give the register a powerOn Value without also giving it a symbol...

[fabianschuiki]

The default builder might help. See comment above.

[dobios]

@uenoku

Thank you for working on this! Looks promising! A few highlevel comments:

1. I'm slightly nervous about having two lowering paths for hasBeenReset op in LTLToCore and VerifToSV. It is possible to unify them? I'm not sure the current two implementations are exactly same behavior in verilog though(LTLToCore lowers a reset value to power-on reset whereas LTLToVerif lowers it to initial statement).

My lowering currently does something similar to the VerifToSV specifically for the HasBeenReset. However, VerifToSV lowers this to sv operations that map neatly to SVA constructs when possible, which is not the case in my lowering which is explicitly avoiding any SVA so that it can be used in any simulator as well as in the formal backend. So I don't think that unifying the two lowerings right now is a useful thing to do, as it would require removing the hasbeenreset lowering from both passes and have it in its own pass that just lowers hasbeenreset (which seems silly to me).

2. I think SV doesn't belong to core dialects since SV is one of target dialects. So the name "LTLToCore" might not fit if we create SV always for verif assert? My impression was rather LTL and Verif are close to core dialect. The pass looks like legalization for btor emission so maybe "PrepareForBtor2Emission"?  Sorry for bikeshedding but let me know what you think.

The reason why I'm using sv.alwaysand sv.assert is that that is currently what is generated when lowering FIRRTL to HW or the Core dialects. Given that those are the only SV operations I generate, I don't think that calling it LTLToSV is a good idea, as this is meant to lower LTL to a state where it can be picked up by the formal backend and not necessarily one that is especially useful for SV. Also I don't want to call it prepare for btro2 as it has use outside of btor2, it makes LTL constructs usable in simulators that don't support property assertions or assertion disabling. The goal is also to extend this pass to lower some basic SVA properties using it.

[fabianschuiki]

Really cool to see this conversion!

The fact that you had to use SV ops here suggests that we're missing something in the core dialects (probably Verif). The stuff in here is probably fine to land as is, but it would be good to have a GitHub issue or a follow-up PR add the missing core ops and get rid of the SV ops here again.

[fabianschuiki]

You might be able to use the default builder instead, which accepts a parameter for every operand and attribute:

  // SeqOps.td: CompRegOp
  let arguments = (ins
    AnyType:$input,
    ClockType:$clk,
    OptionalAttr<StrAttr>:$name,
    Optional<I1>:$reset,
    Optional<AnyType>:$resetValue,
    Optional<AnyType>:$powerOnValue,
    OptionalAttr<InnerSymAttr>:$inner_sym
  );

Something like the following could work:

Suggested change

	// Finally generate the register to set the backedge
	reg.setValue(rewriter.create<seq::CompRegOp>(
	op.getLoc(), orReset,
	rewriter.createOrFold<seq::ToClockOp>(op.getLoc(), adaptor.getClock()),
	reset, resetval, llvm::StringRef("hbr"), constZero));
	// Finally generate the register to set the backedge
	reg.setValue(rewriter.create<seq::CompRegOp>(
	op.getLoc(),
	orReset,
	rewriter.createOrFold<seq::ToClockOp>(op.getLoc(), adaptor.getClock()),
	StringAttr{}, // name (could also be rewriter.getStringAttr("hbr"))
	reset,
	resetval,
	constZero,
	InnerSymAttr{} // inner_sym
	));

[fabianschuiki]

The default builder might help. See comment above.

[fabianschuiki]

I would delete the hw.wire lines from the test, since your conversion doesn't explicitly do anything with them, so they don't add anything to the test.

[dobios]

Thanks for the reviews ! Hopefully we can find a good solution for #6982 that solves this unwanted reliance on sv.assert instead of verif.assert in a future PR.

[uenoku]

Sorry for late review and it looks good to me, thank you for pushing on this!