SystemVerilog queue benchmarks

This adds SystemVerilog benchmarks that implement various queues.

Author: kroening

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,17 @@
+module queue(
+  input data_in, valid_in,
+  output data_out, valid_out,
+  input clk);
+
+  reg data;
+  reg valid;
+
+  always_ff @(posedge clk)
+    {data, valid} <= {data_in, valid_in};
+
+  assign data_out = data;
+  assign valid_out = valid;
+
+  assert property (@(posedge clk) valid_in implies s_eventually valid_out);
+
+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,19 @@
+module queue(
+  input data_in, valid_in,
+  output data_out, valid_out,
+  input clk);
+
+  reg data0, data1;
+  reg valid0, valid1;
+
+  always_ff @(posedge clk) begin
+    {data0, valid0} <= {data_in, valid_in};
+    {data1, valid1} <= {data0, valid0};
+  end
+
+  assign data_out = data1;
+  assign valid_out = valid1;
+
+  assert property (@(posedge clk) valid_in implies s_eventually valid_out);
+
+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,22 @@
+module queue
+  #(parameter N = 10)
+  (input data_in, valid_in,
+  output data_out, valid_out,
+  input clk);
+
+  reg data[N];
+  reg valid[N];
+
+  always_ff @(posedge clk)
+    {data[0], valid[0]} <= {data_in, valid_in};
+
+  always_ff @(posedge clk)
+    for(integer i=1; i<N; i++)
+      {data[i], valid[i]} <= {data[i-1], valid[i-1]};
+
+  assign data_out = data[N-1];
+  assign valid_out = valid[N-1];
+
+  assert property (@(posedge clk) valid_in implies s_eventually valid_out);
+
+endmodule