[Verif] handle self-referencing operations (llvm#8972)

When cloning self-referencing operations like

    %reg = seq.firreg %reg clock %clock reset sync %reset, %c0_i4 : i4

lower-contracts would previously produce something like:

    ^bb0(%arg0: !seq.clock, %arg1: i1):
      ...
      %5 = seq.firreg(%5, %arg0, %arg1, %4) : i4
      ...

    verif.formal():
      ...
      %3 = seq.firreg(%5, %0, %1, %2) : i4
      ...

Here we can see that the verif.formal test refers to a value from `bb0`,
namely `%5`, which results in an error.

The problem appears to be that when cloning the operation, we haven't
yet created a mapping for the operation's result (`%5 -> %3`), so `%5`
is left in place.

This change makes us go through all operands of the cloned operations
once more, _after_ adding the mappings for the operations' results,
which means that the `%5` in verif.formal is remapped to `%3`.

This is done after cloning all operations to also handle cycles longer
than one operation.

Fixes llvm#8952.

Author: ollef

lib/Dialect/Verif/Transforms/LowerContracts.cpp

@@ -56,8 +56,8 @@ Operation *replaceContractOp(OpBuilder &builder, RequireLike op,
   return nullptr;
 }
 
-LogicalResult cloneOp(OpBuilder &builder, Operation *opToClone,
-                      IRMapping &mapping, bool assumeContract) {
+FailureOr<Operation *> cloneOp(OpBuilder &builder, Operation *opToClone,
+                               IRMapping &mapping, bool assumeContract) {
   Operation *clonedOp;
   // Replace ensure/require ops, otherwise clone
   if (auto requireLike = dyn_cast<RequireLike>(*opToClone)) {
@@ -74,7 +74,7 @@ LogicalResult cloneOp(OpBuilder &builder, Operation *opToClone,
        llvm::zip(opToClone->getResults(), clonedOp->getResults())) {
     mapping.map(x, y);
   }
-  return llvm::success();
+  return clonedOp;
 }
 
 void assumeContractHolds(OpBuilder &builder, IRMapping &mapping,
@@ -118,6 +118,7 @@ LogicalResult cloneFanIn(OpBuilder &builder, Operation *contractToClone,
                          IRMapping &mapping) {
   DenseSet<Operation *> seen;
   SmallVector<Operation *> opsToClone;
+  SmallVector<Operation *> clonedOps;
   std::queue<Operation *> workList;
   workList.push(contractToClone);
 
@@ -154,9 +155,24 @@ LogicalResult cloneFanIn(OpBuilder &builder, Operation *contractToClone,
   // Sort ops so mapping is available for all operands when cloning an op
   computeTopologicalSorting(opsToClone);
 
+  clonedOps.reserve(opsToClone.size());
   for (auto *op : opsToClone) {
-    if (failed(cloneOp(builder, op, mapping, true)))
+    if (auto clonedOp = cloneOp(builder, op, mapping, true);
+        succeeded(clonedOp)) {
+      clonedOps.push_back(*clonedOp);
+    } else {
       return failure();
+    }
+  }
+
+  // Remap self-referencing uses of cloned results in the cloned ops
+  for (auto *clonedOp : clonedOps) {
+    for (unsigned i = 0, e = clonedOp->getNumOperands(); i < e; i++) {
+      auto operand = clonedOp->getOperand(i);
+      if (mapping.contains(operand)) {
+        clonedOp->setOperand(i, mapping.lookup(operand));
+      }
+    }
   }
   return success();
 }

test/Dialect/Verif/lower-contracts.mlir

@@ -313,3 +313,38 @@ hw.module @Mul3(in %a: i2, in %b: i2, out z: i4) {
   }
   hw.output %z : i4
 }
+
+// CHECK-LABEL: verif.formal @Counter_CheckContract_0
+// CHECK-NEXT:    [[TMP0:%.+]] = hw.constant -1 : i2
+// CHECK-NEXT:    [[TMP1:%.+]] = hw.constant 1 : i2
+// CHECK-NEXT:    [[TMP2:%.+]] = hw.constant -2 : i2
+// CHECK-NEXT:    [[TMP3:%.+]] = hw.constant 0 : i2
+// CHECK-NEXT:    [[TMP4:%.+]] = verif.symbolic_value : i1
+// CHECK-NEXT:    [[TMP5:%.+]] = verif.symbolic_value : !seq.clock
+// CHECK-NEXT:    [[TMP6:%.+]] = seq.from_clock [[TMP5]]
+// CHECK-NEXT:    [[TMP7:%.+]] = comb.icmp bin eq [[REG:%.+]], [[TMP2]] : i2
+// CHECK-NEXT:    [[TMP8:%.+]] = comb.add bin [[REG]], [[TMP1]] : i2
+// CHECK-NEXT:    [[TMP9:%.+]] = comb.mux bin [[TMP7]], [[TMP3]], [[TMP8]] : i2
+// CHECK-NEXT:    [[REG]] = seq.firreg [[TMP9]] clock [[TMP5]] reset sync [[TMP4]], [[TMP3]] {firrtl.random_init_start = 0 : ui64} : i2
+// CHECK-NEXT:    [[TMP10:%.+]] = comb.icmp bin ne [[REG]], [[TMP0]] : i2
+// CHECK-NEXT:    verif.clocked_assert [[TMP10]], posedge [[TMP6]] : i1
+// CHECK-NEXT: }
+
+hw.module @Counter(in %in : i2, out out : i2, in %clock : !seq.clock, in %reset : i1) {
+  %zero = hw.constant 0 : i2
+  %one = hw.constant 1 : i2
+  %max = hw.constant -2 : i2
+  %0 = seq.from_clock %clock
+  %reg = seq.firreg %next clock %clock reset sync %reset, %zero {firrtl.random_init_start = 0 : ui64} : i2
+  %eq = comb.icmp bin eq %reg, %max : i2
+  %added = comb.add bin %reg, %one : i2
+  %next = comb.mux bin %eq, %zero, %added : i2
+  %4 = verif.contract %reg : i2 {
+    %never = hw.constant -1 : i2
+    %ne = comb.icmp bin ne %4, %never : i2
+    %6 = verif.has_been_reset %0, sync %reset
+    %7 = ltl.clock %ne, posedge %0 : i1
+    verif.ensure %7 if %6 : !ltl.sequence
+  }
+  hw.output %4 : i2
+}