YosysHQ / eqy

Equivalence checking with Yosys
https://yosyshq.readthedocs.io/projects/eqy/en/latest/
Other
30 stars 5 forks source link

Unclear what the error is #67

Closed maliberty closed 3 months ago

maliberty commented 3 months ago

In the OR CI we are getting errors from eqy that I can't understand:

EQY 17:58:34 [logs/nangate45/aes/base/4_eqy_output] run: ERROR: Failed to import cell $flatten\__po_clkbuf_0_clk.A__assert.$assert$../../../partitions/aes_cipher_top.clkbuf_0_clk.A.sv:58$102639 (type $check) to SAT database.

I don't know what this means or how to resolve it.

The test case is at https://drive.google.com/file/d/1MxsYZ1BXajjLpNBu5XhIXaA1shqyeG4y/view?usp=sharing and can be run with

eqy -d logs/nangate45/aes/base/4_eqy_output --force --jobs 40 objects/nangate45/aes/base/4_eqy_test.eqy |& tee logs/nangate45/aes/base/4_equivalence_check.log
jix commented 3 months ago

The .eqy config in the test case contains references to files that are not included, but I'm assuming this is the missing file. I can't reproduce the error with the latest EQY version and the error message also points to an EQY vs yosys version mismatch. Please make sure to always update to the EQY version tagged yosys-0.xy whenever you update to yosys 0.xy.

To make it easier to tell whether there's a version mismatch, I also just opened a PR that adds a --version option to EQY (#68) which will make it possible to check for mismatches between separately installed yosys and EQY versions.

maliberty commented 3 months ago

Thanks I'll update eqy to match and see if that resolves it.

Yes that should be the missing file.

maliberty commented 3 months ago

Updating has resolved the issue. Thanks for the help!