From 2bd44c813a618352801bd129f526ee26ec9352c5 Mon Sep 17 00:00:00 2001 From: Lenny Truong Date: Thu, 31 Oct 2024 16:25:00 -0700 Subject: [PATCH] [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. --- integration_test/circt-test/basic.mlir | 38 +++++++++++++++++++- test/circt-test/basic.mlir | 15 ++++++-- tools/circt-test/circt-test.cpp | 50 ++++++++++++++++++++++---- 3 files changed, 93 insertions(+), 10 deletions(-) diff --git a/integration_test/circt-test/basic.mlir b/integration_test/circt-test/basic.mlir index f40ff867451e..e8cd39c46cec 100644 --- a/integration_test/circt-test/basic.mlir +++ b/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 +} diff --git a/test/circt-test/basic.mlir b/test/circt-test/basic.mlir index ad9e96b43cdf..a8e5cb51dbf1 100644 --- a/test/circt-test/basic.mlir +++ b/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: ] diff --git a/tools/circt-test/circt-test.cpp b/tools/circt-test/circt-test.cpp index cb01c81e41d5..258c44b0c3a1 100644 --- a/tools/circt-test/circt-test.cpp +++ b/tools/circt-test/circt-test.cpp @@ -71,6 +71,9 @@ struct Options { cl::opt json{"json", cl::desc("Emit test list as JSON array"), cl::init(false), cl::cat(cat)}; + cl::opt listIgnored{"list-ignored", cl::desc("List ignored tests"), + cl::init(false), cl::cat(cat)}; + cl::opt 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 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("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 numPassed(0); + std::atomic 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(); }