A topological loop is generated after using async2sync

[ZhiyuanYan]

Version

Yosys 0.36+72

On which OS did this happen?

Linux

Reproduction Steps

Here is the source file: reproduce.tar.gz.

After downloading the source file from the attachment, you can use the following commands to reproduce the issues: tar -xzvf reproduce.tar.gz cd reproduce/ yosys or_1200.ys

Expected Behavior

A Btor file should be generated successfully.

Actual Behavior

After using async2sync, a logic loop was detected by scc. The following figure shows the result of detecting the logic loop before using the command async2sync. And this figure indicates the result of detecting the logic loop after using the command async2sync. We can see that, after applying async2sync, a logic loop was synthesized, which led to an error (Found topological loop) when I tried to generate a BTOR file: Another interesting phenomenon is that, in the original RTL file, we changed the width of the state variable coverage_ and modified the index of the coverage_ to be assigned in the always block, then a BTOR file was generated successfully. You can run the following command to get this result: yosys or_1200_assert.ys Compared to the original file, the changes are only the width of the state variable coverage_ and the index of the coverage_ to be assigned, but no logic loop is produced in this case, thus we can obtain a BTOR file finally.

[rowanG077]

Can you try on current master? There was a patch that improved loop detection and got rid of some false positives not too long ago.

Edit: I can't reproduce this on version 0.40+25. I get a different error:

...
9. Executing SIM pass (simulate the circuit).
Simulating cycle 0.
ERROR: Unsupported cell type: $check (or1200_top.$assert$or1200_dut_new.v:10001$2062)

[ZhiyuanYan]

@rowanG077 After downloading the new version of Yosys (Yosys 0.41+108), I still cannot solve this problem. No logic loop is produced before the async2sync, while 2 logic loops are generated after executing the async2sync.

The different error is because the async2sync needs to be executed before the sim. The attachment is the new version, I have moved the command async2sync before the sim: reproduce.tar.gz