[LTL] Make ltl.delay clocking explicit (add %clock and <edge> operands)

[Clo91eaf]

reopen #9311

[Clo91eaf]

@fabianschuiki very sorry for delay!

[Clo91eaf]

@fabianschuiki @seldridge could u please take a look?

[fabianschuiki]

Adding an explicit clock operand to delays is a great idea, and the clocked delay op looks good.

You've had to go through a lot of pain in this PR to update every single use of DelayOp to deal with this new clock operand. May I suggest that you instead create a ClockedDelayOp such that we can add support for clocked delays step by step, and figure out how the rest of the code base interacts with them? Since this is a very complicated change, having both ops coexist for a while will help you migrate over step-by-step.

For example, the current lowering to DelayOp in ImportVerilog and FIRRTLToHW are clearly wrong, since they just hook a constant 1 clock up to the op. Since this op is load bearing in Chisel, we have to make sure that when we use the new clocked delay op, its use is actually correct. In FIRRTLToHW for example, we'd want to very carefully infer the clock by looking for FIRRTL clock intrinsics attached to the FIRRTL delay intrinsic. Also, if a single delay intrinsic is used by two different clock intrinsics, we need to lower to two copies of the ClockedDelayOp, one for each clock.

Another example is Verilog emission, where we currently just ignore the clock. One key design point of a ClockedDelayOp is going to be figuring out how we print it as Verilog. The explicit clock makes it possible to infer the @(posedge XYZ) pieces on the fly as we emit Verilog.

[fabianschuiki]

This Verilog emission feels incorrect. The IR says "delay a by 4 cycles of posedge clk", but the Verilog then says "delay a by 4 undefined cycles". I would expect the Verilog output to be:

assert property (@(posedge clk) ##4 a);

I think we need to consider the clocks of the delays when printing the Verilog, and insert @(posedge clk) where it is necessary to indicate the clock trigger.

For example, since the delays now nicely encode the clock, which is fantastic, we can figure out when to print the clock when we emit Verilog:

Same clocks:

%0 = delay(clk, a, 4)
%1 = delay(clk, b, 2)
%2 = concat(%0, %1)
assert(%2)

assert property (@(posedge clk) ##4 a ##2 b);

Different clocks in implication, same clocks in concat:

%0 = delay(clk1, a, 4)
%1 = delay(clk1, b, 2)
%2 = concat(%0, %1)
%3 = delay(clk2, c, 1)
%4 = implication(%3, %2)
assert(%4)

assert property ((@(posedge clk2) ##1 c) |-> (@(posedge clk1) ##4 a ##2 b));

Different clocks in implication and concat:

%0 = delay(clk1, a, 4)
%1 = delay(clk2, b, 2)
%2 = concat(%0, %1)
%3 = delay(clk3, c, 1)
%4 = implication(%3, %2)
assert(%4)

assert property ((@(posedge clk3) ##1 c) |-> (@(posedge clk2) (@(posedge clk1) ##4 a) ##2 b));

This would allow us to infer the clocking statements at Verilog printing, and probably get rid of ltl.clock almost everywhere.

[Clo91eaf]

Thanks for the review. Refactoring the delay op has indeed been a challenging process. After reviewing your feedback, I realized the shortcomings in my previous handling of clock inference. Since I have already completed most of the structural changes to pass the type checks, I will now focus on fixing the logic to ensure the clock signal is correctly inferred from the context, rather than simply using a constant.