summaryrefslogtreecommitdiffstats
path: root/scripts/smtbmc
diff options
context:
space:
mode:
Diffstat (limited to 'scripts/smtbmc')
-rw-r--r--scripts/smtbmc/.gitignore18
-rw-r--r--scripts/smtbmc/axicheck.sh13
-rw-r--r--scripts/smtbmc/axicheck.v210
-rw-r--r--scripts/smtbmc/axicheck2.sh12
-rw-r--r--scripts/smtbmc/axicheck2.smtc2
-rw-r--r--scripts/smtbmc/axicheck2.v147
-rw-r--r--scripts/smtbmc/mulcmp.sh12
-rw-r--r--scripts/smtbmc/mulcmp.v87
-rw-r--r--scripts/smtbmc/notrap_validop.sh13
-rw-r--r--scripts/smtbmc/notrap_validop.v67
-rw-r--r--scripts/smtbmc/opcode.v104
-rw-r--r--scripts/smtbmc/tracecmp.gtkw71
-rw-r--r--scripts/smtbmc/tracecmp.sh12
-rw-r--r--scripts/smtbmc/tracecmp.smtc12
-rw-r--r--scripts/smtbmc/tracecmp.v109
-rw-r--r--scripts/smtbmc/tracecmp2.sh12
-rw-r--r--scripts/smtbmc/tracecmp2.smtc2
-rw-r--r--scripts/smtbmc/tracecmp2.v196
-rw-r--r--scripts/smtbmc/tracecmp3.sh17
-rw-r--r--scripts/smtbmc/tracecmp3.v135
20 files changed, 1251 insertions, 0 deletions
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
generated by cgit (git 2.34.1) at 2024-06-02 11:35:08 +0000