Merge pull request #809 from diffblue/ring_buffer_induction

Strengthen ring_buffer induction test

Author: tautschnig

regression/ebmc/k-induction/ring_buffer.desc

@@ -0,0 +1,10 @@
+CORE
+ring_buffer.sv
+--k-induction
+^\[ring_buffer\.assume\.1\] always \(ring_buffer\.empty \|-> !ring_buffer\.read\): ASSUMED$
+^\[ring_buffer\.assume\.2\] always \(ring_buffer\.full \|-> !ring_buffer\.write\): ASSUMED$
+^\[ring_buffer\.p0\] always \(ring_buffer\.writeptr - ring_buffer\.readptr & 15\) == ring_buffer\.count\[3:0\]: PROVED$
+^\[ring_buffer\.p1\] always ring_buffer\.count <= 16: PROVED$
+^\[ring_buffer\.p2\] always ring_buffer.count != 17: INCONCLUSIVE$
+^EXIT=10$
+^SIGNAL=0$

regression/ebmc/ring_buffer_induction/ring_buffer.sv renamed to regression/ebmc/k-induction/ring_buffer.sv

@@ -16,13 +16,14 @@ module ring_buffer(input clk, input read, input write);
 
   end
 
-  wire full=count==15;
+  wire full=count==16;
   wire empty=count==0;
 
   assume property (empty |-> !read);
   assume property (full |-> !write);
 
-  assert property (((writeptr-readptr)&'b1111)==count);
+  p0: assert property (((writeptr-readptr)&'b1111)==count[3:0]);
+  p1: assert property (count <= 16);
+  p2: assert property (count != 17);
 
 endmodule
-