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, 0 insertions, 1251 deletions
diff --git a/scripts/smtbmc/.gitignore b/scripts/smtbmc/.gitignore
deleted file mode 100644
index 1ce906e..0000000
--- a/scripts/smtbmc/.gitignore
+++ /dev/null
@@ -1,18 +0,0 @@
-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
deleted file mode 100644
index 732b3b8..0000000
--- a/scripts/smtbmc/axicheck.sh
+++ /dev/null
@@ -1,13 +0,0 @@
-#!/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
deleted file mode 100644
index 80eda48..0000000
--- a/scripts/smtbmc/axicheck.v
+++ /dev/null
@@ -1,210 +0,0 @@
-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
deleted file mode 100644
index df20855..0000000
--- a/scripts/smtbmc/axicheck2.sh
+++ /dev/null
@@ -1,12 +0,0 @@
-#!/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
deleted file mode 100644
index 1f8c5ea..0000000
--- a/scripts/smtbmc/axicheck2.smtc
+++ /dev/null
@@ -1,2 +0,0 @@
-initial
-assume (= [uut_0] [uut_1])
diff --git a/scripts/smtbmc/axicheck2.v b/scripts/smtbmc/axicheck2.v
deleted file mode 100644
index 3d24a2e..0000000
--- a/scripts/smtbmc/axicheck2.v
+++ /dev/null
@@ -1,147 +0,0 @@
-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
deleted file mode 100644
index 586d72a..0000000
--- a/scripts/smtbmc/mulcmp.sh
+++ /dev/null
@@ -1,12 +0,0 @@
-#!/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
deleted file mode 100644
index 20c47f3..0000000
--- a/scripts/smtbmc/mulcmp.v
+++ /dev/null
@@ -1,87 +0,0 @@
-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
deleted file mode 100644
index 95e0f92..0000000
--- a/scripts/smtbmc/notrap_validop.sh
+++ /dev/null
@@ -1,13 +0,0 @@
-#!/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
deleted file mode 100644
index 8e50304..0000000
--- a/scripts/smtbmc/notrap_validop.v
+++ /dev/null
@@ -1,67 +0,0 @@
-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
deleted file mode 100644
index 7a13bd2..0000000
--- a/scripts/smtbmc/opcode.v
+++ /dev/null
@@ -1,104 +0,0 @@
-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
deleted file mode 100644
index 09dd9b2..0000000
--- a/scripts/smtbmc/tracecmp.gtkw
+++ /dev/null
@@ -1,71 +0,0 @@
-[*]
-[*] 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
deleted file mode 100644
index 449af52..0000000
--- a/scripts/smtbmc/tracecmp.sh
+++ /dev/null
@@ -1,12 +0,0 @@
-#!/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
deleted file mode 100644
index 477c7d0..0000000
--- a/scripts/smtbmc/tracecmp.smtc
+++ /dev/null
@@ -1,12 +0,0 @@
-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
deleted file mode 100644
index 8ac4157..0000000
--- a/scripts/smtbmc/tracecmp.v
+++ /dev/null
@@ -1,109 +0,0 @@
-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
deleted file mode 100644
index ddaf285..0000000
--- a/scripts/smtbmc/tracecmp2.sh
+++ /dev/null
@@ -1,12 +0,0 @@
-#!/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
deleted file mode 100644
index 3b7fd0a..0000000
--- a/scripts/smtbmc/tracecmp2.smtc
+++ /dev/null
@@ -1,2 +0,0 @@
-initial
-assume (= [cpu_0.cpuregs] [cpu_1.cpuregs])
diff --git a/scripts/smtbmc/tracecmp2.v b/scripts/smtbmc/tracecmp2.v
deleted file mode 100644
index 42f39a9..0000000
--- a/scripts/smtbmc/tracecmp2.v
+++ /dev/null
@@ -1,196 +0,0 @@
-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
deleted file mode 100644
index bfa0b3c..0000000
--- a/scripts/smtbmc/tracecmp3.sh
+++ /dev/null
@@ -1,17 +0,0 @@
-#!/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
deleted file mode 100644
index a1bb63b..0000000
--- a/scripts/smtbmc/tracecmp3.v
+++ /dev/null
@@ -1,135 +0,0 @@
-// 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-07-03 11:33:53 +0000