Kepler Formal's failure to parse hierarchical module names

[nagas-design]

Hi,

We’ve run into an equivalence check failure with Kepler Formal during CTS. I’ve attached the full log file for inspection, for context, flat synthesis runs cleanly with no equivalence check issues, but hierarchical synthesis triggers the parser error shown below.

[2026-03-31 12:03:52.298] [critical] [KeplerFormal.cpp:382] Netlist loading failed: In ./results/sky130hd/cva6/base_cva6/4_before_rsz_lec.v at line 105516, column 5: bus net "issue_entry_o" cannot be found in ariane_regfile$cva6.issue_stage_i.i_issue_read_operands.gen_asic_regfile.i_ariane_regfile
child process exited abnormally

We suspect this may be related to KeplerFormal’s handling of hierarchical instance names and would appreciate any intuition you might have on whether this is a known parser limitation or if there are debugging steps we should try.

For Reference, please find the below log file
/home/ubuntu/Tapeouts/OpenROAD-flow-scripts/flow/logs/sky130hd/cva6/base_cva6/4_1_cts.log

OpenROAD 26Q1-1744-g138e57370c
Features included (+) or not (-): +GPU +GUI +Python
This program is licensed under the BSD-3 license. See the LICENSE file for details.
Components of this program may be licensed under more restrictive licenses which must be honored.
[INFO ORD-0030] Using 16 thread(s).
read_liberty /home/ubuntu/Tapeouts/OpenROAD-flow-scripts/flow/platforms/sky130hd/lib/sky130_fd_sc_hd__tt_025C_1v80.lib
read_liberty /home/ubuntu/Tapeouts/OpenROAD-flow-scripts/flow/platforms/sky130ram/sky130_sram_200bytes_1rw_25x64_25/sky130_sram_200bytes_1rw_25x64_25_TT_1p8V_25C.lib
read_liberty /home/ubuntu/Tapeouts/OpenROAD-flow-scripts/flow/platforms/sky130ram/sky130_sram_1kbytes_1rw_128x64_128/sky130_sram_1kbytes_1rw_128x64_128_TT_1p8V_25C.lib
read_liberty /home/ubuntu/Tapeouts/OpenROAD-flow-scripts/flow/platforms/sky130ram/sky130_sram_224bytes_1rw_28x64_28/sky130_sram_224bytes_1rw_28x64_28_TT_1p8V_25C.lib
read_liberty /home/ubuntu/Tapeouts/OpenROAD-flow-scripts/flow/platforms/sky130ram/sky130_sram_1kbytes_1rw_64x128_8/sky130_sram_1kbytes_1rw_64x128_8_TT_1p8V_25C.lib
read_db -hier ./results/sky130hd/cva6/base_cva6/3_place.odb
[WARNING ORD-0012] Hierarchical flow (-hier) is currently in development and may cause multiple issues. Do not use in production environments.
source /home/ubuntu/Tapeouts/OpenROAD-flow-scripts/flow/platforms/sky130hd/setRC.tcl
clock_tree_synthesis -sink_clustering_enable -repair_clock_nets
[INFO CTS-0050] Root buffer is sky130_fd_sc_hd__clkbuf_16.
[INFO CTS-0051] Sink buffer is sky130_fd_sc_hd__clkbuf_16.
[INFO CTS-0052] The following clock buffers will be used for CTS:
sky130_fd_sc_hd__clkbuf_16
[INFO CTS-0049] Characterization buffer is sky130_fd_sc_hd__clkbuf_16.
[INFO CTS-0007] Net "clk_i" found for clock "main_clk".
[INFO CTS-0011] Clock net "clk_i" for macros has 8 sinks.
[INFO CTS-0011] Clock net "clk_i_regs" for registers has 9132 sinks.
[INFO CTS-0008] TritonCTS found 2 clock nets.
[INFO CTS-0097] Characterization used 1 buffer(s) types.
[INFO CTS-0201] 8 blockages from hard placement blockages and placed macros will be used.
[INFO CTS-0027] Generating H-Tree topology for net clk_i.
[INFO CTS-0028] Total number of sinks: 8.
[INFO CTS-0029] Macro sinks will be clustered in groups of up to 4 and with maximum cluster diameter of 1864.9 um.
[INFO CTS-0030] Number of static layers: 0.
[INFO CTS-0020] Wire segment unit: 13600 dbu (13 um).
[INFO CTS-0023] Original sink region: [(62000, 198445), (2939600, 524290)].
[INFO CTS-0024] Normalized sink region: [(4.55882, 14.5915), (216.147, 38.5507)].
[INFO CTS-0025] Width: 211.5882.
[INFO CTS-0026] Height: 23.9592.
Level 1
Direction: Horizontal
Sinks per sub-region: 4
Sub-region size: 105.7941 X 23.9592
[INFO CTS-0034] Segment length (rounded): 52.
[INFO CTS-0032] Stop criterion found. Max number of sinks is 15.
[INFO CTS-0035] Number of sinks covered: 8.
[INFO CTS-0201] 8 blockages from hard placement blockages and placed macros will be used.
[INFO CTS-0027] Generating H-Tree topology for net clk_i_regs.
[INFO CTS-0028] Total number of sinks: 9132.
[INFO CTS-0090] Sinks will be clustered based on buffer max cap.
[INFO CTS-0030] Number of static layers: 0.
[INFO CTS-0020] Wire segment unit: 13600 dbu (13 um).
[INFO CTS-0206] Best clustering solution was found from clustering size of 20 and clustering diameter of 50.
[INFO CTS-0019] Total number of sinks after clustering: 1030.
[INFO CTS-0024] Normalized sink region: [(3.46098, 6.25), (194.053, 160.779)].
[INFO CTS-0025] Width: 190.5919.
[INFO CTS-0026] Height: 154.5291.
Level 1
Direction: Horizontal
Sinks per sub-region: 515
Sub-region size: 95.2959 X 154.5291
[INFO CTS-0034] Segment length (rounded): 48.
Level 2
Direction: Vertical
Sinks per sub-region: 258
Sub-region size: 95.2959 X 77.2646
[INFO CTS-0034] Segment length (rounded): 38.
Level 3
Direction: Horizontal
Sinks per sub-region: 129
Sub-region size: 47.6480 X 77.2646
[INFO CTS-0034] Segment length (rounded): 24.
Level 4
Direction: Vertical
Sinks per sub-region: 65
Sub-region size: 47.6480 X 38.6323
[INFO CTS-0034] Segment length (rounded): 20.
Level 5
Direction: Horizontal
Sinks per sub-region: 33
Sub-region size: 23.8240 X 38.6323
[INFO CTS-0034] Segment length (rounded): 12.
Level 6
Direction: Vertical
Sinks per sub-region: 17
Sub-region size: 23.8240 X 19.3161
[INFO CTS-0034] Segment length (rounded): 10.
Level 7
Direction: Horizontal
Sinks per sub-region: 9
Sub-region size: 11.9120 X 19.3161
[INFO CTS-0034] Segment length (rounded): 6.
[INFO CTS-0032] Stop criterion found. Max number of sinks is 15.
[INFO CTS-0035] Number of sinks covered: 1030.
[INFO CTS-0018] Created 3 clock buffers.
[INFO CTS-0012] Minimum number of buffers in the clock path: 2.
[INFO CTS-0013] Maximum number of buffers in the clock path: 2.
[INFO CTS-0015] Created 3 clock nets.
[INFO CTS-0016] Fanout distribution for the current clock = 4:2..
[INFO CTS-0017] Max level of the clock tree: 1.
[INFO CTS-0018] Created 1250 clock buffers.
[INFO CTS-0012] Minimum number of buffers in the clock path: 7.
[INFO CTS-0013] Maximum number of buffers in the clock path: 8.
[INFO CTS-0015] Created 1250 clock nets.
[INFO CTS-0016] Fanout distribution for the current clock = 2:7, 3:9, 4:42, 5:52, 6:91, 7:137, 8:165, 9:179, 10:188, 11:138, 12:85, 13:45, 14:11, 15:2, 16:2, 17:1, 18:1..
[INFO CTS-0017] Max level of the clock tree: 7.
[INFO CTS-0098] Clock net "clk_i"
[INFO CTS-0099] Sinks 8
[INFO CTS-0100] Leaf buffers 0
[INFO CTS-0101] Average sink wire length 3191.22 um
[INFO CTS-0102] Path depth 2 - 2
[INFO CTS-0207] Dummy loads inserted 0
[INFO CTS-0098] Clock net "clk_i_regs"
[INFO CTS-0099] Sinks 10048
[INFO CTS-0100] Leaf buffers 1027
[INFO CTS-0101] Average sink wire length 1954.62 um
[INFO CTS-0102] Path depth 7 - 8
[INFO CTS-0207] Dummy loads inserted 916
[INFO RSZ-0047] Found 1 long wires.
[INFO RSZ-0048] Inserted 1 buffers in 1 nets.
[INFO CTS-0033] Balancing latency for clock main_clk
[INFO CTS-0036] inserted 9 delay buffers
[INFO CTS-0037] Total number of delay buffers: 9
Took 9 seconds: clock_tree_synthesis -sink_clustering_enable -repair_clock_nets
estimate_parasitics -placement
Placement Analysis
total displacement 17479.0 u
average displacement 0.1 u
max displacement 21.0 u
original HPWL 8409431.4 u
legalized HPWL 8495244.1 u
delta HPWL 1 %

estimate_parasitics -placement
repair_timing -setup_margin 0 -hold_margin 0 -repair_tns 100 -skip_last_gasp -match_cell_footprint -verbose
[INFO RSZ-0100] Repair move sequence: UnbufferMove SizeUpMove SwapPinsMove BufferMove CloneMove SplitLoadMove
[INFO RSZ-0098] No setup violations found
[INFO RSZ-0033] No hold violations found.
Error: cts.tcl, 85 [2026-03-27 18:07:04.547] [info] [KeplerFormal.cpp:258] KEPLER FORMAL: Run.
[2026-03-27 18:07:04.547] [info] [KeplerFormal.cpp:259] Input format: VERILOG
[2026-03-27 18:07:04.547] [info] [KeplerFormal.cpp:260] Netlist 1: ./results/sky130hd/cva6/base_cva6/4_before_rsz_lec.v
[2026-03-27 18:07:04.547] [info] [KeplerFormal.cpp:261] Netlist 2: ./results/sky130hd/cva6/base_cva6/4_after_rsz_lec.v
[2026-03-27 18:07:04.547] [info] [KeplerFormal.cpp:263] Solver: KISSAT
[2026-03-27 18:07:04.547] [info] [KeplerFormal.cpp:266] Liberty: /home/ubuntu/Tapeouts/OpenROAD-flow-scripts/flow/platforms/sky130hd/lib/sky130_fd_sc_hd__tt_025C_1v80.lib
[2026-03-27 18:07:04.547] [info] [KeplerFormal.cpp:266] Liberty: /home/ubuntu/Tapeouts/OpenROAD-flow-scripts/flow/platforms/sky130ram/sky130_sram_200bytes_1rw_25x64_25/sky130_sram_200bytes_1rw_25x64_25_TT_1p8V_25C.lib
[2026-03-27 18:07:04.547] [info] [KeplerFormal.cpp:266] Liberty: /home/ubuntu/Tapeouts/OpenROAD-flow-scripts/flow/platforms/sky130ram/sky130_sram_1kbytes_1rw_128x64_128/sky130_sram_1kbytes_1rw_128x64_128_TT_1p8V_25C.lib
[2026-03-27 18:07:04.547] [info] [KeplerFormal.cpp:266] Liberty: /home/ubuntu/Tapeouts/OpenROAD-flow-scripts/flow/platforms/sky130ram/sky130_sram_224bytes_1rw_28x64_28/sky130_sram_224bytes_1rw_28x64_28_TT_1p8V_25C.lib
[2026-03-27 18:07:04.547] [info] [KeplerFormal.cpp:266] Liberty: /home/ubuntu/Tapeouts/OpenROAD-flow-scripts/flow/platforms/sky130ram/sky130_sram_1kbytes_1rw_64x128_8/sky130_sram_1kbytes_1rw_64x128_8_TT_1p8V_25C.lib
[2026-03-27 18:07:04.547] [info] [KeplerFormal.cpp:285] Loading liberty file: /home/ubuntu/Tapeouts/OpenROAD-flow-scripts/flow/platforms/sky130hd/lib/sky130_fd_sc_hd__tt_025C_1v80.lib
[2026-03-27 18:07:04.605] [info] [KeplerFormal.cpp:285] Loading liberty file: /home/ubuntu/Tapeouts/OpenROAD-flow-scripts/flow/platforms/sky130ram/sky130_sram_200bytes_1rw_25x64_25/sky130_sram_200bytes_1rw_25x64_25_TT_1p8V_25C.lib
[2026-03-27 18:07:04.611] [info] [KeplerFormal.cpp:285] Loading liberty file: /home/ubuntu/Tapeouts/OpenROAD-flow-scripts/flow/platforms/sky130ram/sky130_sram_1kbytes_1rw_128x64_128/sky130_sram_1kbytes_1rw_128x64_128_TT_1p8V_25C.lib
[2026-03-27 18:07:04.611] [info] [KeplerFormal.cpp:285] Loading liberty file: /home/ubuntu/Tapeouts/OpenROAD-flow-scripts/flow/platforms/sky130ram/sky130_sram_224bytes_1rw_28x64_28/sky130_sram_224bytes_1rw_28x64_28_TT_1p8V_25C.lib
[2026-03-27 18:07:04.611] [info] [KeplerFormal.cpp:285] Loading liberty file: /home/ubuntu/Tapeouts/OpenROAD-flow-scripts/flow/platforms/sky130ram/sky130_sram_1kbytes_1rw_64x128_8/sky130_sram_1kbytes_1rw_64x128_8_TT_1p8V_25C.lib
[2026-03-27 18:07:04.611] [info] [KeplerFormal.cpp:292] Parsing verilog file: ./results/sky130hd/cva6/base_cva6/4_before_rsz_lec.v
[2026-03-31 12:03:52.298] [critical] [KeplerFormal.cpp:382] Netlist loading failed: In ./results/sky130hd/cva6/base_cva6/4_before_rsz_lec.v at line 105516, column 5: bus net "issue_entry_o" cannot be found in ariane_regfile$cva6.issue_stage_i.i_issue_read_operands.gen_asic_regfile.i_ariane_regfile
child process exited abnormally
Command exited with non-zero status 1
Elapsed time: 0:43.92[h:]min:sec. CPU time: user 58.01 sys 4.61 (142%). Peak memory: 1384436KB.
make[1]: *** [Makefile:510: do-4_1_cts] Error 1
make: *** [Makefile:510: results/sky130hd/cva6/base_cva6/4_1_cts.odb] Error 2

[maliberty]

What commit id are you using? Are you running the version of this design from ORFS without modifications (it passes in the CI)?

[Blueonics]

The latest commit we are working with is:
5101376937a58731b5038683b2cb7b70404da7fc
Yes that would be good idea to run CI on this, we replaced the fake RAMs with sky130hd SRAM macros generated by OpenRAM.

[nanocoh]

Hello @nagas-design, Can you please share the verilog file ./results/sky130hd/cva6/base_cva6/4_before_rsz_lec.v so we can debug the failure?

For hierarchy vs flat, kepler formal supports both. So it seems like an issue in the verilog input that we need to look at.

[nagas-design]

Hai @nanocoh.
Thank you very much for your prompt response and for highlighting the need for the Verilog file. Please find attached the requested file for your review: 4_before_rsz_lec.zip
I appreciate your support in helping us proceed with the debugging process.

[nanocoh]

Thanks! This will help us in debugging the issue. We will start by looking at the verilog parsing.

• @xtofalex

[nanocoh]

Adding @xtofalex as it looks like the issue is related to the verilog parser.

[xtofalex]

For reference, the ORFS version used is:
The-OpenROAD-Project/OpenROAD-flow-scripts@5101376

[xtofalex]

From what i see there is an issue in the verilog file, when parsing the example you shared, I don't hit exactly same error at same line but equivalent:

Caught SNL error: In 4_before_rsz_lec.v at line 222923, column 5: bus net "rdata_o" cannot be found in cva6_hpdcache_subsystem_axi_arbiter$cva6.gen_cache_hpd.i_cache_subsystem.i_axi_arbiter

The faulty line is:

    .\rdata_o[21]_0 (rdata_o[21]),

while the net that is connected is indeed not a bus, but an input:

 input \rdata_o[21] ;

So there is a missing escaping at the instance connection, it should be:

  .\rdata_o[21]_0 (\rdata_o[21] ),

I know that there has been some fixes related to this in OpenSTA VerilogWriter.cc, see:
79cd373

and I have the impression that the ORFS version used for reporting this bug points to an OR version containing the fix.

@nagas-design are you using ORFS embedded OR version or pointing to your own (maybe older) one ?

[maliberty]

@dsengupta0628 are you aware of an issue with write_verilog?

[dsengupta0628]

Escape sequence related bug should have been fixed already.
ORFS version here is 5101376937a58731b5038683b2cb7b70404da7fc which uses STA version
16ac05c87a2a7f4a85dca8ae571beab7879bb09b that was committed on March 3 that should have the write_verilog escape seq fix.

There was one more fix I put in for read_verilog though issue too that was committed on March 10 related to hierarchical verilog and unconnected pins) fbe9da3fb73f0918b3a1f25bacb4f84c0a7a5aa3 (issue was parallaxsw/OpenSTA#398) So if read_verilog had any bug, it would flow into write_verilog too. Is it possible to use a newer version of OpenROAD (that contains this STA commit)? I can take a look further if a testcase is provided. Thanks