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/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: assertion crash in SNLLogicCloud.cpp:349
+# "Iso have no drivers and more than one reader, not supported"
 export LEC_CHECK = 0

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

@@ -52,7 +52,7 @@
         "compare": ">="
     },
     "globalroute__timing__setup__tns": {
-        "value": -697.0,
+        "value": -750.0,
         "compare": ">="
     },
     "globalroute__timing__hold__ws": {
@@ -68,7 +68,7 @@
         "compare": ">="
     },
     "finish__timing__setup__tns": {
-        "value": -697.0,
+        "value": -750.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

flow/designs/src/cva6/core/csr_regfile.sv

@@ -2531,7 +2531,7 @@ module csr_regfile
 
   // determine if mprv needs to be considered if in debug mode
   assign mprv = (CVA6Cfg.DebugEn && debug_mode_q && !dcsr_q.mprven) ? 1'b0 : mstatus_q.mprv;
-  assign debug_mode_o = debug_mode_q;
+  assign debug_mode_o = CVA6Cfg.DebugEn ? debug_mode_q : 1'b0;
   assign single_step_o = CVA6Cfg.DebugEn ? dcsr_q.step : 1'b0;
   assign mcountinhibit_o = {{29 - MHPMCounterNum{1'b0}}, mcountinhibit_q};
 

flow/designs/src/cva6/core/cva6_mmu/cva6_mmu.sv

@@ -528,6 +528,8 @@ module cva6_mmu
               ((ld_st_priv_lvl_i == riscv::PRIV_LVL_S && (ld_st_v_i ? !vs_sum_i : !sum_i ) && dtlb_pte_q.u) || // SUM is not set and we are trying to access a user page in supervisor mode
     (ld_st_priv_lvl_i == riscv::PRIV_LVL_U && !dtlb_pte_q.u));
 
+    csr_hs_ld_st_inst_o = 1'b0;
+
     if (CVA6Cfg.RVH) begin
       lsu_tinst_n = lsu_tinst_i;
       hs_ld_st_inst_n = hs_ld_st_inst_i;

flow/designs/src/cva6/core/cvxif_fu.sv

@@ -64,6 +64,7 @@ module cvxif_fu
 
   // Handling of illegal instruction exception
   always_comb begin
+    x_exception_o = '0;
     x_exception_o.valid = x_illegal_i;
     x_exception_o.cause = x_illegal_i ? riscv::ILLEGAL_INSTR : '0;
     if (CVA6Cfg.TvalEn)

flow/designs/src/cva6/core/id_stage.sv

@@ -229,6 +229,7 @@ module id_stage #(
       assign is_compressed_zcmt    = is_compressed_rvc;
       assign stall_macro_deco_zcmt = '0;
       assign jump_address          = '0;
+      assign dcache_req_ports_o    = '0;
     end
 
     if (CVA6Cfg.RVZCMT) begin

flow/designs/src/cva6/core/load_store_unit.sv

@@ -349,13 +349,16 @@ module load_store_unit
     assign dcache_req_ports_o[0].address_index = '0;
     assign dcache_req_ports_o[0].address_tag   = '0;
     assign dcache_req_ports_o[0].data_wdata    = '0;
+    assign dcache_req_ports_o[0].data_wuser    = '0;
     assign dcache_req_ports_o[0].data_req      = 1'b0;
     assign dcache_req_ports_o[0].data_be       = '1;
     assign dcache_req_ports_o[0].data_size     = 2'b11;
+    assign dcache_req_ports_o[0].data_id       = '0;
     assign dcache_req_ports_o[0].data_we       = 1'b0;
     assign dcache_req_ports_o[0].kill_req      = '0;
     assign dcache_req_ports_o[0].tag_valid     = 1'b0;
 
+    assign csr_hs_ld_st_inst_o                 = 1'b0;
     assign itlb_miss_o                         = 1'b0;
     assign dtlb_miss_o                         = 1'b0;
     assign dtlb_ppn                            = lsu_paddr[CVA6Cfg.PLEN-1:12];

flow/designs/src/cva6/core/load_unit.sv

@@ -196,6 +196,7 @@ module load_unit
   // this is a read-only interface so set the write enable to 0
   assign req_port_o.data_we = 1'b0;
   assign req_port_o.data_wdata = '0;
+  assign req_port_o.data_wuser = '0;
   // compose the load buffer write data, control is handled in the FSM
   assign ldbuf_wdata = {
     lsu_ctrl_i.trans_id, lsu_ctrl_i.vaddr[CVA6Cfg.XLEN_ALIGN_BYTES-1:0], lsu_ctrl_i.operation