Merge pull request #1218 from diffblue/sva-buechi-and-or-tests

Two tests for SVA->Buechi->BDD

Author: tautschnig

regression/ebmc-spot/sva-buechi/sequence_and2.bdd.desc

@@ -0,0 +1,11 @@
+CORE
+../../verilog/SVA/sequence_and2.sv
+--buechi --bdd
+\[.*\] \(1 and \(##2 1\)\) \|-> main\.x == 2: PROVED$
+\[.*\] \(\(##2 1\) and 1\) \|-> main\.x == 2: PROVED$
+\[.*\] \(\(##2 1\) and 1\) #-# main\.x == 2: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/sva-buechi/sequence_or1.bdd.desc

@@ -0,0 +1,12 @@
+CORE
+../../verilog/SVA/sequence_or1.sv
+--buechi --bdd
+^\[main\.p0\] main\.x == 0 or main\.x == 1: PROVED$
+^\[main\.p1\] strong\(main\.x == 0 or main\.x == 1\): PROVED$
+^\[main\.p2\] main\.x == 0 or \(nexttime main\.x == 1\): PROVED$
+^\[main\.p3\] \(nexttime main\.x == 1\) or main\.x == 1: PROVED$
+^\[main\.p4\] \(main\.x == 0 or main\.x != 10\) |=> main\.x == 1: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+--

regression/verilog/SVA/sequence_and2.sv

@@ -1,6 +1,6 @@
 module main(input clk);
 
-  reg [31:0] x = 0;
+  reg [7:0] x = 0;
 
   always @(posedge clk)
     x<=x+1;

regression/verilog/SVA/sequence_or1.sv

@@ -1,6 +1,6 @@
 module main(input clk);
 
-  reg [31:0] x = 0;
+  reg [7:0] x = 0;
 
   always @(posedge clk)
     x<=x+1;