8 files changed, 230 insertions, 0 deletions
diff --git a/techlibs/ice40/tests/.gitignore b/techlibs/ice40/tests/.gitignore
new file mode 100644
index 000000000..b58f9ad4a
--- /dev/null
+++ b/techlibs/ice40/tests/.gitignore
@@ -0,0 +1,2 @@
+test_ffs_[01][01][01][01][01]_*
+test_bram_[0-9]*
diff --git a/techlibs/ice40/tests/test_arith.v b/techlibs/ice40/tests/test_arith.v
new file mode 100644
index 000000000..77f79b973
--- /dev/null
+++ b/techlibs/ice40/tests/test_arith.v
@@ -0,0 +1,3 @@
+module test(input [4:0] a, b, c, output [4:0] y);
+	assign y = ((a+b) ^ (a-c)) - ((a*b) + (a*c) - (b*c));
+endmodule
diff --git a/techlibs/ice40/tests/test_arith.ys b/techlibs/ice40/tests/test_arith.ys
new file mode 100644
index 000000000..160c767fb
--- /dev/null
+++ b/techlibs/ice40/tests/test_arith.ys
@@ -0,0 +1,10 @@
+read_verilog test_arith.v
+synth_ice40
+techmap -map ../cells_sim.v
+rename test gate
+
+read_verilog test_arith.v
+rename test gold
+
+miter -equiv -flatten -make_outputs gold gate miter
+sat -verify -prove trigger 0 -show-ports miter
diff --git a/techlibs/ice40/tests/test_bram.sh b/techlibs/ice40/tests/test_bram.sh
new file mode 100644
index 000000000..d4d641a9c
--- /dev/null
+++ b/techlibs/ice40/tests/test_bram.sh
@@ -0,0 +1,19 @@
+#!/bin/bash
+
+set -ex
+
+for abits in 7 8 9 10 11 12; do
+for dbits in 2 4 8 16 24 32; do
+	id="test_bram_${abits}_${dbits}"
+	iadr=$((RANDOM % (1 << abits)))
+	idat=$((RANDOM % ((1 << dbits) - 1) + 1))
+	sed -re "s/(ABITS = )0/\1$abits/g; s/(DBITS = )0/\1$dbits/g; s/(INIT_ADDR = )0/\1$iadr/g; s/(INIT_DATA = )0/\1$idat/g;" < test_bram.v > ${id}.v
+	sed -re "s/(ABITS = )0/\1$abits/g; s/(DBITS = )0/\1$dbits/g; s/(INIT_ADDR = )0/\1$iadr/g; s/(INIT_DATA = )0/\1$idat/g;" < test_bram_tb.v > ${id}_tb.v
+	../../../yosys -ql ${id}_syn.log -p "synth_ice40" -o ${id}_syn.v ${id}.v
+	# iverilog -s bram_tb -o ${id}_tb ${id}_syn.v ${id}_tb.v /opt/lscc/iCEcube2.2014.08/verilog/sb_ice_syn.v
+	iverilog -s bram_tb -o ${id}_tb ${id}_syn.v ${id}_tb.v ../cells_sim.v
+	./${id}_tb > ${id}_tb.txt
+	if grep -H ERROR ${id}_tb.txt; then false; fi
+done; done
+echo OK
+
diff --git a/techlibs/ice40/tests/test_bram.v b/techlibs/ice40/tests/test_bram.v
new file mode 100644
index 000000000..320735d07
--- /dev/null
+++ b/techlibs/ice40/tests/test_bram.v
@@ -0,0 +1,24 @@
+module bram #(
+	parameter ABITS = 8, DBITS = 8,
+	parameter INIT_ADDR = 0, INIT_DATA = 0
+) (
+	input clk,
+
+	input [ABITS-1:0] WR_ADDR,
+	input [DBITS-1:0] WR_DATA,
+	input WR_EN,
+
+	input [ABITS-1:0] RD_ADDR,
+	output reg [DBITS-1:0] RD_DATA
+);
+	reg [DBITS-1:0] memory [0:2**ABITS-1];
+
+	initial begin
+		memory[INIT_ADDR] <= INIT_DATA;
+	end
+
+	always @(posedge clk) begin
+		if (WR_EN) memory[WR_ADDR] <= WR_DATA;
+		RD_DATA <= memory[RD_ADDR];
+	end
+endmodule
diff --git a/techlibs/ice40/tests/test_bram_tb.v b/techlibs/ice40/tests/test_bram_tb.v
new file mode 100644
index 000000000..bdb8d4560
--- /dev/null
+++ b/techlibs/ice40/tests/test_bram_tb.v
@@ -0,0 +1,110 @@
+module bram_tb #(
+	parameter ABITS = 8, DBITS = 8,
+	parameter INIT_ADDR = 0, INIT_DATA = 0
+);
+	reg clk;
+	reg [ABITS-1:0] WR_ADDR;
+	reg [DBITS-1:0] WR_DATA;
+	reg WR_EN;
+	reg [ABITS-1:0] RD_ADDR;
+	wire [DBITS-1:0] RD_DATA;
+
+	bram uut  (
+		.clk    (clk    ),
+		.WR_ADDR(WR_ADDR),
+		.WR_DATA(WR_DATA),
+		.WR_EN  (WR_EN  ),
+		.RD_ADDR(RD_ADDR),
+		.RD_DATA(RD_DATA)
+	);
+
+	reg [63:0] xorshift64_state = 64'd88172645463325252 ^ (ABITS << 24) ^ (DBITS << 16);
+
+	task xorshift64_next;
+		begin
+		// see page 4 of Marsaglia, George (July 2003). "Xorshift RNGs". Journal of Statistical Software 8 (14).
+		xorshift64_state = xorshift64_state ^ (xorshift64_state << 13);
+		xorshift64_state = xorshift64_state ^ (xorshift64_state >>  7);
+		xorshift64_state = xorshift64_state ^ (xorshift64_state << 17);
+		end
+	endtask
+
+	reg [ABITS-1:0] randaddr1;
+	reg [ABITS-1:0] randaddr2;
+	reg [ABITS-1:0] randaddr3;
+
+	function [31:0] getaddr(input [3:0] n);
+		begin
+			case (n)
+				0: getaddr = 0;
+				1: getaddr = 2**ABITS-1;
+				2: getaddr = 'b101 << (ABITS / 3);
+				3: getaddr = 'b101 << (2*ABITS / 3);
+				4: getaddr = 'b11011 << (ABITS / 4);
+				5: getaddr = 'b11011 << (2*ABITS / 4);
+				6: getaddr = 'b11011 << (3*ABITS / 4);
+				7: getaddr = randaddr1;
+				8: getaddr = randaddr2;
+				9: getaddr = randaddr3;
+				default: begin
+					getaddr = 1 << (2*n-16);
+					if (!getaddr) getaddr = xorshift64_state;
+				end
+			endcase
+		end
+	endfunction
+
+	reg [DBITS-1:0] memory [0:2**ABITS-1];
+	reg [DBITS-1:0] expected_rd, expected_rd_masked;
+
+	event error;
+	integer i, j;
+
+	initial begin
+		// $dumpfile("testbench.vcd");
+		// $dumpvars(0, bram_tb);
+
+		memory[INIT_ADDR] <= INIT_DATA;
+
+		xorshift64_next;
+		xorshift64_next;
+		xorshift64_next;
+		xorshift64_next;
+
+		randaddr1 = xorshift64_state;
+		xorshift64_next;
+
+		randaddr2 = xorshift64_state;
+		xorshift64_next;
+
+		randaddr3 = xorshift64_state;
+		xorshift64_next;
+
+		clk <= 0;
+		for (i = 0; i < 512; i = i+1) begin
+			WR_DATA = xorshift64_state;
+			xorshift64_next;
+
+			WR_ADDR = getaddr(i < 256 ? i[7:4] : xorshift64_state[63:60]);
+			xorshift64_next;
+
+			RD_ADDR = i == 0 ? INIT_ADDR : getaddr(i < 256 ? i[3:0] : xorshift64_state[59:56]);
+			WR_EN = xorshift64_state[55] && ((WR_ADDR & 'hff) != (RD_ADDR & 'hff));
+			xorshift64_next;
+
+			#1; clk <= 1;
+			#1; clk <= 0;
+
+			expected_rd = memory[RD_ADDR];
+			if (WR_EN) memory[WR_ADDR] = WR_DATA;
+
+			for (j = 0; j < DBITS; j = j+1)
+				expected_rd_masked[j] = expected_rd[j] !== 1'bx ? expected_rd[j] : RD_DATA[j];
+
+			$display("#OUT# %3d | WA=%x WD=%x WE=%x | RA=%x RD=%x (%x) | %s",
+					i, WR_ADDR, WR_DATA, WR_EN, RD_ADDR, RD_DATA, expected_rd,
+					expected_rd_masked === RD_DATA ? "ok" : "ERROR");
+			if (expected_rd_masked !== RD_DATA) begin -> error; end
+		end
+	end
+endmodule
diff --git a/techlibs/ice40/tests/test_ffs.sh b/techlibs/ice40/tests/test_ffs.sh
new file mode 100644
index 000000000..ff79ec534
--- /dev/null
+++ b/techlibs/ice40/tests/test_ffs.sh
@@ -0,0 +1,20 @@
+#!/bin/bash
+set -ex
+for CLKPOL in 0 1; do
+for ENABLE_EN in 0 1; do
+for RESET_EN in 0 1; do
+for RESET_VAL in 0 1; do
+for RESET_SYN in 0 1; do
+	pf="test_ffs_${CLKPOL}${ENABLE_EN}${RESET_EN}${RESET_VAL}${RESET_SYN}"
+	sed -e "s/CLKPOL = 0/CLKPOL = ${CLKPOL}/;" -e "s/ENABLE_EN = 0/ENABLE_EN = ${ENABLE_EN}/;" \
+	    -e "s/RESET_EN = 0/RESET_EN = ${RESET_EN}/;" -e "s/RESET_VAL = 0/RESET_VAL = ${RESET_VAL}/;" \
+	    -e "s/RESET_SYN = 0/RESET_SYN = ${RESET_SYN}/;" test_ffs.v > ${pf}_gold.v
+	../../../yosys -o ${pf}_gate.v -p "synth_ice40" ${pf}_gold.v
+	../../../yosys -p "proc; opt; test_autotb ${pf}_tb.v" ${pf}_gold.v
+	iverilog -s testbench -o ${pf}_gold ${pf}_gold.v ${pf}_tb.v
+	iverilog -s testbench -o ${pf}_gate ${pf}_gate.v ${pf}_tb.v ../cells_sim.v
+	./${pf}_gold > ${pf}_gold.txt
+	./${pf}_gate > ${pf}_gate.txt
+	cmp ${pf}_gold.txt ${pf}_gate.txt
+done; done; done; done; done
+echo OK.
diff --git a/techlibs/ice40/tests/test_ffs.v b/techlibs/ice40/tests/test_ffs.v
new file mode 100644
index 000000000..1f6883f3c
--- /dev/null
+++ b/techlibs/ice40/tests/test_ffs.v
@@ -0,0 +1,42 @@
+module test(D, C, E, R, Q);
+	parameter [0:0] CLKPOL = 0;
+	parameter [0:0] ENABLE_EN = 0;
+	parameter [0:0] RESET_EN = 0;
+	parameter [0:0] RESET_VAL = 0;
+	parameter [0:0] RESET_SYN = 0;
+
+	(* gentb_clock *)
+	input D, C, E, R;
+
+	output Q;
+
+	wire gated_reset = R & RESET_EN;
+	wire gated_enable = E | ~ENABLE_EN;
+	reg posedge_q, negedge_q, posedge_sq, negedge_sq;
+
+	always @(posedge C, posedge gated_reset)
+		if (gated_reset)
+			posedge_q <= RESET_VAL;
+		else if (gated_enable)
+			posedge_q <= D;
+
+	always @(negedge C, posedge gated_reset)
+		if (gated_reset)
+			negedge_q <= RESET_VAL;
+		else if (gated_enable)
+			negedge_q <= D;
+
+	always @(posedge C)
+		if (gated_reset)
+			posedge_sq <= RESET_VAL;
+		else if (gated_enable)
+			posedge_sq <= D;
+
+	always @(negedge C)
+		if (gated_reset)
+			negedge_sq <= RESET_VAL;
+		else if (gated_enable)
+			negedge_sq <= D;
+
+	assign Q = RESET_SYN ? (CLKPOL ? posedge_sq : negedge_sq) : (CLKPOL ? posedge_q : negedge_q);
+endmodule