[circt-test] fix SymbiYosys integration test (#7886)

#7756 adds the SymbiYosys test runner and requires the `sby` feature, 
but did not add the corresponding available feature in `lit.cfg.py`, so 
this test never seems to run, and #7763 introduces a syntax error, a 
backslash in the f-string expression part, in the Python script.

Unlike #7884, there is no need to modify PATH variable for the script 
since `sby` should be in the PATH if we can check it in CMake.

Signed-off-by: unlsycn <unlsycn@unlsycn.com>

.github/workflows/nightlyIntegrationTests.yml

@@ -19,7 +19,7 @@ jobs:
     # John and re-run the job.
     runs-on: ["self-hosted", "1ES.Pool=1ES-CIRCT-builds", "linux"]
     container:
-      image: ghcr.io/circt/images/circt-integration-test:v18.1
+      image: ghcr.io/circt/images/circt-integration-test:v18.2
       volumes:
         - /mnt:/__w/circt
     strategy:

.github/workflows/shortIntegrationTests.yml

@@ -29,7 +29,7 @@ jobs:
     # John and re-run the job.
     runs-on: ["self-hosted", "1ES.Pool=1ES-CIRCT-builds", "linux"]
     container:
-      image: ghcr.io/circt/images/circt-integration-test:v18.1
+      image: ghcr.io/circt/images/circt-integration-test:v18.2
       volumes:
         - /mnt:/__w/circt
     strategy:

CMakeLists.txt

@@ -509,6 +509,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
 #-------------------------------------------------------------------------------

integration_test/lit.cfg.py

@@ -217,6 +217,12 @@ if config.z3_library != "":
   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-runner if the execution engine is built.
 if config.mlir_enable_execution_engine:
   config.available_features.add('mlir-runner')

integration_test/lit.site.cfg.py.in

@@ -60,6 +60,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.

tools/circt-test/circt-test-runner-sby.py

@@ -37,9 +37,9 @@ for task in tasks:
 """
 
 # Generate the SymbiYosys script.
-script = f"""
+script = """
   [tasks]
-  {('\n  ').join(tasks)}
+  {tasks}
 
 {options}
 
@@ -47,12 +47,16 @@ script = f"""
   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")