Giter Club home page Giter Club logo

abc's Introduction

.github/workflows/build-posix.yml .github/workflows/build-windows.yml .github/workflows/build-posix-cmake.yml

ABC: System for Sequential Logic Synthesis and Formal Verification

ABC is always changing but the current snapshot is believed to be stable.

ABC fork with new features

Here is a fork of ABC containing Agdmap, a novel technology mapper for LUT-based FPGAs. Agdmap is based on a technology mapping algorithm with adaptive gate decomposition [1]. It is a cut enumeration based mapping algorithm with bin packing for simultaneous wide gate decomposition, which is a patent pending technology.

The mapper is developed and maintained by Longfei Fan and Prof. Chang Wu at Fudan University in Shanghai, China. The experimental results presented in [1] indicate that Agdmap can substantially improve area (by 10% or more) when compared against the best LUT mapping solutions in ABC, such as command "if".

The source code is provided for research and evaluation only. For commercial usage, please contact Prof. Chang Wu at [email protected].

References:

[1] L. Fan and C. Wu, "FPGA technology mapping with adaptive gate decompostion", ACM/SIGDA FPGA International Symposium on FPGAs, 2023.

Compiling:

To compile ABC as a binary, download and unzip the code, then type make. To compile ABC as a static library, type make libabc.a.

When ABC is used as a static library, two additional procedures, Abc_Start() and Abc_Stop(), are provided for starting and quitting the ABC framework in the calling application. A simple demo program (file src/demo.c) shows how to create a stand-alone program performing DAG-aware AIG rewriting, by calling APIs of ABC compiled as a static library.

To build the demo program

  • Copy demo.c and libabc.a to the working directory
  • Run gcc -Wall -g -c demo.c -o demo.o
  • Run g++ -g -o demo demo.o libabc.a -lm -ldl -lreadline -lpthread

To run the demo program, give it a file with the logic network in AIGER or BLIF. For example:

[...] ~/abc> demo i10.aig
i10          : i/o =  257/  224  lat =    0  and =   2396  lev = 37
i10          : i/o =  257/  224  lat =    0  and =   1851  lev = 35
Networks are equivalent.
Reading =   0.00 sec   Rewriting =   0.18 sec   Verification =   0.41 sec

The same can be produced by running the binary in the command-line mode:

[...] ~/abc> ./abc
UC Berkeley, ABC 1.01 (compiled Oct  6 2012 19:05:18)
abc 01> r i10.aig; b; ps; b; rw -l; rw -lz; b; rw -lz; b; ps; cec
i10          : i/o =  257/  224  lat =    0  and =   2396  lev = 37
i10          : i/o =  257/  224  lat =    0  and =   1851  lev = 35
Networks are equivalent.

or in the batch mode:

[...] ~/abc> ./abc -c "r i10.aig; b; ps; b; rw -l; rw -lz; b; rw -lz; b; ps; cec"
ABC command line: "r i10.aig; b; ps; b; rw -l; rw -lz; b; rw -lz; b; ps; cec".
i10          : i/o =  257/  224  lat =    0  and =   2396  lev = 37
i10          : i/o =  257/  224  lat =    0  and =   1851  lev = 35
Networks are equivalent.

Compiling as C or C++

The current version of ABC can be compiled with C compiler or C++ compiler.

  • To compile as C code (default): make sure that CC=gcc and ABC_NAMESPACE is not defined.
  • To compile as C++ code without namespaces: make sure that CC=g++ and ABC_NAMESPACE is not defined.
  • To compile as C++ code with namespaces: make sure that CC=g++ and ABC_NAMESPACE is set to the name of the requested namespace. For example, add -DABC_NAMESPACE=xxx to OPTFLAGS.

Building a shared library

  • Compile the code as position-independent by adding ABC_USE_PIC=1.

  • Build the libabc.so target:

    make ABC_USE_PIC=1 libabc.so

Bug reporting:

Please try to reproduce all the reported bugs and unexpected features using the latest version of ABC available from https://github.com/berkeley-abc/abc

If the bug still persists, please provide the following information:

  1. ABC version (when it was downloaded from GitHub)
  2. Linux distribution and version (32-bit or 64-bit)
  3. The exact command-line and error message when trying to run the tool
  4. The output of the ldd command run on the exeutable (e.g. ldd abc).
  5. Versions of relevant tools or packages used.

Troubleshooting:

  1. If compilation does not start because of the cyclic dependency check, try touching all files as follows: find ./ -type f -exec touch "{}" \;
  2. If compilation fails because readline is missing, install 'readline' library or compile with make ABC_USE_NO_READLINE=1
  3. If compilation fails because pthreads are missing, install 'pthread' library or compile with make ABC_USE_NO_PTHREADS=1
  4. If compilation fails in file "src/base/main/libSupport.c", try the following:
    • Remove "src/base/main/libSupport.c" from "src/base/main/module.make"
    • Comment out calls to Libs_Init() and Libs_End() in "src/base/main/mainInit.c"
  5. On some systems, readline requires adding '-lcurses' to Makefile.

The following comment was added by Krish Sundaresan:

"I found that the code does compile correctly on Solaris if gcc is used (instead of g++ that I was using for some reason). Also readline which is not available by default on most Sol10 systems, needs to be installed. I downloaded the readline-5.2 package from sunfreeware.com and installed it locally. Also modified CFLAGS to add the local include files for readline and LIBS to add the local libreadline.a. Perhaps you can add these steps in the readme to help folks compiling this on Solaris."

The following tutorial is kindly offered by Ana Petkovska from EPFL: https://www.dropbox.com/s/qrl9svlf0ylxy8p/ABC_GettingStarted.pdf

Final remarks:

Unfortunately, there is no comprehensive regression test. Good luck!

This system is maintained by Alan Mishchenko [email protected]. Consider also using ZZ framework developed by Niklas Een: https://bitbucket.org/niklaseen/abc-zz (or https://github.com/berkeley-abc/abc-zz)

abc's People

Contributors

alanminko avatar aletempiac avatar allen1236 avatar arcanenibble avatar boschmitt avatar coastalwhite avatar davidar avatar eddiehung avatar fatsie avatar gadfort avatar hriener avatar hzeller avatar jamesjer avatar jix avatar ljbrooks avatar mmicko avatar msoeken avatar myskyko avatar niklaseen avatar phsauter avatar povik avatar quantamhd avatar rmanohar avatar rocallahan avatar sterin avatar vinicallegaro avatar whitequark avatar wjrforcyber avatar ycunxi avatar yshotw avatar

Stargazers

 avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar

Watchers

 avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar

abc's Issues

topmost feature request

abc 02> topmost -N 1
Error: Currently expects a single-output miter.

Would it be possible to enhance topmost to work on circuits with more than one output?

installing error abc_ fatal error

hello,
Getting a following error while installing ABC:
fatal error: readline/readline.h: No such file or directory
#include <readline/readline.h>

screenshot from 2019-01-01 23-20-36

ABC: execution of command "..." failed: return code 134.

Hi,

I initially opened the issue in yosys (YosysHQ/yosys#1675), but @eddiehung recommended me to open it here. See his comment here.

Steps to reproduce the issue

git clone https://github.com/adumont/hrm-cpu.git
cd hrm-cpu
git checkout issueABC
cd verilog
make bin

Failing commit is 2b4180c2bf508fead7d1d14def8600957124f50b.

will try to synthesize the design. The step:

yosys -p "synth_ice40 -top top -blif builddir/alhambra/top.blif " \
              -l builddir/alhambra/Echo/top.log -q hrmcpu.v ufifo.v ALU.v MEMORY.v XALU.v LEDS.v RAND.v ram.v mem_wrapper.v REG.v IR.v PROG.v WAIT.v PC.v ControlUnit.v debouncer.v rxuartlite.v txuartlite.v builddir/alhambra/top_wrapper.v top.v

fails with:

ERROR: ABC: execution of command "/home/adumont/toolchain/bin/yosys-abc -s -f /tmp/yosys-abc-eQGZWS/abc.script 2>&1" failed: return code 134.
$ /home/adumont/toolchain/bin/yosys-abc -s -f /tmp/yosys-abc-eQGZWS/abc.script 
ABC command line: "source /tmp/yosys-abc-eQGZWS/abc.script".
+ read_blif /tmp/yosys-abc-eQGZWS/input.blif 
+ read_lut /tmp/yosys-abc-eQGZWS/lutdefs.txt 
+ strash 
+ ifraig 
+ scorr 
Warning: The network is combinational (run "fraig" or "fraig_sweep").
+ dc2 
+ dretime 
+ strash 
+ dch -f 
+ if 
+ mfs2 
+ lutpack -S 1 
yosys-abc: src/opt/lpk/lpkCore.c:549: int Lpk_ResynthesizeNodeNew(Lpk_Man_t *): Assertion `nGain >= 1 - p->pPars->fZeroCost' failed.
Aborted (core dumped)

I've uploaded some stuff from the /tmp/yosys-abc-eQGZWS:

yosys-abc-eQGZWS.zip

My toolchain is updated to latest git version (tool/commit sha):

yosys.ver:9f5613100b360beb60608df1296ee81dc185e56c
arachne-pnr.ver:c40fb2289952f4f120cc10a5a4c82a6fb88442dc
icestorm.ver:0ec00d892a91cc68e45479b46161f649caea2933
iverilog.ver:b1114760fcfba55ee9ca35ba95e2b3ed2b7c7a20
symbiyosys.ver:500b526131f434b9679732fc89515dbed67c8d7d
verilator.ver:0c6c83e2787803d9b7c014ddbc8710f47d0f82f7
yices2.ver:1dcb71c405b5f1d21b363eb33b566068cad2e87d

Previous commit (053c6f1a5f2ab79add807138b24f92de6b3b308c053c6f1a5f2ab79add807138b24f92de6b3b308c) build fine.

Here's the diff in verilog code: adumont/hrm-cpu@2b4180c.

Expected behavior

It should produce the blif file.

Actual behavior

Fails with assertion in ABC.

More info:

Full build log of working commit: (Build 222) https://travis-ci.com/adumont/hrm-cpu/builds/147103961#L1596

Build log of failing commit: (Build 223) https://travis-ci.com/adumont/hrm-cpu/builds/147104799#L1482

Workaruound

I have tried scratchpad -set abc.script +strash;ifraig;scorr;dc2;dretime;strash;dch,-f;if;mfs2 before synth_ice40, as suggested by @eddiehung and it worked.

Compiler warnings

Dear developers,

compiling abc under OpenBSD (-current, cc is clang 6.0.0), I see the following warning messages:

`` Compiling: /src/sat/glucose/Glucose.cpp
c++ -c  -I./src -O2 -pipe -march=native -msse3 -mfpmath=sse -O2 -march=native -msse3 -mfpmath=sse -Wall -Wno-unused-function -Wno-write-strings -Wno-sign-compare -DLIN64 -DSIZEOF_VOID_P=8 -DSIZEOF_LONG=8 -DSIZEOF_INT=4 -DABC_USE_CUDD=1 -DABC_USE_READLINE  -DABC_USE_PTHREADS src/sat/glucose/Glucose.cpp -o src/sat/glucose/Glucose.o
src/sat/glucose/Glucose.cpp:1189:45: warning: format specifies type 'long' but the argument has type 'int64_t' (aka 'long long') [-Wformat]
  printf("c restarts              : %ld\n", starts);
                                    ~~~     ^~~~~~
                                    %lld
src/sat/glucose/Glucose.cpp:1190:45: warning: format specifies type 'long' but the argument has type 'int64_t' (aka 'long long') [-Wformat]
  printf("c nb ReduceDB           : %ld\n", nbReduceDB);
                                    ~~~     ^~~~~~~~~~
                                    %lld
src/sat/glucose/Glucose.cpp:1191:45: warning: format specifies type 'long' but the argument has type 'int64_t' (aka 'long long') [-Wformat]
  printf("c nb removed Clauses    : %ld\n", nbRemovedClauses);
                                    ~~~     ^~~~~~~~~~~~~~~~
                                    %lld
src/sat/glucose/Glucose.cpp:1192:45: warning: format specifies type 'long' but the argument has type 'int64_t' (aka 'long long') [-Wformat]
  printf("c nb learnts DL2        : %ld\n", nbDL2);
                                    ~~~     ^~~~~
                                    %lld
src/sat/glucose/Glucose.cpp:1193:45: warning: format specifies type 'long' but the argument has type 'int64_t' (aka 'long long') [-Wformat]
  printf("c nb learnts size 2     : %ld\n", nbBin);
                                    ~~~     ^~~~~
                                    %lld
src/sat/glucose/Glucose.cpp:1194:45: warning: format specifies type 'long' but the argument has type 'int64_t' (aka 'long long') [-Wformat]
  printf("c nb learnts size 1     : %ld\n", nbUn);
                                    ~~~     ^~~~
                                    %lld
src/sat/glucose/Glucose.cpp:1196:45: warning: format specifies type 'long' but the argument has type 'int64_t' (aka 'long long') [-Wformat]
  printf("c conflicts             : %ld\n", conflicts);
                                    ~~~     ^~~~~~~~~
                                    %lld
src/sat/glucose/Glucose.cpp:1197:45: warning: format specifies type 'long' but the argument has type 'int64_t' (aka 'long long') [-Wformat]
  printf("c decisions             : %ld\n", decisions);
                                    ~~~     ^~~~~~~~~
                                    %lld
src/sat/glucose/Glucose.cpp:1198:45: warning: format specifies type 'long' but the argument has type 'int64_t' (aka 'long long') [-Wformat]
  printf("c propagations          : %ld\n", propagations);
                                    ~~~     ^~~~~~~~~~~~
                                    %lld
9 warnings generated.
`` Compiling: /src/misc/extra/extraUtilMaj.c
cc -c  -I./src -O2 -pipe -march=native -msse3 -mfpmath=sse -O2 -march=native -msse3 -mfpmath=sse -Wall -Wno-unused-function -Wno-write-strings -Wno-sign-compare -DLIN64 -DSIZEOF_VOID_P=8 -DSIZEOF_LONG=8 -DSIZEOF_INT=4 -DABC_USE_CUDD=1 -DABC_USE_READLINE  -DABC_USE_PTHREADS src/misc/extra/extraUtilMaj.c -o src/misc/extra/extraUtilMaj.o
src/misc/extra/extraUtilMaj.c:373:58: warning: data argument not used by format string [-Wformat-extra-args]
    printf( "Finished          (functions = %10d)  ", v, p->nObjs );
            ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~     ^
1 warning generated.

Maybe it's worth a look?

--
Alessandro DE LAURENZIS

Bad read in `Hash_PtrForEachEntry`

Hello,
you have a bug in the Hash_PtrForEachEntry macro:
https://github.com/berkeley-abc/abc/blob/master/src/misc/hash/hashPtr.h#L70

The last pArray[++bin] is accessing out of the allocated memory. The line should be rewritten to something like this:

for(bin=-1, pEntry=NULL; bin < pHash->nBins; (!pEntry)?(++bin < pHash->nBins && (pEntry=pHash->pArray[bin])):(pEntry=pEntry->pNext))

Or something more performing, so that the check would not be performed twice (but the macro invocation for this snippet would be different):

#define Hash_PtrForEachEntry( pHash, pEntry, bin, action )   \
  bin = -1; \
  pEntry = NULL; \
  \
  while ( 1 ) { \
    if (pEntry) { \
      action \
      pEntry = pEntry->pNext; \
    } \
    else { \
      ++bin; \
      if ( bin >= pHash->nBins ) \
        break; \
      pEntry = pHash->pArray[bin]; \
    } \
  } 

[Feature] How to write the output file in topological order?

I have a combinational circuit that is optimized in ABC. When writing the optimized design using the write_verilog command, I get assign statements that are not topologically sorted and therefore, make understanding of the code difficult.

I have read in an online powerpoint presentation of ABC that the internal AIG keeps the nodes in topological order. Is it possible to write them in a file using the same order? How about for a network that is not AIG (e.g. multi is called before writing the file).

--best chooses abc and contrib/get-abc fails

$ contrib/get-abc
Using CC=gcc
Using CXX=g++
Using LD=g++
Compiling with CUDD
Found GCC_VERSION 9.3.0
Found GCC_MAJOR>=4
Using CFLAGS=-Wall -Wno-unused-function -Wno-write-strings -Wno-sign-compare -arch x86_64 -DABC_USE_CUDD=1
`` Generating dependency: /src/bdd/llb/llb4Sweep.c
`` Generating dependency: /src/bdd/llb/llb4Nonlin.c
`` Generating dependency: /src/bdd/llb/llb4Image.c
`` Generating dependency: /src/bdd/llb/llb4Cex.c
`` Generating dependency: /src/bdd/llb/llb3Image.c
`` Generating dependency: /src/bdd/llb/llb3Nonlin.c
`` Generating dependency: /src/bdd/llb/llb2Image.c
`` Generating dependency: /src/bdd/llb/llb2Flow.c
`` Generating dependency: /src/bdd/llb/llb2Dump.c
`` Generating dependency: /src/bdd/llb/llb2Driver.c
`` Generating dependency: /src/bdd/llb/llb2Core.c
`` Generating dependency: /src/bdd/llb/llb2Bad.c
`` Generating dependency: /src/bdd/llb/llb1Sched.c
`` Generating dependency: /src/bdd/llb/llb1Reach.c
`` Generating dependency: /src/bdd/llb/llb1Pivot.c
`` Generating dependency: /src/bdd/llb/llb1Matrix.c
gcc: error: x86_64: No such file or directory
gcc: error: x86_64: No such file or directory
gcc: error: x86_64: No such file or directory
gcc: error: x86_64: No such file or directory
gcc: error: unrecognized command line option โ€˜-archโ€™
...

&dc2 assertion failure

The attached testcase dc2_assertion.tar.gz causes the following assertion to fire in &dc2 on latest master 24d9ce6:

$ ./abc -F abc.script
ABC command line: "source -x abc.script".

abc - > read_box abc9_hx.box;
abc - > &read input.xaig;
abc - > &ps;
input    : i/o =    104/    111  and =    3705  lev =  220 (16.09)  mem = 0.14 MB  box = 915  bb = 0
Warning: AIG with boxes has internal fanout in 0 complex flops and 849 carries.
abc - > &sweep;
abc - > &ps;
input    : i/o =    104/    111  and =    2340  lev =   22 (0.81)  mem = 0.06 MB  box = 285  bb = 0
Warning: AIG with boxes has internal fanout in 0 complex flops and 243 carries.
abc - > &dc2;
yosys-abc: src/opt/dar/darRefact.c:589: int Dar_ManRefactor(Aig_Man_t *, Dar_RefPar_t *): Assertion `(int)Aig_Regular(pObjNew)->Level <= Required' failed.

Removing &sweep (which destroys 630 boxes!) eliminates this assertion, which indicates that there could be some corruption in that command?

Unfortunately, I do apologise for the number of boxes: the original reporter in YosysHQ/yosys#1561 was unable to reproduce it on smaller variants.

Thanks!

Which transformation is used in order to convert a bench file into CNF

I tried converting a .bench file into a .cnf file using the following workflow,

read_cnf AND.bench
strash
write_cnf AND.cnf

The tranformation basically changes the OR gate,
INPUT(pi00)
INPUT(pi01)
OUTPUT(po0)
po0 = OR(pi00, pi01)

Into this following file,

c Result of efficient AIG-to-CNF conversion using package CNF
p cnf 5 5
-2 3 4 0
2 -3 0
2 -4 0
-5 0
2 0

The number of variables in the CNF has increased to 5 and I am not exactly sure which transformation scheme is used here.
It would be of great help if you could clarify this.

Assertion 'Abc_NtkIsStrash(pNtk)' failed in 'write_cnf'

I'm trying to convert verilog file to cnf file. I have read the verilog file successfully and can use command 'sat' to solve the miter. But when I use 'write_cnf' to output the cnf file. The abc aborted by throwing the failure: 'abc: src/base/abci/abcDar.c:1812: Abc_NtkDarToCnf: Assertion `Abc_NtkIsStrash(pNtk)' failed.' Can you give me some advice?

&gla with dump mapping failed

Symptom:

Miter with abstraction map will be continously dumped into file "cnt2_gla.aig".
abc: src/aig/gia/giaAiger.c:1183: Gia_AigerWrite: Assertion `Vec_PtrSize(p->vNamesIn) == Gia_ManCiNum(p)' failed.

how to trigger:

read_blif cnt2.blif
&get -n
&gla -F 30 -v -m

cnt2.zip

How it is triggered:
1 There is a latch with don't-care initialization, and
2 &get -n keeps the name, and
3 Only if dumping the mapping, will &gla checks the name array size.

Shared libary is installed w/out the headers

All installed files:

$ pkg info -l abc
abc-g20191026:
	/usr/local/bin/abc
	/usr/local/lib/libabc.so

Library is useless without headers. Other projects, like vtr-verilog-to-routing expect abc's headers.

Error within lutpack algorithm

Enclosed testCase shows probably functionality error. For specified inputs one of output: n6263 changes its value from 0 to 1 during ABC flow(during lutpack stage).
Tested on ABC(f6dc4a5), Linux 5.6.8-100.fc30.x86_64.
When tried to run test on the newest version of ABC got a runtime error: double free or corruption (!prev).
testCase.zip

Blif -> Aig -> Vlg Bug?

There seems to be a bug of handling latches with don't-care initial value (update: sorry, I cannot localize the source of the extra input, I tried to initialize the latch, but it seems there is still this extra input)

abc 01> read_blif cnt2.blif
abc 02> strash
abc 03> write_aiger nondet.aig

and then

abc 01> read_aiger nondet.aig 
abc 02> write_verilog nondet.v

and in nondet.v there appears an extra unused input.

cnt2.zip

Linking error when using ABC as a static library

When linking to ABC as a static library in my project, I receive a linking error in the final step (the actual linking command is more complex due to the build system, I have somewhat simplified it):

# /usr/bin/c++ -Wall -pedantic -g strix/main.cc.o lib/abc/libabc.a
/usr/bin/ld: lib/abc/libabc.a(dauCanon.c.o): in function `Abc_TtCountOnesInTruth':
~/dev/strix/lib/abc/src/opt/dau/dauCanon.c:320: undefined reference to `Abc_TtVerifySmallTruth'
/usr/bin/ld: lib/abc/libabc.a(dauCanon.c.o): in function `Abc_TtCountOnesInCofs':
~/dev/strix/lib/abc/src/opt/dau/dauCanon.c:332: undefined reference to `Abc_TtVerifySmallTruth'
/usr/bin/ld: lib/abc/libabc.a(dauCanon.c.o): in function `Abc_TtScc6':
~/dev/strix/lib/abc/src/opt/dau/dauCanon.c:384: undefined reference to `shiftFunc'
/usr/bin/ld: lib/abc/libabc.a(dauCanon.c.o): in function `Abc_TtSccInCofs6':
~/dev/strix/lib/abc/src/opt/dau/dauCanon.c:410: undefined reference to `shiftFunc'
/usr/bin/ld: lib/abc/libabc.a(dauCanon.c.o): in function `Abc_TtCannonVerify':
~/dev/strix/lib/abc/src/opt/dau/dauCanon.c:1552: undefined reference to `Abc_TtVerifySmallTruth'
/usr/bin/ld: lib/abc/libabc.a(dauCanon.c.o): in function `Abc_TtCanonicizeAda':
~/dev/strix/lib/abc/src/opt/dau/dauCanon.c:2585: undefined reference to `Abc_TtVerifySmallTruth'
/usr/bin/ld: lib/abc/libabc.a(dauCanon.c.o): in function `Abc_TtCanonicizeCA':
~/dev/strix/lib/abc/src/opt/dau/dauCanon.c:2646: undefined reference to `Abc_TtVerifySmallTruth'
collect2: error: ld returned 1 exit status

I am using GCC 9.1.0 for compiling and linking. The issue can be easily fixed by declaring the following two functions as static in addition to inline, as otherwise the compiler may choose to eliminate them without inlining:

inline void Abc_TtVerifySmallTruth(word * pTruth, int nVars)
inline int shiftFunc(int ci)

Verification success on unsafe model?

Hi,
For this .aig model:

aig 1 0 1 1 0 0 1
0
0
3

(corresponding .aag model is:

aag 1 0 1 1 0 0 1
2 0
0
3

)
abc thinks the model is safe:

$ ./abc/abc -c "read reduced.aig;pdr -g;write_cex -a out.cex"
ABC command line: "read reduced.aig;pdr -g;write_cex -a out.cex".

Warning: The last output is interpreted as a constraint.
Warning: The new network has no primary inputs. It is recommended
to add a dummy PI to make sure all commands work correctly.
Invariant F[1] : 1 clauses with 1 flops (out of 1) (cex = 0, ave = 1.00)
Verification of invariant with 1 clauses was successful.  Time =     0.00 sec
Property proved.  Time =     0.02 sec
Counter-example is not available.
$ cat reduced.aig
aig 1 0 1 1 0 0 1
0
0
3

However, there is a valid counter-example according to the aigsim tool:

$ ./aiger-1.9.4/aigsim -c reduced.aig out
[aigsim] WARNING no bad state properties found using outputs instead
$ cat out
1
b0
0


.

Is it the expected behavior or the bug?

OS: Ubuntu 18.04
Commit: a277d45

bottommost feature request

Would it be possible to add a bottommost command that acts similarly to topmost? That is, the bottommost command would replace the current network by its bottom most level(s).

write_aiger with initialized latches produces wrong output

I save the following circuit with a one-initialized latch and a single output as binary AIGER in test.aig:

aig 1 0 1 1 0
3 1
2
l0 l0
o0 o0

Then I invoke ABC as follows:

abc 01> read_aiger test.aig
abc 02> write_aiger -s test.abc.aig

The resulting output in test.abc.aig is (with stripped comments):

aig 1 0 1 0 0 1 0
3 1
2
l0 l0
b0 o0

This file uses the extended header format, even though this wasn't specified, and the output o0 is incorrectly converted to a "bad state" property (see AIGER 1.9 format).

I expect the same output as the input file, i.e. a single normal output o0 and no extended header.

mltest command not found

In IWLS 2020 contest, the website says we can use "mltest" to evaluate the accuracy of the synthesized aig. But the tool says unknown command.

PDR bug? Invariant does not imply the proved property

The design (attached) is converted from Verilog to Blif (by Yosys).
It is a 2-bit register that can only be updated to 3 or 0, based on other signals. It looks like this:


always @(posedge clk) begin
    if (rst) begin
      reg_mstatus_mpp <= rst_mstatus_mpp;
    end else begin
      if (wen) begin
        if (T_5098) begin
          if (T_6142) begin
            reg_mstatus_mpp <= 2'h3;
          end else begin
            reg_mstatus_mpp <= 2'h0;
          end
        end else begin
          if (insn_ret) begin
            if (T_5454) begin
              reg_mstatus_mpp <= 2'h0;
...

And the property to prove is this register should not be 1 (2'b01)

When the initial value is 00:

abc 01> read_blif wrapper_init00.blif
abc 02> strash
abc 03> pdr
Invariant F[2] : 1 clauses with 2 flops (out of 10) (cex = 0, ave = 2.00)
Verification of invariant with 1 clauses was successful.  Time =     0.00 sec
Property proved.  Time =     0.01 sec
abc 03> inv_print
Invariant contains 1 clauses with 2 literals and 2 flops (out of 10).
abc 03> inv_print -v
Invariant contains 1 clauses with 2 literals and 2 flops (out of 10).
10 1
abc 03> ***EOF***

This is as expected.

When initial value is 11:

UC Berkeley, ABC 1.01 (compiled Apr 30 2019 02:29:30)
abc 01> read_blif wrapper_init11.blif
abc 02> strash
abc 03> pdr
Invariant F[1] : 1 clauses with 2 flops (out of 10) (cex = 0, ave = 2.00)
Verification of invariant with 1 clauses was successful.  Time =     0.00 sec
Property proved.  Time =     0.01 sec
abc 03> inv_print -v
Invariant contains 1 clauses with 2 literals and 2 flops (out of 10).
01 1

This can be interpreted as reg_mstatus_mpp != 2'b10 , which does not imply reg_mstatus_mpp != 2'b01

test.zip

Word Level Identification

Hi,

I'm really new to this field and I've been reading some papers about the topic of "word level components" identification like the following:

  • Structural Reverse Engineering of Arithmetic Circuits
  • WordRev: Finding Word-Level Structures in a Sea of Bit-Level Gates
  • Reverse Engineering Digital Circuits Using Functional Analysis
  • Reverse Engineering Circuits Using Behavioral Pattern Mining
  • Automatic Word-level Abstraction of Datapath
  • Rewriting Environment for Arithmetic Circuit Verification (polynomials as output)

I noticed that some of the exposed ideas have been implemented in ABC, but, while diving in the help -d command, I was wondering if there is a suggested way to achieve the following (with ABC commands):

  • identify candidate word cuts via shape hashing and/or bit-slice aggregation;
  • automatic word-level abstraction (of AND, OR, XOR, ADD, MUL n-bit components).

In my experiments I'm starting with a word-level representation written in Verilog, I'm converting it to BLIF with Yosys and then I would like to ideally get back to the word-level representation (or to having a contained amount of candidate word cuts to apply some kind of synthesis of the sub-circuit). In the examples I'm also using hardcoded constants that are propagated in the circuit (hindering the "shape" of the components):

module example (a, b, c, o);
//-------------Input Ports Declarations----------------------------
input [3:0]a;
input [3:0]b;
input [3:0]c;
//-------------Output Ports Declarations---------------------------
output [3:0]o;
//-------------Wires Declarations----------------------------------
wire [3:0]w1;
wire [3:0]w2;
wire [3:0]w3;
wire [3:0]w4;
//-------------Logic-----------------------------------------------
assign w1 = (a * b);
assign w2 = (w1 | c);
assign w3 = (w2 + 8'h3);
assign w4 = (w3 - w1);
assign o = w4;
endmodule

It's really likely that I'm missing knowledge of the current state-of-the-art on the topic, so I won't mind reading more papers that promise an open source (or well documented) solution. It's my understanding that the polynomial-based rewriting techniques to obtain the circuit signature on the inputs is the current best approach for the verification problem, but I didn't find proper research on using polynomials for word-level abstraction (except for the multiplier P(x) identification in Reverse Engineering of Irreducible Polynomials in GF(2^m) Arithmetic).

bmc2 Segmentation fault

Hi,
For this model:
Segfault.zip

ABC throws out a segmentation fault with bmc2 command:

$ abc/abc -c "read segfault.aig;logic;undc;strash;zero;fold;bmc2;" 
ABC command line: "read segfault.aig;logic;undc;strash;zero;fold;bmc2;".

Warning: The last 10 outputs are interpreted as constraints.
Segmentation fault

While pdr command works well on it:

$ abc/abc -c "read segfault.aig;logic;undc;strash;zero;fold;pdr;" 
ABC command line: "read segfault.aig;logic;undc;strash;zero;fold;pdr;".

Warning: The last 10 outputs are interpreted as constraints.
Invariant F[1] : 1 clauses with 1 flops (out of 3183) (cex = 0, ave = 24.00)
Verification of invariant with 1 clauses was successful.  Time =     0.00 sec
Property proved.  Time =     0.06 sec

OS: Ubuntu 18.04
Commit: dab7168

ABC assertion

Hello, I'm using ABC with Yosys (platform: latest OS X) and got this assert.
YosysHQ/yosys#1028
ABC version: 38e2f41
ABC compiled with these:

[  5%] ABC: Using CC=clang
[  5%] ABC: Using CXX=clang
[  5%] ABC: Using LD=clang
[  5%] ABC: Compiling with CUDD
[  5%] ABC: Using libreadline
[  5%] ABC: Using pthreads
[  5%] ABC: Using explicit -lstdc++
[  5%] ABC: Using CFLAGS=-Wall -Wno-unused-function -Wno-write-strings -Wno-sign-compare -DLIN64 -DSIZEOF_VOID_P=8 -DSIZEOF_LONG=8 -DSIZEOF_INT=4 -DABC_USE_CUDD=1 -DABC_USE_READLINE  -DABC_USE_PTHREADS

Any idea how can I be helpful for debugging this?

Request for release branch or archive

Hello, I'm a packager for Arch Linux, and I want to package abc for Arch Linux in community repository, I wonder if there will be a stable version for releasing?

Segmentation Fault While Trying to Write Verilog

I have tried to output the mapping result by "write_verilog", but after I typed the command, the system showed that there was segmentation fault.
I also tried to output the mapping result in blif format, and it worked.
I tried to search for what caused the segmentation fault problem, but can't get the information.
How can I solve the problem?

Compile warnings.

Hello, got these.

:src/sat/glucose/Glucose.cpp:1189:45: warning: format
      specifies type 'long' but the argument has type
      'int64_t' (aka 'long long') [-Wformat]
  printf("c restarts              : %ld\n", starts);
                                    ~~~     ^~~~~~
                                    %lld
src/sat/glucose/Glucose.cpp:1190:45: warning: format
      specifies type 'long' but the argument has type
      'int64_t' (aka 'long long') [-Wformat]
  printf("c nb ReduceDB           : %ld\n", nbReduceDB);
                                    ~~~     ^~~~~~~~~~
                                    %lld
src/sat/glucose/Glucose.cpp:1191:45: warning: format
      specifies type 'long' but the argument has type
      'int64_t' (aka 'long long') [-Wformat]
  ...nb removed Clauses    : %ld\n", nbRemovedClauses);
                             ~~~     ^~~~~~~~~~~~~~~~
                             %lld
src/sat/glucose/Glucose.cpp:1192:45: warning: format
      specifies type 'long' but the argument has type
      'int64_t' (aka 'long long') [-Wformat]
  printf("c nb learnts DL2        : %ld\n", nbDL2);
                                    ~~~     ^~~~~
                                    %lld
src/sat/glucose/Glucose.cpp:1193:45: warning: format
      specifies type 'long' but the argument has type
      'int64_t' (aka 'long long') [-Wformat]
  printf("c nb learnts size 2     : %ld\n", nbBin);
                                    ~~~     ^~~~~
                                    %lld
src/sat/glucose/Glucose.cpp:1194:45: warning: format
      specifies type 'long' but the argument has type
      'int64_t' (aka 'long long') [-Wformat]
  printf("c nb learnts size 1     : %ld\n", nbUn);
                                    ~~~     ^~~~
                                    %lld
src/sat/glucose/Glucose.cpp:1196:45: warning: format
      specifies type 'long' but the argument has type
      'int64_t' (aka 'long long') [-Wformat]
  printf("c conflicts             : %ld\n", conflicts);
                                    ~~~     ^~~~~~~~~
                                    %lld
src/sat/glucose/Glucose.cpp:1197:45: warning: format
      specifies type 'long' but the argument has type
      'int64_t' (aka 'long long') [-Wformat]
  printf("c decisions             : %ld\n", decisions);
                                    ~~~     ^~~~~~~~~
                                    %lld
src/sat/glucose/Glucose.cpp:1198:45: warning: format
      specifies type 'long' but the argument has type
      'int64_t' (aka 'long long') [-Wformat]
  printf("c propagations          : %ld\n", propagations);
                                    ~~~     ^~~~~~~~~~~~
                                    %lld

./src/sat/satoko/utils/sdbl.h:124:24: warning: format
      specifies type 'unsigned long' but the argument has
      type 'sdbl_t' (aka 'unsigned long long') [-Wformat]
    printf("%016lX\n", double2sdbl(1 /0.95));
            ~~~~~~     ^~~~~~~~~~~~~~~~~~~~
            %016llX
./src/sat/satoko/utils/sdbl.h:125:24: warning: format
      specifies type 'unsigned long' but the argument has
      type 'sdbl_t' (aka 'unsigned long long') [-Wformat]
    printf("%016lX\n", SDBL_CONST1);
            ~~~~~~     ^~~~~~~~~~~
            %016llX


file included from ./src/sat/satoko/satoko.h:12:
In file included from ./src/sat/satoko/types.h:12:
./src/sat/satoko/utils/sdbl.h:124:24: warning: format
      specifies type 'unsigned long' but the argument has
      type 'sdbl_t' (aka 'unsigned long long') [-Wformat]
    printf("%016lX\n", double2sdbl(1 /0.95));
            ~~~~~~     ^~~~~~~~~~~~~~~~~~~~
            %016llX
./src/sat/satoko/utils/sdbl.h:125:24: warning: format
      specifies type 'unsigned long' but the argument has
      type 'sdbl_t' (aka 'unsigned long long') [-Wformat]
    printf("%016lX\n", SDBL_CONST1);
            ~~~~~~     ^~~~~~~~~~~
            %016llX


src/sat/xsat/xsatSolver.h:227:40: warning: format
      specifies type 'long' but the argument has type
      'iword' (aka 'long long') [-Wformat]
  ..."conflicts     : %10ld\n", s->Stats.nConflicts );
                      ~~~~~     ^~~~~~~~~~~~~~~~~~~
                      %10lld
src/sat/xsat/xsatSolver.h:228:40: warning: format
      specifies type 'long' but the argument has type
      'iword' (aka 'long long') [-Wformat]
  ..."decisions     : %10ld\n", s->Stats.nDecisions );
                      ~~~~~     ^~~~~~~~~~~~~~~~~~~
                      %10lld
src/sat/xsat/xsatSolver.h:229:40: warning: format
      specifies type 'long' but the argument has type
      'iword' (aka 'long long') [-Wformat]
  ..."propagations  : %10ld\n", s->Stats.nPropagations );
                      ~~~~~     ^~~~~~~~~~~~~~~~~~~~~~
                      %10lld


src/sat/xsat/xsatSolverAPI.c:341:40: warning: format
      specifies type 'long' but the argument has type
      'iword' (aka 'long long') [-Wformat]
  ..."conflicts     : %10ld\n", s->Stats.nConflicts );
                      ~~~~~     ^~~~~~~~~~~~~~~~~~~
                      %10lld
src/sat/xsat/xsatSolverAPI.c:342:40: warning: format
      specifies type 'long' but the argument has type
      'iword' (aka 'long long') [-Wformat]
  ..."decisions     : %10ld\n", s->Stats.nDecisions );
                      ~~~~~     ^~~~~~~~~~~~~~~~~~~
                      %10lld
src/sat/xsat/xsatSolverAPI.c:343:40: warning: format
      specifies type 'long' but the argument has type
      'iword' (aka 'long long') [-Wformat]
  ..."propagations  : %10ld\n", s->Stats.nPropagations );
                      ~~~~~     ^~~~~~~~~~~~~~~~~~~~~~
                      %10lld

Error thrown by %read while reading Verilog RTL

I was trying to use ABC command %read to read a Verilog RTL file. The command throws a "*** stack smashing detected *** error" at the assign statements (example: while reading line 11 assign w_01_ = X + 4'h1; for the example below).

module counter(clk, prop_neg, en);
  wire [3:0] w_00_;
  wire [3:0] w_01_;
  wire w_02_;
  wire [3:0] w_03_;
  reg [3:0] X;
  input clk;
  input en;
  wire prop;
  output prop_neg;
  assign w_01_ = X + 4'h1;
  assign w_02_ = X == 4'hf;
  assign prop_neg = ! prop;
  assign prop = X != 4'h0;
  initial
    X = 4'h1;
  always @(posedge clk)
      X <= w_00_;
  assign w_03_ = w_02_ ? 4'h1 : w_01_;
  assign w_00_ = en ? w_03_ : X;
endmodule

Is there any specific restriction on Verilog designs ABC can read as of now?

Assertion using &if: `pCutSet->nCuts > 0'

A Yosys user reported the following assertion from ABC on their design:

yosys-abc: src/map/if/ifMap.c:460: void If_ObjPerformMappingAnd(If_Man_t *, If_Obj_t *, int, int, int): Assertion `pCutSet->nCuts > 0' failed.

this is happening inside &if

Attached is the abc input, run abc.script to reproduce.
abc_crash_if.zip

No 'dont care' process in 'resyn' pla

test.pla

.i 3
.o 1
.ilb a b c
.ob x
.type fr
011 1
010 0
.e

step

read_pla test.pla
resyn
write_pla out.pla

I got result

.i 3
.o 1
.ilb a b c
.ob x
.p 1
011 1
.e

expected result

.i 3
.o 1
.ilb a b c
.ob x
.p 1
--1 1
.e

what's wrong with my step ? thanks

vercore Ver_ParseInsertsSuffix: Assertion `nMsb >= 0 && nMsb < 128' failed.

Hi,
I am using a verilog code which has a bus of 1268 bits. I am assuming abc can not handle a bus size of more than 128. Is there any way to solve the issue. The error says as follows:
"abc: src/base/ver/verCore.c:594: Ver_ParseInsertsSuffix: Assertion `nMsb >= 0 && nMsb < 128' failed.
Aborted (core dumped)"

Differet number of LUTs in case different order of input ports

Two similar input.blif files (there are only differences in order of inputs port list) produce different number of LUTs. Enclosed testCase shows following situation. Number of LUTs changes between 18 and 25.
Could you please tell me why order of inputs causes such big differences?
Is there any way to determine sequence of input ports to achieve smaller number of LUTs?
How to reproduce problem:
./abc -F abc.script
testCase.zip

double free or corruption error during yosys abc9 techmap pass

See yosys-abc-test.tgz. Reproduce with:

tar xfz yosys-abc-test.tgz
cd yosys-abc-test
abc -s -f ./abc.script

Program fails with:

+ &write -n ./output.aig 
Error: Gia_ManMappingVerify: Internal node -1 does not have mapping.
+ time 
elapse: 53.38 seconds, total: 53.38 seconds
double free or corruption (out)
Aborted (core dumped)

Any idea as to what might be going wrong much appreciated!

Code compatibility with OpenBSD

Dear developers,

I'm trying to port abc in OpenBSD. The code compiles flawlessly and the program runs as expected (lightly tested on amd64 for a limited set of test-cases), provided the following trivial patch is applied to the Makefile (in order to correctly setup the compiler's options):

Index: Makefile
--- Makefile.orig
+++ Makefile
@@ -75,6 +75,9 @@ endif

 ABC_READLINE_INCLUDES ?=
 ABC_READLINE_LIBRARIES ?= -lreadline
+ifeq ($(OS), OpenBSD)
+  ABC_READLINE_LIBRARIES += -lcurses
+endif

 # whether to use libreadline
 ifndef ABC_USE_NO_READLINE
@@ -135,12 +138,17 @@ endif

 # LIBS := -ldl -lrt
 LIBS += -lm
-ifneq ($(OS), FreeBSD)
+ifneq ($(OS), $(filter $(OS), FreeBSD OpenBSD))
   LIBS += -ldl
 endif

+LIBS += -lrt
+
 ifneq ($(findstring Darwin, $(shell uname)), Darwin)
-   LIBS += -lrt
+   LIBS := $(filter-out -lrt, $(LIBS))
+endif
+ifeq ($(OS), OpenBSD)
+   LIBS := $(filter-out -lrt, $(LIBS))
 endif

 ifdef ABC_USE_LIBSTDCXX

Any chances to include it into the official code?

Thanks and regards

--
Alessandro DE LAURENZIS

Using constraints in verification?

The output other than the first one can be used for constraints in newer AIGER format , as is used by Yosys when translates $assume into AIGER. In read_aiger command, parsing of the new header is supported. I wonder if they can be truly used in any verification command in ABC? (I tried and it seemed that pdr does not support the extra output as constraints, or I just didn't find the right way...)

bmc2 Segmentation fault (core dump)

Hi,
For this model:
segfault.zip

ABC throws out a segmentation fault with bmc2 command on both original model and reduced model, while pdr works well:

$ abc/abc -c "read segfault.aig;logic;undc;strash;zero;fold;bmc2;"
ABC command line: "read segfault.aig;logic;undc;strash;zero;fold;bmc2;".

Warning: The last 2 outputs are interpreted as constraints.
Segmentation fault (core dumped)

$ abc/abc -c "read reduced.aig;logic;undc;strash;zero;fold;bmc2;"
ABC command line: "read reduced.aig;logic;undc;strash;zero;fold;bmc2;".

Warning: The network has no constraints.
Segmentation fault (core dumped)

$ abc/abc -c "read segfault.aig;logic;undc;strash;zero;fold;pdr;"
ABC command line: "read segfault.aig;logic;undc;strash;zero;fold;pdr;".

Warning: The last 2 outputs are interpreted as constraints.
Invariant F[5] : 9 clauses with 10 flops (out of 42) (cex = 0, ave = 21.93)
Verification of invariant with 9 clauses was successful.  Time =     0.00 sec
Property proved.  Time =     0.02 sec

$ abc/abc -c "read reduced.aig;logic;undc;strash;zero;fold;pdr;"
ABC command line: "read reduced.aig;logic;undc;strash;zero;fold;pdr;".

Warning: The network has no constraints.
Output 0 of miter "reduced" was asserted in frame 16384.  Time =    21.19 sec

$ cat reduced.aag 
aag 66 1 16 0 49 1
2
4 63
6 66
8 70
10 74
12 78
14 82
16 86
18 90
20 94
22 98
24 102
26 106
28 110
30 114
32 33
34 126
132
36 32 30
38 36 28
40 38 26
42 40 24
44 42 22
46 44 20
48 46 18
50 48 16
52 50 14
54 52 12
56 54 10
58 56 8
60 58 6
62 61 5
64 59 7
66 65 61
68 57 9
70 69 59
72 55 11
74 73 57
76 53 13
78 77 55
80 51 15
82 81 53
84 49 17
86 85 51
88 47 19
90 89 49
92 45 21
94 93 47
96 43 23
98 97 45
100 41 25
102 101 43
104 39 27
106 105 41
108 37 29
110 109 39
112 33 31
114 113 37
116 34 2
118 35 3
120 119 117
122 120 2
124 121 3
126 125 123
128 35 2
130 128 3
132 131 4

It should be different from #75, since #75 seems to be fixed and does not have (core dump).

OS: Ubuntu 18.04
Commit: 94a2cff

strange behavior: Abc_AigOr(),Abc_AigXor() and Abc_ObjNot()

Hello,
I encounter strange behavior while using Abc_AigOr(), Abc_AigXor() and Abc_ObjNot() from abc/src/base/abc/abc.h.

my code:

     ...
    Abc_Ntk_t * pAig;
    pAig = Abc_NtkAlloc(ABC_NTK_STRASH, ABC_FUNC_AIG,1);

    Abc_Obj_t * pObj, *pObjA,*pObjB,*pObjC,*pObjD,*pObjE;
    int i;  
    for(i=0;i<2;i++)
    {
        pObj = Abc_NtkCreatePi(pAig);
        std::cout <<"Pi " << i << " Id = " << pObj->Id << std::endl;
        std::cout <<"!Pi " <<i << " Id = " << Abc_ObjNot(pObj)->Id << std::endl;
    }
    pObjA = Abc_NtkObj(pAig,1);
    pObjB = Abc_NtkObj(pAig,2);
    std::cout <<"pObjA->Id = " << pObjA->Id << std::endl;
    std::cout <<"pObjB->Id = " << pObjB->Id << std::endl;
    pObjC = Abc_AigOr((Abc_Aig_t *)pAig->pManFunc,pObjA,pObjB);
    pObjD = Abc_AigXor((Abc_Aig_t *)pAig->pManFunc,pObjA,pObjB);
    pObjE = Abc_AigAnd((Abc_Aig_t *)pAig->pManFunc,pObjA,pObjB);
    std::cout <<"pObjC->Id = " << pObjC->Id << std::endl;    
    std::cout <<"pObjD->Id = " << pObjD->Id << std::endl; 
    std::cout <<"pObjE->Id = " << pObjE->Id << std::endl;    

    pObj = Abc_NtkObj(pAig,pObjC->Id); //try to get pt to the or objekt

    Abc_ObjAddFanin(Abc_NtkCreatePo(pAig),pObjC);
    
    Abc_NtkDelete(pAig);
    ...

the output:

> Pi 0 Id = 1
> !Pi 0 Id = 33554432
> Pi 1 Id = 2
> !Pi 1 Id = 33554432
> pObjA->Id = 1
> pObjB->Id = 2
> pObjC->Id = -2030043136
> pObjD->Id = -2030043136
> pObjE->Id = 7
> abc: ./src/misc/vec/vecPtr.h:388: void* Vec_PtrEntry(Vec_Ptr_t*, int): Assertion `i >= 0 && i < p->nSize' failed.

doing the same with abc/src/aig/aig/aig.h works fine.

LUT2 mapping

I have tried to map an application to LUT of size 2. But the resulting netlist contains LUT 2 and 3.
I use abc through yosys (I don't know how to use abc alone).

My RTL:

module Adder8(z, b, a);
    output [7:0] z;
    input [7:0] a, b;

    assign z = a + b;
endmodule

My synthesis script:

proc; opt; fsm; opt; memory; opt
techmap; opt
abc -lut 2 -dress; opt

The netlist:

/* Generated by Yosys 0.9+1706 (git sha1 8b074cc4, gcc 9.2.1+20200130-2 -march=native -O3 -fno-plt -fPIC -Os) */

(* top =  1  *)
(* src = "/home/killruana/projects/kfpga_workspace/testsuite/apps/adder8/rtl/Adder8.v:3.1-8.10" *)
module Adder8(z, b, a);
  (* src = "/home/killruana/projects/kfpga_workspace/testsuite/apps/adder8/rtl/Adder8.v:0|<techmap.v>:295.27-295.69|<techmap.v>:238.21-238.22" *)
  wire _00_;
  (* src = "/home/killruana/projects/kfpga_workspace/testsuite/apps/adder8/rtl/Adder8.v:0|<techmap.v>:295.27-295.69|<techmap.v>:238.21-238.22" *)
  wire _01_;
  (* src = "/home/killruana/projects/kfpga_workspace/testsuite/apps/adder8/rtl/Adder8.v:0|<techmap.v>:295.27-295.69|<techmap.v>:238.21-238.22" *)
  wire _02_;
  (* src = "/home/killruana/projects/kfpga_workspace/testsuite/apps/adder8/rtl/Adder8.v:0|<techmap.v>:295.27-295.69|<techmap.v>:238.21-238.22" *)
  wire _03_;
  (* src = "/home/killruana/projects/kfpga_workspace/testsuite/apps/adder8/rtl/Adder8.v:0|<techmap.v>:295.27-295.69|<techmap.v>:238.21-238.22" *)
  wire _04_;
  (* src = "/home/killruana/projects/kfpga_workspace/testsuite/apps/adder8/rtl/Adder8.v:0|<techmap.v>:295.27-295.69|<techmap.v>:238.21-238.22" *)
  wire _05_;
  (* src = "/home/killruana/projects/kfpga_workspace/testsuite/apps/adder8/rtl/Adder8.v:0|<techmap.v>:295.27-295.69|<techmap.v>:238.21-238.22" *)
  wire _06_;
  wire _07_;
  wire _08_;
  wire _09_;
  wire _10_;
  wire _11_;
  wire _12_;
  wire _13_;
  (* src = "/home/killruana/projects/kfpga_workspace/testsuite/apps/adder8/rtl/Adder8.v:5.17-5.18" *)
  input [7:0] a;
  (* src = "/home/killruana/projects/kfpga_workspace/testsuite/apps/adder8/rtl/Adder8.v:5.20-5.21" *)
  input [7:0] b;
  (* src = "/home/killruana/projects/kfpga_workspace/testsuite/apps/adder8/rtl/Adder8.v:4.18-4.19" *)
  output [7:0] z;
  assign z[1] = 4'h6 >> { _07_, _00_ };
  assign _00_ = 4'h8 >> { b[0], a[0] };
  assign _07_ = 4'h6 >> { b[1], a[1] };
  assign z[2] = 4'h9 >> { _08_, _01_ };
  assign _08_ = 4'h6 >> { b[2], a[2] };
  assign z[3] = 4'h9 >> { _09_, _02_ };
  assign _09_ = 4'h6 >> { b[3], a[3] };
  assign z[4] = 4'h9 >> { _10_, _03_ };
  assign _10_ = 4'h6 >> { b[4], a[4] };
  assign z[5] = 4'h9 >> { _11_, _04_ };
  assign _11_ = 4'h6 >> { b[5], a[5] };
  assign z[6] = 4'h9 >> { _12_, _05_ };
  assign _12_ = 4'h6 >> { b[6], a[6] };
  assign _13_ = 4'h9 >> { b[7], a[7] };
  assign z[0] = 4'h6 >> { b[0], a[0] };
  assign _01_ = 8'h17 >> { _00_, b[1], a[1] };
  assign _02_ = 8'h71 >> { _01_, b[2], a[2] };
  assign _03_ = 8'h71 >> { _02_, b[3], a[3] };
  assign _04_ = 8'h71 >> { _03_, b[4], a[4] };
  assign _05_ = 8'h71 >> { _04_, b[5], a[5] };
  assign _06_ = 8'h71 >> { _05_, b[6], a[6] };
  assign z[7] = 4'h6 >> { _13_, _06_ };
endmodule

The abc script used by yosys for the abc -lut 2 command is strash; ifraig; scorr; dc2; dretime; retime {D}; strash; dch -f; if; mfs2; lutpack {S}. Someone from the Yosys subreddit pointed out that the culprit is probably the lutpack command and recommended me to notify the upstream, so here I am :)

src/base/io/ioReadAiger.c:435: Io_ReadAiger: Assertion failed

Hi,
For this Aiger model (both aig and aag included in the zip file):
assertion.zip
ABC throws out an assertion failed with pdr:

$ abc/abc -c "read assertion.aig;pdr -g;write_cex -a out.cex"
ABC command line: "read assertion.aig;pdr -g;write_cex -a out.cex".

Warning: The last 2 outputs are interpreted as constraints.
abc: src/base/io/ioReadAiger.c:435: Io_ReadAiger: Assertion `Init == Abc_Var2Lit(1+Abc_NtkPiNum(pNtkNew)+i, 0)' failed.
Aborted

Is it the expected behavior? Thanks!

OS: Ubuntu 18.04
Commit: c7bc6b6

Logic network assertion fails in `putontop`

top.aag:

aag 3 2 0 1 1                                                                                                         
2                                                                                                                     
4                                                                                                                     
6                                                                                                                     
6 4 2                                                                                                                 

bot.aag:

aag 1 1 0 2 0                                                                                                         
2                                                                                                                     
2                                                                                                                     
2    

The putontop command results in the following:

$ abc -Q 'read bot.aig; logic; putontop top.aig'
abc: src/base/abci/abcStrash.c:798: Abc_NtkPutOnTop: Assertion `Abc_NtkIsLogic(pNtk2)' failed.
Aborted (core dumped)

In the Abc_CommandPutOnTop() function of src/base/abci/abc.c, the AIG passed to putontop is not converted to a logic network before the call to Abc_NtkPutOnTop(), causing it to fail the assertion. Adding this conversion via Abc_NtkToLogic() lets putontop work as expected.

Constructing AIGs in ABC

I followed the instructions in the tutorial "Constructing AIGs in ABC" and want to compile it with libabc.a.

  1. What should I do with the enums in the functions? For example,
    Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
  2. How do I declare the functions used in the tutorial like the above one(since I don't know the types of the arguments)?
  3. How do I pass the aig network into the framework to do further steps such as FRAIG or SAT?

One of the Glucose header files is an HTML file

This doesn't seem to affect the normal build, so it must not be included anywhere, but one of the header files in src/sat/glucose isn't valid. The contents of stdint.h are HTML, maybe as a result of downloading it from somewhere? Although the build works, this causes trouble for the C2HS tool we use to create Haskell bindings to ABC, and we would love to be able to update those bindings to use the latest ABC version.

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    ๐Ÿ–– Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. ๐Ÿ“Š๐Ÿ“ˆ๐ŸŽ‰

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google โค๏ธ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.