mirror of https://github.com/llvm/circt.git
[circt-test] Add simple SymbiYosys test runner (#7756)
Extend circt-test to export the input MLIR file as Verilog and then run all discovered tests through a simple SymbiYosys runner script. This is currently very rigid: all tests are always run, and they all run through the exact same runner script. In the future, we'll want to add filtering mechanisms to include and exclude tests, and pick among multiple runner scripts for each test. Also add a basic integration test that builds an adder from discrete logic gates and then verifies it through multiple `verif.formal` ops. To run this you need to have SymbiYosys installed. In the future we'll want to have `circt-bmc` and other CIRCT-based verification tools available as runners as well.
This commit is contained in:
Fabian Schuiki
GitHub
parent
f2fbf63152
commit
9b4cc2c70f
|
|
@ -10,6 +10,8 @@ set(CIRCT_INTEGRATION_TEST_DEPENDS
|
|||
circt-rtl-sim
|
||||
circt-lec
|
||||
circt-bmc
|
||||
circt-test
|
||||
circt-test-runner-sby
|
||||
firtool
|
||||
hlstool
|
||||
ibistool
|
||||
|
|
|
|||
|
|
@ -0,0 +1,115 @@
|
|||
// RUN: circt-test %s -r circt-test-runner-sby.py | FileCheck %s
|
||||
// REQUIRES: sby
|
||||
|
||||
// CHECK: all 6 tests passed
|
||||
|
||||
hw.module @FullAdder(in %a: i1, in %b: i1, in %ci: i1, out s: i1, out co: i1) {
|
||||
%0 = comb.xor %a, %b : i1
|
||||
%1 = comb.xor %0, %ci : i1
|
||||
%2 = comb.and %a, %b : i1
|
||||
%3 = comb.and %0, %ci : i1
|
||||
%4 = comb.or %2, %3 : i1
|
||||
hw.output %1, %4 : i1, i1
|
||||
}
|
||||
|
||||
hw.module @CustomAdderWithCarry(in %a: i4, in %b: i4, in %ci: i1, out z: i4, out co: i1) {
|
||||
%a0 = comb.extract %a from 0 : (i4) -> i1
|
||||
%a1 = comb.extract %a from 1 : (i4) -> i1
|
||||
%a2 = comb.extract %a from 2 : (i4) -> i1
|
||||
%a3 = comb.extract %a from 3 : (i4) -> i1
|
||||
%b0 = comb.extract %b from 0 : (i4) -> i1
|
||||
%b1 = comb.extract %b from 1 : (i4) -> i1
|
||||
%b2 = comb.extract %b from 2 : (i4) -> i1
|
||||
%b3 = comb.extract %b from 3 : (i4) -> i1
|
||||
%adder0.s, %adder0.co = hw.instance "adder0" @FullAdder(a: %a0: i1, b: %b0: i1, ci: %ci: i1) -> (s: i1, co: i1)
|
||||
%adder1.s, %adder1.co = hw.instance "adder1" @FullAdder(a: %a1: i1, b: %b1: i1, ci: %adder0.co: i1) -> (s: i1, co: i1)
|
||||
%adder2.s, %adder2.co = hw.instance "adder2" @FullAdder(a: %a2: i1, b: %b2: i1, ci: %adder1.co: i1) -> (s: i1, co: i1)
|
||||
%adder3.s, %adder3.co = hw.instance "adder3" @FullAdder(a: %a3: i1, b: %b3: i1, ci: %adder2.co: i1) -> (s: i1, co: i1)
|
||||
%z = comb.concat %adder3.s, %adder2.s, %adder1.s, %adder0.s : i1, i1, i1, i1
|
||||
hw.output %z, %adder3.co : i4, i1
|
||||
}
|
||||
|
||||
hw.module @CustomAdder(in %a: i4, in %b: i4, out z: i4) {
|
||||
%false = hw.constant false
|
||||
%z, %co = hw.instance "adder" @CustomAdderWithCarry(a: %a: i4, b: %b: i4, ci: %false: i1) -> (z: i4, co: i1)
|
||||
hw.output %z : i4
|
||||
}
|
||||
|
||||
verif.formal @ZeroLhs {
|
||||
%c0_i4 = hw.constant 0 : i4
|
||||
%x = verif.symbolic_value : i4
|
||||
%z = hw.instance "dut" @CustomAdder(a: %c0_i4: i4, b: %x: i4) -> (z: i4)
|
||||
%eq = comb.icmp eq %z, %x : i4
|
||||
verif.assert %eq : i1
|
||||
}
|
||||
|
||||
verif.formal @ZeroRhs {
|
||||
%c0_i4 = hw.constant 0 : i4
|
||||
%x = verif.symbolic_value : i4
|
||||
%z = hw.instance "dut" @CustomAdder(a: %x: i4, b: %c0_i4: i4) -> (z: i4)
|
||||
%eq = comb.icmp eq %z, %x : i4
|
||||
verif.assert %eq : i1
|
||||
}
|
||||
|
||||
verif.formal @CustomAdderWorks {
|
||||
%a = verif.symbolic_value : i4
|
||||
%b = verif.symbolic_value : i4
|
||||
|
||||
// Check against reference adder.
|
||||
%z0 = hw.instance "dut" @CustomAdder(a: %a: i4, b: %b: i4) -> (z: i4)
|
||||
%z1 = comb.add %a, %b : i4
|
||||
%eq = comb.icmp eq %z0, %z1 : i4
|
||||
verif.assert %eq : i1
|
||||
|
||||
// Show this can compute 5 somehow.
|
||||
%c5_i4 = hw.constant 5 : i4
|
||||
%0 = comb.icmp eq %z0, %c5_i4 : i4
|
||||
%1 = comb.icmp ne %a, %b : i4
|
||||
%2 = comb.and %0, %1 : i1
|
||||
verif.cover %2 : i1
|
||||
}
|
||||
|
||||
hw.module @ALU(in %a: i4, in %b: i4, in %sub: i1, out z: i4) {
|
||||
%sub_mask = comb.replicate %sub : (i1) -> i4
|
||||
%b2 = comb.xor %b, %sub_mask : i4
|
||||
%z, %co = hw.instance "adder" @CustomAdderWithCarry(a: %a: i4, b: %b2: i4, ci: %sub: i1) -> (z: i4, co: i1)
|
||||
hw.output %z : i4
|
||||
}
|
||||
|
||||
verif.formal @ALUCanAdd {
|
||||
%a = verif.symbolic_value : i4
|
||||
%b = verif.symbolic_value : i4
|
||||
%false = hw.constant false
|
||||
%z0 = hw.instance "dut" @ALU(a: %a: i4, b: %b: i4, sub: %false: i1) -> (z: i4)
|
||||
%z1 = comb.add %a, %b : i4
|
||||
%eq = comb.icmp eq %z0, %z1 : i4
|
||||
verif.assert %eq : i1
|
||||
}
|
||||
|
||||
verif.formal @ALUCanSub {
|
||||
%a = verif.symbolic_value : i4
|
||||
%b = verif.symbolic_value : i4
|
||||
%true = hw.constant true
|
||||
%z0 = hw.instance "dut" @ALU(a: %a: i4, b: %b: i4, sub: %true: i1) -> (z: i4)
|
||||
%z1 = comb.sub %a, %b : i4
|
||||
%eq = comb.icmp eq %z0, %z1 : i4
|
||||
verif.assert %eq : i1
|
||||
}
|
||||
|
||||
verif.formal @ALUWorks {
|
||||
%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 match.
|
||||
%eq = comb.icmp eq %z0, %z1 : i4
|
||||
verif.assert %eq : i1
|
||||
}
|
||||
|
|
@ -80,7 +80,7 @@ tool_dirs = [
|
|||
tools = [
|
||||
'arcilator', 'circt-opt', 'circt-translate', 'firtool', 'circt-rtl-sim.py',
|
||||
'equiv-rtl.sh', 'handshake-runner', 'hlstool', 'ibistool', 'circt-lec',
|
||||
'circt-bmc'
|
||||
'circt-bmc', 'circt-test', 'circt-test-runner-sby.py'
|
||||
]
|
||||
|
||||
# Enable python if its path was configured
|
||||
|
|
|
|||
|
|
@ -1,11 +1,15 @@
|
|||
set(libs
|
||||
CIRCTComb
|
||||
CIRCTExportVerilog
|
||||
CIRCTHW
|
||||
CIRCTOM
|
||||
CIRCTSeq
|
||||
CIRCTSim
|
||||
CIRCTSV
|
||||
CIRCTSVTransforms
|
||||
CIRCTVerif
|
||||
CIRCTVerifToSV
|
||||
CIRCTVerifTransforms
|
||||
|
||||
MLIRLLVMDialect
|
||||
MLIRArithDialect
|
||||
|
|
@ -24,3 +28,6 @@ target_link_libraries(circt-test PRIVATE ${libs})
|
|||
|
||||
llvm_update_compile_flags(circt-test)
|
||||
mlir_check_all_link_libraries(circt-test)
|
||||
|
||||
configure_file(circt-test-runner-sby.py ${CIRCT_TOOLS_DIR}/circt-test-runner-sby.py)
|
||||
add_custom_target(circt-test-runner-sby SOURCES ${CIRCT_TOOLS_DIR}/circt-test-runner-sby.py)
|
||||
|
|
|
|||
|
|
@ -0,0 +1,55 @@
|
|||
#!/usr/bin/env python3
|
||||
from pathlib import Path
|
||||
import argparse
|
||||
import shlex
|
||||
import subprocess
|
||||
import sys
|
||||
|
||||
parser = argparse.ArgumentParser()
|
||||
parser.add_argument("verilog")
|
||||
parser.add_argument("-t", "--test")
|
||||
parser.add_argument("-d", "--directory")
|
||||
args = parser.parse_args()
|
||||
|
||||
directory = Path(args.directory)
|
||||
source_path = Path(args.verilog)
|
||||
script_path = directory / "script.sby"
|
||||
|
||||
# Generate the SymbiYosys script.
|
||||
script = f"""
|
||||
[tasks]
|
||||
cover
|
||||
bmc
|
||||
induction
|
||||
|
||||
[options]
|
||||
cover:
|
||||
mode cover
|
||||
--
|
||||
bmc:
|
||||
mode bmc
|
||||
--
|
||||
induction:
|
||||
mode prove
|
||||
--
|
||||
|
||||
[engines]
|
||||
smtbmc z3
|
||||
|
||||
[script]
|
||||
read -formal {source_path.name}
|
||||
prep -top {args.test}
|
||||
|
||||
[files]
|
||||
{source_path}
|
||||
"""
|
||||
with open(script_path, "w") as f:
|
||||
for line in script.strip().splitlines():
|
||||
f.write(line.strip() + "\n")
|
||||
|
||||
# Run SymbiYosys.
|
||||
cmd = ["sby", "-f", script_path]
|
||||
sys.stderr.write("# " + shlex.join(str(c) for c in cmd) + "\n")
|
||||
sys.stderr.flush()
|
||||
result = subprocess.call(cmd)
|
||||
sys.exit(result)
|
||||
|
|
@ -11,14 +11,18 @@
|
|||
//
|
||||
//===----------------------------------------------------------------------===//
|
||||
|
||||
#include "circt/Conversion/ExportVerilog.h"
|
||||
#include "circt/Conversion/VerifToSV.h"
|
||||
#include "circt/Dialect/Comb/CombDialect.h"
|
||||
#include "circt/Dialect/HW/HWDialect.h"
|
||||
#include "circt/Dialect/OM/OMDialect.h"
|
||||
#include "circt/Dialect/SV/SVDialect.h"
|
||||
#include "circt/Dialect/SV/SVPasses.h"
|
||||
#include "circt/Dialect/Seq/SeqDialect.h"
|
||||
#include "circt/Dialect/Sim/SimDialect.h"
|
||||
#include "circt/Dialect/Verif/VerifDialect.h"
|
||||
#include "circt/Dialect/Verif/VerifOps.h"
|
||||
#include "circt/Dialect/Verif/VerifPasses.h"
|
||||
#include "circt/Support/JSON.h"
|
||||
#include "circt/Support/Version.h"
|
||||
#include "mlir/Dialect/Arith/IR/Arith.h"
|
||||
|
|
@ -26,17 +30,20 @@
|
|||
#include "mlir/Dialect/Func/IR/FuncOps.h"
|
||||
#include "mlir/Dialect/LLVMIR/LLVMDialect.h"
|
||||
#include "mlir/Dialect/SCF/IR/SCF.h"
|
||||
#include "mlir/IR/Threading.h"
|
||||
#include "mlir/Parser/Parser.h"
|
||||
#include "mlir/Pass/PassManager.h"
|
||||
#include "mlir/Support/FileUtilities.h"
|
||||
#include "llvm/ADT/ScopeExit.h"
|
||||
#include "llvm/Support/CommandLine.h"
|
||||
#include "llvm/Support/FileSystem.h"
|
||||
#include "llvm/Support/InitLLVM.h"
|
||||
#include "llvm/Support/Path.h"
|
||||
#include "llvm/Support/Program.h"
|
||||
#include "llvm/Support/SourceMgr.h"
|
||||
#include "llvm/Support/ToolOutputFile.h"
|
||||
#include "llvm/Support/WithColor.h"
|
||||
|
||||
#include <string>
|
||||
|
||||
using namespace llvm;
|
||||
using namespace mlir;
|
||||
using namespace circt;
|
||||
|
|
@ -63,6 +70,19 @@ struct Options {
|
|||
|
||||
cl::opt<bool> json{"json", cl::desc("Emit test list as JSON array"),
|
||||
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)};
|
||||
|
||||
cl::opt<bool> verifyPasses{
|
||||
"verify-each",
|
||||
cl::desc("Run the verifier after each transformation pass"),
|
||||
cl::init(true), cl::cat(cat)};
|
||||
|
||||
cl::opt<std::string> runner{
|
||||
"r", cl::desc("Program to run individual tests"), cl::value_desc("bin"),
|
||||
cl::init("circt-test-runner-sby.py"), cl::cat(cat)};
|
||||
};
|
||||
Options opts;
|
||||
|
||||
|
|
@ -193,6 +213,108 @@ static LogicalResult execute(MLIRContext *context) {
|
|||
if (opts.listTests)
|
||||
return listTests(suite);
|
||||
|
||||
// Create the output directory where we keep all the run data.
|
||||
if (auto error = llvm::sys::fs::create_directory(opts.resultDir)) {
|
||||
WithColor::error() << "cannot create result directory `" << opts.resultDir
|
||||
<< "`: " << error.message() << "\n";
|
||||
return failure();
|
||||
}
|
||||
|
||||
// Open the Verilog file for writing.
|
||||
SmallString<128> verilogPath(opts.resultDir);
|
||||
llvm::sys::path::append(verilogPath, "design.sv");
|
||||
std::string errorMessage;
|
||||
auto verilogFile = openOutputFile(verilogPath, &errorMessage);
|
||||
if (!verilogFile) {
|
||||
WithColor::error() << errorMessage;
|
||||
return failure();
|
||||
}
|
||||
|
||||
// Generate Verilog output.
|
||||
PassManager pm(context);
|
||||
pm.enableVerifier(opts.verifyPasses);
|
||||
pm.addPass(verif::createLowerFormalToHWPass());
|
||||
pm.addNestedPass<hw::HWModuleOp>(createLowerVerifToSVPass());
|
||||
pm.addNestedPass<hw::HWModuleOp>(sv::createHWLegalizeModulesPass());
|
||||
pm.addNestedPass<hw::HWModuleOp>(sv::createPrettifyVerilogPass());
|
||||
pm.addPass(createExportVerilogPass(verilogFile->os()));
|
||||
if (failed(pm.run(*module)))
|
||||
return failure();
|
||||
verilogFile->keep();
|
||||
|
||||
// Find the runner binary in the search path. Otherwise assume it is a binary
|
||||
// we can run as is.
|
||||
auto findResult = llvm::sys::findProgramByName(opts.runner);
|
||||
if (!findResult) {
|
||||
WithColor::error() << "cannot find runner `" << opts.runner
|
||||
<< "`: " << findResult.getError().message() << "\n";
|
||||
return failure();
|
||||
}
|
||||
auto &runner = findResult.get();
|
||||
|
||||
// Run the tests.
|
||||
std::atomic<unsigned> numPassed(0);
|
||||
mlir::parallelForEach(context, suite.tests, [&](auto &test) {
|
||||
// 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());
|
||||
if (auto error = llvm::sys::fs::create_directory(testDir)) {
|
||||
mlir::emitError(UnknownLoc::get(context))
|
||||
<< "cannot create test directory `" << testDir
|
||||
<< "`: " << error.message() << "\n";
|
||||
return;
|
||||
}
|
||||
|
||||
// Assemble a path for the test runner log file and truncate it.
|
||||
SmallString<128> logPath(testDir);
|
||||
llvm::sys::path::append(logPath, "run.log");
|
||||
{
|
||||
std::error_code ec;
|
||||
raw_fd_ostream trunc(logPath, ec);
|
||||
}
|
||||
|
||||
// Assemble the runner arguments.
|
||||
SmallVector<StringRef> args;
|
||||
args.push_back(runner);
|
||||
args.push_back(verilogPath);
|
||||
args.push_back("-t");
|
||||
args.push_back(test.name.getValue());
|
||||
args.push_back("-d");
|
||||
args.push_back(testDir);
|
||||
|
||||
// Execute the test runner.
|
||||
std::string errorMessage;
|
||||
auto result =
|
||||
llvm::sys::ExecuteAndWait(runner, args, /*Env=*/std::nullopt,
|
||||
/*Redirects=*/{"", logPath, logPath},
|
||||
/*SecondsToWait=*/0,
|
||||
/*MemoryLimit=*/0, &errorMessage);
|
||||
if (result < 0) {
|
||||
mlir::emitError(UnknownLoc::get(context))
|
||||
<< "cannot execute runner: " << errorMessage;
|
||||
} else if (result > 0) {
|
||||
auto d = mlir::emitError(test.loc)
|
||||
<< "test " << test.name.getValue() << " failed";
|
||||
d.attachNote() << "see `" << logPath << "`";
|
||||
} else {
|
||||
++numPassed;
|
||||
}
|
||||
});
|
||||
|
||||
// Print statistics about how many tests passed and failed.
|
||||
assert(numPassed <= suite.tests.size());
|
||||
unsigned numFailed = suite.tests.size() - numPassed;
|
||||
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";
|
||||
return failure();
|
||||
}
|
||||
WithColor(llvm::errs(), raw_ostream::SAVEDCOLOR, true).get()
|
||||
<< "all " << numPassed << " tests ";
|
||||
WithColor(llvm::errs(), raw_ostream::GREEN, true).get() << "passed";
|
||||
llvm::errs() << "\n";
|
||||
return success();
|
||||
}
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue