Merge pull request #260 from diffblue/clock24h

ebmc: add lexicographic ranking function test

Author: tautschnig

regression/ebmc/ranking-function/clock24h.day.desc

@@ -0,0 +1,7 @@
+CORE
+clock24h.sv
+--property main.property.p_day --ranking-function "{23-hours,59-minutes,59-seconds}"
+^\[main\.property\.p_day\] .*: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--

regression/ebmc/ranking-function/clock24h.hour.desc

@@ -0,0 +1,7 @@
+CORE
+clock24h.sv
+--property main.property.p_hour --ranking-function "{59-minutes,59-seconds}"
+^\[main\.property\.p_hour\] .*: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--

regression/ebmc/ranking-function/clock24h.minute.desc

@@ -0,0 +1,7 @@
+CORE
+clock24h.sv
+--property main.property.p_minute --ranking-function "59-seconds"
+^\[main\.property\.p_minute\] .*: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--

regression/ebmc/ranking-function/clock24h.sv

@@ -0,0 +1,43 @@
+module main(input clk);
+
+  reg [7:0] seconds, minutes, hours;
+  reg minute_tick, hour_tick, day_tick;
+
+  wire second_tick = 1;
+
+  initial begin
+    seconds = 0;
+    minutes = 0;
+    hours = 0;
+    day_tick = 0;
+  end
+
+  always @(posedge clk) begin
+    minute_tick <= 0;
+    hour_tick <= 0;
+    day_tick <= 0;
+    if(second_tick) begin
+      if(seconds == 59) begin
+        seconds <= 0;
+        minute_tick <= 1;
+        if(minutes == 59) begin
+          minutes <= 0;
+          hour_tick <= 1;
+          if(hours == 23) begin
+            hours <= 0;
+            day_tick <= 1;
+          end else
+            hours <= hours + 1;
+        end else
+          minutes <= minutes + 1;
+      end else
+        seconds <= seconds + 1;
+    end
+  end
+
+  // expected to pass
+  p_minute: assert property (eventually minute_tick);
+  p_hour: assert property (eventually hour_tick);
+  p_day: assert property (eventually day_tick);
+
+endmodule