From f4d8ea4c403a482e367a3a130a43d9cc92c637a8 Mon Sep 17 00:00:00 2001
From: Miodrag Milanovic <mmicko@gmail.com>
Date: Mon, 20 May 2024 18:26:04 +0200
Subject: [PATCH] Start adding RFB simulation models

---
 techlibs/nanoxplore/cells_bb_u.v  | 103 --------------------
 techlibs/nanoxplore/cells_sim_u.v | 150 ++++++++++++++++++++++++++++++
 techlibs/nanoxplore/rf_rams_u.txt |   6 +-
 tests/arch/nanoxplore/fsm.ys      |   2 +-
 tests/arch/nanoxplore/lutram.ys   |  93 ++++++++++++++++--
 5 files changed, 240 insertions(+), 114 deletions(-)

diff --git a/techlibs/nanoxplore/cells_bb_u.v b/techlibs/nanoxplore/cells_bb_u.v
index 2cc16f410..95cb7158f 100644
--- a/techlibs/nanoxplore/cells_bb_u.v
+++ b/techlibs/nanoxplore/cells_bb_u.v
@@ -2338,109 +2338,6 @@ module NX_PMA_U(CLK_TX_I, CLK_RX_I, CLK_REF_I, DC_E_I, DC_LCSN_I1, DC_LCSN_I2, D
     parameter tx_usrclk_use_pcs_clk_2 = 1'b0;
 endmodule
 
-(* blackbox *)
-module NX_RFB_U(WCK, I1, I2, I3, I4, I5, I6, I7, I8, I9, I10, I11, I12, I13, I14, I15, I16, I17, I18, I19, I20
-, I21, I22, I23, I24, I25, I26, I27, I28, I29, I30, I31, I32, I33, I34, I35, I36, O1, O2, O3, O4, O5
-, O6, O7, O8, O9, O10, O11, O12, O13, O14, O15, O16, O17, O18, O19, O20, O21, O22, O23, O24, O25, O26
-, O27, O28, O29, O30, O31, O32, O33, O34, O35, O36, RA1, RA2, RA3, RA4, RA5, RA6, RA7, RA8, RA9, RA10, WA1
-, WA2, WA3, WA4, WA5, WA6, WE, WEA);
-    input I1;
-    input I10;
-    input I11;
-    input I12;
-    input I13;
-    input I14;
-    input I15;
-    input I16;
-    input I17;
-    input I18;
-    input I19;
-    input I2;
-    input I20;
-    input I21;
-    input I22;
-    input I23;
-    input I24;
-    input I25;
-    input I26;
-    input I27;
-    input I28;
-    input I29;
-    input I3;
-    input I30;
-    input I31;
-    input I32;
-    input I33;
-    input I34;
-    input I35;
-    input I36;
-    input I4;
-    input I5;
-    input I6;
-    input I7;
-    input I8;
-    input I9;
-    output O1;
-    output O10;
-    output O11;
-    output O12;
-    output O13;
-    output O14;
-    output O15;
-    output O16;
-    output O17;
-    output O18;
-    output O19;
-    output O2;
-    output O20;
-    output O21;
-    output O22;
-    output O23;
-    output O24;
-    output O25;
-    output O26;
-    output O27;
-    output O28;
-    output O29;
-    output O3;
-    output O30;
-    output O31;
-    output O32;
-    output O33;
-    output O34;
-    output O35;
-    output O36;
-    output O4;
-    output O5;
-    output O6;
-    output O7;
-    output O8;
-    output O9;
-    input RA1;
-    input RA10;
-    input RA2;
-    input RA3;
-    input RA4;
-    input RA5;
-    input RA6;
-    input RA7;
-    input RA8;
-    input RA9;
-    input WA1;
-    input WA2;
-    input WA3;
-    input WA4;
-    input WA5;
-    input WA6;
-    input WCK;
-    input WE;
-    input WEA;
-    parameter mem_ctxt = "";
-    parameter mode = 0;
-    parameter wck_edge = 1'b0;
-endmodule
-
-
 (* blackbox *)
 module NX_FIFO_U(RCK, WCK, WE, WEA, I1, I2, I3, I4, I5, I6, I7, I8, I9, I10, I11, I12, I13, I14, I15, I16, I17
 , I18, I19, I20, I21, I22, I23, I24, I25, I26, I27, I28, I29, I30, I31, I32, I33, I34, I35, I36, O1, O2
diff --git a/techlibs/nanoxplore/cells_sim_u.v b/techlibs/nanoxplore/cells_sim_u.v
index 794dd4e6a..e7e8fcc9a 100644
--- a/techlibs/nanoxplore/cells_sim_u.v
+++ b/techlibs/nanoxplore/cells_sim_u.v
@@ -1,3 +1,4 @@
+(* abc9_box, lib_whitebox *)
 module NX_GCK_U(SI1, SI2, CMD, SO);
     input CMD;
     input SI1;
@@ -28,3 +29,152 @@ module NX_GCK_U(SI1, SI2, CMD, SO);
     endgenerate
     assign SO = inv_out ? ~SO_int : SO_int;
 endmodule
+
+(* abc9_box, lib_whitebox *)
+module NX_RFB_U(WCK, I1, I2, I3, I4, I5, I6, I7, I8, I9, I10, I11, I12, I13, I14, I15, I16, I17, I18, I19, I20
+, I21, I22, I23, I24, I25, I26, I27, I28, I29, I30, I31, I32, I33, I34, I35, I36, O1, O2, O3, O4, O5
+, O6, O7, O8, O9, O10, O11, O12, O13, O14, O15, O16, O17, O18, O19, O20, O21, O22, O23, O24, O25, O26
+, O27, O28, O29, O30, O31, O32, O33, O34, O35, O36, RA1, RA2, RA3, RA4, RA5, RA6, RA7, RA8, RA9, RA10, WA1
+, WA2, WA3, WA4, WA5, WA6, WE, WEA);
+    input I1;
+    input I10;
+    input I11;
+    input I12;
+    input I13;
+    input I14;
+    input I15;
+    input I16;
+    input I17;
+    input I18;
+    input I19;
+    input I2;
+    input I20;
+    input I21;
+    input I22;
+    input I23;
+    input I24;
+    input I25;
+    input I26;
+    input I27;
+    input I28;
+    input I29;
+    input I3;
+    input I30;
+    input I31;
+    input I32;
+    input I33;
+    input I34;
+    input I35;
+    input I36;
+    input I4;
+    input I5;
+    input I6;
+    input I7;
+    input I8;
+    input I9;
+    output O1;
+    output O10;
+    output O11;
+    output O12;
+    output O13;
+    output O14;
+    output O15;
+    output O16;
+    output O17;
+    output O18;
+    output O19;
+    output O2;
+    output O20;
+    output O21;
+    output O22;
+    output O23;
+    output O24;
+    output O25;
+    output O26;
+    output O27;
+    output O28;
+    output O29;
+    output O3;
+    output O30;
+    output O31;
+    output O32;
+    output O33;
+    output O34;
+    output O35;
+    output O36;
+    output O4;
+    output O5;
+    output O6;
+    output O7;
+    output O8;
+    output O9;
+    input RA1;
+    input RA10;
+    input RA2;
+    input RA3;
+    input RA4;
+    input RA5;
+    input RA6;
+    input RA7;
+    input RA8;
+    input RA9;
+    input WA1;
+    input WA2;
+    input WA3;
+    input WA4;
+    input WA5;
+    input WA6;
+    input WCK;
+    input WE;
+    input WEA;
+    parameter mem_ctxt = "";
+    parameter mode = 0;
+    parameter wck_edge = 1'b0;
+
+    wire clock = WCK ^ wck_edge;
+
+    localparam MEM_SIZE  = mode == 2 ? 64 : 32;
+    localparam MEM_WIDTH = mode == 3 ? 36 : 18;
+    localparam ADDR_WIDTH = mode == 2 ? 6 : 5;
+
+    reg [MEM_WIDTH-1:0] mem [MEM_SIZE-1:0];
+
+    integer i;
+    initial begin
+        for (i = 0; i < MEM_SIZE; i = i + 1)
+            mem[i] = MEM_SIZE'b0;
+    end
+
+    wire [ADDR_WIDTH-1:0] WA = (mode==2) ? { WA6, WA5, WA4, WA3, WA2, WA1 } : { WA5, WA4, WA3, WA2, WA1 };
+    wire [36-1:0] O = { O36, O35, O34, O33, O32, O31, O30, O29, O28, 
+                        O27, O26, O25, O24, O23, O22, O21, O20, O19, 
+                        O18, O17, O16, O15, O14, O13, O12, O11, O10,
+                         O9,  O8,  O7,  O6,  O5,  O4,  O3,  O2,  O1 };
+    wire [36-1:0] I = { I36, I35, I34, I33, I32, I31, I30, I29, I28,
+                        I27, I26, I25, I24, I23, I22, I21, I20, I19,
+                        I18, I17, I16, I15, I14, I13, I12, I11, I10,
+                         I9,  I8,  I7,  I6,  I5,  I4,  I3,  I2,  I1 };
+    generate 
+        if (mode==0) begin
+            assign O[17:0] = mem[{ RA5, RA4, RA3, RA2, RA1 }];
+        end
+        else if (mode==1) begin
+            assign O[17:0] = mem[{ WA5, WA4, WA3, WA2, WA1 }];
+        end
+        else if (mode==2) begin
+            assign O[17:0] = mem[{ RA6, RA5, RA4, RA3, RA2, RA1 }];
+        end
+        else if (mode==3) begin
+            assign O[35:0] = mem[{ RA5, RA4, RA3, RA2, RA1 }];
+        end
+        else if (mode==4) begin
+            assign O[35:0] = { mem[{ RA10, RA9, RA8, RA7, RA6 }], mem[{ RA5, RA4, RA3, RA2, RA1 }] };
+        end
+        else 
+            $error("Unknown NX_RFB_U mode");
+    endgenerate
+
+    always @(posedge clock)
+        if (WE)
+            mem[WA] <= I[MEM_WIDTH-1:0];
+endmodule
\ No newline at end of file
diff --git a/techlibs/nanoxplore/rf_rams_u.txt b/techlibs/nanoxplore/rf_rams_u.txt
index 7b80e2f24..3dd3d3614 100644
--- a/techlibs/nanoxplore/rf_rams_u.txt
+++ b/techlibs/nanoxplore/rf_rams_u.txt
@@ -7,7 +7,7 @@
 
 ram distributed $__NX_RFB_U_DPREG_ {
 	option "MODE" 0 {
-        cost 35;
+        cost 30;
         widthscale 30;
 		abits 5;
 		widths 18 global;
@@ -53,8 +53,8 @@ ram distributed $__NX_RFB_U_SPREG_ {
 # NX_RFB_U in mode 4 (NX_XRFB_2R_1W)
 
 ram distributed $__NX_XRFB_2R_1W_ {
-	cost 30;
-    widthscale;
+	cost 40;
+    widthscale 30;
     abits 5;
     width 18;
 	init no_undef;
diff --git a/tests/arch/nanoxplore/fsm.ys b/tests/arch/nanoxplore/fsm.ys
index 8582d111c..f5d44453d 100644
--- a/tests/arch/nanoxplore/fsm.ys
+++ b/tests/arch/nanoxplore/fsm.ys
@@ -12,5 +12,5 @@ design -load postopt # load the post-opt design (otherwise equiv_opt loads the p
 cd fsm # Constrain all select calls below inside the top module
 
 select -assert-count 6 t:NX_DFF
-select -assert-count 14 t:NX_LUT
+select -assert-min 13 t:NX_LUT
 select -assert-none t:NX_DFF t:NX_LUT %% t:* %D
diff --git a/tests/arch/nanoxplore/lutram.ys b/tests/arch/nanoxplore/lutram.ys
index 72f4919ea..547e03b30 100644
--- a/tests/arch/nanoxplore/lutram.ys
+++ b/tests/arch/nanoxplore/lutram.ys
@@ -1,8 +1,61 @@
+# 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
+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
-synth_nanoxplore
+proc
+memory -nomap
+equiv_opt -run :prove -map +/nanoxplore/cells_sim.v -map +/nanoxplore/cells_sim_u.v synth_nanoxplore
+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
@@ -13,9 +66,17 @@ select -assert-none t:NX_RFB_U t:NX_DFF %% t:* %D
 design -reset
 read_verilog ../common/lutram.v
 hierarchy -top lutram_1w1r -chparam A_WIDTH 6 -chparam D_WIDTH 18
-synth_nanoxplore
+proc
+memory -nomap
+equiv_opt -run :prove -map +/nanoxplore/cells_sim.v -map +/nanoxplore/cells_sim_u.v synth_nanoxplore
+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
-stat
 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
@@ -25,7 +86,16 @@ select -assert-none t:NX_RFB_U t:NX_DFF %% t:* %D
 design -reset
 read_verilog ../common/lutram.v
 hierarchy -top lutram_1w1r -chparam A_WIDTH 5 -chparam D_WIDTH 36
-synth_nanoxplore
+proc
+memory -nomap
+equiv_opt -run :prove -map +/nanoxplore/cells_sim.v -map +/nanoxplore/cells_sim_u.v synth_nanoxplore
+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
@@ -39,8 +109,8 @@ read_verilog <<EOT
 module lutram_1w2r
 #(parameter D_WIDTH=8, A_WIDTH=5)
 (
-	input [D_WIDTH-1:0] data_a, data_b, data_c,
-	input [A_WIDTH:1] addr_a, addr_b, addr_c,
+	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
 );
@@ -59,7 +129,16 @@ endmodule
 EOT
 
 hierarchy -top lutram_1w2r -chparam A_WIDTH 5 -chparam D_WIDTH 18
-synth_nanoxplore
+proc
+memory -nomap
+equiv_opt -run :prove -map +/nanoxplore/cells_sim.v -map +/nanoxplore/cells_sim_u.v synth_nanoxplore
+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