c4 repair does something (not correct)

benchmarks/fpga-debugging/axis-async-fifo-c4/axis_async_fifo.v

@@ -131,13 +131,13 @@ always @(posedge output_clk) begin
 end
 
 // write
+assign wr_ptr_next = wr_ptr + 1;
 always @(posedge input_clk) begin
     if (input_rst_sync3) begin
         wr_ptr <= 0;
         wr_ptr_gray <= 0;
     end else if (write) begin
         mem[wr_ptr[ADDR_WIDTH-1:0]] <= data_in;
-        wr_ptr_next = wr_ptr + 1;
         wr_ptr <= wr_ptr_next;
         wr_ptr_gray <= wr_ptr_next ^ (wr_ptr_next >> 1);
     end
@@ -155,13 +155,13 @@ always @(posedge input_clk) begin
 end
 
 // read
+assign rd_ptr_next = rd_ptr + 1;
 always @(posedge output_clk) begin
     if (output_rst_sync3) begin
         rd_ptr <= 0;
         rd_ptr_gray <= 0;
     end else if (read) begin
         data_out_reg <= mem[rd_ptr[ADDR_WIDTH-1:0]];
-        rd_ptr_next = rd_ptr + 1;
         rd_ptr <= rd_ptr_next;
         rd_ptr_gray <= rd_ptr_next ^ (rd_ptr_next >> 1);
     end

benchmarks/fpga-debugging/axis-async-fifo-c4/axis_async_fifo_bug_c4.v

@@ -131,13 +131,13 @@ always @(posedge output_clk) begin
 end
 
 // write
+assign wr_ptr_next = wr_ptr + 1;
 always @(posedge input_clk) begin
     if (input_rst_sync3) begin
         wr_ptr <= 0;
         wr_ptr_gray <= 0;
     end else if (write) begin
         mem[wr_ptr[ADDR_WIDTH-1:0]] <= data_in;
-        wr_ptr_next = wr_ptr + 1;
         wr_ptr <= wr_ptr_next;
         wr_ptr_gray <= wr_ptr_next ^ (wr_ptr_next >> 1);
     end
@@ -155,13 +155,13 @@ always @(posedge input_clk) begin
 end
 
 // read
+assign rd_ptr_next = rd_ptr + 1;
 always @(posedge output_clk) begin
     if (output_rst_sync3) begin
         rd_ptr <= 0;
         rd_ptr_gray <= 0;
     end else if (read) begin
         data_out_reg <= mem[rd_ptr[ADDR_WIDTH-1:0]];
-        rd_ptr_next = rd_ptr + 1;
         rd_ptr <= rd_ptr_next;
         rd_ptr_gray <= rd_ptr_next ^ (rd_ptr_next >> 1);
     end

benchmarks/fpga-debugging/axis-async-fifo-c4/project.toml

@@ -0,0 +1,14 @@
+[project]
+directory = "."
+sources = ["axis_async_fifo.v", "axis_fifo_wrapper.v", "axis_register.v"]
+toplevel = "axis_fifo_wrapper"
+
+[[bugs]]
+name = "c4"
+original = "axis_async_fifo.v"
+buggy = "axis_async_fifo_bug_c4.v"
+
+[[testbenches]]
+name = "csv"
+table = "tb.csv"
+

test.py

@@ -41,6 +41,7 @@
 d12_dir = fpga_debug_dir / "axis-fifo-d12"
 d11_dir = fpga_debug_dir / "axis-frame-fifo-d11"
 d8_dir = fpga_debug_dir / "axis-switch-d8"
+c4_dir = fpga_debug_dir / "axis-async-fifo-c4"
 
 
 def run_synth(project_path: Path, bug: str, testbench: str = None, solver='z3', init='any', incremental=True, timeout=None, old_synthesizer=False):
@@ -158,6 +159,12 @@ def test_d8(self):
         # TODO: enable some instrumentation in generate blocks
         self.synth_cannot_repair(d8_dir, "d8", solver="yices2", init="zero", incremental=True, timeout=60)
 
+    def test_c4(self):
+        """ AXIS Async Fifo (we turned the reset into a sync reset) signals ready too early, needs one guard in boolean condition """
+        changes = self.synth_success(c4_dir, "c4", solver="yices2", init="zero", incremental=True, timeout=60, max_changes=10)
+        # TODO: this solution is not correct, way too many changes
+        self.assertEqual(changes, 9)
+
 class TestCirFixBenchmarksIncremental(SynthesisTest):
     """ Makes sure that we can handle all benchmarks from the cirfix paper in incremental mode. """
     solver: str = 'bitwuzla'