Merge pull request #3985 from The-OpenROAD-Project-staging/secure-enable-kf-lec-check

maliberty · web-flow · commit 53ad58719adb · 2026-03-30T05:25:54.000Z
Enable Kepler-formal LEC for multiple designs
diff --git a/flow/designs/asap7/ibex/config.mk b/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
-
diff --git a/flow/designs/asap7/jpeg/config.mk b/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
-
 
diff --git a/flow/designs/asap7/mock-alu/config.mk b/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
-
diff --git a/flow/designs/asap7/swerv_wrapper/config.mk b/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
diff --git a/flow/designs/gf12/ariane/config.mk b/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
diff --git a/flow/designs/gf12/bp_dual/config.mk b/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
diff --git a/flow/designs/gf12/bp_single/config.mk b/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
diff --git a/flow/designs/gf12/ca53/config.mk b/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
diff --git a/flow/designs/gf12/tinyRocket/config.mk b/flow/designs/gf12/tinyRocket/config.mk
@@ -41,5 +41,3 @@ endif
 
 export SWAP_ARITH_OPERATORS = 1
 export OPENROAD_HIERARCHICAL = 1
-
-export LEC_CHECK = 0
diff --git a/flow/designs/gf180/ibex/config.mk b/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
-
diff --git a/flow/designs/gf180/uart-blocks/config.mk b/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
-
diff --git a/flow/designs/ihp-sg13g2/i2c-gpio-expander/I2cDeviceCtrl/config.mk b/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
-
diff --git a/flow/designs/ihp-sg13g2/ibex/config.mk b/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
-
diff --git a/flow/designs/nangate45/bp_be_top/config.mk b/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
diff --git a/flow/designs/nangate45/bp_multi_top/config.mk b/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
-
diff --git a/flow/designs/nangate45/bp_multi_top/rules-base.json b/flow/designs/nangate45/bp_multi_top/rules-base.json
@@ -92,7 +92,7 @@
         "compare": ">="
     },
     "finish__timing__hold__tns": {
-        "value": -0.96,
+        "value": -1.32,
         "compare": ">="
     },
     "finish__design__instance__area": {
diff --git a/flow/designs/nangate45/mempool_group/config.mk b/flow/designs/nangate45/mempool_group/config.mk
@@ -78,5 +78,3 @@ export CORE_AREA   = 10 12 1090 1090
 export MACRO_PLACE_HALO = 10 10
 
 export SYNTH_HDL_FRONTEND = slang
-
-export LEC_CHECK = 0
diff --git a/flow/designs/rapidus2hp/cva6/config.mk b/flow/designs/rapidus2hp/cva6/config.mk
@@ -148,6 +148,3 @@ 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
-export LEC_CHECK = 0
diff --git a/flow/designs/sky130hd/chameleon/config.mk b/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
-
diff --git a/flow/designs/sky130hd/chameleon/lec_blackbox_stubs.v b/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
diff --git a/flow/designs/sky130hd/ibex/config.mk b/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
diff --git a/flow/designs/sky130hd/microwatt/config.mk b/flow/designs/sky130hd/microwatt/config.mk
@@ -51,5 +51,3 @@ endif
 
 export SWAP_ARITH_OPERATORS = 1
 export OPENROAD_HIERARCHICAL = 1
-
-export LEC_CHECK = 0
diff --git a/flow/designs/src/cva6/core/cache_subsystem/cva6_hpdcache_if_adapter.sv b/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}
diff --git a/flow/designs/src/cva6/core/cache_subsystem/cva6_hpdcache_wrapper.sv b/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
 
diff --git a/flow/designs/src/cva6/core/cache_subsystem/hpdcache/rtl/src/hwpf_stride/hwpf_stride.sv b/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
diff --git a/flow/designs/src/cva6/core/csr_regfile.sv b/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};
 
diff --git a/flow/designs/src/cva6/core/cva6_mmu/cva6_mmu.sv b/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;
diff --git a/flow/designs/src/cva6/core/cvxif_fu.sv b/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)
diff --git a/flow/designs/src/cva6/core/id_stage.sv b/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
diff --git a/flow/designs/src/cva6/core/load_store_unit.sv b/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];
diff --git a/flow/designs/src/cva6/core/load_unit.sv b/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
diff --git a/flow/scripts/lec_check.tcl b/flow/scripts/lec_check.tcl
diff --git a/tools/OpenROAD b/tools/OpenROAD
diff --git a/tools/kepler-formal b/tools/kepler-formal

Original file line number	Diff line number	Diff line change
`@@ -61,4 +61,3 @@ export ROUTING_LAYER_ADJUSTMENT = 0.2`
`61`	`61`	`export SWAP_ARITH_OPERATORS = 1`
`62`	`62`	`export OPENROAD_HIERARCHICAL = 1`
`63`	`63`
`64`		`-export LEC_CHECK = 0`