Enable Kepler-formal LEC for multiple designs

flow/designs/asap7/ibex/config.mk

@@ -31,5 +31,3 @@ export TNS_END_PERCENT        = 100
 export SWAP_ARITH_OPERATORS = 1
 export OPENROAD_HIERARCHICAL = 1
 
-export LEC_CHECK = 0
-

flow/designs/asap7/jpeg/config.mk

@@ -17,6 +17,4 @@ export TNS_END_PERCENT        = 100
 export EQUIVALENCE_CHECK     ?=   1
 export REMOVE_CELLS_FOR_EQY   = TAPCELL*
 
-export LEC_CHECK = 0
-
 

flow/designs/asap7/mock-alu/config.mk

@@ -11,5 +11,3 @@ export ROUTING_LAYER_ADJUSTMENT = 0.45
 export SWAP_ARITH_OPERATORS = 1
 export OPENROAD_HIERARCHICAL = 1
 
-export LEC_CHECK = 0
-

flow/designs/asap7/swerv_wrapper/config.mk

@@ -61,4 +61,3 @@ export ROUTING_LAYER_ADJUSTMENT = 0.2
 export SWAP_ARITH_OPERATORS = 1
 export OPENROAD_HIERARCHICAL = 1
 
-export LEC_CHECK = 0

flow/designs/gf12/ariane/config.mk

@@ -37,5 +37,3 @@ export REMOVE_ABC_BUFFERS = 1
 
 export SWAP_ARITH_OPERATORS = 1
 export OPENROAD_HIERARCHICAL = 1
-
-export LEC_CHECK = 0

flow/designs/gf12/bp_dual/config.mk

@@ -66,5 +66,3 @@ export MACRO_WRAPPERS = $(PLATFORM_DIR)/bp/wrappers/wrappers.tcl
 export PDN_TCL = $(PLATFORM_DIR)/cfg/pdn_grid_strategy_13m_9T.top.tcl
 
 export MACRO_PLACE_HALO = 7 7
-
-export LEC_CHECK = 0

flow/designs/gf12/bp_single/config.mk

@@ -71,5 +71,3 @@ export SETUP_SLACK_MARGIN ?= 100
 
 export SWAP_ARITH_OPERATORS = 1
 export OPENROAD_HIERARCHICAL = 1
-
-export LEC_CHECK = 0

flow/designs/gf12/ca53/config.mk

@@ -69,5 +69,3 @@ endif
 #export SKIP_PIN_SWAP          = 1
 export SKIP_INCREMENTAL_REPAIR = 1
 export TNS_END_PERCENT = 5
-
-export LEC_CHECK = 0

flow/designs/gf12/tinyRocket/config.mk

@@ -41,5 +41,3 @@ endif
 
 export SWAP_ARITH_OPERATORS = 1
 export OPENROAD_HIERARCHICAL = 1
-
-export LEC_CHECK = 0

flow/designs/gf180/ibex/config.mk

@@ -18,5 +18,3 @@ export PLACE_DENSITY_LB_ADDON = 0.1
 export SWAP_ARITH_OPERATORS = 1
 export OPENROAD_HIERARCHICAL = 1
 
-export LEC_CHECK = 0
-

flow/designs/gf180/uart-blocks/config.mk

@@ -23,5 +23,3 @@ export TAPCELL_TCL ?= $(DESIGN_HOME)/$(PLATFORM)/$(DESIGN_NICKNAME)/tapcell.tcl
 export MACRO_ROWS_HALO_X = 14
 export MACRO_ROWS_HALO_Y = 14
 
-export LEC_CHECK = 0
-

flow/designs/ihp-sg13g2/i2c-gpio-expander/I2cDeviceCtrl/config.mk

@@ -19,5 +19,3 @@ export CORNERS = slow typ fast
 
 export PDN_TCL = $(DESIGN_HOME)/$(PLATFORM)/$(TOP_DESIGN_NICKNAME)/${DESIGN_NAME}/pdn.tcl
 
-export LEC_CHECK = 0
-

flow/designs/ihp-sg13g2/ibex/config.mk

@@ -23,5 +23,3 @@ export CTS_BUF_DISTANCE = 60
 export SWAP_ARITH_OPERATORS = 1
 export OPENROAD_HIERARCHICAL = 1
 
-export LEC_CHECK = 0
-

flow/designs/nangate45/bp_be_top/config.mk

@@ -30,5 +30,3 @@ export CTS_CLUSTER_DIAMETER = 50
 export SYNTH_MINIMUM_KEEP_SIZE = 3000
 
 export FASTROUTE_TCL = $(DESIGN_HOME)/$(PLATFORM)/$(DESIGN_NAME)/fastroute.tcl
-
-export LEC_CHECK = 0

flow/designs/nangate45/bp_multi_top/config.mk

@@ -36,5 +36,3 @@ export SKIP_GATE_CLONING      = 1
 export SWAP_ARITH_OPERATORS = 1
 export OPENROAD_HIERARCHICAL = 1
 
-export LEC_CHECK = 0
-

flow/designs/nangate45/mempool_group/config.mk

@@ -79,4 +79,6 @@ export MACRO_PLACE_HALO = 10 10
 
 export SYNTH_HDL_FRONTEND = slang
 
+# Disable KF LEC: assertion crash in SNLLogicCloud.cpp:349
+# "Iso have no drivers and more than one reader, not supported"
 export LEC_CHECK = 0

flow/designs/nangate45/swerv_wrapper/rules-base.json

@@ -28,11 +28,11 @@
         "compare": "<="
     },
     "cts__timing__setup__ws": {
-        "value": -0.197,
+        "value": -0.466,
         "compare": ">="
     },
     "cts__timing__setup__tns": {
-        "value": -84.6,
+        "value": -290.0,
         "compare": ">="
     },
     "cts__timing__hold__ws": {
@@ -52,7 +52,7 @@
         "compare": ">="
     },
     "globalroute__timing__setup__tns": {
-        "value": -86.3,
+        "value": -211.0,
         "compare": ">="
     },
     "globalroute__timing__hold__ws": {
@@ -64,7 +64,7 @@
         "compare": ">="
     },
     "detailedroute__route__wirelength": {
-        "value": 5546498,
+        "value": 4367567,
         "compare": "<="
     },
     "detailedroute__route__drc_errors": {
@@ -84,7 +84,7 @@
         "compare": ">="
     },
     "finish__timing__setup__tns": {
-        "value": -88.2,
+        "value": -198.0,
         "compare": ">="
     },
     "finish__timing__hold__ws": {

flow/designs/rapidus2hp/cva6/config.mk

@@ -149,5 +149,6 @@ export SYNTH_CANONICALIZE_TCL = $(DESIGN_HOME)/$(PLATFORM)/$(DESIGN_NAME)/canoni
 export SWAP_ARITH_OPERATORS = 1
 export OPENROAD_HIERARCHICAL = 1
 
-# Until the verilog writer fix is merged
+# Disable KF LEC: netlist loading failure
+# bus net "icache_areq_o" cannot be found in ALU module
 export LEC_CHECK = 0

flow/designs/rapidus2hp/cva6/rules-base.json

@@ -52,7 +52,7 @@
         "compare": ">="
     },
     "globalroute__timing__setup__tns": {
-        "value": -452.0,
+        "value": -463.0,
         "compare": ">="
     },
     "globalroute__timing__hold__ws": {
@@ -68,7 +68,7 @@
         "compare": ">="
     },
     "finish__timing__setup__tns": {
-        "value": -452.0,
+        "value": -463.0,
         "compare": ">="
     },
     "finish__timing__hold__ws": {

flow/designs/rapidus2hp/cva6/rules-verific.json

@@ -12,7 +12,7 @@
         "compare": "<="
     },
     "placeopt__design__instance__count__stdcell": {
-        "value": 201058,
+        "value": 200149,
         "compare": "<="
     },
     "detailedplace__design__violations": {
@@ -28,7 +28,7 @@
         "compare": "<="
     },
     "cts__timing__setup__ws": {
-        "value": -0.136,
+        "value": -0.167,
         "compare": ">="
     },
     "cts__timing__setup__tns": {
@@ -68,7 +68,7 @@
         "compare": ">="
     },
     "finish__timing__setup__tns": {
-        "value": -550.0,
+        "value": -738.0,
         "compare": ">="
     },
     "finish__timing__hold__ws": {

flow/designs/sky130hd/chameleon/config.mk

@@ -34,6 +34,7 @@ export CORE_ASPECT_RATIO      = 1.3
 export CORE_MARGIN            = 2
 
 export chameleon_DIR = $(DESIGN_HOME)/$(PLATFORM)/$(DESIGN_NICKNAME)
+export LEC_AUX_VERILOG_FILES = $(chameleon_DIR)/lec_blackbox_stubs.v
 
 export ADDITIONAL_GDS  = $(chameleon_DIR)/gds/apb_sys_0.gds.gz \
                                $(chameleon_DIR)/gds/DMC_32x16HC.gds.gz \
@@ -50,6 +51,3 @@ export ADDITIONAL_LEFS  = $(chameleon_DIR)/lef/apb_sys_0.lef \
 export FP_PDN_RAIL_WIDTH  = 0.48
 export FP_PDN_RAIL_OFFSET = 0
 export TNS_END_PERCENT    = 100
-
-export LEC_CHECK = 0
-

flow/designs/sky130hd/chameleon/lec_blackbox_stubs.v

@@ -0,0 +1,143 @@
+module DFFRAM_4K (
+    CLK,
+    WE,
+    EN,
+    Di,
+    Do,
+    A
+);
+  input CLK;
+  input [3:0] WE;
+  input EN;
+  input [31:0] Di;
+  output [31:0] Do;
+  input [9:0] A;
+endmodule
+
+module DMC_32x16HC (
+    clk,
+    rst_n,
+    A,
+    A_h,
+    Do,
+    hit,
+    line,
+    wr
+);
+  input clk;
+  input rst_n;
+  input [23:0] A;
+  input [23:0] A_h;
+  output [31:0] Do;
+  output hit;
+  input [127:0] line;
+  input wr;
+endmodule
+
+module ibex_wrapper (
+    HCLK,
+    HRESETn,
+    HADDR,
+    HSIZE,
+    HTRANS,
+    HWDATA,
+    HWRITE,
+    HRDATA,
+    HREADY,
+    NMI,
+    EXT_IRQ,
+    IRQ,
+    SYSTICKCLKDIV
+);
+  input HCLK;
+  input HRESETn;
+  output [31:0] HADDR;
+  output [2:0] HSIZE;
+  output [1:0] HTRANS;
+  output [31:0] HWDATA;
+  output HWRITE;
+  input [31:0] HRDATA;
+  input HREADY;
+  input NMI;
+  input EXT_IRQ;
+  input [14:0] IRQ;
+  input [23:0] SYSTICKCLKDIV;
+endmodule
+
+module apb_sys_0 (
+    HCLK,
+    HRESETn,
+    HADDR,
+    HTRANS,
+    HWRITE,
+    HWDATA,
+    HSEL,
+    HREADY,
+    HRDATA,
+    HREADYOUT,
+    RsRx_S0,
+    RsTx_S0,
+    RsRx_S1,
+    RsTx_S1,
+    MSI_S2,
+    MSO_S2,
+    SSn_S2,
+    SCLK_S2,
+    MSI_S3,
+    MSO_S3,
+    SSn_S3,
+    SCLK_S3,
+    scl_i_S4,
+    scl_o_S4,
+    scl_oen_o_S4,
+    sda_i_S4,
+    sda_o_S4,
+    sda_oen_o_S4,
+    scl_i_S5,
+    scl_o_S5,
+    scl_oen_o_S5,
+    sda_i_S5,
+    sda_o_S5,
+    sda_oen_o_S5,
+    pwm_S6,
+    pwm_S7,
+    IRQ
+);
+  input HCLK;
+  input HRESETn;
+  input [31:0] HADDR;
+  input [1:0] HTRANS;
+  input HWRITE;
+  input [31:0] HWDATA;
+  input HSEL;
+  input HREADY;
+  output [31:0] HRDATA;
+  output HREADYOUT;
+  input [0:0] RsRx_S0;
+  output [0:0] RsTx_S0;
+  input [0:0] RsRx_S1;
+  output [0:0] RsTx_S1;
+  input [0:0] MSI_S2;
+  output [0:0] MSO_S2;
+  output [0:0] SSn_S2;
+  output [0:0] SCLK_S2;
+  input [0:0] MSI_S3;
+  output [0:0] MSO_S3;
+  output [0:0] SSn_S3;
+  output [0:0] SCLK_S3;
+  input [0:0] scl_i_S4;
+  output [0:0] scl_o_S4;
+  output [0:0] scl_oen_o_S4;
+  input [0:0] sda_i_S4;
+  output [0:0] sda_o_S4;
+  output [0:0] sda_oen_o_S4;
+  input [0:0] scl_i_S5;
+  output [0:0] scl_o_S5;
+  output [0:0] scl_oen_o_S5;
+  input [0:0] sda_i_S5;
+  output [0:0] sda_o_S5;
+  output [0:0] sda_oen_o_S5;
+  output [0:0] pwm_S6;
+  output [0:0] pwm_S7;
+  output [15:0] IRQ;
+endmodule

flow/designs/sky130hd/ibex/config.mk

@@ -29,5 +29,3 @@ export CTS_CLUSTER_DIAMETER = 50
 export SWAP_ARITH_OPERATORS = 1
 export OPENROAD_HIERARCHICAL = 1
 
-
-export LEC_CHECK = 0

flow/designs/sky130hd/microwatt/config.mk

@@ -51,5 +51,3 @@ endif
 
 export SWAP_ARITH_OPERATORS = 1
 export OPENROAD_HIERARCHICAL = 1
-
-export LEC_CHECK = 0

flow/designs/src/cva6/core/cache_subsystem/cva6_hpdcache_if_adapter.sv

@@ -114,6 +114,9 @@ module cva6_hpdcache_if_adapter
       assign cva6_req_o.data_rdata = hpdcache_rsp_i.rdata;
       assign cva6_req_o.data_rid = hpdcache_rsp_i.tid;
       assign cva6_req_o.data_gnt = hpdcache_req_ready_i;
+      assign cva6_req_o.data_ruser = '0;
+      assign cva6_amo_resp_o = '0;
+      assign cva6_dcache_flush_ack_o = 1'b0;
 
       //  Assertions
       //  {{{
@@ -317,6 +320,7 @@ module cva6_hpdcache_if_adapter
       assign cva6_req_o.data_rdata = hpdcache_rsp_i.rdata;
       assign cva6_req_o.data_rid = hpdcache_rsp_i.tid;
       assign cva6_req_o.data_gnt = hpdcache_req_ready_i;
+      assign cva6_req_o.data_ruser = '0;
 
       assign cva6_amo_resp_o.ack = hpdcache_rsp_valid_i && (hpdcache_rsp_i.tid == '1);
       assign cva6_amo_resp_o.result = amo_is_word ? {{32{amo_resp_word[31]}}, amo_resp_word}

flow/designs/src/cva6/core/cache_subsystem/cva6_hpdcache_wrapper.sv

@@ -248,7 +248,8 @@ module cva6_hpdcache_wrapper
         dcache_req[NumPorts] = '0,
         dcache_req_abort[NumPorts] = 1'b0,
         dcache_req_tag[NumPorts] = '0,
-        dcache_req_pma[NumPorts] = '0;
+        dcache_req_pma[NumPorts] = '0,
+        dcache_cmo_resp_o = '0;
 `endif
   endgenerate
 

flow/designs/src/cva6/core/cache_subsystem/hpdcache/rtl/src/hwpf_stride/hwpf_stride.sv

@@ -147,7 +147,8 @@ import hpdcache_pkg::*;
            hpdcache_req_o.phys_indexed    = 1'b1,
            hpdcache_req_o.addr_tag        = hpdcache_req_tag,
            hpdcache_req_o.pma.uncacheable = 1'b0,
-           hpdcache_req_o.pma.io          = 1'b0;
+           hpdcache_req_o.pma.io          = 1'b0,
+           hpdcache_req_o.pma.wr_policy_hint = HPDCACHE_WR_POLICY_AUTO;
     //  }}}
 
     //  Set state of internal registers