Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Option to use btor2aiger to generate aig files from btor #266

Open
wants to merge 8 commits into
base: main
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -44,6 +44,8 @@ else
sed 's|##yosys-sys-path##|sys.path += [os.path.dirname(__file__) + p for p in ["/share/python3", "/../share/yosys/python3"]]|;' < sbysrc/sby.py > $(DESTDIR)$(PREFIX)/bin/sby
chmod +x $(DESTDIR)$(PREFIX)/bin/sby
endif
cp tools/btor2aig_yw/btor2aig_yw.py $(DESTDIR)$(PREFIX)/bin/btor2aig_yw
chmod +x $(DESTDIR)$(PREFIX)/bin/btor2aig_yw

.PHONY: check_cad_suite run_ci

Expand Down
20 changes: 18 additions & 2 deletions sbysrc/sby_core.py
Original file line number Diff line number Diff line change
Expand Up @@ -1137,8 +1137,11 @@ def instance_hierarchy_error_callback(retcode):
print("delete -output", file=f)
print("dffunmap", file=f)
print("stat", file=f)
print("write_btor {}-i design_{m}.info -ywmap design_btor.ywb design_{m}.btor".format("-c " if self.opt_mode == "cover" else "", m=model_name), file=f)
print("write_btor -s {}-i design_{m}_single.info -ywmap design_btor_single.ywb design_{m}_single.btor".format("-c " if self.opt_mode == "cover" else "", m=model_name), file=f)
btor_flags = ""
if self.opt_mode == "cover": btor_flags += "-c "
if self.opt_btor_aig: btor_flags += "-x "
print("write_btor {}-i design_{m}.info -ywmap design_btor.ywb design_{m}.btor".format(btor_flags, m=model_name), file=f)
print("write_btor -s {}-i design_{m}_single.info -ywmap design_btor_single.ywb design_{m}_single.btor".format(btor_flags, m=model_name), file=f)

proc = SbyProc(
self,
Expand All @@ -1150,6 +1153,18 @@ def instance_hierarchy_error_callback(retcode):

return [proc]

if model_name == "aig" and self.opt_btor_aig:
btor_model = "btor_nomem"
proc = SbyProc(
self,
"btor_aig",
self.model(btor_model),
f"cd {self.workdir}/model; btor2aig_yw design_{btor_model}.btor design_btor.ywb"
)
proc.checkretcode = True

return [proc]

if model_name == "aig":
with open(f"{self.workdir}/model/design_aiger.ys", "w") as f:
print(f"# running in {self.workdir}/model/", file=f)
Expand Down Expand Up @@ -1279,6 +1294,7 @@ def handle_non_engine_options(self):
self.handle_bool_option("aigfolds", False)
self.handle_bool_option("aigvmap", False)
self.handle_bool_option("aigsyms", False)
self.handle_bool_option("btor_aig", False)

self.handle_str_option("smtc", None)
self.handle_int_option("skip", None)
Expand Down
10 changes: 8 additions & 2 deletions sbysrc/sby_engine_abc.py
Original file line number Diff line number Diff line change
Expand Up @@ -166,7 +166,10 @@ def output_callback(line):
match = re.match(r"Writing CEX for output ([0-9]+) to engine_[0-9]+/(.*)\.aiw", line)
if match:
output = int(match[1])
prop = aiger_props[output]
try:
prop = aiger_props[output]
except IndexError:
prop = None
if prop:
prop.status = "FAIL"
task.status_db.set_task_property_status(prop, data=dict(source="abc pdr", engine=f"engine_{engine_idx}"))
Expand All @@ -185,7 +188,10 @@ def output_callback(line):
match = re.match(r"^Proved output +([0-9]+) in frame +-?[0-9]+", line)
if match:
output = int(match[1])
prop = aiger_props[output]
try:
prop = aiger_props[output]
except IndexError:
prop = None
if prop:
prop.status = "PASS"
task.status_db.set_task_property_status(prop, data=dict(source="abc pdr", engine=f"engine_{engine_idx}"))
Expand Down
204 changes: 204 additions & 0 deletions tests/unsorted/btor2aig.sby
Original file line number Diff line number Diff line change
@@ -0,0 +1,204 @@
[tasks]
bmc
prove
prove_f: prove
prove_v: prove_f prove
bmc_b2a: bmc btor_aig
prove_b2a: prove btor_aig
prove_f_b2a: prove_f prove btor_aig
prove_v_b2a: prove_v prove_f prove btor_aig

[options]
prove:
mode prove
--

bmc:
mode bmc
--

prove_f: expect fail
prove_v: vcd_sim on
btor_aig: btor_aig on

[engines]
bmc: abc bmc3
prove: abc --keep-going pdr

[script]
prove_f: read -define NO_FULL_SKIP=1
read -formal fifo.sv
prep -top fifo

[file fifo.sv]
// address generator/counter
module addr_gen
#( parameter MAX_DATA=16
) ( input en, clk, rst,
output reg [3:0] addr
);
initial addr <= 0;

// async reset
// increment address when enabled
always @(posedge clk or posedge rst)
if (rst)
addr <= 0;
else if (en) begin
if (addr == MAX_DATA-1)
addr <= 0;
else
addr <= addr + 1;
end
endmodule

// Define our top level fifo entity
module fifo
#( parameter MAX_DATA=16
) ( input wen, ren, clk, rst,
input [7:0] wdata,
output [7:0] rdata,
output [4:0] count,
output full, empty
);
wire wskip, rskip;
reg [4:0] data_count;

// fifo storage
// async read, sync write
wire [3:0] waddr, raddr;
reg [7:0] data [MAX_DATA-1:0];
always @(posedge clk)
if (wen)
data[waddr] <= wdata;
assign rdata = data[raddr];
// end storage

// addr_gen for both write and read addresses
addr_gen #(.MAX_DATA(MAX_DATA))
fifo_writer (
.en (wen || wskip),
.clk (clk ),
.rst (rst),
.addr (waddr)
);

addr_gen #(.MAX_DATA(MAX_DATA))
fifo_reader (
.en (ren || rskip),
.clk (clk ),
.rst (rst),
.addr (raddr)
);

// status signals
initial data_count <= 0;

always @(posedge clk or posedge rst) begin
if (rst)
data_count <= 0;
else if (wen && !ren && data_count < MAX_DATA)
data_count <= data_count + 1;
else if (ren && !wen && data_count > 0)
data_count <= data_count - 1;
end

assign full = data_count == MAX_DATA;
assign empty = (data_count == 0) && ~rst;
assign count = data_count;

// overflow protection
`ifndef NO_FULL_SKIP
// write while full => overwrite oldest data, move read pointer
assign rskip = wen && !ren && data_count >= MAX_DATA;
// read while empty => read invalid data, keep write pointer in sync
assign wskip = ren && !wen && data_count == 0;
`else
assign rskip = 0;
assign wskip = 0;
`endif // NO_FULL_SKIP

`ifdef FORMAL
// observers
wire [4:0] addr_diff;
assign addr_diff = waddr >= raddr
? waddr - raddr
: waddr + MAX_DATA - raddr;

// tests
always @(posedge clk) begin
if (~rst) begin
// waddr and raddr can only be non zero if reset is low
w_nreset: cover (waddr || raddr);

// count never more than max
a_oflow: assert (count <= MAX_DATA);
a_oflow2: assert (waddr < MAX_DATA);

// count should be equal to the difference between writer and reader address
a_count_diff: assert (count == addr_diff
|| count == MAX_DATA && addr_diff == 0);

// count should only be able to increase or decrease by 1
a_counts: assert (count == 0
|| count == $past(count)
|| count == $past(count) + 1
|| count == $past(count) - 1);

// read/write addresses can only increase (or stay the same)
a_raddr: assert (raddr == 0
|| raddr == $past(raddr)
|| raddr == $past(raddr + 1));
a_waddr: assert (waddr == 0
|| waddr == $past(waddr)
|| waddr == $past(waddr + 1));

// full and empty work as expected
a_full: assert (!full || count == MAX_DATA);
w_full: cover (wen && !ren && count == MAX_DATA-1);
a_empty: assert (!empty || count == 0);
w_empty: cover (ren && !wen && count == 1);

// reading/writing non zero values
w_nzero_write: cover (wen && wdata);
w_nzero_read: cover (ren && rdata);
end else begin
// waddr and raddr are zero while reset is high
a_reset: assert (!waddr && !raddr);
w_reset: cover (rst);

// outputs are zero while reset is high
a_zero_out: assert (!empty && !full && !count);
end
end

// if we have verific we can also do the following additional tests
// read/write enables enable
ap_raddr2: assert property (@(posedge clk) disable iff (rst) ren |=> $changed(raddr));
ap_waddr2: assert property (@(posedge clk) disable iff (rst) wen |=> $changed(waddr));

// read/write needs enable UNLESS full/empty
ap_raddr3: assert property (@(posedge clk) disable iff (rst) !ren && !full |=> $stable(raddr));
ap_waddr3: assert property (@(posedge clk) disable iff (rst) !wen && !empty |=> $stable(waddr));

// use block formatting for w_underfill so it's easier to describe in docs
// and is more readily comparable with the non SVA implementation
property write_skip;
@(posedge clk) disable iff (rst)
!wen |=> $changed(waddr);
endproperty
w_underfill: cover property (write_skip);

// look for an overfill where the value in memory changes
// the change in data makes certain that the value is overriden
let d_change = (wdata != rdata);
property read_skip;
@(posedge clk) disable iff (rst)
!ren && d_change |=> $changed(raddr);
endproperty
w_overfill: cover property (read_skip);

`endif // FORMAL

endmodule

Loading
Loading