eqy stuck in infinite loop with gate design primitives (Xilinx gates) as blackboxes

YosysHQ / eqy

Equivalence checking with Yosys

https://yosyshq.readthedocs.io/projects/eqy/en/latest/

Other

30 stars 5 forks source link

eqy stuck in infinite loop with gate design primitives (Xilinx gates) as blackboxes #55

Open xtofalex opened 8 months ago

xtofalex commented 8 months ago

Hi, I guess I'm using naively the tool by comparing two netlists: initial RTL and one file after synthesis targeting Xilinx and providing Xilinx gates as blackboxes. Still when doing so, the tool hangs in an infinite loop in the eqy execute, in particular in co_flatten_worker method.

I've attached a test case.

Versions I'm using: Yosys 0.38+54 (git sha1 f8d4d7128, clang 15.0.0 -fPIC -Os) eqy: latest (5791c90)

test_case.tar.gz

Thanks. Christophe

maliberty commented 6 months ago

It would be good if there was some response here. Christophe's work will eventually benefit the OSS tool flow but needs to be able to be verified with eqy.

jix commented 6 months ago

Comparing blackboxes on one side to logic on the other side is not supported. This should produce an error, though, and not hang, so this is an error handling bug.