terapines
/
circt
mirror of https://github.com/llvm/circt.git
2
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

[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.
This commit is contained in:
Lenny Truong 2024-10-31 16:25:00 -07:00 committed by GitHub
parent 6405aa7453
commit 2bd44c813a
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
3 changed files with 93 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

38
integration_test/circt-test/basic.mlir
View File

@ -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
}

15
test/circt-test/basic.mlir
View File

@ -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: ]

50
tools/circt-test/circt-test.cpp
View File

@ -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 @@ public:
/// 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 @@ public:
/// 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();
}