From fedfae0e9c1b0e5fdd81b268f7b94e40f08e9349 Mon Sep 17 00:00:00 2001
From: Jannis Harder <me@jix.one>
Date: Wed, 11 May 2022 10:38:54 +0200
Subject: [PATCH 1/5] examples: Fix use of SVA value change expressions

The $stable value change expression cannot be true for a non-x signal in
the initial state. This is now correctly handled by the verific import,
so the dpmem example needs to start assuming `$stable` only after
leaving the initial state.
---
 docs/examples/multiclk/dpmem.sv | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/docs/examples/multiclk/dpmem.sv b/docs/examples/multiclk/dpmem.sv
index 87e4f61..4a920e4 100644
--- a/docs/examples/multiclk/dpmem.sv
+++ b/docs/examples/multiclk/dpmem.sv
@@ -47,9 +47,9 @@ module top (
 	(* gclk *) reg gclk;
 
 	always @(posedge gclk) begin
-		assume ($stable(rc) || $stable(wc));
-
 		if (!init) begin
+			assume ($stable(rc) || $stable(wc));
+
 			if ($rose(rc) && shadow_valid && shadow_addr == $past(ra)) begin
 				assert (shadow_data == rd);
 			end

From ad2c33dd373b8764eb8dff7ad8107632a0bacb88 Mon Sep 17 00:00:00 2001
From: "N. Engelhardt" <nak@yosyshq.com>
Date: Tue, 24 May 2022 11:39:10 +0200
Subject: [PATCH 2/5] docs: add instructions for newer btorsim version required

---
 docs/source/install.rst | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/docs/source/install.rst b/docs/source/install.rst
index 293ee71..50fc45b 100644
--- a/docs/source/install.rst
+++ b/docs/source/install.rst
@@ -142,3 +142,11 @@ http://fmv.jku.at/boolector/
    sudo cp build/bin/{boolector,btor*} /usr/local/bin/
    sudo cp deps/btor2tools/bin/btorsim /usr/local/bin/
 
+To use the ``btor`` engine you additionally need a newer version of btorsim than the boolector setup script builds:
+
+.. code-block:: text
+
+   git clone https://github.com/boolector/btor2tools
+   ./configure.sh
+   cmake .
+   make install

From 3f32deb8c9a8deffeff339c5447464b4f80dea22 Mon Sep 17 00:00:00 2001
From: Jacob Lifshay <programmerjake@gmail.com>
Date: Tue, 24 May 2022 17:51:48 -0700
Subject: [PATCH 3/5] add test for yosys's $divfloor and $modfloor cells

Depends on: https://github.com/YosysHQ/yosys/pull/3335
---
 tests/unsorted/floor_divmod.sby | 44 +++++++++++++++++++++++++++++++++
 1 file changed, 44 insertions(+)
 create mode 100644 tests/unsorted/floor_divmod.sby

diff --git a/tests/unsorted/floor_divmod.sby b/tests/unsorted/floor_divmod.sby
new file mode 100644
index 0000000..53218cc
--- /dev/null
+++ b/tests/unsorted/floor_divmod.sby
@@ -0,0 +1,44 @@
+[options]
+mode bmc
+
+[engines]
+smtbmc
+
+[script]
+read_verilog -icells -formal test.v
+prep -top top
+
+[file test.v]
+module top;
+	wire [7:0] a = $anyconst, b = $anyconst, fdiv, fmod, a2;
+	assign a2 = b * fdiv + fmod;
+
+	\$divfloor #(
+		.A_WIDTH(8),
+		.B_WIDTH(8),
+		.A_SIGNED(1),
+		.B_SIGNED(1),
+		.Y_WIDTH(8),
+	) fdiv_m (
+		.A(a),
+		.B(b),
+		.Y(fdiv)
+	);
+
+	\$modfloor #(
+		.A_WIDTH(8),
+		.B_WIDTH(8),
+		.A_SIGNED(1),
+		.B_SIGNED(1),
+		.Y_WIDTH(8),
+	) fmod_m (
+		.A(a),
+		.B(b),
+		.Y(fmod)
+	);
+
+	always @* begin
+		assume(b != 0);
+		assert(a == a2);
+	end
+endmodule

From a87d21a8020e3f48d0ecdebfa08fe43f0ce7d5fc Mon Sep 17 00:00:00 2001
From: Jacob Lifshay <programmerjake@gmail.com>
Date: Wed, 25 May 2022 03:35:21 -0700
Subject: [PATCH 4/5] add depth 1

---
 tests/unsorted/floor_divmod.sby | 1 +
 1 file changed, 1 insertion(+)

diff --git a/tests/unsorted/floor_divmod.sby b/tests/unsorted/floor_divmod.sby
index 53218cc..df35f8a 100644
--- a/tests/unsorted/floor_divmod.sby
+++ b/tests/unsorted/floor_divmod.sby
@@ -1,5 +1,6 @@
 [options]
 mode bmc
+depth 1
 
 [engines]
 smtbmc

From 41cd8e5b5e6d61b2fb28e00b7aa0616a00348b5d Mon Sep 17 00:00:00 2001
From: "N. Engelhardt" <nak@yosyshq.com>
Date: Wed, 1 Jun 2022 16:51:28 +0200
Subject: [PATCH 5/5] update install instructions for btorsim

---
 docs/source/install.rst | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/docs/source/install.rst b/docs/source/install.rst
index 50fc45b..7fed53c 100644
--- a/docs/source/install.rst
+++ b/docs/source/install.rst
@@ -147,6 +147,8 @@ To use the ``btor`` engine you additionally need a newer version of btorsim than
 .. code-block:: text
 
    git clone https://github.com/boolector/btor2tools
+   cd btor2tools
    ./configure.sh
-   cmake .
-   make install
+   cmake . -DBUILD_SHARED_LIBS=OFF
+   make -j$(nproc)
+   sudo make install