Add FFs and related tests

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

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

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

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

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

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

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