SystemVerilog queue benchmarks

regression/ebmc/Makefile

@@ -3,7 +3,10 @@ default: test
 TEST_PL = ../../lib/cbmc/regression/test.pl
 
 test:
-	@$(TEST_PL) -e -p -c ../../../src/ebmc/ebmc
+	@$(TEST_PL) -e -p -c ../../../src/ebmc/ebmc -X buechi
+
+test-buechi:
+	@$(TEST_PL) -e -p -c ../../../src/ebmc/ebmc -I buechi
 
 test-z3:
-	@$(TEST_PL) -e -p -c "../../../src/ebmc/ebmc --z3" -X broken-smt-backend
+	@$(TEST_PL) -e -p -c "../../../src/ebmc/ebmc --z3" -X broken-smt-backend -X buechi

regression/ebmc/queues/queue_depth1.desc

@@ -0,0 +1,8 @@
+CORE buechi
+queue_depth1.sv
+--bdd --buechi
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc/queues/queue_depth1.sv

@@ -0,0 +1,19 @@
+module queue(
+  input in_data, in_valid,
+  output out_data, out_valid,
+  input clk);
+
+  reg data;
+  reg valid;
+
+  initial valid = 0;
+
+  always_ff @(posedge clk)
+    {data, valid} <= {in_data, in_valid};
+
+  assign out_data = data;
+  assign out_valid = valid;
+
+  assert property (@(posedge clk) in_valid implies s_eventually out_valid);
+
+endmodule

regression/ebmc/queues/queue_depth2.desc

@@ -0,0 +1,8 @@
+CORE buechi
+queue_depth2.sv
+--bdd --buechi
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc/queues/queue_depth2.sv

@@ -0,0 +1,21 @@
+module queue(
+  input in_data, in_valid,
+  output out_data, out_valid,
+  input clk);
+
+  reg data0, data1;
+  reg valid0, valid1;
+
+  initial {valid0, valid1} = 2'b00;
+
+  always_ff @(posedge clk) begin
+    {data0, valid0} <= {in_data, in_valid};
+    {data1, valid1} <= {data0, valid0};
+  end
+
+  assign out_data = data1;
+  assign out_valid = valid1;
+
+  assert property (@(posedge clk) in_valid implies s_eventually out_valid);
+
+endmodule

regression/ebmc/queues/queue_depthN.desc

@@ -0,0 +1,8 @@
+CORE buechi
+queue_depthN.sv
+--bdd --buechi
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc/queues/queue_depthN.sv

@@ -0,0 +1,24 @@
+module queue
+  #(parameter N = 10)
+  (input in_data, in_valid,
+  output out_data, out_valid,
+  input clk);
+
+  reg [N-1:0] data;
+  reg [N-1:0] valid;
+
+  initial valid = {N{1'b0}};
+
+  always_ff @(posedge clk)
+    {data[0], valid[0]} <= {in_data, in_valid};
+
+  always_ff @(posedge clk)
+    for(integer i=1; i<N; i++)
+      {data[i], valid[i]} <= {data[i-1], valid[i-1]};
+
+  assign out_data = data[N-1];
+  assign out_valid = valid[N-1];
+
+  assert property (@(posedge clk) in_valid implies s_eventually out_valid);
+
+endmodule

regression/ebmc/queues/queue_with_simple_stallN.desc

@@ -0,0 +1,8 @@
+CORE buechi
+queue_with_simple_stallN.sv
+--bdd --buechi
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc/queues/queue_with_simple_stallN.sv

@@ -0,0 +1,30 @@
+module queue
+  #(parameter N = 10)
+  (input in_data, in_valid, in_stall,
+  output out_data, out_valid, out_stall,
+  input clk);
+
+  reg [N-1:0] data;
+  reg [N-1:0] valid;
+
+  initial valid = {N{1'b0}};
+
+  always_ff @(posedge clk)
+    if(!out_stall)
+      {data[0], valid[0]} <= {in_data, in_valid};
+
+  always_ff @(posedge clk)
+    for(integer i=1; i<N; i++)
+      if(!out_stall)
+        {data[i], valid[i]} <= {data[i-1], valid[i-1]};
+
+  assign out_data = data[N-1];
+  assign out_valid = valid[N-1];
+  assign out_stall = in_stall;
+
+  // we need to assume we are not stalled indefinitively
+  assume property (@(posedge clk) s_eventually !in_stall);
+
+  assert property (@(posedge clk) (in_valid && !out_stall) implies s_eventually out_valid);
+
+endmodule