[SV] Remove Verif Statements w/ Non-zero Predicate

Add canonicalizers for immediate and concurrent verification statements that erases them if their predicate is a constant true (non-zero). Fixes #2800. Signed-off-by: Schuyler Eldridge <[email protected]>
llvm · Apr 1, 2022 · 1b60400 · 1b60400
1 parent 1722fde
commit 1b60400
Show file tree

Hide file tree

Showing 3 changed files with 81 additions and 0 deletions.
diff --git a/include/circt/Dialect/SV/SVVerification.td b/include/circt/Dialect/SV/SVVerification.td
@@ -58,6 +58,8 @@ class ImmediateVerifOp<string mnemonic, list<Trait> traits = []> :
  [{ build(odsBuilder, odsState, expression, defer, label, StringAttr{},
  ValueRange{}); }]>
  ];
+
+ let hasCanonicalizer = 1;
 }
 
 def AssertOp : ImmediateVerifOp<"assert"> {
@@ -120,6 +122,8 @@ class ConcurrentVerifOp<string mnemonic, list<Trait> traits = []> :
  [{ build(odsBuilder, odsState, event, clock, property, label,
  StringAttr{}, ValueRange{}); }]>
  ];
+
+ let hasCanonicalizer = 1;
 }
 
 def AssertConcurrentOp : ConcurrentVerifOp<"assert.concurrent"> {

diff --git a/lib/Dialect/SV/SVOps.cpp b/lib/Dialect/SV/SVOps.cpp
@@ -1438,6 +1438,63 @@ void printXMRPath(OpAsmPrinter &p, XMROp op, ArrayAttr pathAttr,
  p << ", " << terminalAttr;
 }
 
+//===----------------------------------------------------------------------===//
+// Verification Ops.
+//===----------------------------------------------------------------------===//
+
+static LogicalResult eraseIfNotZero(Operation *op, Value value,
+ PatternRewriter &rewriter) {
+ if (auto constant = value.getDefiningOp<hw::ConstantOp>())
+ if (!constant.getValue().isZero()) {
+ rewriter.eraseOp(op);
+ return success();
+ }
+
+ return failure();
+}
+
+template <class Op>
+static LogicalResult canonicalizeImmediateVerifOp(Op op,
+ PatternRewriter &rewriter) {
+ return eraseIfNotZero(op, op.expression(), rewriter);
+}
+
+void AssertOp::getCanonicalizationPatterns(RewritePatternSet &results,
+ MLIRContext *context) {
+ results.add(canonicalizeImmediateVerifOp<AssertOp>);
+}
+
+void AssumeOp::getCanonicalizationPatterns(RewritePatternSet &results,
+ MLIRContext *context) {
+ results.add(canonicalizeImmediateVerifOp<AssumeOp>);
+}
+
+void CoverOp::getCanonicalizationPatterns(RewritePatternSet &results,
+ MLIRContext *context) {
+ results.add(canonicalizeImmediateVerifOp<CoverOp>);
+}
+
+template <class Op>
+static LogicalResult canonicalizeConcurrentVerifOp(Op op,
+ PatternRewriter &rewriter) {
+ return eraseIfNotZero(op, op.property(), rewriter);
+}
+
+void AssertConcurrentOp::getCanonicalizationPatterns(RewritePatternSet &results,
+ MLIRContext *context) {
+ results.add(canonicalizeConcurrentVerifOp<AssertConcurrentOp>);
+}
+
+void AssumeConcurrentOp::getCanonicalizationPatterns(RewritePatternSet &results,
+ MLIRContext *context) {
+ results.add(canonicalizeConcurrentVerifOp<AssumeConcurrentOp>);
+}
+
+void CoverConcurrentOp::getCanonicalizationPatterns(RewritePatternSet &results,
+ MLIRContext *context) {
+ results.add(canonicalizeConcurrentVerifOp<CoverConcurrentOp>);
+}
+
 //===----------------------------------------------------------------------===//
 // TableGen generated logic.
 //===----------------------------------------------------------------------===//

diff --git a/test/Dialect/SV/canonicalization.mlir b/test/Dialect/SV/canonicalization.mlir
@@ -133,3 +133,23 @@ func @mux_to_cond_assign_t(%clock: i1, %c: i1, %data: i2) {
  }
  return
 }
+
+// CHECK-LABEL; @immediate_assert_canonicalization
+hw.module @assert_canonicalization(%clock: i1) {
+ %true = hw.constant 1 : i1
+ sv.always posedge %clock {
+ // CHECK-NOT: sv.assert
+ sv.assert %true, immediate message "assert"
+ // CHECK-NOT: sv.assume
+ sv.assume %true, immediate message "assume"
+ // CHECK-NOT: sv.cover
+ sv.cover %true, immediate
+ }
+
+ // CHECK-NOT: sv.assert.concurrent
+ sv.assert.concurrent posedge %clock, %true
+ // CHECK-NOT: sv.assume.concurrent
+ sv.assume.concurrent posedge %clock, %true
+ // CHECK-NOT: sv.cover.concurrent
+ sv.cover.concurrent posedge %clock, %true
+}