ABC pass mangles synthesized logic on big endian architectures

[gsomlo]

Steps to reproduce the issue

Using a recent yosys commit (e.g. 9cdc6b5), apply the following patch (suggested by @mwkmwkmwk on IRC):

diff --git a/tests/techmap/shiftx2mux.ys b/tests/techmap/shiftx2mux.ys
index f749e79b..0f8f42a4 100644
--- a/tests/techmap/shiftx2mux.ys
+++ b/tests/techmap/shiftx2mux.ys
@@ -70,6 +70,7 @@ EOT
 
 proc
 pmux2shiftx
+write_rtlil gold.il
 design -save gold
 
 
@@ -77,6 +78,7 @@ design -load gold
 techmap
 abc -lut 6
 select -assert-count 16 t:$lut
+write_rtlil gate1.il
 
 design -stash gate
 design -import gold -as gold
@@ -89,6 +91,7 @@ design -load gold
 techmap
 abc9 -lut 6
 select -assert-count 16 t:$lut
+write_rtlil gate2.il
 
 design -stash gate
 design -import gold -as gold

Then build yosys on a BE architecture, e.g. ppc64 or s390x.

Once build completes, run make test to execute the test suite

Expected behavior

tests succeeds

Actual behavior

tests/techmap/shiftx2mux.ys fails with "ERROR: Called with -verify and proof did fail!!"

Please also see yosys-shiftx2mux-test.tar.gz which contains two folders containing logging and *.il files generated during the (patched as per above) test: one for x86_64 (where the test succeeds), and one for s390x, where it fails before reaching the second gate.

[mwkmwkmwk]

Some more information after a slack discussion:

• this is an abc bug, and is also present in the upstream
• abc uses bitvectors made of 32-bit words in one place and ones made of 64-bit words in another; sometimes it does a raw pointer cast between the two, completely breaking the logic on big-endian machines (and violating aliasing rules in the process on any machine)
• this particular bug is triggered on https://github.com/berkeley-abc/abc/blob/f87c8b434a3024972c6bc85c072d80adbed3e778/src/opt/sfm/sfmCnf.c#L116 but there are a lot more places like this, and it'd take a lot of effort to get that code to working order on big-endian machines
• this means that abc (and, in turn, yosys) should be considered unusably broken on big-endian machines until this issue is fixed (and, preferably, the abc codebase audited to make sure there are no other endianness issues)
• this bug will be reported to upstream, but don't hold your breath; the yosys team doesn't have enough familiarity with the codebase to reasonably fix this issue ourselves

[DanielG]

FYI: we're seeing this test failure with vanilla make test now on Debian's big-endian architectures, no need for OP's patch.