[LTL] Make PastOp clock operand mandatory

Author: TaoBi22

include/circt/Dialect/FIRRTL/FIRRTLExpressions.td

@@ -1823,9 +1823,9 @@ def LTLEventuallyIntrinsicOp : UnaryLTLIntrinsicOp<"eventually">;
 def LTLPastIntrinsicOp : LTLIntrinsicOp<"past"> {
   let arguments = (ins NonConstUInt1Type:$input,
                        I64Attr:$delay,
-                       Optional<ClockType>:$clock);
+                       ClockType:$clock);
   let assemblyFormat = [{
-    $input `,` $delay (`,` $clock^)? attr-dict `:`
+    $input `,` $delay `,` $clock attr-dict `:`
     functional-type(operands, results)
   }];
 }

include/circt/Dialect/LTL/LTLOps.td

@@ -111,16 +111,16 @@ def PastOp : LTLOp<"past", [TypesMatchWith<"input and result types must match",
   let arguments = (ins
     HWIntegerType:$input,
     I64Attr:$delay,
-    Optional<I1>:$clk);
+    I1:$clk);
   let results = (outs HWIntegerType:$result);
   let assemblyFormat = [{
-    $input `,` $delay (`clk` $clk^)? attr-dict `:` type($input)
+    $input `,` $delay `clk` $clk attr-dict `:` type($input)
   }];
 
   let summary = "Observe the sequence $delay cycles earlier.";
   let description = [{
       Semantically works like `ltl.delay %seq, -$delay, 0`, clocked by the
-      optional `$clk` operand if given.
+      `$clk` operand.
   }];
 }
 

lib/Conversion/FIRRTLToHW/LowerToHW.cpp

@@ -4745,9 +4745,7 @@ LogicalResult FIRRTLLowering::visitExpr(LTLEventuallyIntrinsicOp op) {
 }
 
 LogicalResult FIRRTLLowering::visitExpr(LTLPastIntrinsicOp op) {
-  Value clk;
-  if (op.getClock())
-    clk = getLoweredNonClockValue(op.getClock());
+  Value clk = getLoweredNonClockValue(op.getClock());
   return setLoweringToLTL<ltl::PastOp>(op, getLoweredValue(op.getInput()),
                                        op.getDelayAttr(), clk);
 }

lib/Dialect/FIRRTL/FIRRTLIntrinsics.cpp

@@ -380,11 +380,11 @@ class CirctLTLPastConverter : public IntrinsicConverter {
   using IntrinsicConverter::IntrinsicConverter;
 
   bool check(GenericIntrinsic gi) override {
-    if (gi.hasNInputs(1, 1) || gi.sizedInput<UIntType>(0, 1) ||
+    if (gi.hasNInputs(2) || gi.sizedInput<UIntType>(0, 1) ||
         gi.sizedOutput<UIntType>(1) || gi.namedIntParam("delay") ||
         gi.hasNParam(1))
       return true;
-    if (gi.op.getNumOperands() > 1 && gi.typedInput<ClockType>(1))
+    if (gi.typedInput<ClockType>(1))
       return true;
     return false;
   }
@@ -394,9 +394,7 @@ class CirctLTLPastConverter : public IntrinsicConverter {
     auto delay = rewriter.getI64IntegerAttr(
         gi.getParamValue<IntegerAttr>("delay").getValue().getZExtValue());
     auto operands = adaptor.getOperands();
-    Value clock;
-    if (operands.size() > 1)
-      clock = operands[1];
+    Value clock = operands[1];
     rewriter.replaceOpWithNewOp<LTLPastIntrinsicOp>(
         gi.op, gi.op.getResultTypes(), operands[0], delay, clock);
   }

lib/Dialect/FIRRTL/FIRRTLIntrinsics.td

@@ -260,7 +260,7 @@ def CirctLTLPast : FIRRTLIntrinsic {
     | Argument | Type    | Description               |
     | -------- | ------- | ------------------------- |
     | in       | UInt<1> | input boolean             |
-    | clock    | Clock   | clock for delay; optional |
+    | clock    | Clock   | clock for delay           |
 
     | Result | Type    | Description            |
     | ------ | ------- | ---------------------- |

test/Conversion/FIRRTLToHW/intrinsics.mlir

@@ -104,8 +104,6 @@ firrtl.circuit "Intrinsics" {
     // CHECK-NEXT: [[E0:%.+]] = ltl.eventually [[I0]] : !ltl.property
     %e0 = firrtl.int.ltl.eventually %i0 : (!firrtl.uint<1>) -> !firrtl.uint<1>
 
-    // CHECK-NEXT: [[P0:%.+]] = ltl.past %a, 1 : i1
-    %p0 = firrtl.int.ltl.past %a, 1 : (!firrtl.uint<1>) -> !firrtl.uint<1>
     // CHECK-NEXT: [[P1:%.+]] = ltl.past %b, 3 clk [[CLK]] : i1
     %p1 = firrtl.int.ltl.past %b, 3, %clk : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1>
 

test/Conversion/LTLToCore/assume-first-clock-errors.mlir

@@ -77,8 +77,6 @@ firrtl.circuit "Foo" {
     // CHECK-NEXT: firrtl.int.ltl.eventually %in0 :
     firrtl.int.generic "circt_ltl_eventually"  %in0 : (!firrtl.uint<1>) -> !firrtl.uint<1>
 
-    // CHECK-NEXT: firrtl.int.ltl.past %in0, 42 :
-    firrtl.int.generic "circt_ltl_past" <delay: i64 = 42> %in0 : (!firrtl.uint<1>) -> !firrtl.uint<1>
     // CHECK-NEXT: firrtl.int.ltl.past %in0, 42, %clk :
     firrtl.int.generic "circt_ltl_past" <delay: i64 = 42> %in0, %clk : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1>