synth_nexus: Initial implementation

Signed-off-by: David Shah <dave@ds0.me>

tests/arch/nexus/.gitignore

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

tests/arch/nexus/add_sub.ys

@@ -0,0 +1,21 @@
+read_verilog ../common/add_sub.v
+hierarchy -top top
+proc
+design -save orig
+
+equiv_opt -assert -map +/nexus/cells_sim.v synth_nexus # 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
+stat
+select -assert-count 10 t:LUT4
+select -assert-none t:IB t:OB t:VLO t:LUT4 %% t:* %D
+
+design -load orig
+
+equiv_opt -assert -map +/nexus/cells_sim.v synth_nexus -abc9 # 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
+stat
+select -assert-count 6 t:LUT4
+select -assert-count 4 t:WIDEFN9
+select -assert-none t:IB t:OB t:VLO t:LUT4 t:WIDEFN9 %% t:* %D

tests/arch/nexus/adffs.ys

@@ -0,0 +1,44 @@
+read_verilog ../common/adffs.v
+design -save read
+
+hierarchy -top adff
+proc
+equiv_opt -async2sync -assert -map +/nexus/cells_sim.v synth_nexus # 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
+stat
+select -assert-count 1 t:FD1P3DX
+select -assert-none t:FD1P3DX t:IB t:OB t:VLO t:VHI %% t:* %D
+
+design -load read
+hierarchy -top adffn
+proc
+equiv_opt -async2sync -assert -map +/nexus/cells_sim.v synth_nexus # 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
+stat
+select -assert-count 1 t:FD1P3DX
+select -assert-count 1 t:INV
+select -assert-none t:FD1P3DX t:INV t:LUT4 t:IB t:OB t:VLO t:VHI %% t:* %D
+
+design -load read
+hierarchy -top dffs
+proc
+equiv_opt -async2sync -assert -map +/nexus/cells_sim.v synth_nexus # 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
+stat
+select -assert-count 1 t:FD1P3IX
+select -assert-count 1 t:LUT4
+select -assert-none t:FD1P3IX t:LUT4 t:IB t:OB t:VLO t:VHI %% t:* %D
+
+design -load read
+hierarchy -top ndffnr
+proc
+equiv_opt -async2sync -assert -map +/nexus/cells_sim.v synth_nexus # 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
+stat
+select -assert-count 1 t:FD1P3IX
+select -assert-count 2 t:INV
+select -assert-none t:FD1P3IX t:INV t:LUT4 t:IB t:OB t:VLO t:VHI %% t:* %D

tests/arch/nexus/blockram.ys

@@ -0,0 +1,18 @@
+read_verilog ../common/blockram.v
+design -save read
+
+# Check that we use the right dual and single clock variants
+
+chparam -set ADDRESS_WIDTH 10 -set DATA_WIDTH 18 sync_ram_sdp
+synth_nexus -top sync_ram_sdp
+cd sync_ram_sdp
+select -assert-count 1 t:PDPSC16K
+select -assert-none t:PDPSC16K t:INV t:IB t:OB t:VLO t:VHI %% t:* %D
+
+design -reset
+read_verilog blockram_dc.v
+chparam -set ADDRESS_WIDTH 10 -set DATA_WIDTH 18 sync_ram_sdp_dc
+synth_nexus -top sync_ram_sdp_dc
+cd sync_ram_sdp_dc
+select -assert-count 1 t:PDP16K
+select -assert-none t:PDP16K t:INV t:IB t:OB t:VLO t:VHI  %% t:* %D

tests/arch/nexus/blockram_dc.v

@@ -0,0 +1,25 @@
+
+`default_nettype none
+module sync_ram_sdp_dc #(parameter DATA_WIDTH=8, ADDRESS_WIDTH=10)
+   (input  wire                      clkw, clkr, write_enable,
+    input  wire  [DATA_WIDTH-1:0]    data_in,
+    input  wire  [ADDRESS_WIDTH-1:0] address_in_r, address_in_w,
+    output wire  [DATA_WIDTH-1:0]    data_out);
+
+  localparam WORD  = (DATA_WIDTH-1);
+  localparam DEPTH = (2**ADDRESS_WIDTH-1);
+
+  reg [WORD:0] data_out_r;
+  reg [WORD:0] memory [0:DEPTH];
+
+  always @(posedge clkw) begin
+    if (write_enable)
+      memory[address_in_w] <= data_in;
+  end
+  always @(posedge clkr) begin
+    data_out_r <= memory[address_in_r];
+  end
+
+  assign data_out = data_out_r;
+
+endmodule // sync_ram_sdp_dc

tests/arch/nexus/counter.ys

@@ -0,0 +1,11 @@
+read_verilog ../common/counter.v
+hierarchy -top top
+proc
+flatten
+equiv_opt -assert -multiclock -map +/nexus/cells_sim.v synth_nexus # 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
+stat
+select -assert-count 5 t:CCU2
+select -assert-count 8 t:FD1P3DX
+select -assert-none t:CCU2 t:FD1P3DX t:IB t:OB t:VLO t:VHI %% t:* %D

tests/arch/nexus/dffs.ys

@@ -0,0 +1,19 @@
+read_verilog ../common/dffs.v
+design -save read
+
+hierarchy -top dff
+proc
+equiv_opt -assert -map +/nexus/cells_sim.v synth_nexus # 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:FD1P3IX
+select -assert-none t:FD1P3IX t:IB t:OB t:VHI t:VLO %% t:* %D
+
+design -load read
+hierarchy -top dffe
+proc
+equiv_opt -assert -map +/nexus/cells_sim.v synth_nexus # 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
+select -assert-count 1 t:FD1P3IX
+select -assert-none t:FD1P3IX t:IB t:OB t:VHI t:VLO %% t:* %D

tests/arch/nexus/fsm.ys

@@ -0,0 +1,19 @@
+read_verilog ../common/fsm.v
+hierarchy -top fsm
+proc
+flatten
+
+equiv_opt -run :prove -map +/nexus/cells_sim.v synth_nexus
+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
+
+stat
+
+select -assert-max 1 t:INV
+select -assert-max 2 t:LUT4
+select -assert-max 6 t:WIDEFN9
+select -assert-count 6 t:FD1P3IX
+select -assert-none t:LUT4 t:FD1P3IX t:WIDEFN9 t:INV t:IB t:OB t:VLO t:VHI %% t:* %D

tests/arch/nexus/logic.ys

@@ -0,0 +1,8 @@
+read_verilog ../common/logic.v
+hierarchy -top top
+proc
+equiv_opt -assert -map +/nexus/cells_sim.v synth_nexus # 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:LUT4
+select -assert-none t:LUT4 t:INV t:IB t:OB t:VLO t:VHI %% t:* %D

tests/arch/nexus/lutram.ys

@@ -0,0 +1,19 @@
+read_verilog ../common/lutram.v
+hierarchy -top lutram_1w1r
+proc
+memory -nomap
+equiv_opt -run :prove -map +/nexus/cells_sim.v synth_nexus
+memory
+opt -full
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -seq 5 -set-init-zero -show-inputs -show-outputs miter
+
+design -load postopt
+cd lutram_1w1r
+stat
+select -assert-count 8 t:WIDEFN9
+select -assert-count 16 t:LUT4
+select -assert-count 8 t:DPR16X4
+select -assert-count 36 t:FD1P3IX
+select -assert-none t:DPR16X4 t:FD1P3IX t:WIDEFN9 t:LUT4 t:INV t:IB t:OB t:VLO t:VHI %% t:* %D

tests/arch/nexus/mul.ys

@@ -0,0 +1,28 @@
+read_verilog ../common/mul.v
+hierarchy -top top
+proc
+
+design -save read
+
+equiv_opt -assert -map +/nexus/cells_sim.v synth_nexus
+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 7 t:CCU2
+select -assert-max 5 t:WIDEFN9
+select -assert-max 62 t:LUT4
+
+select -assert-none t:IB t:OB t:VLO t:VHI t:LUT4 t:CCU2 t:WIDEFN9 %% t:* %D
+
+design -load read
+
+equiv_opt -assert -map +/nexus/cells_sim.v synth_nexus -abc9
+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
+
+stat
+
+select -assert-count 7 t:CCU2
+select -assert-max 12 t:WIDEFN9
+select -assert-max 58 t:LUT4
+
+select -assert-none t:IB t:OB t:VLO t:VHI t:LUT4 t:CCU2 t:WIDEFN9 %% t:* %D

tests/arch/nexus/mux.ys

@@ -0,0 +1,43 @@
+read_verilog ../common/mux.v
+design -save read
+
+hierarchy -top mux2
+proc
+equiv_opt -assert -map +/nexus/cells_sim.v synth_nexus # 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:LUT4
+select -assert-none t:IB t:OB t:VLO t:VHI t:LUT4 t:WIDEFN9 %% t:* %D
+
+design -load read
+hierarchy -top mux4
+proc
+equiv_opt -assert -map +/nexus/cells_sim.v synth_nexus # 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 1 t:WIDEFN9
+
+select -assert-none t:IB t:OB t:VLO t:VHI t:LUT4 t:WIDEFN9 %% t:* %D
+
+design -load read
+hierarchy -top mux8
+proc
+equiv_opt -assert -map +/nexus/cells_sim.v synth_nexus # 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 4 t:LUT4
+select -assert-count 1 t:WIDEFN9
+
+select -assert-none t:IB t:OB t:VLO t:VHI t:LUT4 t:WIDEFN9 %% t:* %D
+
+design -load read
+hierarchy -top mux16
+proc
+equiv_opt -assert -map +/nexus/cells_sim.v synth_nexus # 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-min 11 t:LUT4
+select -assert-max 12 t:LUT4
+select -assert-count 1 t:WIDEFN9
+
+select -assert-none t:IB t:OB t:VLO t:VHI t:LUT4 t:WIDEFN9 %% t:* %D

tests/arch/nexus/run-test.sh

@@ -0,0 +1,20 @@
+#!/usr/bin/env bash
+set -e
+{
+echo "all::"
+for x in *.ys; do
+	echo "all:: run-$x"
+	echo "run-$x:"
+	echo "	@echo 'Running $x..'"
+	echo "	@../../../yosys -ql ${x%.ys}.log -w 'Yosys has only limited support for tri-state logic at the moment.' $x"
+done
+for s in *.sh; do
+	if [ "$s" != "run-test.sh" ]; then
+		echo "all:: run-$s"
+		echo "run-$s:"
+		echo "	@echo 'Running $s..'"
+		echo "	@bash $s"
+	fi
+done
+} > run-test.mk
+exec ${MAKE:-make} -f run-test.mk

tests/arch/nexus/shifter.ys

@@ -0,0 +1,9 @@
+read_verilog ../common/shifter.v
+hierarchy -top top
+proc
+flatten
+equiv_opt -assert -map +/nexus/cells_sim.v synth_nexus # 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:FD1P3IX
+select -assert-none t:FD1P3IX t:WIDEFN9 t:INV t:IB t:OB t:VLO t:VHI %% t:* %D

tests/arch/nexus/tribuf.ys

@@ -0,0 +1,12 @@
+read_verilog ../common/tribuf.v
+hierarchy -top tristate
+proc
+tribuf
+flatten
+synth
+equiv_opt -assert -map +/nexus/cells_sim.v -map +/simcells.v synth_nexus # 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
+select -assert-count 1 t:OBZ
+select -assert-count 1 t:INV
+select -assert-none t:OBZ t:INV t:IB t:OB t:VLO t:VHI %% t:* %D