From: Jannis Harder Date: Tue, 14 Jun 2022 15:15:32 +0000 (+0200) Subject: aiger: check supported modes and aigbmc fixes X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=05d963b0df224767c8fc0e09e9d93821218e1cfa;p=SymbiYosys.git aiger: check supported modes and aigbmc fixes --- diff --git a/sbysrc/sby_engine_aiger.py b/sbysrc/sby_engine_aiger.py index 4665691..2850d46 100644 --- a/sbysrc/sby_engine_aiger.py +++ b/sbysrc/sby_engine_aiger.py @@ -28,16 +28,25 @@ def run(mode, task, engine_idx, engine): for o, a in opts: task.error("Unexpected AIGER engine options.") + status_2 = "UNKNOWN" + if solver_args[0] == "suprove": + if mode not in ["live", "prove"]: + task.error("The aiger solver 'suprove' is only supported in live and prove modes.") if mode == "live" and (len(solver_args) == 1 or solver_args[1][0] != "+"): solver_args.insert(1, "+simple_liveness") solver_cmd = " ".join([task.exe_paths["suprove"]] + solver_args[1:]) elif solver_args[0] == "avy": + if mode != "prove": + task.error("The aiger solver 'avy' is only supported in prove mode.") solver_cmd = " ".join([task.exe_paths["avy"], "--cex", "-"] + solver_args[1:]) elif solver_args[0] == "aigbmc": - solver_cmd = " ".join([task.exe_paths["aigbmc"]] + solver_args[1:]) + if mode != "bmc": + task.error("The aiger solver 'aigbmc' is only supported in bmc mode.") + solver_cmd = " ".join([task.exe_paths["aigbmc"], str(task.opt_depth - 1)] + solver_args[1:]) + status_2 = "PASS" # aigbmc outputs status 2 when BMC passes else: task.error(f"Invalid solver command {solver_args[0]}.") @@ -76,7 +85,7 @@ def run(mode, task, engine_idx, engine): print(line, file=aiw_file) if line == "0": proc_status = "PASS" if line == "1": proc_status = "FAIL" - if line == "2": proc_status = "UNKNOWN" + if line == "2": proc_status = status_2 return None diff --git a/sbysrc/sby_mode_bmc.py b/sbysrc/sby_mode_bmc.py index fd128ed..85ef882 100644 --- a/sbysrc/sby_mode_bmc.py +++ b/sbysrc/sby_mode_bmc.py @@ -39,6 +39,10 @@ def run(task): import sby_engine_abc sby_engine_abc.run("bmc", task, engine_idx, engine) + elif engine[0] == "aiger": + import sby_engine_aiger + sby_engine_aiger.run("bmc", task, engine_idx, engine) + elif engine[0] == "btor": import sby_engine_btor sby_engine_btor.run("bmc", task, engine_idx, engine) diff --git a/tests/unsorted/bmc_len.sby b/tests/unsorted/bmc_len.sby new file mode 100644 index 0000000..938a1bd --- /dev/null +++ b/tests/unsorted/bmc_len.sby @@ -0,0 +1,36 @@ +[tasks] +smtbmc_pass: smtbmc pass +smtbmc_fail: smtbmc fail +aigbmc_pass: aigbmc pass +aigbmc_fail: aigbmc fail +btormc_pass: btormc pass +btormc_fail: btormc fail +abc_pass: abc pass +abc_fail: abc fail + +[options] +mode bmc +pass: expect pass +fail: expect fail +pass: depth 5 +fail: depth 6 + +[engines] +smtbmc: smtbmc boolector +aigbmc: aiger aigbmc +btormc: btor btormc +abc: abc bmc3 + +[script] +read -formal top.sv +prep -top top + +[file top.sv] +module top(input clk); + reg [7:0] counter = 0; + + always @(posedge clk) begin + counter <= counter + 1; + assert (counter < 4); + end +endmodule