diff --git a/Makefile b/Makefile index 28f05657..fd66497d 100644 --- a/Makefile +++ b/Makefile @@ -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 diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index c366e1be..99631f55 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -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, @@ -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) @@ -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) diff --git a/sbysrc/sby_engine_abc.py b/sbysrc/sby_engine_abc.py index 1fabe6fa..bd9d51d3 100644 --- a/sbysrc/sby_engine_abc.py +++ b/sbysrc/sby_engine_abc.py @@ -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}")) @@ -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}")) diff --git a/tests/unsorted/btor2aig.sby b/tests/unsorted/btor2aig.sby new file mode 100644 index 00000000..c080b499 --- /dev/null +++ b/tests/unsorted/btor2aig.sby @@ -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 + diff --git a/tools/btor2aig_yw/btor2aig_yw.py b/tools/btor2aig_yw/btor2aig_yw.py new file mode 100644 index 00000000..c8c727d2 --- /dev/null +++ b/tools/btor2aig_yw/btor2aig_yw.py @@ -0,0 +1,136 @@ +#!/usr/bin/env python3 +from __future__ import annotations + +import argparse +import asyncio +import json +import re +from pathlib import Path + +def arg_parser(): + parser = argparse.ArgumentParser() + + parser.add_argument( + "btor_file", + type=Path + ) + + parser.add_argument( + "ywb_file", + type=Path + ) + + parser.add_argument( + "-d", "--dest", + dest="dest", + required=False, + type=Path + ) + + return parser + +def fix_path(path: str) -> list[str]: + if path[0] == '$': + fixed = [path] + else: + fixed = [f"\\{s}" for s in path.replace('[','.[').split('.')] + return fixed + +async def main() -> None: + args = arg_parser().parse_args() + + work_dir: Path = args.dest or Path() + + proc = await asyncio.create_subprocess_shell( + f"btor2aiger {args.btor_file}", + stdout=asyncio.subprocess.PIPE + ) + + data = True + + # output aig + aig_file = work_dir / "design_aiger.aig" + aigf = open(aig_file, mode="wb") + data = await proc.stdout.readline() + aig_header = data.decode() + while data: + aigf.write(data) + data = await proc.stdout.readline() + if b'i0' in data: + break + end_pos = data.find(b'i0') + aigf.write(data[:end_pos]) + aigf.close() + + # initialize yw aiger map + aig_MILOA = aig_header.split() + ywa = { + "version": "Yosys Witness Aiger map", + "generator": "btor2aig_yw.py", + "latch_count": int(aig_MILOA[3]), + "input_count": int(aig_MILOA[2]), + "clocks": [], + "inputs": [], + "seqs": [], + "inits": [], + "latches": [], + "asserts": [], + "assumes": [] + } + + # output aim & build ywa + aim_file = work_dir / "design_aiger.aim" + aimf = open(aim_file, mode="w") + data = data[end_pos:] + while data: + # decode data + string = data.decode().rstrip() + pattern = r"(?P[cil])(?P\d+) (?P.*?)(\[(?P\d+)\])?$" + m = re.match(pattern, string) + md = m.groupdict() + md['input'] = int(md['input']) + if md['type'] == 'i': + md['type'] = 'input' + elif md['type'] == 'c': + md['type'] = 'clk' + elif md['type'] == 'l': + md['type'] = 'latch' + md['input'] += ywa['input_count'] + else: + raise ValueError(f"Unknown type identifier {md['type']!r}") + for k in ['input', 'offset']: + if md[k]: + md[k] = int(md[k]) + else: + md[k] = 0 + + # output to aim + if md['type'] in ['input', 'latch']: + print("{type} {input} {offset} {path}".format(**md), file=aimf) + + # update ywa + md_type = md.pop('type') + md['path'] = fix_path(md['path']) + if md_type == 'clk': + md['edge'] = "posedge" # always? + ywa['clocks'].append(md) + elif md_type == 'input': + ywa['inputs'].append(md) + elif md_type == 'latch': + ywa['inits'].append(md) + + # get next line + data = await proc.stdout.readline() + aimf.close() + + with open(args.ywb_file, mode='r') as f: + data = json.load(f) + ywa['asserts'].extend(data['asserts']) + ywa['assumes'].extend(data['assumes']) + + + with open(work_dir / "design_aiger.ywa", mode="w") as f: + json.dump(ywa, f, indent=2) + +if __name__ == "__main__": + asyncio.run(main())