btor2aiger: Add test

Based on fifo.sby, running both with and without `btor_aig on`, as well as combined with `vcd_sim on` (after an earlier version had issues when using `vcd_sim off`).

Has both pass and fail checks, so should be able to catch any major issues, although it doesn't fully check equivalence.

Author: KrystalDelusion

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
+