Two tests for SVA->Buechi->BDD

.github/workflows/pull-request-checks.yaml

@@ -175,10 +175,12 @@ jobs:
           DEBIAN_FRONTEND: noninteractive
         run: |
           # spot
-          wget -q -O - https://www.lrde.epita.fr/repo/debian.gpg | sudo apt-key add -
-          sudo sh -c 'echo "deb http://www.lrde.epita.fr/repo/debian/ stable/" >> /etc/apt/sources.list'
-          sudo apt-get update
-          sudo apt-get install spot
+          SPOT_VERSION=2.14.1
+          wget https://www.lre.epita.fr/repo/debian/stable/libbddx0_${SPOT_VERSION}.0-1_amd64.deb
+          wget https://www.lre.epita.fr/repo/debian/stable/libspotgen0_${SPOT_VERSION}.0-1_amd64.deb
+          wget https://www.lre.epita.fr/repo/debian/stable/libspot0_${SPOT_VERSION}.0-1_amd64.deb
+          wget https://www.lre.epita.fr/repo/debian/stable/spot_${SPOT_VERSION}.0-1_amd64.deb
+          sudo dpkg -i libbddx0_${SPOT_VERSION}.0-1_amd64.deb libspotgen0_${SPOT_VERSION}.0-1_amd64.deb libspot0_${SPOT_VERSION}.0-1_amd64.deb spot_${SPOT_VERSION}.0-1_amd64.deb
       - name: Confirm ltl2tgba is available and log the version installed
         run: ltl2tgba --version
       - name: Get the ebmc binary

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;