From deb647193c314d73ee5b6bf332594b13cc45d972 Mon Sep 17 00:00:00 2001
From: Dobios <adobis@student.ethz.ch>
Date: Thu, 29 Feb 2024 17:21:23 -0800
Subject: [PATCH] Made all non a ##n true |-> b patterns explicitly illegal

---
 lib/Conversion/LTLToCore/LTLToCore.cpp | 27 +++++++++++++++++++++-----
 1 file changed, 22 insertions(+), 5 deletions(-)

diff --git a/lib/Conversion/LTLToCore/LTLToCore.cpp b/lib/Conversion/LTLToCore/LTLToCore.cpp
index f4a5f85a3273..9269e8b42f0c 100644
--- 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");