Closed andrew-research closed 2 years ago
I tried to run some of the formal tests from https://github.com/ZipCPU/wb2axip/tree/master/bench/formal (@ZipCPU) using the oss-cad-suite https://github.com/YosysHQ/oss-cad-suite-build/releases/tag/2022-03-30 release. Unfortunately the tests failed during cover testing with the following output:
make axilsingle ... SBY 12:23:33 [axilsingle_cvr] engine_0: ## 0:00:00 Solver: boolector SBY 12:23:33 [axilsingle_cvr] engine_0: ## 0:00:00 Checking cover reachability in step 0.. SBY 12:23:33 [axilsingle_cvr] engine_0: ## 0:00:00 Checking cover reachability in step 1.. SBY 12:23:34 [axilsingle_cvr] engine_0: ## 0:00:00 Checking cover reachability in step 2.. SBY 12:23:34 [axilsingle_cvr] engine_0: ## 0:00:00 Checking cover reachability in step 3.. SBY 12:23:34 [axilsingle_cvr] engine_0: ## 0:00:01 Checking cover reachability in step 4.. SBY 12:23:34 [axilsingle_cvr] engine_0: ## 0:00:01 Checking cover reachability in step 5.. Traceback (most recent call last): File "/opt/oss-cad-suite/2022-03-30/libexec/sby", line 469, in <module> task_retcode = run_task(task) File "/opt/oss-cad-suite/2022-03-30/libexec/sby", line 442, in run_task task.run(setupmode) File "/opt/oss-cad-suite/2022-03-30/libexec/../share/yosys/python3/sby_core.py", line 712, in run self.taskloop() File "/opt/oss-cad-suite/2022-03-30/libexec/../share/yosys/python3/sby_core.py", line 281, in taskloop proc.poll() File "/opt/oss-cad-suite/2022-03-30/libexec/../share/yosys/python3/sby_core.py", line 175, in poll self.handle_output(outs) File "/opt/oss-cad-suite/2022-03-30/libexec/../share/yosys/python3/sby_core.py", line 107, in handle_output line = self.output_callback(line) File "/opt/oss-cad-suite/2022-03-30/libexec/../share/yosys/python3/sby_engine_smtbmc.py", line 196, in output_callback prop = task.design_hierarchy.find_property_by_cellname(cell_name, trans_dict=smt2_trans) File "/opt/oss-cad-suite/2022-03-30/libexec/../share/yosys/python3/sby_design.py", line 100, in find_property_by_cellname raise KeyError(f"No such property: {smt2_name}") NameError: name 'smt2_name' is not defined make: *** [Makefile:678: axilsingle_cvr/PASS] Error 1
After removing the smt2_name issue with a small modification in the python (#152) the issue that triggered the error obviously still exists:
make axilsingle ... SBY 12:33:06 [axilsingle_cvr] engine_0: ## 0:00:00 Solver: boolector SBY 12:33:06 [axilsingle_cvr] engine_0: ## 0:00:00 Checking cover reachability in step 0.. SBY 12:33:07 [axilsingle_cvr] engine_0: ## 0:00:00 Checking cover reachability in step 1.. SBY 12:33:07 [axilsingle_cvr] engine_0: ## 0:00:00 Checking cover reachability in step 2.. SBY 12:33:07 [axilsingle_cvr] engine_0: ## 0:00:01 Checking cover reachability in step 3.. SBY 12:33:07 [axilsingle_cvr] engine_0: ## 0:00:01 Checking cover reachability in step 4.. SBY 12:33:08 [axilsingle_cvr] engine_0: ## 0:00:01 Checking cover reachability in step 5.. Traceback (most recent call last): File "/opt/oss-cad-suite/2022-03-30/libexec/sby", line 469, in <module> task_retcode = run_task(task) File "/opt/oss-cad-suite/2022-03-30/libexec/sby", line 442, in run_task task.run(setupmode) File "/opt/oss-cad-suite/2022-03-30/libexec/../share/yosys/python3/sby_core.py", line 712, in run self.taskloop() File "/opt/oss-cad-suite/2022-03-30/libexec/../share/yosys/python3/sby_core.py", line 281, in taskloop proc.poll() File "/opt/oss-cad-suite/2022-03-30/libexec/../share/yosys/python3/sby_core.py", line 175, in poll self.handle_output(outs) File "/opt/oss-cad-suite/2022-03-30/libexec/../share/yosys/python3/sby_core.py", line 107, in handle_output line = self.output_callback(line) File "/opt/oss-cad-suite/2022-03-30/libexec/../share/yosys/python3/sby_engine_smtbmc.py", line 196, in output_callback prop = task.design_hierarchy.find_property_by_cellname(cell_name, trans_dict=smt2_trans) File "/opt/oss-cad-suite/2022-03-30/libexec/../share/yosys/python3/sby_design.py", line 100, in find_property_by_cellname raise KeyError(f"No such property: {cell_name}") KeyError: 'No such property: $cover$faxil_master.v:763$1076' make: *** [Makefile:678: axilsingle_cvr/PASS] Error 1
However, running the same sby file through an older version of sby https://github.com/YosysHQ/sby/commit/69ef444464ef6b79ce4279234898e355d4c41e44 succeeds:
sby -f axilsingle.sby ... SBY 12:38:43 [axilsingle_cvr] engine_0: ## 0:00:00 Solver: boolector SBY 12:38:43 [axilsingle_cvr] engine_0: ## 0:00:00 Checking cover reachability in step 0.. SBY 12:38:43 [axilsingle_cvr] engine_0: ## 0:00:00 Checking cover reachability in step 1.. SBY 12:38:44 [axilsingle_cvr] engine_0: ## 0:00:00 Checking cover reachability in step 2.. SBY 12:38:44 [axilsingle_cvr] engine_0: ## 0:00:01 Checking cover reachability in step 3.. SBY 12:38:44 [axilsingle_cvr] engine_0: ## 0:00:01 Checking cover reachability in step 4.. SBY 12:38:45 [axilsingle_cvr] engine_0: ## 0:00:01 Checking cover reachability in step 5.. SBY 12:38:45 [axilsingle_cvr] engine_0: ## 0:00:02 Reached cover statement at faxil_master.v:763.26-765.41 in step 5. SBY 12:38:45 [axilsingle_cvr] engine_0: ## 0:00:02 Reached cover statement at faxil_master.v:753.26-755.41 in step 5. SBY 12:38:45 [axilsingle_cvr] engine_0: ## 0:00:02 Writing trace to VCD file: engine_0/trace0.vcd SBY 12:38:46 [axilsingle_cvr] engine_0: ## 0:00:02 Writing trace to Verilog testbench: engine_0/trace0_tb.v SBY 12:38:46 [axilsingle_cvr] engine_0: ## 0:00:02 Writing trace to constraints file: engine_0/trace0.smtc SBY 12:38:46 [axilsingle_cvr] engine_0: ## 0:00:03 Checking cover reachability in step 5.. SBY 12:38:46 [axilsingle_cvr] engine_0: ## 0:00:03 Reached cover statement at faxil_master.v:753.26-755.41 in step 5. ... SBY 12:39:19 [axilsingle_cvr] engine_0: ## 0:00:36 Reached cover statement at axilsingle.v:702.13-703.23 in step 11. SBY 12:39:20 [axilsingle_cvr] engine_0: ## 0:00:37 Writing trace to VCD file: engine_0/trace33.vcd SBY 12:39:20 [axilsingle_cvr] engine_0: ## 0:00:37 Writing trace to Verilog testbench: engine_0/trace33_tb.v SBY 12:39:20 [axilsingle_cvr] engine_0: ## 0:00:37 Writing trace to constraints file: engine_0/trace33.smtc SBY 12:39:21 [axilsingle_cvr] engine_0: ## 0:00:37 Checking cover reachability in step 11.. SBY 12:39:21 [axilsingle_cvr] engine_0: ## 0:00:38 Reached cover statement at axilsingle.v:708.13-709.45 in step 11. SBY 12:39:21 [axilsingle_cvr] engine_0: ## 0:00:38 Reached cover statement at axilsingle.v:705.13-706.24 in step 11. SBY 12:39:21 [axilsingle_cvr] engine_0: ## 0:00:38 Writing trace to VCD file: engine_0/trace34.vcd SBY 12:39:22 [axilsingle_cvr] engine_0: ## 0:00:39 Writing trace to Verilog testbench: engine_0/trace34_tb.v SBY 12:39:22 [axilsingle_cvr] engine_0: ## 0:00:39 Writing trace to constraints file: engine_0/trace34.smtc SBY 12:39:22 [axilsingle_cvr] engine_0: ## 0:00:39 Status: passed SBY 12:39:22 [axilsingle_cvr] engine_0: finished (returncode=0) SBY 12:39:22 [axilsingle_cvr] engine_0: Status returned by engine: pass SBY 12:39:22 [axilsingle_cvr] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:40 (40) SBY 12:39:22 [axilsingle_cvr] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:43 (43) SBY 12:39:22 [axilsingle_cvr] summary: engine_0 (smtbmc boolector) returned pass SBY 12:39:22 [axilsingle_cvr] DONE (PASS, rc=0)
I tried to run some of the formal tests from https://github.com/ZipCPU/wb2axip/tree/master/bench/formal (@ZipCPU) using the oss-cad-suite https://github.com/YosysHQ/oss-cad-suite-build/releases/tag/2022-03-30 release. Unfortunately the tests failed during cover testing with the following output:
After removing the smt2_name issue with a small modification in the python (#152) the issue that triggered the error obviously still exists:
However, running the same sby file through an older version of sby https://github.com/YosysHQ/sby/commit/69ef444464ef6b79ce4279234898e355d4c41e44 succeeds: