[SV] Add Intermediary Assert Op for better enable polarity flip (#7302)

This PR introduces a new assert property op to the sv dialect and uses that as an intermediary for property assertion emission. This should solve the issue of the polarity being different in SV and in verif for the enable signals ( enable in verif, disable in sv ).

Author: dobios

include/circt/Dialect/SV/SVDialect.td

@@ -22,7 +22,8 @@ def SVDialect : Dialect {
     This dialect defines the `sv` dialect, which represents various
     SystemVerilog-specific constructs in an AST-like representation.
   }];
-  let dependentDialects = ["circt::comb::CombDialect", "circt::hw::HWDialect"];
+  let dependentDialects = ["circt::comb::CombDialect", "circt::hw::HWDialect", 
+    "circt::ltl::LTLDialect"];
 
   let useDefaultTypePrinterParser = 1;
   let useDefaultAttributePrinterParser = 1;

include/circt/Dialect/SV/SVOps.h

@@ -15,6 +15,8 @@
 
 #include "circt/Dialect/HW/HWAttributes.h"
 #include "circt/Dialect/HW/HWOps.h"
+#include "circt/Dialect/LTL/LTLDialect.h"
+#include "circt/Dialect/LTL/LTLTypes.h"
 #include "circt/Dialect/SV/SVAttributes.h"
 #include "circt/Dialect/SV/SVDialect.h"
 #include "circt/Dialect/SV/SVTypes.h"

include/circt/Dialect/SV/SVVerification.td

@@ -10,6 +10,7 @@
 // declarations.
 //
 //===----------------------------------------------------------------------===//
+include "circt/Dialect/LTL/LTLTypes.td"
 
 /// Immediate assertions, like `assert`.
 def ImmediateAssert: I32EnumAttrCase<"Immediate", 0, "immediate">;
@@ -159,3 +160,56 @@ def CoverConcurrentOp : ConcurrentVerifOp<"cover.concurrent",
     section 16.5 of the SystemVerilog 2017 specification.
   }];
 }
+
+
+/// Property Assertions/Assumptions/Cover analogous to SVA property verification ops.
+class PropertyVerifOp<string mnemonic, list<Trait> traits = [AttrSizedOperandSegments]> :
+    SVOp<mnemonic, traits> {
+  let arguments = (ins
+    LTLAnyPropertyType:$property,
+    OptionalAttr<EventControlAttr>:$event, Optional<I1>:$clock, 
+    Optional<I1>:$disable,
+    OptionalAttr<StrAttr>:$label);
+
+  let assemblyFormat = [{
+    $property (`on` $event^)? ($clock^)? (`disable_iff` $disable^)?
+    (`label` $label^)? attr-dict `:` type($property)
+  }];
+
+  let builders = [
+    // no clock or event
+    OpBuilder<(ins "mlir::Value":$property,
+      "mlir::Value":$disable,
+       CArg<"StringAttr","StringAttr()">: $label),
+      [{ build(odsBuilder, odsState, property, EventControlAttr{}, Value(), disable, label); }]>
+  ];
+
+  let hasVerifier = true;
+}
+
+def AssertPropertyOp : PropertyVerifOp<"assert_property"> {
+  let summary = "property assertion -- can be disabled and clocked";
+  let description = [{
+    Assert that a given SVA-style property holds. This is only checked when 
+    the disable signal is low and a clock event occurs. This is analogous to 
+    the verif.assert operation, but with a flipped enable polarity.
+  }];
+}
+
+def AssumePropertyOp : PropertyVerifOp<"assume_property"> {
+  let summary = "property assumption -- can be disabled and clocked";
+  let description = [{
+    Assume that a given SVA-style property holds. This is only considered when 
+    the disable signal is low and a clock event occurs. This is analogous to 
+    the verif.assume operation, but with a flipped enable polarity.
+  }];
+}
+
+def CoverPropertyOp : PropertyVerifOp<"cover_property"> {
+  let summary = "property cover point -- can be disabled and clocked";
+  let description = [{
+    Cover when a given SVA-style property holds. This is only checked when 
+    the disable signal is low and a clock event occurs. This is analogous to 
+    the verif.cover operation, but with a flipped enable polarity.
+  }];
+}

include/circt/Dialect/SV/SVVisitors.h

@@ -48,7 +48,8 @@ class Visitor {
             FuncDPIImportOp,
             // Verification statements.
             AssertOp, AssumeOp, CoverOp, AssertConcurrentOp, AssumeConcurrentOp,
-            CoverConcurrentOp,
+            CoverConcurrentOp, AssertPropertyOp, AssumePropertyOp,
+            CoverPropertyOp,
             // Bind Statements
             BindOp,
             // Simulator control tasks
@@ -154,6 +155,9 @@ class Visitor {
   HANDLE(AssertConcurrentOp, Unhandled);
   HANDLE(AssumeConcurrentOp, Unhandled);
   HANDLE(CoverConcurrentOp, Unhandled);
+  HANDLE(AssertPropertyOp, Unhandled);
+  HANDLE(AssumePropertyOp, Unhandled);
+  HANDLE(CoverPropertyOp, Unhandled);
 
   // Bind statements.
   HANDLE(BindOp, Unhandled);