Emit companion Assumes for UNR Only SVAs as Immediate (instead of con…

…current) (llvm#5561)
jiahanxie353 · Aug 2, 2023 · b48ffd1 · b48ffd1
1 parent cc61339
commit b48ffd1
Show file tree

Hide file tree

Showing 2 changed files with 34 additions and 10 deletions.
diff --git a/lib/Conversion/FIRRTLToHW/LowerToHW.cpp b/lib/Conversion/FIRRTLToHW/LowerToHW.cpp
@@ -3977,9 +3977,24 @@ LogicalResult FIRRTLLowering::lowerVerificationStatement(
     Value opEnable, StringAttr opMessageAttr, ValueRange opOperands,
     StringAttr opNameAttr, bool isConcurrent, EventControl opEventControl) {
   StringRef opName = op->getName().stripDialect();
+
+  // The attribute holding the compile guards
+  ArrayRef<Attribute> guards{};
+  if (auto guardsAttr = op->template getAttrOfType<ArrayAttr>("guards"))
+    guards = guardsAttr.getValue();
+
   auto isAssert = opName == "assert";
   auto isCover = opName == "cover";
 
+  // TODO : Need to figure out if there is a cleaner way to get the string which
+  // indicates the assert is UNR only. Or better - not rely on this at all -
+  // ideally there should have been some other attribute which indicated that
+  // this assert for UNR only.
+  auto isUnrOnlyAssert = llvm::any_of(guards, [](Attribute attr) {
+    StringAttr strAttr = dyn_cast<StringAttr>(attr);
+    return strAttr && strAttr.getValue() == "USE_UNR_ONLY_CONSTRAINTS";
+  });
+
   auto clock = getLoweredValue(opClock);
   auto enable = getLoweredValue(opEnable);
   auto predicate = getLoweredValue(opPredicate);
@@ -4098,19 +4113,27 @@ LogicalResult FIRRTLLowering::lowerVerificationStatement(
         assumeLabel = StringAttr::get(builder.getContext(),
                                       "assume__" + label.getValue());
       addToIfDefBlock("USE_PROPERTY_AS_CONSTRAINT", [&]() {
-        builder.create<sv::AssumeConcurrentOp>(
-            circt::sv::EventControlAttr::get(builder.getContext(), event),
-            clock, predicate, assumeLabel);
+        if (!isUnrOnlyAssert) {
+          builder.create<sv::AssumeConcurrentOp>(
+              circt::sv::EventControlAttr::get(builder.getContext(), event),
+              clock, predicate, assumeLabel);
+        } else {
+          builder.create<sv::AlwaysOp>(
+              ArrayRef(sv::EventControl::AtEdge), ArrayRef(predicate), [&]() {
+                buildImmediateVerifOp(builder, "assume", predicate,
+                                      circt::sv::DeferAssertAttr::get(
+                                          builder.getContext(),
+                                          circt::sv::DeferAssert::Immediate),
+                                      assumeLabel);
+              });
+        }
       });
     }
   };
 
   // Wrap the verification statement up in the optional preprocessor
   // guards. This is a bit awkward since we want to translate an array of
-  // guards into a recursive call to `addToIfDefBlock`.
-  ArrayRef<Attribute> guards{};
-  if (auto guardsAttr = op->template getAttrOfType<ArrayAttr>("guards"))
-    guards = guardsAttr.getValue();
+  // guards  into a recursive call to `addToIfDefBlock`.
   bool anyFailed = false;
   std::function<void()> emitWrapped = [&]() {
     if (guards.empty()) {
@@ -4129,7 +4152,6 @@ LogicalResult FIRRTLLowering::lowerVerificationStatement(
   emitWrapped();
   if (anyFailed)
     return failure();
-
   return success();
 }
 

diff --git a/test/Dialect/FIRRTL/SFCTests/complex-asserts.fir b/test/Dialect/FIRRTL/SFCTests/complex-asserts.fir
@@ -115,7 +115,8 @@ circuit Foo:
     ; CHECK-NEXT:   assert__verif_library_1: assert property (@(posedge clock) [[TMP4]])
     ; CHECK-SAME:     else $error("Assertion failed (verification library): Conditional compilation example for UNR-only assert");
     ; CHECK-NEXT:   `ifdef USE_PROPERTY_AS_CONSTRAINT
-    ; CHECK-NEXT:     assume__verif_library_1: assume property (@(posedge clock) [[TMP4]]);
+    ; CHECK-NEXT:     always @(edge [[TMP4]])
+    ; CHECK-NEXT:       assume__verif_library_1: assume([[TMP4]]);
     ; CHECK-NEXT:   `endif
     when not(or(predicate8, asUInt(reset))) :
       printf(clock, enable, "foo [verif-library-assert]<extraction-summary>{\"predicateModifier\":{\"type\":\"noMod\"},\"conditionalCompileToggles\":[{\"type\":\"unrOnly\"}],\"format\":{\"type\":\"sva\"},\"baseMsg\":\"Assertion failed (verification library): Conditional compilation example for UNR-only assert\"}</extraction-summary> bar")
@@ -144,7 +145,8 @@ circuit Foo:
     ; CHECK-NEXT:     assert__verif_library_2: assert property (@(posedge clock) [[TMP5]])
     ; CHECK-SAME:       else $error("Assertion failed (verification library): Conditional compilation example for UNR-only and formal-only assert");
     ; CHECK-NEXT:     `ifdef USE_PROPERTY_AS_CONSTRAINT
-    ; CHECK-NEXT:       assume__verif_library_2: assume property (@(posedge clock) [[TMP5]]);
+    ; CHECK-NEXT:       always @(edge [[TMP5]])
+    ; CHECK-NEXT:         assume__verif_library_2: assume([[TMP5]]);
     ; CHECK-NEXT:     `endif
     ; CHECK-NEXT:   `endif
     ; CHECK-NEXT: `endif