From b4e9bb0d85f38ce81fd3eb7733e8ea35a269dc82 Mon Sep 17 00:00:00 2001 From: Lofty Date: Fri, 1 Mar 2024 10:55:54 +0100 Subject: [PATCH] Add FFs and related tests --- techlibs/nanoxplore/cells_map.v | 33 +++++++++++++++++++++++ techlibs/nanoxplore/cells_sim.v | 25 +++++++++++++++++ tests/arch/nanoxplore/adffs.ys | 46 ++++++++++++++++++++++++++++++++ tests/arch/nanoxplore/dffs.ys | 22 +++++++++++++++ tests/arch/nanoxplore/fsm.ys | 16 +++++++++++ tests/arch/nanoxplore/latches.ys | 35 ++++++++++++++++++++++++ tests/arch/nanoxplore/shifter.ys | 10 +++++++ 7 files changed, 187 insertions(+) create mode 100644 tests/arch/nanoxplore/adffs.ys create mode 100644 tests/arch/nanoxplore/dffs.ys create mode 100644 tests/arch/nanoxplore/fsm.ys create mode 100644 tests/arch/nanoxplore/latches.ys create mode 100644 tests/arch/nanoxplore/shifter.ys diff --git a/techlibs/nanoxplore/cells_map.v b/techlibs/nanoxplore/cells_map.v index a0d0e6957..efa2a2af5 100644 --- a/techlibs/nanoxplore/cells_map.v +++ b/techlibs/nanoxplore/cells_map.v @@ -33,3 +33,36 @@ module \$lut (A, Y); end endgenerate endmodule + +(* techmap_celltype = "$_DFF_[NP]P[01]_" *) +module dff(input D, C, R, output Q); + parameter _TECHMAP_CELLTYPE = "$_DFF_PP1_"; + localparam dff_edge = _TECHMAP_CELLTYPE[6*8 +: 8] == "N"; + localparam dff_type = _TECHMAP_CELLTYPE[8*8 +: 8] == "1"; + wire _TECHMAP_REMOVEINIT_Q_ = 1'b1; + NX_DFF #(.dff_ctxt(1'b0), .dff_edge(dff_edge), .dff_init(1'b1), .dff_load(1'b0), .dff_sync(1'b0), .dff_type(dff_type)) _TECHMAP_REPLACE_ (.I(D), .CK(C), .L(1'b0), .R(R), .O(Q)); +endmodule + +(* techmap_celltype = "$_ALDFF_[NP]P_" *) +module aldff(input D, C, L, AD, output Q); + parameter _TECHMAP_CELLTYPE = "$_ALDFF_PP_"; + localparam dff_edge = _TECHMAP_CELLTYPE[8*8 +: 8] == "N"; + wire _TECHMAP_REMOVEINIT_Q_ = 1'b1; + NX_DFF #(.dff_ctxt(1'b0), .dff_edge(dff_edge), .dff_init(1'b1), .dff_load(1'b1), .dff_sync(1'b0), .dff_type(2)) _TECHMAP_REPLACE_ (.I(D), .CK(C), .L(AD), .R(L), .O(Q)); +endmodule + +module \$_SDFF_PP0_ (input D, C, R, output Q); + NX_DFF #(.dff_ctxt(1'b0), .dff_edge(1'b0), .dff_init(1'b1), .dff_load(1'b0), .dff_sync(1'b1), .dff_type(1'b0)) _TECHMAP_REPLACE_ (.I(D), .CK(C), .L(1'b0), .R(R), .O(Q)); +endmodule + +module \$_SDFF_PP1_ (input D, C, R, output Q); + NX_DFF #(.dff_ctxt(1'b0), .dff_edge(1'b0), .dff_init(1'b1), .dff_load(1'b0), .dff_sync(1'b1), .dff_type(1'b1)) _TECHMAP_REPLACE_ (.I(D), .CK(C), .L(1'b0), .R(R), .O(Q)); +endmodule + +module \$_SDFF_NP0_ (input D, C, R, output Q); + NX_DFF #(.dff_ctxt(1'b0), .dff_edge(1'b1), .dff_init(1'b1), .dff_load(1'b0), .dff_sync(1'b1), .dff_type(1'b0)) _TECHMAP_REPLACE_ (.I(D), .CK(C), .L(1'b0), .R(R), .O(Q)); +endmodule + +module \$_SDFF_NP1_ (input D, C, R, output Q); + NX_DFF #(.dff_ctxt(1'b0), .dff_edge(1'b1), .dff_init(1'b1), .dff_load(1'b0), .dff_sync(1'b1), .dff_type(1'b1)) _TECHMAP_REPLACE_ (.I(D), .CK(C), .L(1'b0), .R(R), .O(Q)); +endmodule diff --git a/techlibs/nanoxplore/cells_sim.v b/techlibs/nanoxplore/cells_sim.v index d665e0f89..0a69a8a6a 100644 --- a/techlibs/nanoxplore/cells_sim.v +++ b/techlibs/nanoxplore/cells_sim.v @@ -8,3 +8,28 @@ wire [1:0] s3 = I2 ? s2[3:2] : s2[1:0]; assign O = I1 ? s3[1] : s3[0]; endmodule + +module NX_DFF(input I, CK, L, R, output reg O); + +parameter dff_ctxt = 1'bx; +parameter dff_edge = 1'b0; +parameter dff_init = 1'b0; +parameter dff_load = 1'b0; +parameter dff_sync = 1'b0; +parameter dff_type = 1'b0; + +initial begin + O = dff_ctxt; +end + +wire clock = CK ^ dff_edge; +wire load = (dff_type == 2) ? (dff_load ? L : 1'bx) : dff_type; +wire async_reset = !dff_sync && dff_init && R; +wire sync_reset = dff_sync && dff_init && R; + +always @(posedge clock, posedge async_reset) + if (async_reset) O <= load; + else if (sync_reset) O <= load; + else O <= I; + +endmodule diff --git a/tests/arch/nanoxplore/adffs.ys b/tests/arch/nanoxplore/adffs.ys new file mode 100644 index 000000000..6a4f63ad7 --- /dev/null +++ b/tests/arch/nanoxplore/adffs.ys @@ -0,0 +1,46 @@ +read_verilog ../common/adffs.v +design -save read + +hierarchy -top adff +proc +equiv_opt -async2sync -assert -map +/nanoxplore/cells_sim.v synth_nanoxplore # 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 # 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 # 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-none t:NX_DFF %% t:* %D + + +design -load read +hierarchy -top ndffnr +proc +equiv_opt -async2sync -assert -map +/nanoxplore/cells_sim.v synth_nanoxplore # 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 diff --git a/tests/arch/nanoxplore/dffs.ys b/tests/arch/nanoxplore/dffs.ys new file mode 100644 index 000000000..ba7dff41c --- /dev/null +++ b/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 # 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 # 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:NX_DFF +select -assert-count 1 t:NX_LUT + +select -assert-none t:NX_DFF t:NX_LUT %% t:* %D diff --git a/tests/arch/nanoxplore/fsm.ys b/tests/arch/nanoxplore/fsm.ys new file mode 100644 index 000000000..ee00be4e1 --- /dev/null +++ b/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 +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-count 13 t:NX_LUT +select -assert-none t:NX_DFF t:NX_LUT %% t:* %D diff --git a/tests/arch/nanoxplore/latches.ys b/tests/arch/nanoxplore/latches.ys new file mode 100644 index 000000000..32609dbce --- /dev/null +++ b/tests/arch/nanoxplore/latches.ys @@ -0,0 +1,35 @@ +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 +cd latchp # 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 latchn +proc +# Can't run any sort of equivalence check because latches are blown to LUTs +synth_nanoxplore +cd latchn # Constrain all select calls below inside the top module +select -assert-count 1 t:NX_LUT +select -assert-count 1 t:NX_DFF + +select -assert-none t:NX_LUT t:NX_DFF %% 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 +cd latchsr # Constrain all select calls below inside the top module +select -assert-count 2 t:NX_LUT +select -assert-count 1 t:NX_DFF + +select -assert-none t:NX_LUT t:NX_DFF %% t:* %D diff --git a/tests/arch/nanoxplore/shifter.ys b/tests/arch/nanoxplore/shifter.ys new file mode 100644 index 000000000..a3502df2a --- /dev/null +++ b/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 # 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