[Verif] Add ignore attribute to formal (#7719)

By default, `circt-test` will not include "ignored" verif.formal ops
in the output list but has an option `--list-ignored` to emit them.

Author: leonardt

integration_test/circt-test/basic.mlir

@@ -1,7 +1,7 @@
 // RUN: circt-test %s -r circt-test-runner-sby.py | FileCheck %s
 // REQUIRES: sby
 
-// CHECK: all 6 tests passed
+// CHECK: 1 tests FAILED, 6 passed, 1 ignored
 
 hw.module @FullAdder(in %a: i1, in %b: i1, in %ci: i1, out s: i1, out co: i1) {
   %0 = comb.xor %a, %b : i1
@@ -113,3 +113,39 @@ verif.formal @ALUWorks {
   %eq = comb.icmp eq %z0, %z1 : i4
   verif.assert %eq : i1
 }
+
+verif.formal @ALUIgnoreFailure attributes {ignore = true} {
+  %a = verif.symbolic_value : i4
+  %b = verif.symbolic_value : i4
+  %sub = verif.symbolic_value : i1
+
+  // Custom ALU implementation.
+  %z0 = hw.instance "dut" @ALU(a: %a: i4, b: %b: i4, sub: %sub: i1) -> (z: i4)
+
+  // Reference add/sub function.
+  %ref_add = comb.add %a, %b : i4
+  %ref_sub = comb.sub %a, %b : i4
+  %z1 = comb.mux %sub, %ref_sub, %ref_add : i4
+
+  // Check the two don't match (failure will be ignored).
+  %ne = comb.icmp ne %z0, %z1 : i4
+  verif.assert %ne : i1
+}
+
+verif.formal @ALUFailure {
+  %a = verif.symbolic_value : i4
+  %b = verif.symbolic_value : i4
+  %sub = verif.symbolic_value : i1
+
+  // Custom ALU implementation.
+  %z0 = hw.instance "dut" @ALU(a: %a: i4, b: %b: i4, sub: %sub: i1) -> (z: i4)
+
+  // Reference add/sub function.
+  %ref_add = comb.add %a, %b : i4
+  %ref_sub = comb.sub %a, %b : i4
+  %z1 = comb.mux %sub, %ref_sub, %ref_add : i4
+
+  // Check the two don't match (should fail).
+  %ne = comb.icmp ne %z0, %z1 : i4
+  verif.assert %ne : i1
+}

test/circt-test/basic.mlir

@@ -1,6 +1,7 @@
 // RUN: circt-test -l %s | FileCheck %s
 // RUN: circt-test -l --json %s | FileCheck --check-prefix=JSON %s
 // RUN: circt-as %s -o - | circt-test -l | FileCheck %s
+// RUN: circt-test -l %s --list-ignored | FileCheck --check-prefix=CHECK-WITH-IGNORED %s
 
 // JSON: [
 
@@ -23,6 +24,7 @@ verif.formal @Some.TestB {}
 // JSON-NEXT:   "attrs": {
 // JSON-NEXT:     "awesome": true
 // JSON-NEXT:     "engine": "bmc"
+// JSON-NEXT:     "ignore": false
 // JSON-NEXT:     "offset": 42
 // JSON-NEXT:     "tags": [
 // JSON-NEXT:       "sby"
@@ -31,13 +33,22 @@ verif.formal @Some.TestB {}
 // JSON-NEXT:     "wow": false
 // JSON-NEXT:   }
 // JSON-NEXT: }
-// CHECK: Attrs formal {awesome = true, engine = "bmc", offset = 42 : i64, tags = ["sby", "induction"], wow = false}
+// CHECK: Attrs formal {awesome = true, engine = "bmc", ignore = false, offset = 42 : i64, tags = ["sby", "induction"], wow = false}
 verif.formal @Attrs attributes {
     awesome = true,
     engine = "bmc",
     offset = 42 : i64,
     tags = ["sby", "induction"],
-    wow = false
+    wow = false,
+    ignore = false
+} {}
+
+// CHECK-NOT: "name": "Ignore"
+// JSON-NOT: "name": "Ignore"
+// CHECK-WITH-IGNORED: Ignore formal {another = "attr", ignore = true}
+verif.formal @Ignore attributes {
+    ignore = true,
+    another = "attr"
 } {}
 
 // JSON: ]

tools/circt-test/circt-test.cpp

@@ -71,6 +71,9 @@ struct Options {
   cl::opt<bool> json{"json", cl::desc("Emit test list as JSON array"),
                      cl::init(false), cl::cat(cat)};
 
+  cl::opt<bool> listIgnored{"list-ignored", cl::desc("List ignored tests"),
+                            cl::init(false), cl::cat(cat)};
+
   cl::opt<std::string> resultDir{
       "d", cl::desc("Result directory (default `.circt-test`)"),
       cl::value_desc("dir"), cl::init(".circt-test"), cl::cat(cat)};
@@ -107,6 +110,8 @@ class Test {
   /// An optional location indicating where this test was discovered. This can
   /// be the location of an MLIR op, or a line in some other source file.
   LocationAttr loc;
+  /// Whether or not the test should be ignored
+  bool ignore;
   /// The user-defined attributes of this test.
   DictionaryAttr attrs;
 };
@@ -120,7 +125,10 @@ class TestSuite {
   /// The tests discovered in the input.
   std::vector<Test> tests;
 
-  TestSuite(MLIRContext *context) : context(context) {}
+  bool listIgnored;
+
+  TestSuite(MLIRContext *context, bool listIgnored)
+      : context(context), listIgnored(listIgnored) {}
   void discoverInModule(ModuleOp module);
 };
 } // namespace
@@ -141,6 +149,10 @@ void TestSuite::discoverInModule(ModuleOp module) {
     test.name = op.getSymNameAttr();
     test.kind = TestKind::Formal;
     test.loc = op.getLoc();
+    if (auto boolAttr = op->getAttrOfType<BoolAttr>("ignore"))
+      test.ignore = boolAttr.getValue();
+    else
+      test.ignore = false;
     test.attrs = op->getDiscardableAttrDictionary();
     tests.push_back(std::move(test));
   });
@@ -150,6 +162,11 @@ void TestSuite::discoverInModule(ModuleOp module) {
 // Tool Implementation
 //===----------------------------------------------------------------------===//
 
+// Check if test should be included in output listing
+bool ignoreTestListing(Test &test, TestSuite &suite) {
+  return !suite.listIgnored && test.ignore;
+}
+
 /// List all the tests in a given module.
 static LogicalResult listTests(TestSuite &suite) {
   // Open the output file for writing.
@@ -164,6 +181,8 @@ static LogicalResult listTests(TestSuite &suite) {
     json.arrayBegin();
     auto guard = make_scope_exit([&] { json.arrayEnd(); });
     for (auto &test : suite.tests) {
+      if (ignoreTestListing(test, suite))
+        continue;
       json.objectBegin();
       auto guard = make_scope_exit([&] { json.objectEnd(); });
       json.attribute("name", test.name.getValue());
@@ -182,13 +201,22 @@ static LogicalResult listTests(TestSuite &suite) {
   }
 
   // Handle regular text output.
-  for (auto &test : suite.tests)
+  for (auto &test : suite.tests) {
+    if (ignoreTestListing(test, suite))
+      continue;
     output->os() << test.name.getValue() << "  " << toString(test.kind) << "  "
                  << test.attrs << "\n";
+  }
   output->keep();
   return success();
 }
 
+void reportIgnored(unsigned numIgnored) {
+  if (numIgnored > 0)
+    WithColor(llvm::errs(), raw_ostream::SAVEDCOLOR, true).get()
+        << ", " << numIgnored << " ignored";
+}
+
 /// Entry point for the circt-test tool. At this point an MLIRContext is
 /// available, all dialects have been registered, and all command line options
 /// have been parsed.
@@ -202,7 +230,7 @@ static LogicalResult execute(MLIRContext *context) {
     return failure();
 
   // Discover all tests in the input.
-  TestSuite suite(context);
+  TestSuite suite(context, opts.listIgnored);
   suite.discoverInModule(*module);
   if (suite.tests.empty()) {
     llvm::errs() << "no tests discovered\n";
@@ -254,7 +282,12 @@ static LogicalResult execute(MLIRContext *context) {
 
   // Run the tests.
   std::atomic<unsigned> numPassed(0);
+  std::atomic<unsigned> numIgnored(0);
   mlir::parallelForEach(context, suite.tests, [&](auto &test) {
+    if (test.ignore) {
+      ++numIgnored;
+      return;
+    }
     // Create the directory in which we are going to run the test.
     SmallString<128> testDir(opts.resultDir);
     llvm::sys::path::append(testDir, test.name.getValue());
@@ -302,18 +335,21 @@ static LogicalResult execute(MLIRContext *context) {
   });
 
   // Print statistics about how many tests passed and failed.
-  assert(numPassed <= suite.tests.size());
-  unsigned numFailed = suite.tests.size() - numPassed;
+  assert((numPassed + numIgnored) <= suite.tests.size());
+  unsigned numFailed = suite.tests.size() - numPassed - numIgnored;
   if (numFailed > 0) {
     WithColor(llvm::errs(), raw_ostream::SAVEDCOLOR, true).get()
         << numFailed << " tests ";
     WithColor(llvm::errs(), raw_ostream::RED, true).get() << "FAILED";
-    llvm::errs() << ", " << numPassed << " passed\n";
+    llvm::errs() << ", " << numPassed << " passed";
+    reportIgnored(numIgnored);
+    llvm::errs() << "\n";
     return failure();
   }
   WithColor(llvm::errs(), raw_ostream::SAVEDCOLOR, true).get()
-      << "all " << numPassed << " tests ";
+      << numPassed << " tests ";
   WithColor(llvm::errs(), raw_ostream::GREEN, true).get() << "passed";
+  reportIgnored(numIgnored);
   llvm::errs() << "\n";
   return success();
 }