Merge f17a6e118a into 17b74bf3d6

Makefile

@@ -52,6 +52,8 @@ else
 		-e "s|##yosys-release-version##|release_version = '$(YOSYS_RELEASE_VERSION)'|;" < 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
 

sbysrc/sby_core.py

@@ -1142,8 +1142,11 @@ class SbyTask(SbyConfig):
                 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)
+                btor_flags = ""
-                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)
+                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,
@@ -1155,6 +1158,18 @@ class SbyTask(SbyConfig):
 
             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)
@@ -1284,6 +1299,7 @@ class SbyTask(SbyConfig):
         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)

sbysrc/sby_engine_abc.py

@@ -176,7 +176,10 @@ def run(mode, task, engine_idx, engine):
             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}"))
@@ -195,7 +198,10 @@ def run(mode, task, engine_idx, engine):
         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}"))

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
+

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<type>[cil])(?P<input>\d+) (?P<path>.*?)(\[(?P<offset>\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())