From ab666b8f663004beece0cf63c7cf6a9fa7c305bf Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Sun, 3 Aug 2025 13:04:08 -0700
Subject: [PATCH 1/2] CI: workaround for installation failure of spot

The recommended installation steps fail since a recent update, owing to
broken signing.  This pulls the .deb packages directly.
---
 .github/workflows/pull-request-checks.yaml | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/.github/workflows/pull-request-checks.yaml b/.github/workflows/pull-request-checks.yaml
index e99fb03e4..cf3ac3cf8 100644
--- a/.github/workflows/pull-request-checks.yaml
+++ b/.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

From 3310cedbd33128e9b54cc0871a04b81ab2136d1b Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Fri, 1 Aug 2025 13:36:10 -0700
Subject: [PATCH 2/2] Two tests for SVA->Buechi->BDD

This adds two further tests for the SVA->Buechi->BDD flow.
---
 .../ebmc-spot/sva-buechi/sequence_and2.bdd.desc      | 11 +++++++++++
 .../ebmc-spot/sva-buechi/sequence_or1.bdd.desc       | 12 ++++++++++++
 regression/verilog/SVA/sequence_and2.sv              |  2 +-
 regression/verilog/SVA/sequence_or1.sv               |  2 +-
 4 files changed, 25 insertions(+), 2 deletions(-)
 create mode 100644 regression/ebmc-spot/sva-buechi/sequence_and2.bdd.desc
 create mode 100644 regression/ebmc-spot/sva-buechi/sequence_or1.bdd.desc

diff --git a/regression/ebmc-spot/sva-buechi/sequence_and2.bdd.desc b/regression/ebmc-spot/sva-buechi/sequence_and2.bdd.desc
new file mode 100644
index 000000000..6995d8f94
--- /dev/null
+++ b/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
+--
diff --git a/regression/ebmc-spot/sva-buechi/sequence_or1.bdd.desc b/regression/ebmc-spot/sva-buechi/sequence_or1.bdd.desc
new file mode 100644
index 000000000..f53b4b91d
--- /dev/null
+++ b/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$
+--
+--
diff --git a/regression/verilog/SVA/sequence_and2.sv b/regression/verilog/SVA/sequence_and2.sv
index f6fb0d467..0ea6fc80f 100644
--- a/regression/verilog/SVA/sequence_and2.sv
+++ b/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;
diff --git a/regression/verilog/SVA/sequence_or1.sv b/regression/verilog/SVA/sequence_or1.sv
index 5f73ac511..9f5cb427a 100644
--- a/regression/verilog/SVA/sequence_or1.sv
+++ b/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;