Option to use btor2aiger to generate aig files from btor

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
 

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)

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}"))

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
+