synth_ice40 -abc9 fails assertion `(int)Aig_Regular(pObjNew)->Level <= Required'

[eddyb]

Steps to reproduce the issue

See top.il + top.ys.

Also, make sure that the issue is actually reproducable in current git
master of Yosys.

TODO: check this (only tried it on Yosys 0.9+932 (git sha1 3c41599ee1, g++ 8.3.0 -fPIC -Os))
EDIT: confirmed by @eddiehung, see below.

Expected behavior

Should succeed, worst case with an error because it can't fit the 24-bit division by 3, into an iCEstick.
Smaller sizes, such as 17-bit or 20-bit do succeed and perform correctly AFAICT, with -abc9.
EDIT: 27-bit works as well, which was surprising to me, as I assumed larger bitwidths would only aggravate the issue, but apparently not.

Actual behavior

Crashes with:

ABC: yosys-abc: src/opt/dar/darRefact.c:589: Dar_ManRefactor:
    Assertion `(int)Aig_Regular(pObjNew)->Level <= Required' failed`.

[eddiehung]

Can repro on master (ecb0c68). Am suspecting an upstream abc issue...

EDIT: Yosys' abc is 33 commits behind upstream abc master. I can also reproduce this on same Yosys + abc master (berkeley-abc/abc@24d9ce6)

EDIT2: Problem goes away if synth_ice40 -nocarry (which are the source of the only whiteboxes passed to abc9). Will report upstream.

[eddiehung]

@eddyb Actually before I report this upstream, can you try and minimise the number of SB_CARRY cells (there are 915 in your example!) and/or share the original source for this *.il?
I understand from your edit that more bits doesn't equate to sustained breakage.. but can we reduce the width/depth? I had a go at minimising the *.il by deleting some output ports to no avail...

[eddyb]

@eddiehung I'm not sure I can reduce this, as decreasing the main parameter (number of decimal digits, which leads to the bitwidths I mentioned before), or removing the division by 3, results in success.

Here's the source aoc-2019-1.py, but note that it uses nmigen which outputs IL directly.
I had set the NMIGEN_synth_opts=-abc9 environment variable to have yosys use abc9.

[eddiehung]

Reported upstream: berkeley-abc/abc#61

[eddiehung]

Can still reproduce this on the latest master 5ebdc0f

[Ravenslofty]

It's now 2021 and I just hit this again while working on multiplier inference for QuickLogic...

[Ravenslofty]

I attempted to reduce the testcase with bugpoint but to little avail. Still, having multiple testcases might help.

dc2crash.tar.gz

[Ravenslofty]

Some more information that might be useful: if I replace the timings in qlal4s3_mult_cell_macro with this monstrosity I autogenerated a while back it gets accepted, despite the netlists being identical.

[eddiehung]

Can no longer reproduce with linked top.il + top.ys on b2e9717. Closing for now.