3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-04-05 06:04:06 +00:00

aiger: check supported modes and aigbmc fixes

This commit is contained in:
Jannis Harder 2022-06-14 17:15:32 +02:00
parent 1e1402474a
commit 05d963b0df
3 changed files with 51 additions and 2 deletions

View file

@ -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

View file

@ -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)

View file

@ -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