Made all non a ##n true |-> b patterns explicitly illegal

llvm · Mar 1, 2024 · deb6471 · deb6471
1 parent 2d2e8e8
commit deb6471
Showing 1 changed file with 22 additions and 5 deletions.
diff --git a/lib/Conversion/LTLToCore/LTLToCore.cpp b/lib/Conversion/LTLToCore/LTLToCore.cpp
@@ -306,13 +306,30 @@ struct AssertOpConversionPattern : OpConversionPattern<verif::AssertOp> {
           if (!isa<BlockArgument>(inputs.back())) {
             if ((delayN =
                      dyn_cast<ltl::DelayOp>(inputs.back().getDefiningOp()))) {
-              // NOI case: generate the hardware needed to encode the
-              // non-overlapping implication
-              if (!makeNonOverlappingImplication(implop, delayN, ltlclock,
-                                                 concat, rewriter, res))
+
+              // Make sure that you only allow for a ##n true |-> b
+              hw::ConstantOp hwconst;
+              if (!(hwconst = dyn_cast<hw::ConstantOp>(
+                        delayN.getInput().getDefiningOp()))) {
+                delayN->emitError("Only a ##n true |-> b is supported. RHS of "
+                                  "the concatenation must be true");
                 return false;
+              } else {
+                if (hwconst.getValue().isZero()) {
+                  delayN->emitError(
+                      "Only a ##n true |-> b is supported. RHS of "
+                      "the concatenation must be true");
+                  return false;
+                }
+
+                // NOI case: generate the hardware needed to encode the
+                // non-overlapping implication
+                if (!makeNonOverlappingImplication(implop, delayN, ltlclock,
+                                                   concat, rewriter, res))
+                  return false;
 
-              rewriter.eraseOp(delayN);
+                rewriter.eraseOp(delayN);
+              }
             }
           } else {
             concat->emitError("Antecedent must be of the form a ##n true");