Merge pull request #4504 from YosysHQ/nanoxplore

NanoXplore synthesis

tests/arch/nanoxplore/.gitignore

@@ -0,0 +1,2 @@
+*.log
+/run-test.mk

tests/arch/nanoxplore/add_sub.ys

@@ -0,0 +1,71 @@
+read_verilog ../common/add_sub.v
+hierarchy -top top
+proc
+equiv_opt -run :prove -map +/nanoxplore/cells_sim.v -map +/nanoxplore/cells_sim_u.v synth_nanoxplore -noiopad
+opt -full
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd top # Constrain all select calls below inside the top module
+select -assert-count 2 t:NX_CY
+select -assert-count 4 t:NX_LUT
+select -assert-none t:NX_CY t:NX_LUT %% t:* %D
+
+design -reset
+read_verilog <<EOT
+module top
+(
+    input [5:0] x,
+    input [5:0] y,
+
+    output [5:0] A,
+    input CI,
+    output CO
+);
+
+    assign {CO, A} =  x + y + CI;
+endmodule
+EOT
+
+hierarchy -top top
+proc
+equiv_opt -run :prove -map +/nanoxplore/cells_sim.v -map +/nanoxplore/cells_sim_u.v synth_nanoxplore -noiopad
+opt -full
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter
+
+design -load postopt
+cd top
+stat
+select -assert-count 2 t:NX_CY
+select -assert-none t:NX_CY %% t:* %D
+
+design -reset
+read_verilog <<EOT
+module top
+(
+    input [189:0] x,
+    input [189:0] y,
+
+    output [189:0] A
+);
+
+    assign A =  x + y;
+endmodule
+EOT
+
+hierarchy -top top
+proc
+equiv_opt -run :prove -map +/nanoxplore/cells_sim.v -map +/nanoxplore/cells_sim_u.v synth_nanoxplore -noiopad
+opt -full
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter
+
+design -load postopt
+cd top
+stat
+select -assert-count 48 t:NX_CY
+select -assert-none t:NX_CY %% t:* %D

tests/arch/nanoxplore/adffs.ys

@@ -0,0 +1,47 @@
+read_verilog ../common/adffs.v
+design -save read
+
+hierarchy -top adff
+proc
+equiv_opt -async2sync -assert -map +/nanoxplore/cells_sim.v synth_nanoxplore -noiopad # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd adff # Constrain all select calls below inside the top module
+select -assert-count 1 t:NX_DFF
+
+select -assert-none t:NX_DFF %% t:* %D
+
+
+design -load read
+hierarchy -top adffn
+proc
+equiv_opt -async2sync -assert -map +/nanoxplore/cells_sim.v synth_nanoxplore -noiopad # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd adffn # Constrain all select calls below inside the top module
+select -assert-count 1 t:NX_DFF
+select -assert-count 1 t:NX_LUT
+
+select -assert-none t:NX_DFF t:NX_LUT %% t:* %D
+
+
+design -load read
+hierarchy -top dffs
+proc
+equiv_opt -async2sync -assert -map +/nanoxplore/cells_sim.v synth_nanoxplore -noiopad # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd dffs # Constrain all select calls below inside the top module
+select -assert-count 1 t:NX_DFF
+select -assert-count 1 t:NX_LUT
+
+select -assert-none t:NX_DFF t:NX_LUT %% t:* %D
+
+
+design -load read
+hierarchy -top ndffnr
+proc
+equiv_opt -async2sync -assert -map +/nanoxplore/cells_sim.v synth_nanoxplore -noiopad # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd ndffnr # Constrain all select calls below inside the top module
+select -assert-count 1 t:NX_DFF
+select -assert-count 1 t:NX_LUT
+
+select -assert-none t:NX_DFF t:NX_LUT %% t:* %D

tests/arch/nanoxplore/dffs.ys

@@ -0,0 +1,22 @@
+read_verilog ../common/dffs.v
+design -save read
+
+hierarchy -top dff
+proc
+equiv_opt -assert -async2sync -map +/nanoxplore/cells_sim.v synth_nanoxplore -noiopad # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd dff # Constrain all select calls below inside the top module
+select -assert-count 1 t:NX_DFF
+
+select -assert-none t:NX_DFF %% t:* %D
+
+design -load read
+hierarchy -top dffe
+proc
+equiv_opt -assert -async2sync -map +/nanoxplore/cells_sim.v synth_nanoxplore -noiopad -min_ce_use 0 # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd dffe # Constrain all select calls below inside the top module
+stat
+select -assert-count 1 t:NX_DFF
+
+select -assert-none t:NX_DFF %% t:* %D

tests/arch/nanoxplore/fsm.ys

@@ -0,0 +1,16 @@
+read_verilog ../common/fsm.v
+hierarchy -top fsm
+proc
+flatten
+
+equiv_opt -run :prove -map +/nanoxplore/cells_sim.v synth_nanoxplore -noiopad
+async2sync
+miter -equiv -make_assert -flatten gold gate miter
+sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip 1 miter
+
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd fsm # Constrain all select calls below inside the top module
+
+select -assert-count 6 t:NX_DFF
+select -assert-min 13 t:NX_LUT
+select -assert-none t:NX_DFF t:NX_LUT %% t:* %D

tests/arch/nanoxplore/latches.ys

@@ -0,0 +1,33 @@
+read_verilog ../common/latches.v
+design -save read
+
+hierarchy -top latchp
+proc
+# Can't run any sort of equivalence check because latches are blown to LUTs
+synth_nanoxplore -noiopad
+cd latchp # Constrain all select calls below inside the top module
+select -assert-count 1 t:NX_LUT
+
+select -assert-none t:NX_LUT %% t:* %D
+
+
+design -load read
+hierarchy -top latchn
+proc
+# Can't run any sort of equivalence check because latches are blown to LUTs
+synth_nanoxplore -noiopad
+cd latchn # Constrain all select calls below inside the top module
+select -assert-count 1 t:NX_LUT
+
+select -assert-none t:NX_LUT %% t:* %D
+
+
+design -load read
+hierarchy -top latchsr
+proc
+# Can't run any sort of equivalence check because latches are blown to LUTs
+synth_nanoxplore -noiopad
+cd latchsr # Constrain all select calls below inside the top module
+select -assert-count 2 t:NX_LUT
+
+select -assert-none t:NX_LUT %% t:* %D

tests/arch/nanoxplore/logic.ys

@@ -0,0 +1,9 @@
+read_verilog ../common/logic.v
+hierarchy -top top
+proc
+equiv_opt -assert -map +/nanoxplore/cells_sim.v synth_nanoxplore -noiopad # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd top # Constrain all select calls below inside the top module
+
+select -assert-count 9 t:NX_LUT
+select -assert-none t:NX_LUT %% t:* %D

tests/arch/nanoxplore/lutram.ys

@@ -0,0 +1,145 @@
+# Dual-port RAMs.
+# NX_RFB_U in mode 0 (DPREG)
+
+read_verilog <<EOT
+module lutram_dpreg
+#(parameter D_WIDTH=18, A_WIDTH=5)
+(
+	input [D_WIDTH-1:0] data,
+	input [A_WIDTH:1] addr_w, addr_r,
+	input we, clk,
+	output reg [D_WIDTH-1:0] q
+);
+	// Declare the RAM variable
+	reg [D_WIDTH-1:0] ram[(2**A_WIDTH)-1:0];
+
+	// Port A
+	always @ (posedge clk)
+	begin
+		if (we)
+			ram[addr_w] <= data;
+		q <= ram[addr_r];
+	end
+endmodule
+EOT
+
+hierarchy -top lutram_dpreg
+proc
+memory -nomap
+equiv_opt -run :prove -map +/nanoxplore/cells_sim.v -map +/nanoxplore/cells_sim_u.v synth_nanoxplore -noiopad
+memory
+opt -full
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter
+
+design -load postopt
+cd lutram_dpreg
+stat
+select -assert-count 1 t:NX_RFB_U r:mode=0 %i
+select -assert-count 18 t:NX_DFF
+select -assert-none t:NX_RFB_U t:NX_DFF %% t:* %D
+
+# Single-port RAMs.
+# NX_RFB_U in mode 1 (SPREG)
+design -reset
+
+read_verilog ../common/lutram.v
+hierarchy -top lutram_1w1r -chparam A_WIDTH 5 -chparam D_WIDTH 18
+proc
+memory -nomap
+equiv_opt -run :prove -map +/nanoxplore/cells_sim.v -map +/nanoxplore/cells_sim_u.v synth_nanoxplore -noiopad
+memory
+opt -full
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter
+
+design -load postopt
+cd lutram_1w1r
+select -assert-count 1 t:NX_RFB_U r:mode=1 %i
+select -assert-count 18 t:NX_DFF
+select -assert-none t:NX_RFB_U t:NX_DFF %% t:* %D
+
+# Dual-port RAMs.
+# NX_RFB_U in mode 2 (NX_XRFB_64x18)
+design -reset
+read_verilog ../common/lutram.v
+hierarchy -top lutram_1w1r -chparam A_WIDTH 6 -chparam D_WIDTH 18
+proc
+memory -nomap
+equiv_opt -run :prove -map +/nanoxplore/cells_sim.v -map +/nanoxplore/cells_sim_u.v synth_nanoxplore -noiopad
+memory
+opt -full
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter
+
+design -load postopt
+cd lutram_1w1r
+select -assert-count 1 t:NX_RFB_U r:mode=2 %i
+select -assert-count 18 t:NX_DFF
+select -assert-none t:NX_RFB_U t:NX_DFF %% t:* %D
+
+# Dual-port RAMs.
+# NX_RFB_U in mode 3 (NX_XRFB_32x36)
+design -reset
+read_verilog ../common/lutram.v
+hierarchy -top lutram_1w1r -chparam A_WIDTH 5 -chparam D_WIDTH 36
+proc
+memory -nomap
+equiv_opt -run :prove -map +/nanoxplore/cells_sim.v -map +/nanoxplore/cells_sim_u.v synth_nanoxplore -noiopad
+memory
+opt -full
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter
+
+design -load postopt
+cd lutram_1w1r
+select -assert-count 1 t:NX_RFB_U r:mode=3 %i
+select -assert-count 36 t:NX_DFF
+select -assert-none t:NX_RFB_U t:NX_DFF %% t:* %D
+
+# Single write dual read RAMs.
+# NX_RFB_U in mode 4 (NX_XRFB_2R_1W)
+design -reset
+
+read_verilog <<EOT
+module lutram_1w2r
+#(parameter D_WIDTH=8, A_WIDTH=5)
+(
+	input [D_WIDTH-1:0] data_a, data_b,
+	input [A_WIDTH:1] addr_a, addr_b,
+	input we_a, clk,
+	output reg [D_WIDTH-1:0] q_a, q_b
+);
+	// Declare the RAM variable
+	reg [D_WIDTH-1:0] ram[(2**A_WIDTH)-1:0];
+
+	// Port A
+	always @ (posedge clk)
+	begin
+		if (we_a)
+			ram[addr_a] <= data_a;
+		q_a <= ram[addr_a];
+		q_b <= ram[addr_b];
+	end
+endmodule
+EOT
+
+hierarchy -top lutram_1w2r -chparam A_WIDTH 5 -chparam D_WIDTH 18
+proc
+memory -nomap
+equiv_opt -run :prove -map +/nanoxplore/cells_sim.v -map +/nanoxplore/cells_sim_u.v synth_nanoxplore -noiopad
+memory
+opt -full
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter
+
+design -load postopt
+cd lutram_1w2r
+select -assert-count 1 t:NX_RFB_U r:mode=4 %i
+select -assert-count 36 t:NX_DFF
+select -assert-none t:NX_RFB_U t:NX_DFF %% t:* %D

tests/arch/nanoxplore/meminit.v

@@ -0,0 +1,50 @@
+module top(clk);
+parameter DEPTH_LOG2 = 10;
+parameter WIDTH = 36;
+parameter PRIME = 237481091;
+localparam DEPTH = 2**DEPTH_LOG2;
+
+input wire clk;
+
+(* syn_ramstyle = "distributed" *)
+reg [WIDTH-1:0] mem [DEPTH-1:0];
+
+integer i;
+initial begin
+    for (i = 0; i < DEPTH; i = i + 1) begin
+        // Make up data by multiplying a large prime with the address,
+        // then cropping and retaining the lower bits
+        mem[i] = PRIME * (i*2+1);
+    end
+end
+
+reg [DEPTH_LOG2-1:0] counter = 0;
+reg done = 1'b0;
+
+reg did_read = 1'b0;
+reg [DEPTH_LOG2-1:0] read_addr;
+reg [WIDTH-1:0] read_val;
+
+always @(posedge clk) begin
+    if (!done) begin
+        did_read <= 1'b1;
+        read_addr <= counter;
+        read_val <= mem[counter];
+    end else begin
+        did_read <= 1'b0; 
+    end
+
+    if (!done)
+        counter = counter + 1;
+    if (counter == 0)
+        done = 1;
+end
+
+wire [WIDTH-1:0] expect_val = PRIME * (read_addr*2+1);
+always @(posedge clk) begin
+    if (did_read) begin
+        $display("addr %x expected %x actual %x", read_addr, expect_val, read_val);
+        assert(read_val == expect_val);
+    end
+end
+endmodule

tests/arch/nanoxplore/meminit.ys

@@ -0,0 +1,44 @@
+read_verilog -sv meminit.v
+chparam -set DEPTH_LOG2 5 -set WIDTH 36
+prep
+opt_dff
+prep -rdff
+synth_nanoxplore 
+clean_zerowidth
+select -assert-none t:$mem_v2 t:$mem
+read_verilog +/nanoxplore/cells_sim.v +/nanoxplore/cells_sim_u.v
+prep
+async2sync
+hierarchy -top top
+sim -assert -q -n 66 -clock clk
+
+design -reset
+read_verilog -sv meminit.v
+chparam -set DEPTH_LOG2 6 -set WIDTH 18
+prep
+opt_dff
+prep -rdff
+synth_nanoxplore 
+clean_zerowidth
+select -assert-none t:$mem_v2 t:$mem
+read_verilog +/nanoxplore/cells_sim.v +/nanoxplore/cells_sim_u.v
+prep
+async2sync
+hierarchy -top top
+sim -assert -q -n 34 -clock clk
+
+
+design -reset
+read_verilog -sv meminit.v
+chparam -set DEPTH_LOG2 8 -set WIDTH 18
+prep
+opt_dff
+prep -rdff
+synth_nanoxplore 
+clean_zerowidth
+select -assert-none t:$mem_v2 t:$mem
+read_verilog +/nanoxplore/cells_sim.v +/nanoxplore/cells_sim_u.v
+prep
+async2sync
+hierarchy -top top
+sim -assert -q -n 258 -clock clk

tests/arch/nanoxplore/mux.ys

@@ -0,0 +1,41 @@
+read_verilog ../common/mux.v
+design -save read
+
+hierarchy -top mux2
+proc
+equiv_opt -assert -map +/nanoxplore/cells_sim.v synth_nanoxplore -noiopad # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd mux2 # Constrain all select calls below inside the top module
+select -assert-count 1 t:NX_LUT
+
+select -assert-none t:NX_LUT %% t:* %D
+
+design -load read
+hierarchy -top mux4
+proc
+equiv_opt -assert -map +/nanoxplore/cells_sim.v synth_nanoxplore -noiopad # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd mux4 # Constrain all select calls below inside the top module
+#select -assert-count 2 t:NX_LUT
+
+select -assert-none t:NX_LUT %% t:* %D
+
+design -load read
+hierarchy -top mux8
+proc
+equiv_opt -assert -map +/nanoxplore/cells_sim.v synth_nanoxplore -noiopad # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd mux8 # Constrain all select calls below inside the top module
+#select -assert-count 5 t:NX_LUT
+
+select -assert-none t:NX_LUT %% t:* %D
+
+design -load read
+hierarchy -top mux16
+proc
+equiv_opt -assert -map +/nanoxplore/cells_sim.v synth_nanoxplore -noiopad # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd mux16 # Constrain all select calls below inside the top module
+select -assert-max 13 t:NX_LUT
+
+select -assert-none t:NX_LUT %% t:* %D

tests/arch/nanoxplore/run-test.sh

@@ -0,0 +1,4 @@
+#!/usr/bin/env bash
+set -eu
+source ../../gen-tests-makefile.sh
+run_tests --yosys-scripts --bash --yosys-args "-w 'Yosys has only limited support for tri-state logic at the moment.'"

tests/arch/nanoxplore/shifter.ys

@@ -0,0 +1,10 @@
+read_verilog ../common/shifter.v
+hierarchy -top top
+proc
+flatten
+equiv_opt -async2sync -assert -map +/nanoxplore/cells_sim.v synth_nanoxplore -noiopad # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd top # Constrain all select calls below inside the top module
+
+select -assert-count 8  t:NX_DFF
+select -assert-none t:NX_DFF %% t:* %D

tests/arch/nanoxplore/tribuf.ys

@@ -0,0 +1,13 @@
+read_verilog ../common/tribuf.v
+hierarchy -top tristate
+proc
+tribuf
+flatten
+synth
+equiv_opt -assert -map +/nanoxplore/cells_sim.v -map +/simcells.v synth_nanoxplore # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd tristate # Constrain all select calls below inside the top module
+#Internal cell type used. Need support it.
+select -assert-count 1 t:NX_IOB
+select -assert-count 2 t:NX_IOB_I
+select -assert-none t:NX_IOB t:NX_IOB_I %% t:* %D