From 3c10f58d043432197fdf5169404710f8ab68db8c Mon Sep 17 00:00:00 2001
From: SergeyDegtyar <sndegtyar@gmail.com>
Date: Fri, 23 Aug 2019 17:00:16 +0300
Subject: Fix run-test.sh; Add new test for dpram.
---
tests/ice40/dpram.v | 20 ++++++++++++
tests/ice40/dpram.ys | 18 +++++++++++
tests/ice40/dpram_tb.v | 81 +++++++++++++++++++++++++++++++++++++++++++++++++
tests/ice40/run-test.sh | 2 +-
4 files changed, 120 insertions(+), 1 deletion(-)
create mode 100644 tests/ice40/dpram.v
create mode 100644 tests/ice40/dpram.ys
create mode 100644 tests/ice40/dpram_tb.v
diff --git a/tests/ice40/dpram.v b/tests/ice40/dpram.v
new file mode 100644
index 000000000..2e69d6b3b
--- /dev/null
+++ b/tests/ice40/dpram.v
@@ -0,0 +1,20 @@
+module top (din, write_en, waddr, wclk, raddr, rclk, dout);
+parameter addr_width = 8;
+parameter data_width = 8;
+input [addr_width-1:0] waddr, raddr;
+input [data_width-1:0] din;
+input write_en, wclk, rclk;
+output [data_width-1:0] dout;
+reg [data_width-1:0] dout;
+reg [data_width-1:0] mem [(1<<addr_width)-1:0]
+/* synthesis syn_ramstyle = "no_rw_check" */ ;
+always @(posedge wclk) // Write memory.
+begin
+if (write_en)
+mem[waddr] <= din; // Using write address bus.
+end
+always @(posedge rclk) // Read memory.
+begin
+dout <= mem[raddr]; // Using read address bus.
+end
+endmodule
diff --git a/tests/ice40/dpram.ys b/tests/ice40/dpram.ys
new file mode 100644
index 000000000..77364e5ae
--- /dev/null
+++ b/tests/ice40/dpram.ys
@@ -0,0 +1,18 @@
+read_verilog dpram.v
+hierarchy -top top
+proc
+memory -nomap
+equiv_opt -run :prove -map +/ice40/cells_sim.v synth_ice40
+memory
+opt -full
+
+# TODO
+#equiv_opt -run prove: -assert null
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+#sat -verify -prove-asserts -tempinduct -show-inputs -show-outputs miter
+
+design -load postopt
+cd top
+select -assert-count 1 t:SB_RAM40_4K
+select -assert-none t:SB_RAM40_4K %% t:* %D
+write_verilog dpram_synth.v
diff --git a/tests/ice40/dpram_tb.v b/tests/ice40/dpram_tb.v
new file mode 100644
index 000000000..dede64614
--- /dev/null
+++ b/tests/ice40/dpram_tb.v
@@ -0,0 +1,81 @@
+module testbench;
+ reg clk;
+
+ initial begin
+ // $dumpfile("testbench.vcd");
+ // $dumpvars(0, testbench);
+
+ #5 clk = 0;
+ repeat (10000) begin
+ #5 clk = 1;
+ #5 clk = 0;
+ end
+ end
+
+
+ reg [7:0] data_a = 0;
+ reg [7:0] addr_a = 0;
+ reg [7:0] addr_b = 0;
+ reg we_a = 0;
+ reg re_a = 1;
+ wire [7:0] q_a;
+ reg mem_init = 0;
+
+ reg [7:0] pq_a;
+
+ always @(posedge clk) begin
+ #3;
+ data_a <= data_a + 17;
+
+ addr_a <= addr_a + 1;
+ addr_b <= addr_b + 1;
+ end
+
+ always @(posedge addr_a) begin
+ #10;
+ if(addr_a > 6'h3E)
+ mem_init <= 1;
+ end
+
+ always @(posedge clk) begin
+ //#3;
+ we_a <= !we_a;
+ end
+
+ reg [7:0] mem [(1<<8)-1:0];
+
+ always @(posedge clk) // Write memory.
+ begin
+ if (we_a)
+ mem[addr_a] <= data_a; // Using write address bus.
+ end
+ always @(posedge clk) // Read memory.
+ begin
+ pq_a <= mem[addr_b]; // Using read address bus.
+ end
+
+ top uut (
+ .din(data_a),
+ .write_en(we_a),
+ .waddr(addr_a),
+ .wclk(clk),
+ .raddr(addr_b),
+ .rclk(clk),
+ .dout(q_a)
+ );
+
+ uut_mem_checker port_a_test(.clk(clk), .init(mem_init), .en(!we_a), .A(q_a), .B(pq_a));
+
+endmodule
+
+module uut_mem_checker(input clk, input init, input en, input [7:0] A, input [7:0] B);
+ always @(posedge clk)
+ begin
+ #1;
+ if (en == 1 & init == 1 & A !== B)
+ begin
+ $display("ERROR: ASSERTION FAILED in %m:",$time," ",A," ",B);
+ $stop;
+ end
+ end
+endmodule
diff --git a/tests/ice40/run-test.sh b/tests/ice40/run-test.sh
index ddd6d349f..75aa08339 100755
--- a/tests/ice40/run-test.sh
+++ b/tests/ice40/run-test.sh
@@ -16,7 +16,7 @@ for x in *.ys; do
done
for t in *_tb.v; do
echo "all:: run-$t"
- echo "run-$t:"
+ echo "run-$t: ${t%_tb.v}_synth.v"
echo " @echo 'Running $t..'"
echo " @iverilog -o ${t%_tb.v}_testbench $t ${t%_tb.v}_synth.v common.v $TECHLIBS_PREFIX/ice40/cells_sim.v"
echo " @vvp -N ${t%_tb.v}_testbench"
--
cgit v1.2.3