When verifying a design that includes memory IP from an IP vendor, we're hitting:
[2026-08-06 21:40:15.799] [kepler_formal_main_logger] [critical] [KeplerFormal.cpp:2653] Netlist loading failed: Conflicting sequential clocks `clk_a` and `clk_b` for term problem_child
I've trimmed down the design into something that can be shared. Is it possible to provide additional configuration information to KF that would allow the design to pass? I'm currently working around the issue by using a Verilog blackbox instead of the Liberty file.
Here are the files for the test case:
mem.lib.txt
single_mem.yml.txt
top.v.txt
When verifying a design that includes memory IP from an IP vendor, we're hitting:
I've trimmed down the design into something that can be shared. Is it possible to provide additional configuration information to KF that would allow the design to pass? I'm currently working around the issue by using a Verilog blackbox instead of the Liberty file.
Here are the files for the test case:
mem.lib.txt
single_mem.yml.txt
top.v.txt