[FIRRTL][Verif][LTL] Replace ltl.disable with an enable folded into verif.assert

lib/Dialect/FIRRTL/Transforms/ExpandWhens.cpp

@@ -535,19 +535,52 @@ class WhenOpVisitor : public LastConnectResolver<WhenOpVisitor> {
   /// scope, i.e. not in a WhenOp region, then there is no condition.
   Value andWithCondition(Operation *op, Value value) {
     // 'and' the value with the current condition.
-    return OpBuilder(op).createOrFold<AndPrimOp>(
+    OpBuilder builder(op);
+    return andWithCondition(builder, value);
+  }
+
+  /// And a 1-bit value with the current condition.  If we are in the outer
+  /// scope, i.e. not in a WhenOp region, then there is no condition.
+  Value andWithCondition(OpBuilder &builder, Value value) {
+    // 'and' the value with the current condition.
+    return builder.createOrFold<AndPrimOp>(
         condition.getLoc(), condition.getType(), condition, value);
   }
 
-  // Create an implication from the condition to the given value
-  // This is implemented as (or (not condition) value) to avoid
-  // the corner case where value is an implication.
-  Value impliesLTLCondition(Operation *op, Value value) {
-    OpBuilder builder = OpBuilder(op);
-    Value notCond = builder.createOrFold<LTLNotIntrinsicOp>(
-        condition.getLoc(), condition.getType(), condition);
-    return builder.createOrFold<LTLOrIntrinsicOp>(
-        condition.getLoc(), condition.getType(), notCond, value);
+  // Or a 1-bit value with the current condition.  If we are in the outer
+  /// scope, i.e. not in a WhenOp region, then there is no condition.
+  Value orWithCondition(OpBuilder &builder, Value value) {
+    // 'or' the value with the current condition.
+    return builder.createOrFold<OrPrimOp>(
+        condition.getLoc(), condition.getType(), condition, value);
+  }
+
+  template <typename Op>
+  void visitVerifIntrinsic(Op op) {
+    OpBuilder builder(op);
+    Value foldedWhen;
+    LTLClockIntrinsicOp clockOp;
+    LTLDisableIntrinsicOp disable;
+    // Extract the clock and disable from the UInt<1>
+    if ((clockOp =
+             dyn_cast<LTLClockIntrinsicOp>(op.getProperty().getDefiningOp()))) {
+      if ((disable = dyn_cast<LTLDisableIntrinsicOp>(
+               clockOp.getInput().getDefiningOp()))) {
+
+        Value newDisable = orWithCondition(builder, disable.getRhs());
+        foldedWhen = builder.create<LTLDisableIntrinsicOp>(
+            op.getLoc(), newDisable.getType(), disable.getLhs(), newDisable);
+      }
+      foldedWhen = builder.create<LTLClockIntrinsicOp>(
+          op.getLoc(), foldedWhen.getType(), foldedWhen, clockOp.getClock());
+    }
+    if (foldedWhen) {
+      op.getPropertyMutable().assign(foldedWhen);
+
+      // destroy the old clock and disable ops
+      clockOp.erase();
+      disable.erase();
+    }
   }
 
 private:
@@ -571,15 +604,15 @@ void WhenOpVisitor::visitStmt(StopOp op) {
 }
 
 void WhenOpVisitor::visitStmt(VerifAssertIntrinsicOp op) {
-  op.getPropertyMutable().assign(impliesLTLCondition(op, op.getProperty()));
+  visitVerifIntrinsic(op);
 }
 
 void WhenOpVisitor::visitStmt(VerifAssumeIntrinsicOp op) {
-  op.getPropertyMutable().assign(impliesLTLCondition(op, op.getProperty()));
+  visitVerifIntrinsic(op);
 }
 
 void WhenOpVisitor::visitStmt(VerifCoverIntrinsicOp op) {
-  op.getPropertyMutable().assign(impliesLTLCondition(op, op.getProperty()));
+  visitVerifIntrinsic(op);
 }
 
 void WhenOpVisitor::visitStmt(AssertOp op) {

test/Dialect/FIRRTL/expand-whens.mlir

@@ -637,38 +637,79 @@ firrtl.module @ModuleWithObjectWire(in %in: !firrtl.class<@ClassWithInput(in in:
 }
 
 // Test all verif assert/assume/cover constructs
-// CHECK:   firrtl.module @verif(in %clock: !firrtl.clock, in %cond: !firrtl.uint<1>, in %prop: !firrtl.uint<1>, in %enable: !firrtl.uint<1>, in %reset: !firrtl.uint<1>) {
-firrtl.module @verif(
-  in %clock : !firrtl.clock, in %cond : !firrtl.uint<1>, in %prop : !firrtl.uint<1>,
-  in %enable : !firrtl.uint<1>, in %reset : !firrtl.uint<1>
+// CHECK:   firrtl.module @verifassert(in %clock: !firrtl.clock, in %cond: !firrtl.uint<1>, in %prop: !firrtl.uint<1>,  in %prop1: !firrtl.uint<1>, in %disable: !firrtl.uint<1>, in %disable1: !firrtl.uint<1>, in %reset: !firrtl.uint<1>) {
+firrtl.module @verifassert(
+  in %clock : !firrtl.clock, in %cond : !firrtl.uint<1>, in %prop : !firrtl.uint<1>, in %prop1 : !firrtl.uint<1>,
+  in %disable : !firrtl.uint<1>, in %disable1 : !firrtl.uint<1>, in %reset : !firrtl.uint<1>
 ) {
   firrtl.when %cond : !firrtl.uint<1> {
-    // CHECK:   [[TMP0:%.+]] = firrtl.int.ltl.not %cond : (!firrtl.uint<1>) -> !firrtl.uint<1>
-    // CHECK:   [[TMP1:%.+]] = firrtl.int.ltl.or [[TMP0]], %prop : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
-    // CHECK:   firrtl.int.verif.assert [[TMP1]] : !firrtl.uint<1>
-    firrtl.int.verif.assert %prop : !firrtl.uint<1>
-    // CHECK:   %2 = firrtl.int.ltl.not %cond : (!firrtl.uint<1>) -> !firrtl.uint<1>
-    // CHECK:   %3 = firrtl.int.ltl.or %2, %prop : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
-    // CHECK:   firrtl.int.verif.assume %3 : !firrtl.uint<1>
-    firrtl.int.verif.assume %prop : !firrtl.uint<1>
-    // CHECK:   %4 = firrtl.int.ltl.not %cond : (!firrtl.uint<1>) -> !firrtl.uint<1>
-    // CHECK:   %5 = firrtl.int.ltl.or %4, %prop : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
-    // CHECK:   firrtl.int.verif.cover %5 : !firrtl.uint<1>
-    firrtl.int.verif.cover %prop : !firrtl.uint<1>
+    // CHECK:   [[TMP0A:%.+]] = firrtl.or %cond, %disable : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
+    // CHECK:   [[TMP1A:%.+]] = firrtl.int.ltl.disable %prop, [[TMP0A]] : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
+    // CHECK:   [[TMP2A:%.+]] = firrtl.int.ltl.clock [[TMP1A]], %clock : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1>
+    // CHECK:   firrtl.int.verif.assert [[TMP2A]] : !firrtl.uint<1>
+    %dis_prop = firrtl.int.ltl.disable %prop, %disable : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
+    %clk_prop = firrtl.int.ltl.clock %dis_prop, %clock : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1>
+
+    firrtl.int.verif.assert %clk_prop : !firrtl.uint<1>
   } else {
-    // CHECK:   %6 = firrtl.not %cond : (!firrtl.uint<1>) -> !firrtl.uint<1>
-    // CHECK:   %7 = firrtl.int.ltl.not %6 : (!firrtl.uint<1>) -> !firrtl.uint<1>
-    // CHECK:   %8 = firrtl.int.ltl.or %7, %prop : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
-    // CHECK:   firrtl.int.verif.assert %8 : !firrtl.uint<1>
-    firrtl.int.verif.assert %prop : !firrtl.uint<1>
-    // CHECK:   %9 = firrtl.int.ltl.not %6 : (!firrtl.uint<1>) -> !firrtl.uint<1>
-    // CHECK:   %10 = firrtl.int.ltl.or %9, %prop : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
-    // CHECK:   firrtl.int.verif.assume %10 : !firrtl.uint<1>
-    firrtl.int.verif.assume %prop : !firrtl.uint<1>
-    // CHECK:   %11 = firrtl.int.ltl.not %6 : (!firrtl.uint<1>) -> !firrtl.uint<1>
-    // CHECK:   %12 = firrtl.int.ltl.or %11, %prop : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
-    // CHECK:   firrtl.int.verif.cover %12 : !firrtl.uint<1>
-    firrtl.int.verif.cover %prop : !firrtl.uint<1>
+    // CHECK:   [[TMP3A:%.+]] = firrtl.not %cond : (!firrtl.uint<1>) -> !firrtl.uint<1>
+    // CHECK:   [[TMP4A:%.+]] = firrtl.or [[TMP3A]], %disable1 : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
+    // CHECK:   [[TMP5A:%.+]] = firrtl.int.ltl.disable %prop1, [[TMP4A]] : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
+    // CHECK:   [[TMP6A:%.+]] = firrtl.int.ltl.clock [[TMP5A]], %clock : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1>
+    // CHECK:   firrtl.int.verif.assert [[TMP6A]] : !firrtl.uint<1>
+    %dis_prop = firrtl.int.ltl.disable %prop1, %disable1 : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
+    %clk_prop = firrtl.int.ltl.clock %dis_prop, %clock : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1>
+    firrtl.int.verif.assert %clk_prop : !firrtl.uint<1>
+  }
+}
+
+// CHECK:   firrtl.module @verifassume(in %clock: !firrtl.clock, in %cond: !firrtl.uint<1>, in %prop: !firrtl.uint<1>,  in %prop1: !firrtl.uint<1>, in %disable: !firrtl.uint<1>, in %disable1: !firrtl.uint<1>, in %reset: !firrtl.uint<1>) {
+firrtl.module @verifassume(
+  in %clock : !firrtl.clock, in %cond : !firrtl.uint<1>, in %prop : !firrtl.uint<1>, in %prop1 : !firrtl.uint<1>,
+  in %disable : !firrtl.uint<1>, in %disable1 : !firrtl.uint<1>, in %reset : !firrtl.uint<1>
+) {
+  firrtl.when %cond : !firrtl.uint<1> {
+    // CHECK:   [[TMP0:%.+]] = firrtl.or %cond, %disable : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
+    // CHECK:   [[TMP1:%.+]] = firrtl.int.ltl.disable %prop, [[TMP0]] : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
+    // CHECK:   [[TMP2:%.+]] = firrtl.int.ltl.clock [[TMP1]], %clock : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1>
+    // CHECK:   firrtl.int.verif.assume [[TMP2]] : !firrtl.uint<1>
+    %dis_prop = firrtl.int.ltl.disable %prop, %disable : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
+    %clk_prop = firrtl.int.ltl.clock %dis_prop, %clock : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1>
+    firrtl.int.verif.assume %clk_prop : !firrtl.uint<1>
+  } else {
+    // CHECK:   [[TMP3:%.+]] = firrtl.not %cond : (!firrtl.uint<1>) -> !firrtl.uint<1>
+    // CHECK:   [[TMP4:%.+]] = firrtl.or [[TMP3]], %disable1 : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
+    // CHECK:   [[TMP5:%.+]] = firrtl.int.ltl.disable %prop1, [[TMP4]] : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
+    // CHECK:   [[TMP6:%.+]] = firrtl.int.ltl.clock [[TMP5]], %clock : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1>
+    // CHECK:   firrtl.int.verif.assume [[TMP6]] : !firrtl.uint<1>
+    %dis_prop = firrtl.int.ltl.disable %prop1, %disable1 : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
+    %clk_prop = firrtl.int.ltl.clock %dis_prop, %clock : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1>
+    firrtl.int.verif.assume %clk_prop : !firrtl.uint<1>
+  }
+}
+
+// CHECK:   firrtl.module @verifcover(in %clock: !firrtl.clock, in %cond: !firrtl.uint<1>, in %prop: !firrtl.uint<1>,  in %prop1: !firrtl.uint<1>, in %disable: !firrtl.uint<1>, in %disable1: !firrtl.uint<1>, in %reset: !firrtl.uint<1>) {
+firrtl.module @verifcover(
+  in %clock : !firrtl.clock, in %cond : !firrtl.uint<1>, in %prop : !firrtl.uint<1>,  in %prop1 : !firrtl.uint<1>,
+  in %disable : !firrtl.uint<1>, in %disable1 : !firrtl.uint<1>, in %reset : !firrtl.uint<1>
+) {
+  firrtl.when %cond : !firrtl.uint<1> {
+    // CHECK:   [[TMP0C:%.+]] = firrtl.or %cond, %disable : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
+    // CHECK:   [[TMP1C:%.+]] = firrtl.int.ltl.disable %prop, [[TMP0C]] : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
+    // CHECK:   [[TMP2C:%.+]] = firrtl.int.ltl.clock [[TMP1C]], %clock : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1>
+    // CHECK:   firrtl.int.verif.cover [[TMP2C]] : !firrtl.uint<1>
+    %dis_prop = firrtl.int.ltl.disable %prop, %disable : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
+    %clk_prop = firrtl.int.ltl.clock %dis_prop, %clock : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1>
+    firrtl.int.verif.cover %clk_prop : !firrtl.uint<1>
+  } else {
+    // CHECK:   [[TMP3C:%.+]] = firrtl.not %cond : (!firrtl.uint<1>) -> !firrtl.uint<1>
+    // CHECK:   [[TMP4C:%.+]] = firrtl.or [[TMP3C]], %disable1 : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
+    // CHECK:   [[TMP5C:%.+]] = firrtl.int.ltl.disable %prop1, [[TMP4C]] : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
+    // CHECK:   [[TMP6C:%.+]] = firrtl.int.ltl.clock [[TMP5C]], %clock : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1>
+    // CHECK:   firrtl.int.verif.cover [[TMP6C]] : !firrtl.uint<1>
+    %dis_prop = firrtl.int.ltl.disable %prop1, %disable1 : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
+    %clk_prop = firrtl.int.ltl.clock %dis_prop, %clock : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1>
+    firrtl.int.verif.cover %clk_prop : !firrtl.uint<1>
   }
 }