Repository navigation
kepler-formal 9dd032c breaks liberty cell #195
Description
Activity
@nanocoh, the first relevant change appears to be 13778f4 (“Use Liberty sequential models in SEC”), which upgraded Naja and started parsing Liberty sequential expressions. The current Naja implementation registers state identifiers from ff(...) groups (Q1/QN` here), but not from sibling latch(...) groups (Q2/QN2). As a result, Q2 in the FF’s clear expression is incorrectly looked up as an interface pin and rejected.
The older version accepted the cell because it did not fully model these sequential expressions.
Full support would require representing both FF and latch states in the Naja sequential model.
Hello @jeffng-or , did yoy face it with LEC or SEC? It is now fixed for LEC in latest main, for SEC some additional work is pending. Will update this issue when SEC work is finalized as well.
I originally encountered the issue with LEC and confirm that 453cc25 parses the liberty file.
When I switch to SEC, I see:
[2026-08-17 16:45:13.350] [kepler_formal_main_logger] [info] [KeplerFormal.cpp:2751] Found top design: top [2026-08-17 16:45:13.350] [kepler_formal_main_logger] [critical] [KeplerFormal.cpp:2191] SEC cannot run on this design pair: No aligned observed outputs remain after skipping cones with no-driver, multi-driver, or logical-loop connectivity.FYI. I'm going to hold off on merging the KF update into ORFS until #197 is resolved. I ran into an issue where the IP vendor put conditionals in the identifier names, which breaks the parser.
Yes. With current SEC implementation this is the expacted behavior. There will need to be some futher development to handle this type of cell. will update the issue when done.
Upgrading kepler-formal to 9dd032c causes a liberty cell in a proprietary library to break. I've created a sample that repro's the same issue.
Here's the error:
The prior version 08fa023 did not error out.
here are the data files:
power_cell.lib.txt
power_cell.yml.txt
top.v.txt