I'm trying to compare two post-synth netlists: one where clock gates are inferred and one where the clock gates are not inferred. SEC is reporting a difference, so I'm not sure if it's an issue in kepler-formal or in yosys clockgate.
I've captured the output after setting the KEPLER_SEC_DIAG and KEPLER_SEC_PDR_TRACE env vars.
The nangate45 based example is attached.
infer.v.txt
miter_log_0.txt
no_infer.v.txt
output.log
verify.yml.txt
I'm trying to compare two post-synth netlists: one where clock gates are inferred and one where the clock gates are not inferred. SEC is reporting a difference, so I'm not sure if it's an issue in kepler-formal or in yosys clockgate.
I've captured the output after setting the KEPLER_SEC_DIAG and KEPLER_SEC_PDR_TRACE env vars.
The nangate45 based example is attached.
infer.v.txt
miter_log_0.txt
no_infer.v.txt
output.log
verify.yml.txt