From 3291d86ec38031e191ec1e7e5e8ddfa74b77cb7c Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Thu, 24 Nov 2022 18:49:44 +0000
Subject: Squashed 'picorv32/' content from commit f00a88c

git-subtree-dir: picorv32
git-subtree-split: f00a88c36eaab478b64ee27d8162e421049bcc66
---
 scripts/smtbmc/.gitignore        |  18 ++++
 scripts/smtbmc/axicheck.sh       |  13 +++
 scripts/smtbmc/axicheck.v        | 210 +++++++++++++++++++++++++++++++++++++++
 scripts/smtbmc/axicheck2.sh      |  12 +++
 scripts/smtbmc/axicheck2.smtc    |   2 +
 scripts/smtbmc/axicheck2.v       | 147 +++++++++++++++++++++++++++
 scripts/smtbmc/mulcmp.sh         |  12 +++
 scripts/smtbmc/mulcmp.v          |  87 ++++++++++++++++
 scripts/smtbmc/notrap_validop.sh |  13 +++
 scripts/smtbmc/notrap_validop.v  |  67 +++++++++++++
 scripts/smtbmc/opcode.v          | 104 +++++++++++++++++++
 scripts/smtbmc/tracecmp.gtkw     |  71 +++++++++++++
 scripts/smtbmc/tracecmp.sh       |  12 +++
 scripts/smtbmc/tracecmp.smtc     |  12 +++
 scripts/smtbmc/tracecmp.v        | 109 ++++++++++++++++++++
 scripts/smtbmc/tracecmp2.sh      |  12 +++
 scripts/smtbmc/tracecmp2.smtc    |   2 +
 scripts/smtbmc/tracecmp2.v       | 196 ++++++++++++++++++++++++++++++++++++
 scripts/smtbmc/tracecmp3.sh      |  17 ++++
 scripts/smtbmc/tracecmp3.v       | 135 +++++++++++++++++++++++++
 20 files changed, 1251 insertions(+)
 create mode 100644 scripts/smtbmc/.gitignore
 create mode 100644 scripts/smtbmc/axicheck.sh
 create mode 100644 scripts/smtbmc/axicheck.v
 create mode 100644 scripts/smtbmc/axicheck2.sh
 create mode 100644 scripts/smtbmc/axicheck2.smtc
 create mode 100644 scripts/smtbmc/axicheck2.v
 create mode 100644 scripts/smtbmc/mulcmp.sh
 create mode 100644 scripts/smtbmc/mulcmp.v
 create mode 100644 scripts/smtbmc/notrap_validop.sh
 create mode 100644 scripts/smtbmc/notrap_validop.v
 create mode 100644 scripts/smtbmc/opcode.v
 create mode 100644 scripts/smtbmc/tracecmp.gtkw
 create mode 100644 scripts/smtbmc/tracecmp.sh
 create mode 100644 scripts/smtbmc/tracecmp.smtc
 create mode 100644 scripts/smtbmc/tracecmp.v
 create mode 100644 scripts/smtbmc/tracecmp2.sh
 create mode 100644 scripts/smtbmc/tracecmp2.smtc
 create mode 100644 scripts/smtbmc/tracecmp2.v
 create mode 100644 scripts/smtbmc/tracecmp3.sh
 create mode 100644 scripts/smtbmc/tracecmp3.v

(limited to 'scripts/smtbmc')

diff --git a/scripts/smtbmc/.gitignore b/scripts/smtbmc/.gitignore
new file mode 100644
index 0000000..1ce906e
--- /dev/null
+++ b/scripts/smtbmc/.gitignore
@@ -0,0 +1,18 @@
+tracecmp.smt2
+tracecmp.yslog
+tracecmp2.smt2
+tracecmp2.yslog
+tracecmp3.blif
+tracecmp3.cex
+tracecmp3.smt2
+tracecmp3.yslog
+axicheck.smt2
+axicheck.yslog
+axicheck2.smt2
+axicheck2.yslog
+notrap_validop.smt2
+notrap_validop.yslog
+mulcmp.smt2
+mulcmp.yslog
+output.vcd
+output.smtc
diff --git a/scripts/smtbmc/axicheck.sh b/scripts/smtbmc/axicheck.sh
new file mode 100644
index 0000000..732b3b8
--- /dev/null
+++ b/scripts/smtbmc/axicheck.sh
@@ -0,0 +1,13 @@
+#!/bin/bash
+
+set -ex
+
+yosys -ql axicheck.yslog \
+	-p 'read_verilog -formal -norestrict -assume-asserts ../../picorv32.v' \
+	-p 'read_verilog -formal axicheck.v' \
+	-p 'prep -top testbench -nordff' \
+	-p 'write_smt2 -wires axicheck.smt2'
+
+yosys-smtbmc -t 50 -s boolector --dump-vcd output.vcd --dump-smtc output.smtc axicheck.smt2
+# yosys-smtbmc -t 50 -i -s boolector --dump-vcd output.vcd --dump-smtc output.smtc axicheck.smt2
+
diff --git a/scripts/smtbmc/axicheck.v b/scripts/smtbmc/axicheck.v
new file mode 100644
index 0000000..80eda48
--- /dev/null
+++ b/scripts/smtbmc/axicheck.v
@@ -0,0 +1,210 @@
+module testbench (
+	input         clk,
+	output        trap,
+
+	output        mem_axi_awvalid,
+	input         mem_axi_awready,
+	output [31:0] mem_axi_awaddr,
+	output [ 2:0] mem_axi_awprot,
+
+	output        mem_axi_wvalid,
+	input         mem_axi_wready,
+	output [31:0] mem_axi_wdata,
+	output [ 3:0] mem_axi_wstrb,
+
+	input         mem_axi_bvalid,
+	output        mem_axi_bready,
+
+	output        mem_axi_arvalid,
+	input         mem_axi_arready,
+	output [31:0] mem_axi_araddr,
+	output [ 2:0] mem_axi_arprot,
+
+	input         mem_axi_rvalid,
+	output        mem_axi_rready,
+	input  [31:0] mem_axi_rdata
+);
+	reg resetn = 0;
+
+	always @(posedge clk)
+		resetn <= 1;
+
+	picorv32_axi #(
+		.ENABLE_COUNTERS(1),
+		.ENABLE_COUNTERS64(1),
+		.ENABLE_REGS_16_31(1),
+		.ENABLE_REGS_DUALPORT(1),
+		.BARREL_SHIFTER(1),
+		.TWO_CYCLE_COMPARE(0),
+		.TWO_CYCLE_ALU(0),
+		.COMPRESSED_ISA(0),
+		.CATCH_MISALIGN(1),
+		.CATCH_ILLINSN(1)
+	) uut (
+		.clk             (clk            ),
+		.resetn          (resetn         ),
+		.trap            (trap           ),
+		.mem_axi_awvalid (mem_axi_awvalid),
+		.mem_axi_awready (mem_axi_awready),
+		.mem_axi_awaddr  (mem_axi_awaddr ),
+		.mem_axi_awprot  (mem_axi_awprot ),
+		.mem_axi_wvalid  (mem_axi_wvalid ),
+		.mem_axi_wready  (mem_axi_wready ),
+		.mem_axi_wdata   (mem_axi_wdata  ),
+		.mem_axi_wstrb   (mem_axi_wstrb  ),
+		.mem_axi_bvalid  (mem_axi_bvalid ),
+		.mem_axi_bready  (mem_axi_bready ),
+		.mem_axi_arvalid (mem_axi_arvalid),
+		.mem_axi_arready (mem_axi_arready),
+		.mem_axi_araddr  (mem_axi_araddr ),
+		.mem_axi_arprot  (mem_axi_arprot ),
+		.mem_axi_rvalid  (mem_axi_rvalid ),
+		.mem_axi_rready  (mem_axi_rready ),
+		.mem_axi_rdata   (mem_axi_rdata  )
+	);
+
+	reg expect_bvalid_aw = 0;
+	reg expect_bvalid_w  = 0;
+	reg expect_rvalid    = 0;
+
+	reg [3:0] timeout_aw = 0;
+	reg [3:0] timeout_w  = 0;
+	reg [3:0] timeout_b  = 0;
+	reg [3:0] timeout_ar = 0;
+	reg [3:0] timeout_r  = 0;
+	reg [3:0] timeout_ex = 0;
+
+	always @(posedge clk) begin
+		timeout_aw <= !mem_axi_awvalid || mem_axi_awready ? 0 : timeout_aw + 1;
+		timeout_w  <= !mem_axi_wvalid  || mem_axi_wready  ? 0 : timeout_w  + 1;
+		timeout_b  <= !mem_axi_bvalid  || mem_axi_bready  ? 0 : timeout_b  + 1;
+		timeout_ar <= !mem_axi_arvalid || mem_axi_arready ? 0 : timeout_ar + 1;
+		timeout_r  <= !mem_axi_rvalid  || mem_axi_rready  ? 0 : timeout_r  + 1;
+		timeout_ex <= !{expect_bvalid_aw, expect_bvalid_w, expect_rvalid} ? 0 : timeout_ex + 1;
+		restrict(timeout_aw != 15);
+		restrict(timeout_w  != 15);
+		restrict(timeout_b  != 15);
+		restrict(timeout_ar != 15);
+		restrict(timeout_r  != 15);
+		restrict(timeout_ex != 15);
+		restrict(!trap);
+
+	end
+
+	always @(posedge clk) begin
+		if (resetn) begin
+			if (!$past(resetn)) begin
+				assert(!mem_axi_awvalid);
+				assert(!mem_axi_wvalid );
+				assume(!mem_axi_bvalid );
+				assert(!mem_axi_arvalid);
+				assume(!mem_axi_rvalid );
+			end else begin
+				// Only one read/write transaction in flight at each point in time
+
+				if (expect_bvalid_aw) begin
+					assert(!mem_axi_awvalid);
+				end
+
+				if (expect_bvalid_w) begin
+					assert(!mem_axi_wvalid);
+				end
+
+				if (expect_rvalid) begin
+					assert(!mem_axi_arvalid);
+				end
+
+				expect_bvalid_aw = expect_bvalid_aw || (mem_axi_awvalid && mem_axi_awready);
+				expect_bvalid_w  = expect_bvalid_w  || (mem_axi_wvalid  && mem_axi_wready );
+				expect_rvalid    = expect_rvalid    || (mem_axi_arvalid && mem_axi_arready);
+
+				if (expect_bvalid_aw || expect_bvalid_w) begin
+					assert(!expect_rvalid);
+				end
+
+				if (expect_rvalid) begin
+					assert(!expect_bvalid_aw);
+					assert(!expect_bvalid_w);
+				end
+
+				if (!expect_bvalid_aw || !expect_bvalid_w) begin
+					assume(!mem_axi_bvalid);
+				end
+
+				if (!expect_rvalid) begin
+					assume(!mem_axi_rvalid);
+				end
+
+				if (mem_axi_bvalid && mem_axi_bready) begin
+					expect_bvalid_aw = 0;
+					expect_bvalid_w = 0;
+				end
+
+				if (mem_axi_rvalid && mem_axi_rready) begin
+					expect_rvalid = 0;
+				end
+
+				// Check AXI Master Streams
+
+				if ($past(mem_axi_awvalid && !mem_axi_awready)) begin
+					assert(mem_axi_awvalid);
+					assert($stable(mem_axi_awaddr));
+					assert($stable(mem_axi_awprot));
+				end
+				if ($fell(mem_axi_awvalid)) begin
+					assert($past(mem_axi_awready));
+				end
+				if ($fell(mem_axi_awready)) begin
+					assume($past(mem_axi_awvalid));
+				end
+
+				if ($past(mem_axi_arvalid && !mem_axi_arready)) begin
+					assert(mem_axi_arvalid);
+					assert($stable(mem_axi_araddr));
+					assert($stable(mem_axi_arprot));
+				end
+				if ($fell(mem_axi_arvalid)) begin
+					assert($past(mem_axi_arready));
+				end
+				if ($fell(mem_axi_arready)) begin
+					assume($past(mem_axi_arvalid));
+				end
+
+				if ($past(mem_axi_wvalid && !mem_axi_wready)) begin
+					assert(mem_axi_wvalid);
+					assert($stable(mem_axi_wdata));
+					assert($stable(mem_axi_wstrb));
+				end
+				if ($fell(mem_axi_wvalid)) begin
+					assert($past(mem_axi_wready));
+				end
+				if ($fell(mem_axi_wready)) begin
+					assume($past(mem_axi_wvalid));
+				end
+
+				// Check AXI Slave Streams
+
+				if ($past(mem_axi_bvalid && !mem_axi_bready)) begin
+					assume(mem_axi_bvalid);
+				end
+				if ($fell(mem_axi_bvalid)) begin
+					assume($past(mem_axi_bready));
+				end
+				if ($fell(mem_axi_bready)) begin
+					assert($past(mem_axi_bvalid));
+				end
+
+				if ($past(mem_axi_rvalid && !mem_axi_rready)) begin
+					assume(mem_axi_rvalid);
+					assume($stable(mem_axi_rdata));
+				end
+				if ($fell(mem_axi_rvalid)) begin
+					assume($past(mem_axi_rready));
+				end
+				if ($fell(mem_axi_rready)) begin
+					assert($past(mem_axi_rvalid));
+				end
+			end
+		end
+	end
+endmodule
diff --git a/scripts/smtbmc/axicheck2.sh b/scripts/smtbmc/axicheck2.sh
new file mode 100644
index 0000000..df20855
--- /dev/null
+++ b/scripts/smtbmc/axicheck2.sh
@@ -0,0 +1,12 @@
+#!/bin/bash
+
+set -ex
+
+yosys -ql axicheck2.yslog \
+	-p 'read_verilog -formal -norestrict -assume-asserts ../../picorv32.v' \
+	-p 'read_verilog -formal axicheck2.v' \
+	-p 'prep -top testbench -nordff' \
+	-p 'write_smt2 -wires axicheck2.smt2'
+
+yosys-smtbmc -t 6 -s yices --dump-vcd output.vcd --dump-smtc output.smtc --smtc axicheck2.smtc axicheck2.smt2
+
diff --git a/scripts/smtbmc/axicheck2.smtc b/scripts/smtbmc/axicheck2.smtc
new file mode 100644
index 0000000..1f8c5ea
--- /dev/null
+++ b/scripts/smtbmc/axicheck2.smtc
@@ -0,0 +1,2 @@
+initial
+assume (= [uut_0] [uut_1])
diff --git a/scripts/smtbmc/axicheck2.v b/scripts/smtbmc/axicheck2.v
new file mode 100644
index 0000000..3d24a2e
--- /dev/null
+++ b/scripts/smtbmc/axicheck2.v
@@ -0,0 +1,147 @@
+module testbench (
+	input         clk,
+	input         resetn,
+	output        trap_0,
+	output        trap_1,
+
+	output        mem_axi_awvalid_0,
+	input         mem_axi_awready_0,
+	output [31:0] mem_axi_awaddr_0,
+	output [ 2:0] mem_axi_awprot_0,
+
+	output        mem_axi_awvalid_1,
+	input         mem_axi_awready_1,
+	output [31:0] mem_axi_awaddr_1,
+	output [ 2:0] mem_axi_awprot_1,
+
+	output        mem_axi_wvalid_0,
+	input         mem_axi_wready_0,
+	output [31:0] mem_axi_wdata_0,
+	output [ 3:0] mem_axi_wstrb_0,
+
+	output        mem_axi_wvalid_1,
+	input         mem_axi_wready_1,
+	output [31:0] mem_axi_wdata_1,
+	output [ 3:0] mem_axi_wstrb_1,
+
+	input         mem_axi_bvalid,
+	output        mem_axi_bready_0,
+	output        mem_axi_bready_1,
+
+	output        mem_axi_arvalid_0,
+	input         mem_axi_arready_0,
+	output [31:0] mem_axi_araddr_0,
+	output [ 2:0] mem_axi_arprot_0,
+
+	output        mem_axi_arvalid_1,
+	input         mem_axi_arready_1,
+	output [31:0] mem_axi_araddr_1,
+	output [ 2:0] mem_axi_arprot_1,
+
+	input         mem_axi_rvalid,
+	output        mem_axi_rready_0,
+	output        mem_axi_rready_1,
+	input  [31:0] mem_axi_rdata
+);
+	picorv32_axi #(
+		.ENABLE_COUNTERS(1),
+		.ENABLE_COUNTERS64(1),
+		.ENABLE_REGS_16_31(1),
+		.ENABLE_REGS_DUALPORT(1),
+		.BARREL_SHIFTER(1),
+		.TWO_CYCLE_COMPARE(0),
+		.TWO_CYCLE_ALU(0),
+		.COMPRESSED_ISA(0),
+		.CATCH_MISALIGN(1),
+		.CATCH_ILLINSN(1)
+	) uut_0 (
+		.clk             (clk              ),
+		.resetn          (resetn           ),
+		.trap            (trap_0           ),
+		.mem_axi_awvalid (mem_axi_awvalid_0),
+		.mem_axi_awready (mem_axi_awready_0),
+		.mem_axi_awaddr  (mem_axi_awaddr_0 ),
+		.mem_axi_awprot  (mem_axi_awprot_0 ),
+		.mem_axi_wvalid  (mem_axi_wvalid_0 ),
+		.mem_axi_wready  (mem_axi_wready_0 ),
+		.mem_axi_wdata   (mem_axi_wdata_0  ),
+		.mem_axi_wstrb   (mem_axi_wstrb_0  ),
+		.mem_axi_bvalid  (mem_axi_bvalid   ),
+		.mem_axi_bready  (mem_axi_bready_0 ),
+		.mem_axi_arvalid (mem_axi_arvalid_0),
+		.mem_axi_arready (mem_axi_arready_0),
+		.mem_axi_araddr  (mem_axi_araddr_0 ),
+		.mem_axi_arprot  (mem_axi_arprot_0 ),
+		.mem_axi_rvalid  (mem_axi_rvalid   ),
+		.mem_axi_rready  (mem_axi_rready_0 ),
+		.mem_axi_rdata   (mem_axi_rdata    )
+	);
+
+	picorv32_axi #(
+		.ENABLE_COUNTERS(1),
+		.ENABLE_COUNTERS64(1),
+		.ENABLE_REGS_16_31(1),
+		.ENABLE_REGS_DUALPORT(1),
+		.BARREL_SHIFTER(1),
+		.TWO_CYCLE_COMPARE(0),
+		.TWO_CYCLE_ALU(0),
+		.COMPRESSED_ISA(0),
+		.CATCH_MISALIGN(1),
+		.CATCH_ILLINSN(1)
+	) uut_1 (
+		.clk             (clk              ),
+		.resetn          (resetn           ),
+		.trap            (trap_1           ),
+		.mem_axi_awvalid (mem_axi_awvalid_1),
+		.mem_axi_awready (mem_axi_awready_1),
+		.mem_axi_awaddr  (mem_axi_awaddr_1 ),
+		.mem_axi_awprot  (mem_axi_awprot_1 ),
+		.mem_axi_wvalid  (mem_axi_wvalid_1 ),
+		.mem_axi_wready  (mem_axi_wready_1 ),
+		.mem_axi_wdata   (mem_axi_wdata_1  ),
+		.mem_axi_wstrb   (mem_axi_wstrb_1  ),
+		.mem_axi_bvalid  (mem_axi_bvalid   ),
+		.mem_axi_bready  (mem_axi_bready_1 ),
+		.mem_axi_arvalid (mem_axi_arvalid_1),
+		.mem_axi_arready (mem_axi_arready_1),
+		.mem_axi_araddr  (mem_axi_araddr_1 ),
+		.mem_axi_arprot  (mem_axi_arprot_1 ),
+		.mem_axi_rvalid  (mem_axi_rvalid   ),
+		.mem_axi_rready  (mem_axi_rready_1 ),
+		.mem_axi_rdata   (mem_axi_rdata    )
+	);
+
+	always @(posedge clk) begin
+		if (resetn && $past(resetn)) begin
+			assert(trap_0            == trap_1           );
+			assert(mem_axi_awvalid_0 == mem_axi_awvalid_1);
+			assert(mem_axi_awaddr_0  == mem_axi_awaddr_1 );
+			assert(mem_axi_awprot_0  == mem_axi_awprot_1 );
+			assert(mem_axi_wvalid_0  == mem_axi_wvalid_1 );
+			assert(mem_axi_wdata_0   == mem_axi_wdata_1  );
+			assert(mem_axi_wstrb_0   == mem_axi_wstrb_1  );
+			assert(mem_axi_bready_0  == mem_axi_bready_1 );
+			assert(mem_axi_arvalid_0 == mem_axi_arvalid_1);
+			assert(mem_axi_araddr_0  == mem_axi_araddr_1 );
+			assert(mem_axi_arprot_0  == mem_axi_arprot_1 );
+			assert(mem_axi_rready_0  == mem_axi_rready_1 );
+
+			if (mem_axi_awvalid_0) assume(mem_axi_awready_0 == mem_axi_awready_1);
+			if (mem_axi_wvalid_0 ) assume(mem_axi_wready_0  == mem_axi_wready_1 );
+			if (mem_axi_arvalid_0) assume(mem_axi_arready_0 == mem_axi_arready_1);
+
+			if ($fell(mem_axi_awready_0)) assume($past(mem_axi_awvalid_0));
+			if ($fell(mem_axi_wready_0 )) assume($past(mem_axi_wvalid_0 ));
+			if ($fell(mem_axi_arready_0)) assume($past(mem_axi_arvalid_0));
+
+			if ($fell(mem_axi_awready_1)) assume($past(mem_axi_awvalid_1));
+			if ($fell(mem_axi_wready_1 )) assume($past(mem_axi_wvalid_1 ));
+			if ($fell(mem_axi_arready_1)) assume($past(mem_axi_arvalid_1));
+
+			if ($fell(mem_axi_bvalid)) assume($past(mem_axi_bready_0));
+			if ($fell(mem_axi_rvalid)) assume($past(mem_axi_rready_0));
+
+			if (mem_axi_rvalid && $past(mem_axi_rvalid)) assume($stable(mem_axi_rdata));
+		end
+	end
+endmodule
diff --git a/scripts/smtbmc/mulcmp.sh b/scripts/smtbmc/mulcmp.sh
new file mode 100644
index 0000000..586d72a
--- /dev/null
+++ b/scripts/smtbmc/mulcmp.sh
@@ -0,0 +1,12 @@
+#!/bin/bash
+
+set -ex
+
+yosys -ql mulcmp.yslog \
+        -p 'read_verilog -formal -norestrict -assume-asserts ../../picorv32.v' \
+        -p 'read_verilog -formal mulcmp.v' \
+	-p 'prep -top testbench -nordff' \
+	-p 'write_smt2 -wires mulcmp.smt2'
+
+yosys-smtbmc -s yices -t 100 --dump-vcd output.vcd --dump-smtc output.smtc mulcmp.smt2
+
diff --git a/scripts/smtbmc/mulcmp.v b/scripts/smtbmc/mulcmp.v
new file mode 100644
index 0000000..20c47f3
--- /dev/null
+++ b/scripts/smtbmc/mulcmp.v
@@ -0,0 +1,87 @@
+module testbench(input clk, mem_ready_0, mem_ready_1);
+
+	reg resetn = 0;
+
+	always @(posedge clk)
+		resetn <= 1;
+
+	reg          pcpi_valid_0 = 1;
+	reg          pcpi_valid_1 = 1;
+
+	wire [31:0] pcpi_insn = $anyconst;
+	wire [31:0] pcpi_rs1 = $anyconst;
+	wire [31:0] pcpi_rs2 = $anyconst;
+
+	wire        pcpi_wr_0;
+	wire [31:0] pcpi_rd_0;
+	wire        pcpi_wait_0;
+	wire        pcpi_ready_0;
+
+	wire        pcpi_wr_1;
+	wire [31:0] pcpi_rd_1;
+	wire        pcpi_wait_1;
+	wire        pcpi_ready_1;
+
+	reg         pcpi_wr_ref;
+	reg  [31:0] pcpi_rd_ref;
+	reg         pcpi_ready_ref = 0;
+
+	picorv32_pcpi_mul mul_0 (
+		.clk       (clk         ),
+		.resetn    (resetn      ),
+		.pcpi_valid(pcpi_valid_0),
+		.pcpi_insn (pcpi_insn   ),
+		.pcpi_rs1  (pcpi_rs1    ),
+		.pcpi_rs2  (pcpi_rs2    ),
+		.pcpi_wr   (pcpi_wr_0   ),
+		.pcpi_rd   (pcpi_rd_0   ),
+		.pcpi_wait (pcpi_wait_0 ),
+		.pcpi_ready(pcpi_ready_0),
+
+	);
+
+	picorv32_pcpi_fast_mul mul_1 (
+		.clk       (clk         ),
+		.resetn    (resetn      ),
+		.pcpi_valid(pcpi_valid_1),
+		.pcpi_insn (pcpi_insn   ),
+		.pcpi_rs1  (pcpi_rs1    ),
+		.pcpi_rs2  (pcpi_rs2    ),
+		.pcpi_wr   (pcpi_wr_1   ),
+		.pcpi_rd   (pcpi_rd_1   ),
+		.pcpi_wait (pcpi_wait_1 ),
+		.pcpi_ready(pcpi_ready_1),
+
+	);
+
+	always @(posedge clk) begin
+		if (resetn) begin
+			if (pcpi_ready_0 && pcpi_ready_1) begin
+				assert(pcpi_wr_0 == pcpi_wr_1);
+				assert(pcpi_rd_0 == pcpi_rd_1);
+			end
+
+			if (pcpi_ready_0) begin
+				pcpi_valid_0 <= 0;
+				pcpi_wr_ref <= pcpi_wr_0;
+				pcpi_rd_ref <= pcpi_rd_0;
+				pcpi_ready_ref <= 1;
+				if (pcpi_ready_ref) begin
+					assert(pcpi_wr_0 == pcpi_wr_ref);
+					assert(pcpi_rd_0 == pcpi_rd_ref);
+				end
+			end
+
+			if (pcpi_ready_1) begin
+				pcpi_valid_1 <= 0;
+				pcpi_wr_ref <= pcpi_wr_1;
+				pcpi_rd_ref <= pcpi_rd_1;
+				pcpi_ready_ref <= 1;
+				if (pcpi_ready_ref) begin
+					assert(pcpi_wr_1 == pcpi_wr_ref);
+					assert(pcpi_rd_1 == pcpi_rd_ref);
+				end
+			end
+		end
+	end
+endmodule
diff --git a/scripts/smtbmc/notrap_validop.sh b/scripts/smtbmc/notrap_validop.sh
new file mode 100644
index 0000000..95e0f92
--- /dev/null
+++ b/scripts/smtbmc/notrap_validop.sh
@@ -0,0 +1,13 @@
+#!/bin/bash
+
+set -ex
+
+yosys -ql notrap_validop.yslog \
+        -p 'read_verilog -formal -norestrict -assume-asserts ../../picorv32.v' \
+        -p 'read_verilog -formal notrap_validop.v' \
+	-p 'prep -top testbench -nordff' \
+	-p 'write_smt2 -wires notrap_validop.smt2'
+
+yosys-smtbmc -s yices -t 30 --dump-vcd output.vcd --dump-smtc output.smtc notrap_validop.smt2
+yosys-smtbmc -s yices -i -t 30 --dump-vcd output.vcd --dump-smtc output.smtc notrap_validop.smt2
+
diff --git a/scripts/smtbmc/notrap_validop.v b/scripts/smtbmc/notrap_validop.v
new file mode 100644
index 0000000..8e50304
--- /dev/null
+++ b/scripts/smtbmc/notrap_validop.v
@@ -0,0 +1,67 @@
+module testbench(input clk, mem_ready);
+	`include "opcode.v"
+
+	reg resetn = 0;
+	always @(posedge clk) resetn <= 1;
+
+	(* keep *) wire trap, mem_valid, mem_instr;
+	(* keep *) wire [3:0] mem_wstrb;
+	(* keep *) wire [31:0] mem_addr, mem_wdata, mem_rdata;
+	(* keep *) wire [35:0] trace_data;
+
+	reg [31:0] mem [0:2**30-1];
+
+	assign mem_rdata = mem[mem_addr >> 2];
+
+	always @(posedge clk) begin
+		if (resetn && mem_valid && mem_ready) begin
+			if (mem_wstrb[3]) mem[mem_addr >> 2][31:24] <= mem_wdata[31:24];
+			if (mem_wstrb[2]) mem[mem_addr >> 2][23:16] <= mem_wdata[23:16];
+			if (mem_wstrb[1]) mem[mem_addr >> 2][15: 8] <= mem_wdata[15: 8];
+			if (mem_wstrb[0]) mem[mem_addr >> 2][ 7: 0] <= mem_wdata[ 7: 0];
+		end
+	end
+
+	reg [1:0] mem_ready_stall = 0;
+
+	always @(posedge clk) begin
+		mem_ready_stall <= {mem_ready_stall, mem_valid && !mem_ready};
+		restrict(&mem_ready_stall == 0);
+
+		if (mem_instr && mem_ready && mem_valid) begin
+			assume(opcode_valid(mem_rdata));
+			assume(!opcode_branch(mem_rdata));
+			assume(!opcode_load(mem_rdata));
+			assume(!opcode_store(mem_rdata));
+		end
+
+		if (!mem_valid)
+			assume(!mem_ready);
+
+		if (resetn)
+			assert(!trap);
+	end
+
+	picorv32 #(
+		// change this settings as you like
+		.ENABLE_REGS_DUALPORT(1),
+		.TWO_STAGE_SHIFT(1),
+		.BARREL_SHIFTER(0),
+		.TWO_CYCLE_COMPARE(0),
+		.TWO_CYCLE_ALU(0),
+		.COMPRESSED_ISA(0),
+		.ENABLE_MUL(0),
+		.ENABLE_DIV(0)
+	) cpu (
+		.clk         (clk        ),
+		.resetn      (resetn     ),
+		.trap        (trap       ),
+		.mem_valid   (mem_valid  ),
+		.mem_instr   (mem_instr  ),
+		.mem_ready   (mem_ready  ),
+		.mem_addr    (mem_addr   ),
+		.mem_wdata   (mem_wdata  ),
+		.mem_wstrb   (mem_wstrb  ),
+		.mem_rdata   (mem_rdata  )
+	);
+endmodule
diff --git a/scripts/smtbmc/opcode.v b/scripts/smtbmc/opcode.v
new file mode 100644
index 0000000..7a13bd2
--- /dev/null
+++ b/scripts/smtbmc/opcode.v
@@ -0,0 +1,104 @@
+function opcode_jump;
+	input [31:0] opcode;
+	begin
+		opcode_jump = 0;
+		if (opcode[6:0] == 7'b1101111) opcode_jump = 1; // JAL
+		if (opcode[14:12] == 3'b000 && opcode[6:0] == 7'b1100111) opcode_jump = 1; // JALR
+	end
+endfunction
+
+function opcode_branch;
+	input [31:0] opcode;
+	begin
+		opcode_branch = 0;
+		if (opcode[14:12] == 3'b000 && opcode[6:0] == 7'b1100011) opcode_branch = 1; // BEQ
+		if (opcode[14:12] == 3'b001 && opcode[6:0] == 7'b1100011) opcode_branch = 1; // BNE
+		if (opcode[14:12] == 3'b100 && opcode[6:0] == 7'b1100011) opcode_branch = 1; // BLT
+		if (opcode[14:12] == 3'b101 && opcode[6:0] == 7'b1100011) opcode_branch = 1; // BGE
+		if (opcode[14:12] == 3'b110 && opcode[6:0] == 7'b1100011) opcode_branch = 1; // BLTU
+		if (opcode[14:12] == 3'b111 && opcode[6:0] == 7'b1100011) opcode_branch = 1; // BGEU
+	end
+endfunction
+
+function opcode_load;
+	input [31:0] opcode;
+	begin
+		opcode_load = 0;
+		if (opcode[14:12] == 3'b000 && opcode[6:0] == 7'b0000011) opcode_load = 1; // LB
+		if (opcode[14:12] == 3'b001 && opcode[6:0] == 7'b0000011) opcode_load = 1; // LH
+		if (opcode[14:12] == 3'b010 && opcode[6:0] == 7'b0000011) opcode_load = 1; // LW
+		if (opcode[14:12] == 3'b100 && opcode[6:0] == 7'b0000011) opcode_load = 1; // LBU
+		if (opcode[14:12] == 3'b101 && opcode[6:0] == 7'b0000011) opcode_load = 1; // LHU
+	end
+endfunction
+
+function opcode_store;
+	input [31:0] opcode;
+	begin
+		opcode_store = 0;
+		if (opcode[14:12] == 3'b000 && opcode[6:0] == 7'b0100011) opcode_store = 1; // SB
+		if (opcode[14:12] == 3'b001 && opcode[6:0] == 7'b0100011) opcode_store = 1; // SH
+		if (opcode[14:12] == 3'b010 && opcode[6:0] == 7'b0100011) opcode_store = 1; // SW
+	end
+endfunction
+
+function opcode_alui;
+	input [31:0] opcode;
+	begin
+		opcode_alui = 0;
+		if (opcode[14:12] == 3'b000 && opcode[6:0] == 7'b0010011) opcode_alui = 1; // ADDI
+		if (opcode[14:12] == 3'b010 && opcode[6:0] == 7'b0010011) opcode_alui = 1; // SLTI
+		if (opcode[14:12] == 3'b011 && opcode[6:0] == 7'b0010011) opcode_alui = 1; // SLTIU
+		if (opcode[14:12] == 3'b100 && opcode[6:0] == 7'b0010011) opcode_alui = 1; // XORI
+		if (opcode[14:12] == 3'b110 && opcode[6:0] == 7'b0010011) opcode_alui = 1; // ORI
+		if (opcode[14:12] == 3'b111 && opcode[6:0] == 7'b0010011) opcode_alui = 1; // ANDI
+		if (opcode[31:25] == 7'b0000000 && opcode[14:12] == 3'b001 && opcode[6:0] == 7'b0010011) opcode_alui = 1; // SLLI
+		if (opcode[31:25] == 7'b0000000 && opcode[14:12] == 3'b101 && opcode[6:0] == 7'b0010011) opcode_alui = 1; // SRLI
+		if (opcode[31:25] == 7'b0100000 && opcode[14:12] == 3'b101 && opcode[6:0] == 7'b0010011) opcode_alui = 1; // SRAI
+	end
+endfunction
+
+function opcode_alu;
+	input [31:0] opcode;
+	begin
+		opcode_alu = 0;
+		if (opcode[31:25] == 7'b0000000 && opcode[14:12] == 3'b000 && opcode[6:0] == 7'b0110011) opcode_alu = 1; // ADD
+		if (opcode[31:25] == 7'b0100000 && opcode[14:12] == 3'b000 && opcode[6:0] == 7'b0110011) opcode_alu = 1; // SUB
+		if (opcode[31:25] == 7'b0000000 && opcode[14:12] == 3'b001 && opcode[6:0] == 7'b0110011) opcode_alu = 1; // SLL
+		if (opcode[31:25] == 7'b0000000 && opcode[14:12] == 3'b010 && opcode[6:0] == 7'b0110011) opcode_alu = 1; // SLT
+		if (opcode[31:25] == 7'b0000000 && opcode[14:12] == 3'b011 && opcode[6:0] == 7'b0110011) opcode_alu = 1; // SLTU
+		if (opcode[31:25] == 7'b0000000 && opcode[14:12] == 3'b100 && opcode[6:0] == 7'b0110011) opcode_alu = 1; // XOR
+		if (opcode[31:25] == 7'b0000000 && opcode[14:12] == 3'b101 && opcode[6:0] == 7'b0110011) opcode_alu = 1; // SRL
+		if (opcode[31:25] == 7'b0100000 && opcode[14:12] == 3'b101 && opcode[6:0] == 7'b0110011) opcode_alu = 1; // SRA
+		if (opcode[31:25] == 7'b0000000 && opcode[14:12] == 3'b110 && opcode[6:0] == 7'b0110011) opcode_alu = 1; // OR
+		if (opcode[31:25] == 7'b0000000 && opcode[14:12] == 3'b111 && opcode[6:0] == 7'b0110011) opcode_alu = 1; // AND
+	end
+endfunction
+
+function opcode_sys;
+	input [31:0] opcode;
+	begin
+		opcode_sys = 0;
+		if (opcode[31:20] == 12'hC00 && opcode[19:12] == 3'b010 && opcode[6:0] == 7'b1110011) opcode_sys = 1; // RDCYCLE
+		if (opcode[31:20] == 12'hC01 && opcode[19:12] == 3'b010 && opcode[6:0] == 7'b1110011) opcode_sys = 1; // RDTIME
+		if (opcode[31:20] == 12'hC02 && opcode[19:12] == 3'b010 && opcode[6:0] == 7'b1110011) opcode_sys = 1; // RDINSTRET
+		if (opcode[31:20] == 12'hC80 && opcode[19:12] == 3'b010 && opcode[6:0] == 7'b1110011) opcode_sys = 1; // RDCYCLEH
+		if (opcode[31:20] == 12'hC81 && opcode[19:12] == 3'b010 && opcode[6:0] == 7'b1110011) opcode_sys = 1; // RDTIMEH
+		if (opcode[31:20] == 12'hC82 && opcode[19:12] == 3'b010 && opcode[6:0] == 7'b1110011) opcode_sys = 1; // RDINSTRETH
+	end
+
+endfunction
+
+function opcode_valid;
+	input [31:0] opcode;
+	begin
+		opcode_valid = 0;
+		if (opcode_jump  (opcode)) opcode_valid = 1;
+		if (opcode_branch(opcode)) opcode_valid = 1;
+		if (opcode_load  (opcode)) opcode_valid = 1;
+		if (opcode_store (opcode)) opcode_valid = 1;
+		if (opcode_alui  (opcode)) opcode_valid = 1;
+		if (opcode_alu   (opcode)) opcode_valid = 1;
+		if (opcode_sys   (opcode)) opcode_valid = 1;
+	end
+endfunction
diff --git a/scripts/smtbmc/tracecmp.gtkw b/scripts/smtbmc/tracecmp.gtkw
new file mode 100644
index 0000000..09dd9b2
--- /dev/null
+++ b/scripts/smtbmc/tracecmp.gtkw
@@ -0,0 +1,71 @@
+[*]
+[*] GTKWave Analyzer v3.3.65 (w)1999-2015 BSI
+[*] Fri Aug 26 15:42:37 2016
+[*]
+[dumpfile] "/home/clifford/Work/picorv32/scripts/smtbmc/output.vcd"
+[dumpfile_mtime] "Fri Aug 26 15:33:18 2016"
+[dumpfile_size] 80106
+[savefile] "/home/clifford/Work/picorv32/scripts/smtbmc/tracecmp.gtkw"
+[timestart] 0
+[size] 1216 863
+[pos] -1 -1
+*-2.860312 10 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1
+[treeopen] testbench.
+[sst_width] 241
+[signals_width] 337
+[sst_expanded] 1
+[sst_vpaned_height] 252
+@28
+smt_clock
+testbench.resetn
+testbench.trap_0
+testbench.trap_1
+@200
+-
+-Trace CMP
+@28
+testbench.trace_valid_0
+testbench.trace_valid_1
+@22
+testbench.trace_data_0[35:0]
+testbench.trace_data_1[35:0]
+@420
+testbench.trace_balance[7:0]
+@200
+-
+-CPU #0
+@28
+testbench.mem_valid_0
+testbench.mem_ready_0
+testbench.mem_instr_0
+@22
+testbench.mem_addr_0[31:0]
+testbench.mem_rdata_0[31:0]
+testbench.mem_wdata_0[31:0]
+@28
+testbench.mem_wstrb_0[3:0]
+@22
+testbench.cpu_0.cpu_state[7:0]
+@28
+testbench.cpu_0.mem_state[1:0]
+@200
+-
+-CPU #1
+@28
+testbench.mem_valid_1
+testbench.mem_ready_1
+testbench.mem_instr_1
+@22
+testbench.mem_addr_1[31:0]
+testbench.mem_rdata_1[31:0]
+testbench.mem_wdata_1[31:0]
+@28
+testbench.mem_wstrb_1[3:0]
+@22
+testbench.cpu_1.cpu_state[7:0]
+@28
+testbench.cpu_1.mem_state[1:0]
+@200
+-
+[pattern_trace] 1
+[pattern_trace] 0
diff --git a/scripts/smtbmc/tracecmp.sh b/scripts/smtbmc/tracecmp.sh
new file mode 100644
index 0000000..449af52
--- /dev/null
+++ b/scripts/smtbmc/tracecmp.sh
@@ -0,0 +1,12 @@
+#!/bin/bash
+
+set -ex
+
+yosys -ql tracecmp.yslog \
+        -p 'read_verilog -formal -norestrict -assume-asserts ../../picorv32.v' \
+        -p 'read_verilog -formal tracecmp.v' \
+	-p 'prep -top testbench -nordff' \
+	-p 'write_smt2 -wires tracecmp.smt2'
+
+yosys-smtbmc -s yices --smtc tracecmp.smtc --dump-vcd output.vcd --dump-smtc output.smtc tracecmp.smt2
+
diff --git a/scripts/smtbmc/tracecmp.smtc b/scripts/smtbmc/tracecmp.smtc
new file mode 100644
index 0000000..477c7d0
--- /dev/null
+++ b/scripts/smtbmc/tracecmp.smtc
@@ -0,0 +1,12 @@
+initial
+assume (= [mem_0] [mem_1])
+assume (= [cpu_0.cpuregs] [cpu_1.cpuregs])
+assume (= [trace_data_0] [trace_data_1])
+
+always
+assume (=> (not [mem_valid_0]) (not [mem_ready_0]))
+assume (=> (not [mem_valid_1]) (not [mem_ready_1]))
+# assume (= [mem_ready_0] [mem_ready_1])
+
+always -1
+assert (=> (= [trace_balance] #x00) (= [trace_data_0] [trace_data_1]))
diff --git a/scripts/smtbmc/tracecmp.v b/scripts/smtbmc/tracecmp.v
new file mode 100644
index 0000000..8ac4157
--- /dev/null
+++ b/scripts/smtbmc/tracecmp.v
@@ -0,0 +1,109 @@
+module testbench(input clk, mem_ready_0, mem_ready_1);
+	// set this to 1 to test generation of counter examples
+	localparam ENABLE_COUNTERS = 0;
+
+	reg resetn = 0;
+	always @(posedge clk) resetn <= 1;
+
+	(* keep *) wire trap_0, trace_valid_0, mem_valid_0, mem_instr_0;
+	(* keep *) wire [3:0] mem_wstrb_0;
+	(* keep *) wire [31:0] mem_addr_0, mem_wdata_0, mem_rdata_0;
+	(* keep *) wire [35:0] trace_data_0;
+
+	(* keep *) wire trap_1, trace_valid_1, mem_valid_1, mem_instr_1;
+	(* keep *) wire [3:0] mem_wstrb_1;
+	(* keep *) wire [31:0] mem_addr_1, mem_wdata_1, mem_rdata_1;
+	(* keep *) wire [35:0] trace_data_1;
+
+	reg [31:0] mem_0 [0:2**30-1];
+	reg [31:0] mem_1 [0:2**30-1];
+
+	assign mem_rdata_0 = mem_0[mem_addr_0 >> 2];
+	assign mem_rdata_1 = mem_1[mem_addr_1 >> 2];
+
+	always @(posedge clk) begin
+		if (resetn && mem_valid_0 && mem_ready_0) begin
+			if (mem_wstrb_0[3]) mem_0[mem_addr_0 >> 2][31:24] <= mem_wdata_0[31:24];
+			if (mem_wstrb_0[2]) mem_0[mem_addr_0 >> 2][23:16] <= mem_wdata_0[23:16];
+			if (mem_wstrb_0[1]) mem_0[mem_addr_0 >> 2][15: 8] <= mem_wdata_0[15: 8];
+			if (mem_wstrb_0[0]) mem_0[mem_addr_0 >> 2][ 7: 0] <= mem_wdata_0[ 7: 0];
+		end
+		if (resetn && mem_valid_1 && mem_ready_1) begin
+			if (mem_wstrb_1[3]) mem_1[mem_addr_1 >> 2][31:24] <= mem_wdata_1[31:24];
+			if (mem_wstrb_1[2]) mem_1[mem_addr_1 >> 2][23:16] <= mem_wdata_1[23:16];
+			if (mem_wstrb_1[1]) mem_1[mem_addr_1 >> 2][15: 8] <= mem_wdata_1[15: 8];
+			if (mem_wstrb_1[0]) mem_1[mem_addr_1 >> 2][ 7: 0] <= mem_wdata_1[ 7: 0];
+		end
+	end
+
+	(* keep *) reg [7:0] trace_balance;
+	reg [7:0] trace_balance_q;
+
+	always @* begin
+		trace_balance = trace_balance_q;
+		if (trace_valid_0) trace_balance = trace_balance + 1;
+		if (trace_valid_1) trace_balance = trace_balance - 1;
+	end
+
+	always @(posedge clk) begin
+		trace_balance_q <= resetn ? trace_balance : 0;
+	end
+
+	picorv32 #(
+		// do not change this settings
+		.ENABLE_COUNTERS(ENABLE_COUNTERS),
+		.ENABLE_TRACE(1),
+
+		// change this settings as you like
+		.ENABLE_REGS_DUALPORT(1),
+		.TWO_STAGE_SHIFT(1),
+		.BARREL_SHIFTER(0),
+		.TWO_CYCLE_COMPARE(0),
+		.TWO_CYCLE_ALU(0),
+		.COMPRESSED_ISA(0),
+		.ENABLE_MUL(0),
+		.ENABLE_DIV(0)
+	) cpu_0 (
+		.clk         (clk          ),
+		.resetn      (resetn       ),
+		.trap        (trap_0       ),
+		.mem_valid   (mem_valid_0  ),
+		.mem_instr   (mem_instr_0  ),
+		.mem_ready   (mem_ready_0  ),
+		.mem_addr    (mem_addr_0   ),
+		.mem_wdata   (mem_wdata_0  ),
+		.mem_wstrb   (mem_wstrb_0  ),
+		.mem_rdata   (mem_rdata_0  ),
+		.trace_valid (trace_valid_0),
+		.trace_data  (trace_data_0 )
+	);
+
+	picorv32 #(
+		// do not change this settings
+		.ENABLE_COUNTERS(ENABLE_COUNTERS),
+		.ENABLE_TRACE(1),
+
+		// change this settings as you like
+		.ENABLE_REGS_DUALPORT(1),
+		.TWO_STAGE_SHIFT(1),
+		.BARREL_SHIFTER(0),
+		.TWO_CYCLE_COMPARE(0),
+		.TWO_CYCLE_ALU(0),
+		.COMPRESSED_ISA(0),
+		.ENABLE_MUL(0),
+		.ENABLE_DIV(0)
+	) cpu_1 (
+		.clk         (clk          ),
+		.resetn      (resetn       ),
+		.trap        (trap_1       ),
+		.mem_valid   (mem_valid_1  ),
+		.mem_instr   (mem_instr_1  ),
+		.mem_ready   (mem_ready_1  ),
+		.mem_addr    (mem_addr_1   ),
+		.mem_wdata   (mem_wdata_1  ),
+		.mem_wstrb   (mem_wstrb_1  ),
+		.mem_rdata   (mem_rdata_1  ),
+		.trace_valid (trace_valid_1),
+		.trace_data  (trace_data_1 )
+	);
+endmodule
diff --git a/scripts/smtbmc/tracecmp2.sh b/scripts/smtbmc/tracecmp2.sh
new file mode 100644
index 0000000..ddaf285
--- /dev/null
+++ b/scripts/smtbmc/tracecmp2.sh
@@ -0,0 +1,12 @@
+#!/bin/bash
+
+set -ex
+
+yosys -ql tracecmp2.yslog \
+        -p 'read_verilog -formal -norestrict -assume-asserts ../../picorv32.v' \
+        -p 'read_verilog -formal tracecmp2.v' \
+	-p 'prep -top testbench -nordff' \
+	-p 'write_smt2 -wires tracecmp2.smt2'
+
+yosys-smtbmc -s boolector --smtc tracecmp2.smtc --dump-vcd output.vcd --dump-smtc output.smtc tracecmp2.smt2
+
diff --git a/scripts/smtbmc/tracecmp2.smtc b/scripts/smtbmc/tracecmp2.smtc
new file mode 100644
index 0000000..3b7fd0a
--- /dev/null
+++ b/scripts/smtbmc/tracecmp2.smtc
@@ -0,0 +1,2 @@
+initial
+assume (= [cpu_0.cpuregs] [cpu_1.cpuregs])
diff --git a/scripts/smtbmc/tracecmp2.v b/scripts/smtbmc/tracecmp2.v
new file mode 100644
index 0000000..42f39a9
--- /dev/null
+++ b/scripts/smtbmc/tracecmp2.v
@@ -0,0 +1,196 @@
+module testbench(
+	input clk, mem_ready_0, mem_ready_1,
+	input [31:0] mem_rdata
+);
+	// set this to 1 to test generation of counterexamples
+	localparam ENABLE_COUNTERS = 0;
+
+	reg resetn = 0;
+	always @(posedge clk) resetn <= 1;
+
+	(* keep *) wire trap_0, trace_valid_0, mem_valid_0, mem_instr_0;
+	(* keep *) wire [3:0] mem_wstrb_0;
+	(* keep *) wire [31:0] mem_addr_0, mem_wdata_0, mem_rdata_0;
+	(* keep *) wire [35:0] trace_data_0;
+
+	(* keep *) wire trap_1, trace_valid_1, mem_valid_1, mem_instr_1;
+	(* keep *) wire [3:0] mem_wstrb_1;
+	(* keep *) wire [31:0] mem_addr_1, mem_wdata_1, mem_rdata_1;
+	(* keep *) wire [35:0] trace_data_1;
+
+	reg [31:0] last_mem_rdata;
+
+	assign mem_rdata_0 = mem_rdata;
+	assign mem_rdata_1 = mem_rdata;
+
+	wire mem_xfer_0 = resetn && mem_valid_0 && mem_ready_0;
+	wire mem_xfer_1 = resetn && mem_valid_1 && mem_ready_1;
+
+	reg [1:0] cmp_mem_state = 0;
+	reg [31:0] cmp_mem_addr;
+	reg [31:0] cmp_mem_wdata;
+	reg [3:0] cmp_mem_wstrb;
+
+	always @* begin
+		if (mem_valid_0 == 0)
+			assume(!mem_ready_0 == 0);
+		if (mem_valid_1 == 0)
+			assume(mem_ready_1 == 0);
+	end
+
+	always @(posedge clk) begin
+		if (cmp_mem_state)
+			assume(last_mem_rdata == mem_rdata);
+		last_mem_rdata <= mem_rdata;
+	end
+
+	always @(posedge clk) begin
+		case (cmp_mem_state)
+			2'b 00: begin
+				case ({mem_xfer_1, mem_xfer_0})
+					2'b 11: begin
+						assert(mem_addr_0 == mem_addr_1);
+						assert(mem_wstrb_0 == mem_wstrb_1);
+						if (mem_wstrb_0[3]) assert(mem_wdata_0[31:24] == mem_wdata_1[31:24]);
+						if (mem_wstrb_0[2]) assert(mem_wdata_0[23:16] == mem_wdata_1[23:16]);
+						if (mem_wstrb_0[1]) assert(mem_wdata_0[15: 8] == mem_wdata_1[15: 8]);
+						if (mem_wstrb_0[0]) assert(mem_wdata_0[ 7: 0] == mem_wdata_1[ 7: 0]);
+					end
+					2'b 01: begin
+						cmp_mem_state <= 2'b 01;
+						cmp_mem_addr <= mem_addr_0;
+						cmp_mem_wdata <= mem_wdata_0;
+						cmp_mem_wstrb <= mem_wstrb_0;
+					end
+					2'b 10: begin
+						cmp_mem_state <= 2'b 10;
+						cmp_mem_addr <= mem_addr_1;
+						cmp_mem_wdata <= mem_wdata_1;
+						cmp_mem_wstrb <= mem_wstrb_1;
+					end
+				endcase
+			end
+			2'b 01: begin
+				assume(!mem_xfer_0);
+				if (mem_xfer_1) begin
+					cmp_mem_state <= 2'b 00;
+					assert(cmp_mem_addr == mem_addr_1);
+					assert(cmp_mem_wstrb == mem_wstrb_1);
+					if (cmp_mem_wstrb[3]) assert(cmp_mem_wdata[31:24] == mem_wdata_1[31:24]);
+					if (cmp_mem_wstrb[2]) assert(cmp_mem_wdata[23:16] == mem_wdata_1[23:16]);
+					if (cmp_mem_wstrb[1]) assert(cmp_mem_wdata[15: 8] == mem_wdata_1[15: 8]);
+					if (cmp_mem_wstrb[0]) assert(cmp_mem_wdata[ 7: 0] == mem_wdata_1[ 7: 0]);
+				end
+			end
+			2'b 10: begin
+				assume(!mem_xfer_1);
+				if (mem_xfer_0) begin
+					cmp_mem_state <= 2'b 00;
+					assert(cmp_mem_addr == mem_addr_0);
+					assert(cmp_mem_wstrb == mem_wstrb_0);
+					if (cmp_mem_wstrb[3]) assert(cmp_mem_wdata[31:24] == mem_wdata_0[31:24]);
+					if (cmp_mem_wstrb[2]) assert(cmp_mem_wdata[23:16] == mem_wdata_0[23:16]);
+					if (cmp_mem_wstrb[1]) assert(cmp_mem_wdata[15: 8] == mem_wdata_0[15: 8]);
+					if (cmp_mem_wstrb[0]) assert(cmp_mem_wdata[ 7: 0] == mem_wdata_0[ 7: 0]);
+				end
+			end
+		endcase
+	end
+
+	reg [1:0] cmp_trace_state = 0;
+	reg [35:0] cmp_trace_data;
+
+	always @(posedge clk) begin
+		if (resetn) begin
+			case (cmp_trace_state)
+				2'b 00: begin
+					case ({trace_valid_1, trace_valid_0})
+						2'b 11: begin
+							assert(trace_data_0 == trace_data_1);
+						end
+						2'b 01: begin
+							cmp_trace_state <= 2'b 01;
+							cmp_trace_data <= trace_data_0;
+						end
+						2'b 10: begin
+							cmp_trace_state <= 2'b 10;
+							cmp_trace_data <= trace_data_1;
+						end
+					endcase
+				end
+				2'b 01: begin
+					assume(!trace_valid_0);
+					if (trace_valid_1) begin
+						cmp_trace_state <= 2'b 00;
+						assert(cmp_trace_data == trace_data_1);
+					end
+				end
+				2'b 10: begin
+					assume(!trace_valid_1);
+					if (trace_valid_0) begin
+						cmp_trace_state <= 2'b 00;
+						assert(cmp_trace_data == trace_data_0);
+					end
+				end
+			endcase
+		end
+	end
+
+	picorv32 #(
+		// do not change this settings
+		.ENABLE_COUNTERS(ENABLE_COUNTERS),
+		.ENABLE_TRACE(1),
+
+		// change this settings as you like
+		.ENABLE_REGS_DUALPORT(1),
+		.TWO_STAGE_SHIFT(0),
+		.BARREL_SHIFTER(0),
+		.TWO_CYCLE_COMPARE(0),
+		.TWO_CYCLE_ALU(0),
+		.COMPRESSED_ISA(1),
+		.ENABLE_MUL(0),
+		.ENABLE_DIV(0)
+	) cpu_0 (
+		.clk         (clk          ),
+		.resetn      (resetn       ),
+		.trap        (trap_0       ),
+		.mem_valid   (mem_valid_0  ),
+		.mem_instr   (mem_instr_0  ),
+		.mem_ready   (mem_ready_0  ),
+		.mem_addr    (mem_addr_0   ),
+		.mem_wdata   (mem_wdata_0  ),
+		.mem_wstrb   (mem_wstrb_0  ),
+		.mem_rdata   (mem_rdata_0  ),
+		.trace_valid (trace_valid_0),
+		.trace_data  (trace_data_0 )
+	);
+
+	picorv32 #(
+		// do not change this settings
+		.ENABLE_COUNTERS(ENABLE_COUNTERS),
+		.ENABLE_TRACE(1),
+
+		// change this settings as you like
+		.ENABLE_REGS_DUALPORT(1),
+		.TWO_STAGE_SHIFT(1),
+		.BARREL_SHIFTER(0),
+		.TWO_CYCLE_COMPARE(0),
+		.TWO_CYCLE_ALU(0),
+		.COMPRESSED_ISA(1),
+		.ENABLE_MUL(0),
+		.ENABLE_DIV(0)
+	) cpu_1 (
+		.clk         (clk          ),
+		.resetn      (resetn       ),
+		.trap        (trap_1       ),
+		.mem_valid   (mem_valid_1  ),
+		.mem_instr   (mem_instr_1  ),
+		.mem_ready   (mem_ready_1  ),
+		.mem_addr    (mem_addr_1   ),
+		.mem_wdata   (mem_wdata_1  ),
+		.mem_wstrb   (mem_wstrb_1  ),
+		.mem_rdata   (mem_rdata_1  ),
+		.trace_valid (trace_valid_1),
+		.trace_data  (trace_data_1 )
+	);
+endmodule
diff --git a/scripts/smtbmc/tracecmp3.sh b/scripts/smtbmc/tracecmp3.sh
new file mode 100644
index 0000000..bfa0b3c
--- /dev/null
+++ b/scripts/smtbmc/tracecmp3.sh
@@ -0,0 +1,17 @@
+#!/bin/bash
+
+set -ex
+
+yosys -l tracecmp3.yslog \
+        -p 'read_verilog ../../picorv32.v' \
+        -p 'read_verilog -formal tracecmp3.v' \
+	-p 'prep -top testbench -nordff' \
+	-p 'write_smt2 -wires tracecmp3.smt2' \
+	-p 'miter -assert -flatten testbench miter' \
+	-p 'hierarchy -top miter; memory_map; opt -full' \
+	-p 'techmap; opt; abc; opt -fast' \
+	-p 'write_blif tracecmp3.blif'
+
+yosys-abc -c 'read_blif tracecmp3.blif; undc; strash; zero; sim3 -v; undc -c; write_cex -n tracecmp3.cex'
+yosys-smtbmc -s yices --cex tracecmp3.cex --dump-vcd output.vcd --dump-smtc output.smtc tracecmp3.smt2
+
diff --git a/scripts/smtbmc/tracecmp3.v b/scripts/smtbmc/tracecmp3.v
new file mode 100644
index 0000000..a1bb63b
--- /dev/null
+++ b/scripts/smtbmc/tracecmp3.v
@@ -0,0 +1,135 @@
+// Based on the benchmark from 2016 Yosys-SMTBMC presentation, which in turn is
+// based on the tracecmp2 test from this directory.
+
+module testbench (
+	input clk,
+	input [31:0] mem_rdata_in,
+
+	input             pcpi_wr,
+	input      [31:0] pcpi_rd,
+	input             pcpi_wait,
+	input             pcpi_ready
+);
+	reg resetn = 0;
+
+	always @(posedge clk)
+		resetn <= 1;
+
+	wire        cpu0_trap;
+	wire        cpu0_mem_valid;
+	wire        cpu0_mem_instr;
+	wire        cpu0_mem_ready;
+	wire [31:0] cpu0_mem_addr;
+	wire [31:0] cpu0_mem_wdata;
+	wire [3:0]  cpu0_mem_wstrb;
+	wire [31:0] cpu0_mem_rdata;
+	wire        cpu0_trace_valid;
+	wire [35:0] cpu0_trace_data;
+
+	wire        cpu1_trap;
+	wire        cpu1_mem_valid;
+	wire        cpu1_mem_instr;
+	wire        cpu1_mem_ready;
+	wire [31:0] cpu1_mem_addr;
+	wire [31:0] cpu1_mem_wdata;
+	wire [3:0]  cpu1_mem_wstrb;
+	wire [31:0] cpu1_mem_rdata;
+	wire        cpu1_trace_valid;
+	wire [35:0] cpu1_trace_data;
+
+	wire        mem_ready;
+	wire [31:0] mem_rdata;
+
+	assign mem_ready = cpu0_mem_valid && cpu1_mem_valid;
+	assign mem_rdata = mem_rdata_in;
+
+	assign cpu0_mem_ready = mem_ready;
+	assign cpu0_mem_rdata = mem_rdata;
+
+	assign cpu1_mem_ready = mem_ready;
+	assign cpu1_mem_rdata = mem_rdata;
+
+	reg [ 2:0] trace_balance = 3'b010;
+	reg [35:0] trace_buffer_cpu0 = 0, trace_buffer_cpu1 = 0;
+
+	always @(posedge clk) begin
+		if (resetn) begin
+			if (cpu0_trace_valid)
+				trace_buffer_cpu0 <= cpu0_trace_data;
+
+			if (cpu1_trace_valid)
+				trace_buffer_cpu1 <= cpu1_trace_data;
+
+			if (cpu0_trace_valid && !cpu1_trace_valid)
+				trace_balance <= trace_balance << 1;
+
+			if (!cpu0_trace_valid && cpu1_trace_valid)
+				trace_balance <= trace_balance >> 1;
+		end
+	end
+
+	always @* begin
+		if (resetn && cpu0_mem_ready) begin
+			assert(cpu0_mem_addr == cpu1_mem_addr);
+			assert(cpu0_mem_wstrb == cpu1_mem_wstrb);
+			if (cpu0_mem_wstrb[3]) assert(cpu0_mem_wdata[31:24] == cpu1_mem_wdata[31:24]);
+			if (cpu0_mem_wstrb[2]) assert(cpu0_mem_wdata[23:16] == cpu1_mem_wdata[23:16]);
+			if (cpu0_mem_wstrb[1]) assert(cpu0_mem_wdata[15: 8] == cpu1_mem_wdata[15: 8]);
+			if (cpu0_mem_wstrb[0]) assert(cpu0_mem_wdata[ 7: 0] == cpu1_mem_wdata[ 7: 0]);
+		end
+		if (trace_balance == 3'b010) begin
+			assert(trace_buffer_cpu0 == trace_buffer_cpu1);
+		end
+	end
+
+	picorv32 #(
+		.ENABLE_COUNTERS(0),
+		.REGS_INIT_ZERO(1),
+		.COMPRESSED_ISA(1),
+		.ENABLE_TRACE(1),
+
+		.TWO_STAGE_SHIFT(0),
+		.ENABLE_PCPI(1)
+	) cpu0 (
+		.clk         (clk             ),
+		.resetn      (resetn          ),
+		.trap        (cpu0_trap       ),
+		.mem_valid   (cpu0_mem_valid  ),
+		.mem_instr   (cpu0_mem_instr  ),
+		.mem_ready   (cpu0_mem_ready  ),
+		.mem_addr    (cpu0_mem_addr   ),
+		.mem_wdata   (cpu0_mem_wdata  ),
+		.mem_wstrb   (cpu0_mem_wstrb  ),
+		.mem_rdata   (cpu0_mem_rdata  ),
+		.pcpi_wr     (pcpi_wr         ),
+		.pcpi_rd     (pcpi_rd         ),
+		.pcpi_wait   (pcpi_wait       ),
+		.pcpi_ready  (pcpi_ready      ),
+		.trace_valid (cpu0_trace_valid),
+		.trace_data  (cpu0_trace_data )
+	);
+
+	picorv32 #(
+		.ENABLE_COUNTERS(0),
+		.REGS_INIT_ZERO(1),
+		.COMPRESSED_ISA(1),
+		.ENABLE_TRACE(1),
+
+		.TWO_STAGE_SHIFT(1),
+		.TWO_CYCLE_COMPARE(1),
+		.TWO_CYCLE_ALU(1)
+	) cpu1 (
+		.clk         (clk             ),
+		.resetn      (resetn          ),
+		.trap        (cpu1_trap       ),
+		.mem_valid   (cpu1_mem_valid  ),
+		.mem_instr   (cpu1_mem_instr  ),
+		.mem_ready   (cpu1_mem_ready  ),
+		.mem_addr    (cpu1_mem_addr   ),
+		.mem_wdata   (cpu1_mem_wdata  ),
+		.mem_wstrb   (cpu1_mem_wstrb  ),
+		.mem_rdata   (cpu1_mem_rdata  ),
+		.trace_valid (cpu1_trace_valid),
+		.trace_data  (cpu1_trace_data )
+	);
+endmodule
-- 
cgit