From ccfacf59406af040a4b8f7089f4040b133f3d2ab Mon Sep 17 00:00:00 2001 From: unlsycn Date: Sun, 24 Nov 2024 17:45:01 +0000 Subject: [PATCH] [circt-test] fix SymbiYosys integration test Signed-off-by: unlsycn --- CMakeLists.txt | 18 ++++++++++++++++++ integration_test/lit.cfg.py | 6 ++++++ integration_test/lit.site.cfg.py.in | 1 + tools/circt-test/circt-test-runner-sby.py | 14 +++++++++----- 4 files changed, 34 insertions(+), 5 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 9e9e31f019cb..e35e4dc1b058 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -525,6 +525,24 @@ else() endif() endif() +#------------------------------------------------------------------------------- +# SymbiYosys Configuration +#------------------------------------------------------------------------------- + +# If SymbiYosys hasn't been explicitly disabled, find it. +option(SBY_DISABLE "Disable the SymbiYosys tests.") +if (SBY_DISABLE) + message(STATUS "Disabling SymbiYosys tests.") +else() + find_program(SBY_PATH "sby") + if(EXISTS ${SBY_PATH}) + message(STATUS "Found SymbiYosys at ${SBY_PATH}.") + else() + set(SBY_PATH "") + message(STATUS "Did not find SymbiYosys.") + endif() +endif() + #------------------------------------------------------------------------------- # Tcl bindings #------------------------------------------------------------------------------- diff --git a/integration_test/lit.cfg.py b/integration_test/lit.cfg.py index 022607617c81..7b116a1d72e5 100644 --- a/integration_test/lit.cfg.py +++ b/integration_test/lit.cfg.py @@ -213,6 +213,12 @@ tools.append(ToolSubst(f"%libz3", config.z3_library)) config.available_features.add('libz3') +# Enable SymbiYosys if it has been detected. +if config.sby_path != "": + tool_dirs.append(config.sby_path) + tools.append('sby') + config.available_features.add('sby') + # Add mlir-cpu-runner if the execution engine is built. if config.mlir_enable_execution_engine: config.available_features.add('mlir-cpu-runner') diff --git a/integration_test/lit.site.cfg.py.in b/integration_test/lit.site.cfg.py.in index 4d63e8ff3b28..65468d823215 100644 --- a/integration_test/lit.site.cfg.py.in +++ b/integration_test/lit.site.cfg.py.in @@ -59,6 +59,7 @@ config.mlir_enable_execution_engine = "@MLIR_ENABLE_EXECUTION_ENGINE@" config.slang_frontend_enabled = "@CIRCT_SLANG_FRONTEND_ENABLED@" config.arcilator_jit_enabled = @ARCILATOR_JIT_ENABLED@ config.driver = "@CIRCT_SOURCE_DIR@/tools/circt-rtl-sim/driver.cpp" +config.sby_path = "@SBY_PATH@" # Support substitution of the tools_dir with user parameters. This is # used when we can't determine the tool dir at configuration time. diff --git a/tools/circt-test/circt-test-runner-sby.py b/tools/circt-test/circt-test-runner-sby.py index 31dfcff0775d..ef9ab28273e5 100755 --- a/tools/circt-test/circt-test-runner-sby.py +++ b/tools/circt-test/circt-test-runner-sby.py @@ -37,9 +37,9 @@ """ # Generate the SymbiYosys script. -script = f""" +script = """ [tasks] - {('\n ').join(tasks)} + {tasks} {options} @@ -47,12 +47,16 @@ smtbmc z3 [script] - read -formal {source_path.name} - prep -top {args.test} + read -formal {source_path_name} + prep -top {test} [files] {source_path} -""" +""".format(tasks='\n '.join(tasks), + options=options, + source_path_name=source_path.name, + test=args.test, + source_path=source_path) with open(script_path, "w") as f: for line in script.strip().splitlines(): f.write(line.strip() + "\n")