From a1f5e4541b64f28f6bacbbe3dddd408eb6c6ab6f Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Mon, 20 Oct 2025 07:38:00 +0200 Subject: [PATCH 1/9] Fix compilation for mingw and wasi --- src/opt/eslim/synthesisEngine.tpp | 4 ++++ src/sat/cadical/cadical_congruence.cpp | 2 +- src/sat/cadical/cadical_file.cpp | 14 +++++++++++--- src/sat/cadical/cadical_random.cpp | 4 ++-- src/sat/cadical/cadical_resources.cpp | 4 ++++ src/sat/cadical/cadical_signal.cpp | 20 ++++++++++++++++---- src/sat/cadical/cadical_vivify.cpp | 4 ++-- src/sat/cadical/file.hpp | 2 +- src/sat/cadical/internal.hpp | 2 ++ src/sat/kissat/colors.c | 2 +- 10 files changed, 44 insertions(+), 14 deletions(-) diff --git a/src/opt/eslim/synthesisEngine.tpp b/src/opt/eslim/synthesisEngine.tpp index 6a8485f7f..ef94d9226 100644 --- a/src/opt/eslim/synthesisEngine.tpp +++ b/src/opt/eslim/synthesisEngine.tpp @@ -614,7 +614,11 @@ namespace eSLIM { // sprintf( pCommand, "%s -q %s > %s", pKissat, pFileNameIn, pFileNameOut ); sprintf( pCommand, "%s -q %s > %s", pKissat, pFileNameIn, pFileNameOut ); +#ifdef __wasm + if ( 1 ) { +#else if ( system( pCommand ) == -1 ) { +#endif std::cerr << "Command " << pCommand << " failed\n"; return nullptr; } diff --git a/src/sat/cadical/cadical_congruence.cpp b/src/sat/cadical/cadical_congruence.cpp index 8fbceee24..dd5f30b7a 100644 --- a/src/sat/cadical/cadical_congruence.cpp +++ b/src/sat/cadical/cadical_congruence.cpp @@ -5981,7 +5981,7 @@ void Closure::rewrite_ite_gate (Gate *g, int dst, int src) { #endif } else { CADICAL_assert (false); -#ifdef WIN32 +#if defined(WIN32) && !defined(__MINGW32__) __assume(false); #else __builtin_unreachable (); diff --git a/src/sat/cadical/cadical_file.cpp b/src/sat/cadical/cadical_file.cpp index 98f19f752..d48193e93 100644 --- a/src/sat/cadical/cadical_file.cpp +++ b/src/sat/cadical/cadical_file.cpp @@ -33,7 +33,9 @@ extern "C" { #else extern "C" { +#if !defined(__wasm) #include +#endif #include } @@ -245,6 +247,7 @@ void File::delete_str_vector (std::vector &argv) { FILE *File::open_pipe (Internal *internal, const char *fmt, const char *path, const char *mode) { +#if !defined(__wasm) #ifdef CADICAL_QUIET (void) internal; #endif @@ -269,6 +272,9 @@ FILE *File::open_pipe (Internal *internal, const char *fmt, FILE *res = popen (cmd, mode); delete[] cmd; return res; +#else + return 0; +#endif } FILE *File::read_pipe (Internal *internal, const char *fmt, const int *sig, @@ -285,7 +291,7 @@ FILE *File::read_pipe (Internal *internal, const char *fmt, const int *sig, return open_pipe (internal, fmt, path, "r"); } -#ifndef _WIN32 +#if !defined(_WIN32) && !defined(__wasm) #if defined(__APPLE__) || defined(__MACH__) static std::mutex compressed_file_writing_mutex; @@ -420,7 +426,7 @@ File *File::read (Internal *internal, const char *path) { File *File::write (Internal *internal, const char *path) { FILE *file; int close_output = 3, child_pid = 0; -#ifndef _WIN32 +#if !defined(_WIN32) && !defined(__wasm) if (has_suffix (path, ".xz")) file = write_pipe (internal, "xz -c", path, child_pid); else if (has_suffix (path, ".bz2")) @@ -456,12 +462,14 @@ void File::close (bool print) { MSG ("closing file '%s'", name ()); fclose (file); } +#if !defined(__wasm) if (close_file == 2) { if (print) MSG ("closing input pipe to read '%s'", name ()); pclose (file); } -#ifndef _WIN32 +#endif +#if !defined(_WIN32) && !defined(__wasm) if (close_file == 3) { if (print) MSG ("closing output pipe to write '%s'", name ()); diff --git a/src/sat/cadical/cadical_random.cpp b/src/sat/cadical/cadical_random.cpp index 85d022e8f..044f6aba0 100644 --- a/src/sat/cadical/cadical_random.cpp +++ b/src/sat/cadical/cadical_random.cpp @@ -84,7 +84,7 @@ ABC_NAMESPACE_IMPL_END // work. As an additional measure to increase the possibility to get // different seeds we are now also using network addresses (explicitly). -#ifndef WIN32 +#if !defined(_WIN32) && !defined(__wasm) extern "C" { #include @@ -110,7 +110,7 @@ static uint64_t hash_network_addresses () { // you really need to run 'mobical' on a Windows cluster where each node // has identical IP addresses. -#ifndef WIN32 +#if !defined(_WIN32) && !defined(__wasm) struct ifaddrs *addrs; if (!getifaddrs (&addrs)) { for (struct ifaddrs *addr = addrs; addr; addr = addr->ifa_next) { diff --git a/src/sat/cadical/cadical_resources.cpp b/src/sat/cadical/cadical_resources.cpp index 9a2b421e5..912a40568 100644 --- a/src/sat/cadical/cadical_resources.cpp +++ b/src/sat/cadical/cadical_resources.cpp @@ -131,10 +131,14 @@ uint64_t maximum_resident_set_size () { // This seems to work on Linux (man page says since Linux 2.6.32). uint64_t maximum_resident_set_size () { +#ifdef __wasm + return 0; +#else struct rusage u; if (getrusage (RUSAGE_SELF, &u)) return 0; return ((uint64_t) u.ru_maxrss) << 10; +#endif } // Unfortunately 'getrusage' on Linux does not support current resident set diff --git a/src/sat/cadical/cadical_signal.cpp b/src/sat/cadical/cadical_signal.cpp index 099277f03..7e8fc965b 100644 --- a/src/sat/cadical/cadical_signal.cpp +++ b/src/sat/cadical/cadical_signal.cpp @@ -7,11 +7,13 @@ /*------------------------------------------------------------------------*/ #include +#if !defined(__wasm) #include +#endif /*------------------------------------------------------------------------*/ -#ifndef WIN32 +#if !defined(_WIN32) && !defined(__wasm) extern "C" { #include } @@ -28,7 +30,7 @@ namespace CaDiCaL { static volatile bool caught_signal = false; static Handler *signal_handler; -#ifndef WIN32 +#if !defined(_WIN32) && !defined(__wasm) static volatile bool caught_alarm = false; static volatile bool alarm_set = false; @@ -38,6 +40,7 @@ void Handler::catch_alarm () { catch_signal (SIGALRM); } #endif +#if !defined(__wasm) #define SIGNALS \ SIGNAL (SIGABRT) \ SIGNAL (SIGINT) \ @@ -47,8 +50,9 @@ void Handler::catch_alarm () { catch_signal (SIGALRM); } #define SIGNAL(SIG) static void (*SIG##_handler) (int); SIGNALS #undef SIGNAL +#endif -#ifndef WIN32 +#if !defined(_WIN32) && !defined(__wasm) static void (*SIGALRM_handler) (int); @@ -66,6 +70,7 @@ void Signal::reset_alarm () { void Signal::reset () { signal_handler = 0; +#if !defined(__wasm) #define SIGNAL(SIG) \ (void) signal (SIG, SIG##_handler); \ SIG##_handler = 0; @@ -73,11 +78,13 @@ void Signal::reset () { #undef SIGNAL #ifndef WIN32 reset_alarm (); +#endif #endif caught_signal = false; } const char *Signal::name (int sig) { +#if !defined(__wasm) #define SIGNAL(SIG) \ if (sig == SIG) \ return #SIG; @@ -86,6 +93,7 @@ const char *Signal::name (int sig) { #ifndef WIN32 if (sig == SIGALRM) return "SIGALRM"; +#endif #endif return "UNKNOWN"; } @@ -97,6 +105,7 @@ const char *Signal::name (int sig) { // exclusive access to. All these solutions are painful and not elegant. static void catch_signal (int sig) { +#if !defined(__wasm) #ifndef WIN32 if (sig == SIGALRM && absolute_real_time () >= alarm_time) { if (!caught_alarm) { @@ -116,16 +125,19 @@ static void catch_signal (int sig) { Signal::reset (); ::raise (sig); } +#endif } void Signal::set (Handler *h) { +#if !defined(__wasm) signal_handler = h; #define SIGNAL(SIG) SIG##_handler = signal (SIG, catch_signal); SIGNALS #undef SIGNAL +#endif } -#ifndef WIN32 +#if !defined(_WIN32) && !defined(__wasm) void Signal::alarm (int seconds) { CADICAL_assert (seconds >= 0); diff --git a/src/sat/cadical/cadical_vivify.cpp b/src/sat/cadical/cadical_vivify.cpp index 8d99c2932..5ec6401cf 100644 --- a/src/sat/cadical/cadical_vivify.cpp +++ b/src/sat/cadical/cadical_vivify.cpp @@ -1501,7 +1501,7 @@ inline std::vector ¤t_refs_schedule (Vivifier &vivifier) { return vivifier.refs_schedule_irred; break; } -#ifdef WIN32 +#if defined(WIN32) && !defined(__MINGW32__) __assume(false); #else __builtin_unreachable (); @@ -1523,7 +1523,7 @@ inline std::vector ¤t_schedule (Vivifier &vivifier) { return vivifier.schedule_irred; break; } -#ifdef WIN32 +#if defined(WIN32) && !defined(__MINGW32__) __assume(false); #else __builtin_unreachable (); diff --git a/src/sat/cadical/file.hpp b/src/sat/cadical/file.hpp index 860e9613a..a8baf82b9 100644 --- a/src/sat/cadical/file.hpp +++ b/src/sat/cadical/file.hpp @@ -66,7 +66,7 @@ class File { const char *mode); static FILE *read_pipe (Internal *, const char *fmt, const int *sig, const char *path); -#ifndef WIN32 +#if !defined(_WIN32) && !defined(__wasm) static FILE *write_pipe (Internal *, const char *fmt, const char *path, int &child_pid); #endif diff --git a/src/sat/cadical/internal.hpp b/src/sat/cadical/internal.hpp index d86479a52..53c698c58 100644 --- a/src/sat/cadical/internal.hpp +++ b/src/sat/cadical/internal.hpp @@ -17,7 +17,9 @@ #include #include #include +#if !defined(__wasm) #include +#endif #include #include #include diff --git a/src/sat/kissat/colors.c b/src/sat/kissat/colors.c index f45260b29..c6141b749 100644 --- a/src/sat/kissat/colors.c +++ b/src/sat/kissat/colors.c @@ -1,6 +1,6 @@ #include "colors.h" -#ifdef WIN32 +#if defined(WIN32) && !defined(__MINGW32__) #define isatty _isatty #else #include From 7f64516f23af558bc2a3e98756909d2fbbbdac20 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 24 Nov 2025 08:01:26 -0800 Subject: [PATCH 2/9] Fix to maintain correct order of boxes after "&mfs". --- src/aig/gia/giaMfs.c | 70 ++++++++++++++++++++++++++++---------------- 1 file changed, 44 insertions(+), 26 deletions(-) diff --git a/src/aig/gia/giaMfs.c b/src/aig/gia/giaMfs.c index 7ddef2b89..fe50e7b5e 100644 --- a/src/aig/gia/giaMfs.c +++ b/src/aig/gia/giaMfs.c @@ -290,15 +290,16 @@ Gia_Man_t * Gia_ManInsertMfs( Gia_Man_t * p, Sfm_Ntk_t * pNtk, int fAllBoxes ) int nBoxes = Gia_ManBoxNum(p); int nRealPis = nBoxes ? Tim_ManPiNum(pManTime) : Gia_ManPiNum(p); int nRealPos = nBoxes ? Tim_ManPoNum(pManTime) : Gia_ManPoNum(p); - int i, k, Id, curCi, curCo, nBoxIns, nBoxOuts, iLitNew, iMfsId, iGroup, Fanin; + int i, k, curCi, curCo, nBoxIns, nBoxOuts, iLitNew, iMfsId, iGroup, Fanin, iBox; int nMfsNodes; word * pTruth, uTruthVar = ABC_CONST(0xAAAAAAAAAAAAAAAA); Vec_Wec_t * vGroups = Vec_WecStart( nBoxes ); Vec_Int_t * vMfs2Gia, * vMfs2Old; Vec_Int_t * vGroupMap; - Vec_Int_t * vMfsTopo, * vCover, * vBoxesLeft; + Vec_Int_t * vMfsTopo, * vCover, * vBoxesLeft, * vBoxKeep; Vec_Int_t * vArray, * vLeaves; Vec_Int_t * vMapping, * vMapping2; + Vec_Int_t * vCoDrivers; int nBbIns = 0, nBbOuts = 0; if ( pManTime ) Tim_ManBlackBoxIoNum( pManTime, &nBbIns, &nBbOuts ); nMfsNodes = 1 + Gia_ManCiNum(p) + Gia_ManLutNum(p) + Gia_ManCoNum(p) + nBbIns + nBbOuts; @@ -342,6 +343,10 @@ Gia_Man_t * Gia_ManInsertMfs( Gia_Man_t * p, Sfm_Ntk_t * pNtk, int fAllBoxes ) // collect nodes in the given order vBoxesLeft = Vec_IntAlloc( nBoxes ); vMfsTopo = Sfm_NtkDfs( pNtk, vGroups, vGroupMap, vBoxesLeft, fAllBoxes ); + Vec_IntUniqify( vBoxesLeft ); // reduce to sorted unique indices expected by the timing manager + vBoxKeep = Vec_IntStart( nBoxes ); + Vec_IntForEachEntry( vBoxesLeft, iBox, i ) + Vec_IntWriteEntry( vBoxKeep, iBox, 1 ); assert( Vec_IntSize(vBoxesLeft) <= nBoxes ); assert( Vec_IntSize(vMfsTopo) > 0 ); @@ -360,13 +365,22 @@ Gia_Man_t * Gia_ManInsertMfs( Gia_Man_t * p, Sfm_Ntk_t * pNtk, int fAllBoxes ) // map constant Vec_IntWriteEntry( vMfs2Gia, Gia_ObjCopyArray(p, 0), 0 ); - // map primary inputs - Gia_ManForEachCiId( p, Id, i ) - if ( i < nRealPis ) - Vec_IntWriteEntry( vMfs2Gia, Gia_ObjCopyArray(p, Id), Gia_ManAppendCi(pNew) ); + // map primary inputs (real ones and preserved box outputs) + Gia_ManForEachCi( p, pObj, i ) + { + int iCiId = Gia_ObjId( p, pObj ); + int iBox = pManTime ? Tim_ManBoxForCi( pManTime, Gia_ObjCioId(pObj) ) : -1; + if ( iBox >= 0 && !Vec_IntEntry(vBoxKeep, iBox) ) + { + Vec_IntWriteEntry( vMfs2Gia, Gia_ObjCopyArray(p, iCiId), -1 ); + continue; + } + Vec_IntWriteEntry( vMfs2Gia, Gia_ObjCopyArray(p, iCiId), Gia_ManAppendCi(pNew) ); + } // map internal nodes vLeaves = Vec_IntAlloc( 6 ); vCover = Vec_IntAlloc( 1 << 16 ); + vCoDrivers = Vec_IntStartFull( Gia_ManCoNum(p) ); Vec_IntForEachEntry( vMfsTopo, iMfsId, i ) { pTruth = Sfm_NodeReadTruth( pNtk, iMfsId ); @@ -374,10 +388,13 @@ Gia_Man_t * Gia_ManInsertMfs( Gia_Man_t * p, Sfm_Ntk_t * pNtk, int fAllBoxes ) vArray = Sfm_NodeReadFanins( pNtk, iMfsId ); // belongs to pNtk if ( Vec_IntSize(vArray) == 1 && Vec_IntEntry(vArray,0) < nBbOuts ) // skip unreal inputs { - // create CI for the output of black box assert( Abc_LitIsCompl(iGroup) ); - iLitNew = Gia_ManAppendCi( pNew ); - Vec_IntWriteEntry( vMfs2Gia, iMfsId, iLitNew ); + iLitNew = Vec_IntEntry( vMfs2Gia, iMfsId ); + if ( iLitNew == -1 ) + { + iLitNew = Gia_ManAppendCi( pNew ); + Vec_IntWriteEntry( vMfs2Gia, iMfsId, iLitNew ); + } continue; } Vec_IntClear( vLeaves ); @@ -411,36 +428,36 @@ Gia_Man_t * Gia_ManInsertMfs( Gia_Man_t * p, Sfm_Ntk_t * pNtk, int fAllBoxes ) Abc_TtFlipVar5( pTruth, Vec_IntSize(vLeaves) ); } } - else if ( Abc_LitIsCompl(iGroup) ) // internal CI + else if ( Abc_LitIsCompl(iGroup) ) // internal CI (box output) { - //Dau_DsdPrintFromTruth( pTruth, Vec_IntSize(vLeaves) ); - iLitNew = Gia_ManAppendCi( pNew ); + iLitNew = Vec_IntEntry( vMfs2Gia, iMfsId ); + if ( iLitNew < 0 ) + continue; } else // internal CO { + int iObjOld = Vec_IntEntry( vMfs2Old, iMfsId ); + int iCoIdx; + assert( iObjOld >= 0 ); assert( pTruth[0] == uTruthVar || pTruth[0] == ~uTruthVar ); - iLitNew = Gia_ManAppendCo( pNew, Abc_LitNotCond(Vec_IntEntry(vLeaves, 0), pTruth[0] == ~uTruthVar) ); - //printf("Group = %d. po = %d\n", iGroup>>1, iMfsId ); + iLitNew = Abc_LitNotCond( Vec_IntEntry(vLeaves, 0), pTruth[0] == ~uTruthVar ); + iCoIdx = Gia_ObjCioId( Gia_ManObj(p, iObjOld) ); + Vec_IntWriteEntry( vCoDrivers, iCoIdx, iLitNew ); } Vec_IntWriteEntry( vMfs2Gia, iMfsId, iLitNew ); } Vec_IntFree( vCover ); Vec_IntFree( vLeaves ); - // map primary outputs + // map primary outputs (internal box inputs followed by real POs) Gia_ManForEachCo( p, pObj, i ) { - if ( i < Gia_ManCoNum(p) - nRealPos ) // internal COs + if ( i < Gia_ManCoNum(p) - nRealPos ) { - iMfsId = Gia_ObjCopyArray( p, Gia_ObjId(p, pObj) ); - iGroup = Vec_IntEntry( vGroupMap, iMfsId ); - if ( Vec_IntFind(vMfsTopo, iGroup) >= 0 ) - { - iLitNew = Vec_IntEntry( vMfs2Gia, iMfsId ); - if ( iLitNew < 0 ) - continue; - assert( iLitNew >= 0 ); - } + iLitNew = Vec_IntEntry( vCoDrivers, i ); + if ( iLitNew == -1 ) + continue; + Gia_ManAppendCo( pNew, iLitNew ); continue; } iLitNew = Vec_IntEntry( vMfs2Gia, Gia_ObjCopyArray(p, Gia_ObjFaninId0p(p, pObj)) ); @@ -483,6 +500,8 @@ Gia_Man_t * Gia_ManInsertMfs( Gia_Man_t * p, Sfm_Ntk_t * pNtk, int fAllBoxes ) Vec_IntFree( vMfs2Gia ); Vec_IntFree( vMfs2Old ); Vec_IntFree( vBoxesLeft ); + Vec_IntFree( vBoxKeep ); + Vec_IntFree( vCoDrivers ); return pNew; } @@ -550,4 +569,3 @@ Gia_Man_t * Gia_ManPerformMfs( Gia_Man_t * p, Sfm_Par_t * pPars ) //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_IMPL_END - From ee899284b854bbd37acc9ddbe1dc598c9a2cf151 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 24 Nov 2025 19:37:26 -0800 Subject: [PATCH 3/9] Updating printing APIs. --- src/aig/gia/giaMulFind.c | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/aig/gia/giaMulFind.c b/src/aig/gia/giaMulFind.c index 5e7d8d7b2..9a6df208c 100644 --- a/src/aig/gia/giaMulFind.c +++ b/src/aig/gia/giaMulFind.c @@ -839,15 +839,15 @@ void Gia_ManMulFindPrintSet( Vec_Int_t * vSet, int fLit, int fSkipLast ) } printf( "}" ); } -void Gia_ManMulFindPrintOne( Vec_Wec_t * vTerms, int m, int fBooth ) +void Gia_ManMulFindPrintOne( Vec_Wec_t * vTerms, int m, int fBooth, int fInputLits ) { Vec_Int_t * vIn0 = Vec_WecEntry(vTerms, 3*m+0); Vec_Int_t * vIn1 = Vec_WecEntry(vTerms, 3*m+1); Vec_Int_t * vOut = Vec_WecEntry(vTerms, 3*m+2); printf( "%sooth %ssigned %d x %d: ", fBooth ? "B" : "Non-b", Vec_IntEntryLast(vOut) ? "" : "un", Vec_IntSize(vIn0), Vec_IntSize(vIn1) ); - Gia_ManMulFindPrintSet( vIn0, 0, 0 ); + Gia_ManMulFindPrintSet( vIn0, fInputLits, 0 ); printf( " * " ); - Gia_ManMulFindPrintSet( vIn1, 0, 0 ); + Gia_ManMulFindPrintSet( vIn1, fInputLits, 0 ); printf( " = " ); Gia_ManMulFindPrintSet( vOut, 1, 1 ); printf( "\n" ); @@ -862,9 +862,9 @@ void Gia_ManMulFind( Gia_Man_t * p, int nCutNum, int fVerbose ) Vec_Wec_t * vTermsA = Gia_ManMulFindA( p, vCuts3, fVerbose ); printf( "Detected %d booth and %d non-booth multipliers.\n", Vec_WecSize(vTermsB)/3, Vec_WecSize(vTermsA)/3 ); for ( m = 0; m < Vec_WecSize(vTermsA)/3; m++ ) - Gia_ManMulFindPrintOne( vTermsA, m, 0 ); + Gia_ManMulFindPrintOne( vTermsA, m, 0, 0 ); for ( m = 0; m < Vec_WecSize(vTermsB)/3; m++ ) - Gia_ManMulFindPrintOne( vTermsB, m, 1 ); + Gia_ManMulFindPrintOne( vTermsB, m, 1, 0 ); Vec_WecFree( vTermsB ); Vec_WecFree( vTermsA ); Vec_WecFree( vCuts3 ); From 7691e2ed3cf3d7fc5ed99a1d8f9c092680f02a75 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 26 Nov 2025 17:57:16 -0800 Subject: [PATCH 4/9] Fixing a bug in &mfs when black boxes are present. --- src/aig/gia/giaMfs.c | 60 ++++++++++++++++++++++++++++++++++------ src/opt/sfm/sfm.h | 3 +- src/opt/sfm/sfmWin.c | 66 +++++++++++++++++++++++++++----------------- 3 files changed, 92 insertions(+), 37 deletions(-) diff --git a/src/aig/gia/giaMfs.c b/src/aig/gia/giaMfs.c index fe50e7b5e..c21c05cf5 100644 --- a/src/aig/gia/giaMfs.c +++ b/src/aig/gia/giaMfs.c @@ -300,6 +300,9 @@ Gia_Man_t * Gia_ManInsertMfs( Gia_Man_t * p, Sfm_Ntk_t * pNtk, int fAllBoxes ) Vec_Int_t * vArray, * vLeaves; Vec_Int_t * vMapping, * vMapping2; Vec_Int_t * vCoDrivers; + Vec_Int_t * vPiBoxes = NULL; + Vec_Int_t * vBbCiMap = NULL; + Vec_Int_t * vBbOutLit = NULL; int nBbIns = 0, nBbOuts = 0; if ( pManTime ) Tim_ManBlackBoxIoNum( pManTime, &nBbIns, &nBbOuts ); nMfsNodes = 1 + Gia_ManCiNum(p) + Gia_ManLutNum(p) + Gia_ManCoNum(p) + nBbIns + nBbOuts; @@ -341,8 +344,36 @@ Gia_Man_t * Gia_ManInsertMfs( Gia_Man_t * p, Sfm_Ntk_t * pNtk, int fAllBoxes ) assert( curCo == Gia_ManCoNum(p) ); // collect nodes in the given order + if ( nBbOuts > 0 ) + { + int iBbOut = 0; + vPiBoxes = Vec_IntStartFull( nBbOuts + nRealPis ); + vBbCiMap = Vec_IntStartFull( Gia_ManCiNum(p) ); + vBbOutLit = Vec_IntStartFull( nBbOuts ); + curCi = nRealPis; + curCo = 0; + for ( i = 0; i < nBoxes; i++ ) + { + nBoxIns = Tim_ManBoxInputNum( pManTime, i ); + nBoxOuts = Tim_ManBoxOutputNum( pManTime, i ); + if ( Tim_ManBoxIsBlack(pManTime, i) ) + for ( k = 0; k < nBoxOuts; k++ ) + { + assert( iBbOut < nBbOuts ); + Vec_IntWriteEntry( vPiBoxes, iBbOut, i ); + Vec_IntWriteEntry( vBbCiMap, curCi + k, iBbOut ); + iBbOut++; + } + curCo += nBoxIns; + curCi += nBoxOuts; + } + curCo += nRealPos; + assert( curCi == Gia_ManCiNum(p) ); + assert( curCo == Gia_ManCoNum(p) ); + assert( iBbOut == nBbOuts ); + } vBoxesLeft = Vec_IntAlloc( nBoxes ); - vMfsTopo = Sfm_NtkDfs( pNtk, vGroups, vGroupMap, vBoxesLeft, fAllBoxes ); + vMfsTopo = Sfm_NtkDfs( pNtk, vGroups, vGroupMap, vBoxesLeft, fAllBoxes, vPiBoxes ); Vec_IntUniqify( vBoxesLeft ); // reduce to sorted unique indices expected by the timing manager vBoxKeep = Vec_IntStart( nBoxes ); Vec_IntForEachEntry( vBoxesLeft, iBox, i ) @@ -370,12 +401,18 @@ Gia_Man_t * Gia_ManInsertMfs( Gia_Man_t * p, Sfm_Ntk_t * pNtk, int fAllBoxes ) { int iCiId = Gia_ObjId( p, pObj ); int iBox = pManTime ? Tim_ManBoxForCi( pManTime, Gia_ObjCioId(pObj) ) : -1; + int iBbOut = vBbCiMap ? Vec_IntEntry(vBbCiMap, i) : -1; if ( iBox >= 0 && !Vec_IntEntry(vBoxKeep, iBox) ) { Vec_IntWriteEntry( vMfs2Gia, Gia_ObjCopyArray(p, iCiId), -1 ); + if ( iBbOut >= 0 && vBbOutLit ) + Vec_IntWriteEntry( vBbOutLit, iBbOut, -1 ); continue; } - Vec_IntWriteEntry( vMfs2Gia, Gia_ObjCopyArray(p, iCiId), Gia_ManAppendCi(pNew) ); + iLitNew = Gia_ManAppendCi(pNew); + Vec_IntWriteEntry( vMfs2Gia, Gia_ObjCopyArray(p, iCiId), iLitNew ); + if ( iBbOut >= 0 && vBbOutLit ) + Vec_IntWriteEntry( vBbOutLit, iBbOut, iLitNew ); } // map internal nodes vLeaves = Vec_IntAlloc( 6 ); @@ -389,18 +426,20 @@ Gia_Man_t * Gia_ManInsertMfs( Gia_Man_t * p, Sfm_Ntk_t * pNtk, int fAllBoxes ) if ( Vec_IntSize(vArray) == 1 && Vec_IntEntry(vArray,0) < nBbOuts ) // skip unreal inputs { assert( Abc_LitIsCompl(iGroup) ); - iLitNew = Vec_IntEntry( vMfs2Gia, iMfsId ); - if ( iLitNew == -1 ) - { - iLitNew = Gia_ManAppendCi( pNew ); - Vec_IntWriteEntry( vMfs2Gia, iMfsId, iLitNew ); - } + assert( vBbOutLit != NULL ); + iLitNew = Vec_IntEntry( vBbOutLit, Vec_IntEntry(vArray,0) ); + assert( iLitNew >= 0 ); + Vec_IntWriteEntry( vMfs2Gia, iMfsId, iLitNew ); continue; } Vec_IntClear( vLeaves ); Vec_IntForEachEntry( vArray, Fanin, k ) { - iLitNew = Vec_IntEntry( vMfs2Gia, Fanin ); assert( iLitNew >= 0 ); + if ( Fanin < nBbOuts ) + iLitNew = Vec_IntEntry( vBbOutLit, Fanin ); + else + iLitNew = Vec_IntEntry( vMfs2Gia, Fanin ); + assert( iLitNew >= 0 ); Vec_IntPush( vLeaves, iLitNew ); } if ( iGroup == -1 ) // internal node @@ -502,6 +541,9 @@ Gia_Man_t * Gia_ManInsertMfs( Gia_Man_t * p, Sfm_Ntk_t * pNtk, int fAllBoxes ) Vec_IntFree( vBoxesLeft ); Vec_IntFree( vBoxKeep ); Vec_IntFree( vCoDrivers ); + Vec_IntFreeP( &vPiBoxes ); + Vec_IntFreeP( &vBbCiMap ); + Vec_IntFreeP( &vBbOutLit ); return pNew; } diff --git a/src/opt/sfm/sfm.h b/src/opt/sfm/sfm.h index f9c95c83e..24a798e5b 100644 --- a/src/opt/sfm/sfm.h +++ b/src/opt/sfm/sfm.h @@ -95,7 +95,7 @@ extern word * Sfm_NodeReadTruth( Sfm_Ntk_t * p, int i ); extern int Sfm_NodeReadFixed( Sfm_Ntk_t * p, int i ); extern int Sfm_NodeReadUsed( Sfm_Ntk_t * p, int i ); /*=== sfmWin.c ==========================================================*/ -extern Vec_Int_t * Sfm_NtkDfs( Sfm_Ntk_t * p, Vec_Wec_t * vGroups, Vec_Int_t * vGroupMap, Vec_Int_t * vBoxesLeft, int fAllBoxes ); +extern Vec_Int_t * Sfm_NtkDfs( Sfm_Ntk_t * p, Vec_Wec_t * vGroups, Vec_Int_t * vGroupMap, Vec_Int_t * vBoxesLeft, int fAllBoxes, Vec_Int_t * vPiBoxes ); ABC_NAMESPACE_HEADER_END @@ -105,4 +105,3 @@ ABC_NAMESPACE_HEADER_END //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// - diff --git a/src/opt/sfm/sfmWin.c b/src/opt/sfm/sfmWin.c index 53f9a71ef..5bb71d3f8 100644 --- a/src/opt/sfm/sfmWin.c +++ b/src/opt/sfm/sfmWin.c @@ -133,37 +133,52 @@ static inline int Sfm_ObjIsTravIdCurrent2( Sfm_Ntk_t * p, int Id ) { return SeeAlso [] ***********************************************************************/ -void Sfm_NtkDfs_rec( Sfm_Ntk_t * p, int iNode, Vec_Int_t * vNodes, Vec_Wec_t * vGroups, Vec_Int_t * vGroupMap, Vec_Int_t * vBoxesLeft ) +static void Sfm_NtkDfs_rec( Sfm_Ntk_t * p, int iNode, Vec_Int_t * vNodes, Vec_Wec_t * vGroups, Vec_Int_t * vGroupMap, Vec_Int_t * vBoxesLeft, Vec_Int_t * vPiBoxes ); +static void Sfm_NtkDfsVisitGroup( Sfm_Ntk_t * p, int iGroup, Vec_Int_t * vNodes, Vec_Wec_t * vGroups, Vec_Int_t * vGroupMap, Vec_Int_t * vBoxesLeft, Vec_Int_t * vPiBoxes ) { - int i, iFanin; - if ( Sfm_ObjIsPi(p, iNode) ) - return; + int i, iFanin, k, Obj; + Vec_Int_t * vGroup = Vec_WecEntry( vGroups, iGroup ); + Vec_IntForEachEntry( vGroup, Obj, i ) + assert( Sfm_ObjIsNode(p, Obj) ); + Vec_IntForEachEntry( vGroup, Obj, i ) + Sfm_ObjSetTravIdCurrent( p, Obj ); + Vec_IntForEachEntry( vGroup, Obj, i ) + Sfm_ObjForEachFanin( p, Obj, iFanin, k ) + Sfm_NtkDfs_rec( p, iFanin, vNodes, vGroups, vGroupMap, vBoxesLeft, vPiBoxes ); + Vec_IntForEachEntry( vGroup, Obj, i ) + Vec_IntPush( vNodes, Obj ); + Vec_IntPush( vBoxesLeft, iGroup ); +} +static void Sfm_NtkDfs_rec( Sfm_Ntk_t * p, int iNode, Vec_Int_t * vNodes, Vec_Wec_t * vGroups, Vec_Int_t * vGroupMap, Vec_Int_t * vBoxesLeft, Vec_Int_t * vPiBoxes ) +{ + int i, iFanin, iGroup; if ( Sfm_ObjIsTravIdCurrent(p, iNode) ) return; - if ( Vec_IntEntry(vGroupMap, iNode) >= 0 ) + iGroup = Vec_IntEntry(vGroupMap, iNode); + if ( iGroup >= 0 ) { - int k, iGroup = Abc_Lit2Var( Vec_IntEntry(vGroupMap, iNode) ); - Vec_Int_t * vGroup = Vec_WecEntry( vGroups, iGroup ); - Vec_IntForEachEntry( vGroup, iNode, i ) - assert( Sfm_ObjIsNode(p, iNode) ); - Vec_IntForEachEntry( vGroup, iNode, i ) - Sfm_ObjSetTravIdCurrent( p, iNode ); - Vec_IntForEachEntry( vGroup, iNode, i ) - Sfm_ObjForEachFanin( p, iNode, iFanin, k ) - Sfm_NtkDfs_rec( p, iFanin, vNodes, vGroups, vGroupMap, vBoxesLeft ); - Vec_IntForEachEntry( vGroup, iNode, i ) - Vec_IntPush( vNodes, iNode ); - Vec_IntPush( vBoxesLeft, iGroup ); + Sfm_NtkDfsVisitGroup( p, Abc_Lit2Var(iGroup), vNodes, vGroups, vGroupMap, vBoxesLeft, vPiBoxes ); + return; } - else + if ( Sfm_ObjIsPi(p, iNode) ) { - Sfm_ObjSetTravIdCurrent(p, iNode); - Sfm_ObjForEachFanin( p, iNode, iFanin, i ) - Sfm_NtkDfs_rec( p, iFanin, vNodes, vGroups, vGroupMap, vBoxesLeft ); - Vec_IntPush( vNodes, iNode ); + if ( vPiBoxes && iNode < Vec_IntSize(vPiBoxes) ) + { + int iBox = Vec_IntEntry( vPiBoxes, iNode ); + if ( iBox >= 0 ) + { + Sfm_ObjSetTravIdCurrent( p, iNode ); + Sfm_NtkDfsVisitGroup( p, iBox, vNodes, vGroups, vGroupMap, vBoxesLeft, vPiBoxes ); + } + } + return; } + Sfm_ObjSetTravIdCurrent(p, iNode); + Sfm_ObjForEachFanin( p, iNode, iFanin, i ) + Sfm_NtkDfs_rec( p, iFanin, vNodes, vGroups, vGroupMap, vBoxesLeft, vPiBoxes ); + Vec_IntPush( vNodes, iNode ); } -Vec_Int_t * Sfm_NtkDfs( Sfm_Ntk_t * p, Vec_Wec_t * vGroups, Vec_Int_t * vGroupMap, Vec_Int_t * vBoxesLeft, int fAllBoxes ) +Vec_Int_t * Sfm_NtkDfs( Sfm_Ntk_t * p, Vec_Wec_t * vGroups, Vec_Int_t * vGroupMap, Vec_Int_t * vBoxesLeft, int fAllBoxes, Vec_Int_t * vPiBoxes ) { Vec_Int_t * vNodes; int i; @@ -174,10 +189,10 @@ Vec_Int_t * Sfm_NtkDfs( Sfm_Ntk_t * p, Vec_Wec_t * vGroups, Vec_Int_t * vGroupMa { Vec_Int_t * vGroup; Vec_WecForEachLevel( vGroups, vGroup, i ) - Sfm_NtkDfs_rec( p, Vec_IntEntry(vGroup, 0), vNodes, vGroups, vGroupMap, vBoxesLeft ); + Sfm_NtkDfs_rec( p, Vec_IntEntry(vGroup, 0), vNodes, vGroups, vGroupMap, vBoxesLeft, vPiBoxes ); } Sfm_NtkForEachPo( p, i ) - Sfm_NtkDfs_rec( p, Sfm_ObjFanin(p, i, 0), vNodes, vGroups, vGroupMap, vBoxesLeft ); + Sfm_NtkDfs_rec( p, Sfm_ObjFanin(p, i, 0), vNodes, vGroups, vGroupMap, vBoxesLeft, vPiBoxes ); return vNodes; } @@ -478,4 +493,3 @@ void Sfm_NtkWindowTest( Sfm_Ntk_t * p, int iNode ) ABC_NAMESPACE_IMPL_END - From b9074a754ba7860b852049eb82d857de88945848 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 26 Nov 2025 17:58:28 -0800 Subject: [PATCH 5/9] Adding verbose mode to &permute. --- src/aig/gia/giaDup.c | 20 ++++++++++++++------ src/base/abci/abc.c | 4 ++-- 2 files changed, 16 insertions(+), 8 deletions(-) diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index ea58ba8b2..c88ec06e7 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -1103,23 +1103,31 @@ Vec_Int_t * Gia_ManCreatePerm( int n ) } return vPerm; } -Gia_Man_t * Gia_ManDupRandPerm( Gia_Man_t * p ) +Gia_Man_t * Gia_ManDupRandPerm( Gia_Man_t * p, int fVerbose ) { Vec_Int_t * vPiPerm = Gia_ManCreatePerm( Gia_ManCiNum(p) ); Vec_Int_t * vPoPerm = Gia_ManCreatePerm( Gia_ManCoNum(p) ); Gia_Man_t * pNew; Gia_Obj_t * pObj; - int i; + int i, fCompl = 0; pNew = Gia_ManStart( Gia_ManObjNum(p) ); pNew->pName = Abc_UtilStrsav( p->pName ); pNew->pSpec = Abc_UtilStrsav( p->pSpec ); Gia_ManConst0(p)->Value = 0; - Gia_ManForEachPi( p, pObj, i ) - Gia_ManPi(p, Vec_IntEntry(vPiPerm,i))->Value = Gia_ManAppendCi(pNew) ^ (Abc_Random(0) & 1); + if ( fVerbose ) printf( "Input NP transform: " ); + Gia_ManForEachPi( p, pObj, i ) { + Gia_ManPi(p, Vec_IntEntry(vPiPerm,i))->Value = Gia_ManAppendCi(pNew) ^ (fCompl = (Abc_Random(0) & 1)); + if ( fVerbose ) printf( "%s%d ", fCompl ? "~":"", Vec_IntEntry(vPiPerm,i) ); + } + if ( fVerbose ) printf( "\n" ); Gia_ManForEachAnd( p, pObj, i ) pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); - Gia_ManForEachPo( p, pObj, i ) - Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ManPo(p, Vec_IntEntry(vPoPerm,i))) ^ (Abc_Random(0) & 1) ); + if ( fVerbose ) printf( "Output NP transform: " ); + Gia_ManForEachPo( p, pObj, i ) { + Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ManPo(p, Vec_IntEntry(vPoPerm,i))) ^ (fCompl = (Abc_Random(0) & 1)) ); + if ( fVerbose ) printf( "%s%d ", fCompl ? "~":"", Vec_IntEntry(vPoPerm,i) ); + } + if ( fVerbose ) printf( "\n" ); Vec_IntFree( vPiPerm ); Vec_IntFree( vPoPerm ); return pNew; diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 75130bedd..9ce0dc107 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -48156,7 +48156,7 @@ usage: ***********************************************************************/ int Abc_CommandAbc9Permute( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern Gia_Man_t * Gia_ManDupRandPerm( Gia_Man_t * p ); + extern Gia_Man_t * Gia_ManDupRandPerm( Gia_Man_t * p, int fVerbose ); Gia_Man_t * pTemp; int c, RandSeed = 0, fVerbose = 0; Extra_UtilGetoptReset(); @@ -48197,7 +48197,7 @@ int Abc_CommandAbc9Permute( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Random(1); for ( c = 0; c < RandSeed; c++ ) Abc_Random(0); - pTemp = Gia_ManDupRandPerm( pAbc->pGia ); + pTemp = Gia_ManDupRandPerm( pAbc->pGia, fVerbose ); Abc_FrameUpdateGia( pAbc, pTemp ); return 0; From 9b0786fe89795b026c1414677089ecc057624fcd Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 27 Nov 2025 19:46:16 -0800 Subject: [PATCH 6/9] Experiments with multipliers. --- src/aig/gia/gia.h | 2 + src/aig/gia/giaCut.c | 6 +- src/aig/gia/giaDup.c | 58 ++++++++++ src/aig/gia/giaMulFind.c | 51 ++++++-- src/misc/util/module.make | 1 + src/misc/util/utilMulSim.c | 230 +++++++++++++++++++++++++++++++++++++ src/misc/vec/vecInt.h | 6 +- 7 files changed, 338 insertions(+), 16 deletions(-) create mode 100644 src/misc/util/utilMulSim.c diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 0799a0c96..efc85813b 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -1419,6 +1419,8 @@ typedef struct Gia_ChMan_t_ Gia_ChMan_t; extern Gia_ChMan_t * Gia_ManDupChoicesStart( Gia_Man_t * pGia ); extern void Gia_ManDupChoicesAdd( Gia_ChMan_t * pMan, Gia_Man_t * pGia ); extern Gia_Man_t * Gia_ManDupChoicesFinish( Gia_ChMan_t * pMan ); +extern Vec_Int_t * Gia_ManComputeMffc( Gia_Man_t * p, Vec_Int_t * vLits, Vec_Int_t * vOuts ); +extern Gia_Man_t * Gia_ManDupExtractMffc( Gia_Man_t * p, Vec_Int_t * vLits, Vec_Int_t * vAnds, Vec_Int_t * vCos ); /*=== giaEdge.c ==========================================================*/ extern void Gia_ManEdgeFromArray( Gia_Man_t * p, Vec_Int_t * vArray ); extern Vec_Int_t * Gia_ManEdgeToArray( Gia_Man_t * p ); diff --git a/src/aig/gia/giaCut.c b/src/aig/gia/giaCut.c index 35e3c34ee..5efc358ff 100644 --- a/src/aig/gia/giaCut.c +++ b/src/aig/gia/giaCut.c @@ -292,8 +292,8 @@ static inline int Gia_CutCompare2( Gia_Cut_t * pCut0, Gia_Cut_t * pCut1 ) } static inline int Gia_CutCompare( Gia_Cut_t * pCut0, Gia_Cut_t * pCut1 ) { - if ( pCut0->CostF > pCut1->CostF ) return -1; - if ( pCut0->CostF < pCut1->CostF ) return 1; + if ( pCut0->CostF > pCut1->CostF ) return -1; + if ( pCut0->CostF < pCut1->CostF ) return 1; if ( pCut0->nLeaves < pCut1->nLeaves ) return -1; if ( pCut0->nLeaves > pCut1->nLeaves ) return 1; return 0; @@ -1230,7 +1230,7 @@ void Gia_ManComputeCutsCore( Gia_Man_t * pGia, int nCutSize, int nCutNum, int fT Vec_Wec_t * Gia_ManCompute54Cuts( Gia_Man_t * pGia, int fVerbose ) { - Gia_Sto_t * pSto = Gia_ManMatchCutsInt( pGia, 5, 16, 0, fVerbose ); + Gia_Sto_t * pSto = Gia_ManMatchCutsInt( pGia, 5, 8, 0, fVerbose ); Vec_Wec_t * vRes = Vec_WecAlloc( 1000 ); Vec_Int_t * vLevel; int i, k, c, * pCut; Vec_WecForEachLevel( pSto->vCuts, vLevel, i ) if ( Vec_IntSize(vLevel) ) { diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index c88ec06e7..2b4a0199f 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -6609,6 +6609,64 @@ Gia_Man_t * Gia_ManDupChoicesFinish( Gia_ChMan_t * p ) return pTemp; } +/**Function************************************************************* + + Synopsis [Extracting MFFC of the nodes supported by a set of literals.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + +// collecting internal nodes and outputs in the MFF of a given set of literals +Vec_Int_t * Gia_ManComputeMffc( Gia_Man_t * p, Vec_Int_t * vLits, Vec_Int_t * vOuts ) +{ + Vec_Int_t * vTfo = Vec_IntAlloc( 100 ); + Gia_Obj_t * pObj; int i, Lit; + Vec_IntClear( vOuts ); + Gia_ManIncrementTravId( p ); + Vec_IntForEachEntry( vLits, Lit, i ) + Gia_ObjSetTravIdCurrentId( p, Abc_Lit2Var(Lit) ); + Gia_ManForEachAnd( p, pObj, i ) { + if ( Gia_ObjIsTravIdCurrentId(p, i) ) + continue; + if ( Gia_ObjIsTravIdCurrentId(p, Gia_ObjFaninId0(pObj, i)) && Gia_ObjIsTravIdCurrentId(p, Gia_ObjFaninId1(pObj, i)) ) + Gia_ObjSetTravIdCurrentId( p, i ), Vec_IntPush( vTfo, i ); + else if ( Gia_ObjIsTravIdCurrentId(p, Gia_ObjFaninId0(pObj, i)) ) + Vec_IntPushUniqueOrder( vOuts, Gia_ObjFaninId0(pObj, i) ); + else if ( Gia_ObjIsTravIdCurrentId(p, Gia_ObjFaninId1(pObj, i)) ) + Vec_IntPushUniqueOrder( vOuts, Gia_ObjFaninId1(pObj, i) ); + } + Gia_ManForEachCo( p, pObj, i ) + if ( Gia_ObjIsTravIdCurrentId(p, Gia_ObjFaninId0p(p, pObj)) ) + Vec_IntPushUniqueOrder( vOuts, Gia_ObjFaninId0p(p, pObj) ); + Vec_IntTwoFilter( vOuts, vTfo ); + return vTfo; +} + +// extracting the AIG of the MFFC defined by a given set of literals +Gia_Man_t * Gia_ManDupExtractMffc( Gia_Man_t * p, Vec_Int_t * vLits, Vec_Int_t * vAnds, Vec_Int_t * vCos ) +{ + Gia_Man_t * pNew; + Gia_Obj_t * pObj; + int i, Lit; + pNew = Gia_ManStart( 5000 ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + pNew->fGiaSimple = 1; + Gia_ManConst0(p)->Value = 0; + Vec_IntForEachEntry( vLits, Lit, i ) + Gia_ManObj(p, Abc_Lit2Var(Lit))->Value = Abc_LitNotCond( Gia_ManAppendCi(pNew), Abc_LitIsCompl(Lit) ); + Gia_ManForEachObjVec( vAnds, p, pObj, i ) + pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManForEachObjVec( vCos, p, pObj, i ) + pObj->Value = Gia_ManAppendCo( pNew, pObj->Value ); + return pNew; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/giaMulFind.c b/src/aig/gia/giaMulFind.c index 9a6df208c..3dd454194 100644 --- a/src/aig/gia/giaMulFind.c +++ b/src/aig/gia/giaMulFind.c @@ -726,8 +726,16 @@ Vec_Wrd_t * Gia_ManMulFindSim( Vec_Wrd_t * vSim0, Vec_Wrd_t * vSim1, int fSigned } return vRes; } -void Gia_ManMulFindOutputs( Gia_Man_t * p, Vec_Wec_t * vTerms, int fLits, int fVerbose ) +Vec_Wrd_t * Gia_ManMulFindSim2( Vec_Wrd_t * vSim0, Vec_Wrd_t * vSim1, int fSigned ) { + extern word * product_many(word *pInfo1, int nBits1, word *pInfo2, int nBits2, int fSigned ); + word * pRes = product_many( Vec_WrdArray(vSim0), Vec_WrdSize(vSim0), Vec_WrdArray(vSim1), Vec_WrdSize(vSim1), fSigned ); + return Vec_WrdAllocArray( pRes, Vec_WrdSize(vSim0) + Vec_WrdSize(vSim1) ); +} +int Gia_ManMulFindOutputs( Gia_Man_t * p, Vec_Wec_t * vTerms, int fLits, int fVerbose ) +{ + //abctime clkTotal = Abc_Clock(); + int nDetected = 0; Abc_Random(1); for ( int m = 0; m < Vec_WecSize(vTerms)/3; m++ ) { Vec_Int_t * vIn0 = Vec_WecEntry(vTerms, 3*m+0); @@ -735,8 +743,8 @@ void Gia_ManMulFindOutputs( Gia_Man_t * p, Vec_Wec_t * vTerms, int fLits, int fV Vec_Int_t * vOut = Vec_WecEntry(vTerms, 3*m+2); Vec_Wrd_t * vSim0 = Vec_WrdStartRandom( Vec_IntSize(vIn0) ); Vec_Wrd_t * vSim1 = Vec_WrdStartRandom( Vec_IntSize(vIn1) ); - Vec_Wrd_t * vSimU = Gia_ManMulFindSim( vSim0, vSim1, 0 ); - Vec_Wrd_t * vSimS = Gia_ManMulFindSim( vSim0, vSim1, 1 ); + Vec_Wrd_t * vSimU = Gia_ManMulFindSim2( vSim0, vSim1, 0 ); + Vec_Wrd_t * vSimS = Gia_ManMulFindSim2( vSim0, vSim1, 1 ); Vec_Int_t * vTfo = Gia_ManMulFindTfo( p, vIn0, vIn1, fLits ); Vec_Wrd_t * vSims = Gia_ManMulFindSimCone( p, vIn0, vIn1, vSim0, vSim1, vTfo, fLits ); Vec_Int_t * vOutU = Vec_IntAlloc( 100 ); @@ -762,10 +770,14 @@ void Gia_ManMulFindOutputs( Gia_Man_t * p, Vec_Wec_t * vTerms, int fLits, int fV if ( Vec_IntCountEntry(vOutU, -1) < Vec_IntSize(vOutU) || Vec_IntCountEntry(vOutS, -1) < Vec_IntSize(vOutS) ) { - if ( Vec_IntCountEntry(vOutU, -1) < Vec_IntCountEntry(vOutS, -1) ) + if ( Vec_IntCountEntry(vOutU, -1) < Vec_IntCountEntry(vOutS, -1) ) { Vec_IntAppend( vOut, vOutU ), Vec_IntPush(vOut, 0); - else + nDetected = Vec_IntSize(vOutU) - Vec_IntCountEntry(vOutU, -1); + } + else { Vec_IntAppend( vOut, vOutS ), Vec_IntPush(vOut, 1); + nDetected = Vec_IntSize(vOutS) - Vec_IntCountEntry(vOutS, -1); + } } else { @@ -782,6 +794,8 @@ void Gia_ManMulFindOutputs( Gia_Man_t * p, Vec_Wec_t * vTerms, int fLits, int fV Vec_IntFree( vOutS ); } Vec_WecRemoveEmpty( vTerms ); + //Abc_PrintTime( 1, "Output detection time", Abc_Clock() - clkTotal ); + return nDetected; } /**Function************************************************************* @@ -831,11 +845,28 @@ void Gia_ManMulFindPrintSet( Vec_Int_t * vSet, int fLit, int fSkipLast ) { int i, Temp, Limit = Vec_IntSize(vSet) - fSkipLast; printf( "{" ); - Vec_IntForEachEntryStop( vSet, Temp, i, Limit ) { - if ( Temp == -1 ) - printf( "n/a%s", i < Limit-1 ? " ":"" ); - else - printf( "%s%d%s", (fLit & Abc_LitIsCompl(Temp)) ? "~":"", fLit ? Abc_Lit2Var(Temp) : Temp, i < Limit-1 ? " ":"" ); + if ( Vec_IntSize(vSet) > 16 ) { + Vec_IntForEachEntryStop( vSet, Temp, i, 4 ) { + if ( Temp == -1 ) + printf( "n/a%s", i < Limit-1 ? " ":"" ); + else + printf( "%s%d%s", (fLit & Abc_LitIsCompl(Temp)) ? "~":"", fLit ? Abc_Lit2Var(Temp) : Temp, i < Limit-1 ? " ":"" ); + } + printf( "... " ); + Vec_IntForEachEntryStartStop( vSet, Temp, i, Limit-4, Limit ) { + if ( Temp == -1 ) + printf( "n/a%s", i < Limit-1 ? " ":"" ); + else + printf( "%s%d%s", (fLit & Abc_LitIsCompl(Temp)) ? "~":"", fLit ? Abc_Lit2Var(Temp) : Temp, i < Limit-1 ? " ":"" ); + } + } + else { + Vec_IntForEachEntryStop( vSet, Temp, i, Limit ) { + if ( Temp == -1 ) + printf( "n/a%s", i < Limit-1 ? " ":"" ); + else + printf( "%s%d%s", (fLit & Abc_LitIsCompl(Temp)) ? "~":"", fLit ? Abc_Lit2Var(Temp) : Temp, i < Limit-1 ? " ":"" ); + } } printf( "}" ); } diff --git a/src/misc/util/module.make b/src/misc/util/module.make index 991f6f311..205e2a734 100644 --- a/src/misc/util/module.make +++ b/src/misc/util/module.make @@ -7,6 +7,7 @@ SRC += src/misc/util/utilBridge.c \ src/misc/util/utilIsop.c \ src/misc/util/utilLinear.c \ src/misc/util/utilMiniver.c \ + src/misc/util/utilMulSim.c \ src/misc/util/utilNam.c \ src/misc/util/utilPrefix.cpp \ src/misc/util/utilPth.c \ diff --git a/src/misc/util/utilMulSim.c b/src/misc/util/utilMulSim.c new file mode 100644 index 000000000..d5542e519 --- /dev/null +++ b/src/misc/util/utilMulSim.c @@ -0,0 +1,230 @@ +/**CFile**************************************************************** + + FileName [utilMulSim.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Generating multiplier simulation info.] + + Synopsis [Generating multiplier simulation info.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - Feburary 13, 2011.] + + Revision [$Id: utilMulSim.c,v 1.00 2011/02/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include +#include +#include +#include +#include +#include "misc/util/abc_global.h" + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +#define SIG_WIDTH 64 // 64 simulation patterns in each signature word + +// ---------------------------------------------------------------------- +// Core 32-bit-limb big integer unsigned multiply +// ---------------------------------------------------------------------- + +uint32_t * product(const uint32_t *pArg1, int nInts1, + const uint32_t *pArg2, int nInts2) +{ + assert( pArg1 && pArg2 && nInts1 > 0 && nInts2 > 0 ); + int nRes = nInts1 + nInts2; + uint32_t *pRes = (uint32_t *)calloc((size_t)nRes, sizeof(uint32_t)); + if (!pRes) return NULL; + // Schoolbook multiplication in base 2^32 + for (int i = 0; i < nInts1; ++i) { + uint64_t a = pArg1[i]; + if (a == 0) continue; + uint64_t carry = 0; + for (int j = 0; j < nInts2; ++j) { + uint64_t t = (uint64_t)pRes[i + j] + a * (uint64_t)pArg2[j] + carry; + pRes[i + j] = (uint32_t)t; + carry = t >> 32; + } + pRes[i + nInts2] = (uint32_t)carry; + } + return pRes; +} + +// ---------------------------------------------------------------------- +// Bit-matrix helpers: signatures <-> per-pattern 32-bit-limb big ints +// ---------------------------------------------------------------------- + +static void transpose_signatures_to_pattern(const uint64_t *sigs, + int nBits, + uint32_t *dst, + int nInts, + int patternIdx) +{ + memset(dst, 0, (size_t)nInts * sizeof(uint32_t)); + for (int bit = 0; bit < nBits; ++bit) { + uint64_t sigWord = sigs[bit]; + uint64_t bitVal = (sigWord >> patternIdx) & 1ULL; + if (!bitVal) continue; + int word = bit / 32; + int offset = bit & 31; + dst[word] |= (uint32_t)(1u << offset); + } +} + +static void transpose_pattern_to_signatures(const uint32_t *src, + int nIntsRes, + int nBitsRes, + uint64_t *outSigs, + int patternIdx) +{ + for (int bit = 0; bit < nBitsRes; ++bit) { + int word = bit / 32; + int offset = bit & 31; + if (word >= nIntsRes) + break; + uint32_t bitVal = (src[word] >> offset) & 1u; + if (bitVal) + outSigs[bit] |= (uint64_t)1ULL << patternIdx; + } +} + +// ---------------------------------------------------------------------- +// Signed helpers for 32-bit-limb big ints (two's complement on nBits) +// ---------------------------------------------------------------------- + +static int is_negative(const uint32_t *x, int nBits) +{ + int bitPos = nBits - 1; + int word = bitPos / 32; + int offset = bitPos & 31; + return (x[word] >> offset) & 1u; +} + +static void mask_to_nBits(uint32_t *x, int nInts, int nBits) +{ + if (nBits <= 0) { + for (int i = 0; i < nInts; ++i) + x[i] = 0; + return; + } + int lastWord = (nBits - 1) / 32; // index of last used word + int usedBitsInLast = nBits - lastWord * 32; // 1..32 + // Zero any words above the last used word + for (int i = lastWord + 1; i < nInts; ++i) + x[i] = 0; + // If nBits is not a multiple of 32, mask off the high bits of last word + if (usedBitsInLast < 32) { + uint32_t mask = ((uint32_t)1u << usedBitsInLast) - 1u; + x[lastWord] &= mask; + } +} + +static void twos_complement_inplace(uint32_t *x, int nInts, int nBits) +{ + // Invert + for (int i = 0; i < nInts; ++i) + x[i] = ~x[i]; + mask_to_nBits(x, nInts, nBits); + // Add 1 + uint64_t carry = 1; + for (int i = 0; i < nInts; ++i) { + uint64_t sum = (uint64_t)x[i] + carry; + x[i] = (uint32_t)sum; + carry = sum >> 32; + if (!carry) + break; + } + mask_to_nBits(x, nInts, nBits); +} + +// ---------------------------------------------------------------------- +// product_many: unsigned and signed (two's-complement) versions +// ---------------------------------------------------------------------- + +uint64_t * product_many_unsigned(uint64_t *pInfo1, int nBits1, + uint64_t *pInfo2, int nBits2) +{ + assert( pInfo1 && pInfo2 && nBits1 > 0 && nBits2 > 0 ); + int nInts1 = (nBits1 + 31) / 32; + int nInts2 = (nBits2 + 31) / 32; + int nBitsRes = nBits1 + nBits2; + int nIntsRes = nInts1 + nInts2; + uint64_t *outSigs = (uint64_t *)calloc((size_t)nBitsRes, sizeof(uint64_t)); + if (!outSigs) return NULL; + uint32_t *tmp1 = (uint32_t *)calloc((size_t)nInts1, sizeof(uint32_t)); + uint32_t *tmp2 = (uint32_t *)calloc((size_t)nInts2, sizeof(uint32_t)); + assert( tmp1 && tmp2 ); + for (int pattern = 0; pattern < SIG_WIDTH; ++pattern) { + transpose_signatures_to_pattern(pInfo1, nBits1, tmp1, nInts1, pattern); + transpose_signatures_to_pattern(pInfo2, nBits2, tmp2, nInts2, pattern); + uint32_t *tmpRes = product(tmp1, nInts1, tmp2, nInts2); assert( tmpRes ); + transpose_pattern_to_signatures(tmpRes, nIntsRes, nBitsRes, outSigs, pattern); + free(tmpRes); + } + free(tmp1); + free(tmp2); + return outSigs; +} + +uint64_t * product_many_signed(uint64_t *pInfo1, int nBits1, + uint64_t *pInfo2, int nBits2) +{ + assert( pInfo1 && pInfo2 && nBits1 > 0 && nBits2 > 0 ); + int nInts1 = (nBits1 + 31) / 32; + int nInts2 = (nBits2 + 31) / 32; + int nBitsRes = nBits1 + nBits2; + int nIntsRes = nInts1 + nInts2; + uint64_t *outSigs = (uint64_t *)calloc((size_t)nBitsRes, sizeof(uint64_t)); + if (!outSigs) return NULL; + uint32_t *op1 = (uint32_t *)calloc((size_t)nInts1, sizeof(uint32_t)); + uint32_t *op2 = (uint32_t *)calloc((size_t)nInts2, sizeof(uint32_t)); + assert( op1 && op2 ); + for (int pattern = 0; pattern < SIG_WIDTH; ++pattern) { + transpose_signatures_to_pattern(pInfo1, nBits1, op1, nInts1, pattern); + transpose_signatures_to_pattern(pInfo2, nBits2, op2, nInts2, pattern); + int neg1 = is_negative(op1, nBits1); + int neg2 = is_negative(op2, nBits2); + int negRes = neg1 ^ neg2; + if (neg1) twos_complement_inplace(op1, nInts1, nBits1); + if (neg2) twos_complement_inplace(op2, nInts2, nBits2); + uint32_t *tmpRes = product(op1, nInts1, op2, nInts2); assert( tmpRes ); + if (negRes) + twos_complement_inplace(tmpRes, nIntsRes, nBitsRes); + else + mask_to_nBits(tmpRes, nIntsRes, nBitsRes); + transpose_pattern_to_signatures(tmpRes, nIntsRes, nBitsRes, outSigs, pattern); + free(tmpRes); + } + free(op1); + free(op2); + return outSigs; +} + +word * product_many(word *pInfo1, int nBits1, word *pInfo2, int nBits2, int fSigned ) +{ + if ( fSigned ) + return (word *)product_many_signed((uint64_t *)pInfo1, nBits1, (uint64_t *)pInfo2, nBits2); + else + return (word *)product_many_unsigned((uint64_t *)pInfo1, nBits1, (uint64_t *)pInfo2, nBits2); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h index a03cd30b8..e32a2dd18 100644 --- a/src/misc/vec/vecInt.h +++ b/src/misc/vec/vecInt.h @@ -1947,16 +1947,16 @@ static inline int Vec_IntTwoRemove( Vec_Int_t * vArr1, Vec_Int_t * vArr2 ) /**Function************************************************************* - Synopsis [Returns the result of merging the two vectors.] + Synopsis [Keeps only those entries in vArr1, which are in vArr2.] - Description [Keeps only those entries of vArr1, which are in vArr2.] + Description [Assumes that the vectors are sorted in the increasing order.] SideEffects [] SeeAlso [] ***********************************************************************/ -static inline void Vec_IntTwoMerge1( Vec_Int_t * vArr1, Vec_Int_t * vArr2 ) +static inline void Vec_IntTwoFilter( Vec_Int_t * vArr1, Vec_Int_t * vArr2 ) { int * pBeg = vArr1->pArray; int * pBeg1 = vArr1->pArray; From c4b2b5c180263a1840c7ddfcb99e0eba54ebf216 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 29 Nov 2025 17:30:23 -0800 Subject: [PATCH 7/9] Adding extension "y" for obj ID mapping. --- src/aig/gia/gia.h | 3 +- src/aig/gia/giaAiger.c | 30 ++++++++- src/aig/gia/giaMan.c | 3 +- src/aig/gia/giaTim.c | 134 +++++++++++++++++++++++++++++++++++++++-- src/base/abci/abc.c | 12 ++-- src/proof/cec/cec.h | 1 + src/proof/cec/cecCec.c | 3 + 7 files changed, 174 insertions(+), 12 deletions(-) diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index efc85813b..6e77e26c0 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -189,6 +189,7 @@ struct Gia_Man_t_ Vec_Int_t * vCoNumsOrig; // original CO names Vec_Int_t * vIdsOrig; // original object IDs Vec_Int_t * vIdsEquiv; // original object IDs proved equivalent + Vec_Int_t * vEquLitIds; // original object IDs proved equivalent Vec_Int_t * vCofVars; // cofactoring variables Vec_Vec_t * vClockDoms; // clock domains Vec_Flt_t * vTiming; // arrival/required/slack @@ -1729,7 +1730,7 @@ extern void * Gia_ManUpdateTimMan2( Gia_Man_t * p, Vec_Int_t * vBox extern Gia_Man_t * Gia_ManUpdateExtraAig( void * pTime, Gia_Man_t * pAig, Vec_Int_t * vBoxPres ); extern Gia_Man_t * Gia_ManUpdateExtraAig2( void * pTime, Gia_Man_t * pAig, Vec_Int_t * vBoxesLeft ); extern Gia_Man_t * Gia_ManDupCollapse( Gia_Man_t * p, Gia_Man_t * pBoxes, Vec_Int_t * vBoxPres, int fSeq ); -extern int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, int nBTLimit, int nTimeLim, int fSeq, int fDumpFiles, int fVerbose, char * pFileSpec ); +extern int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, int nBTLimit, int nTimeLim, int fSeq, int fNameMap, int fDumpFiles, int fVerbose, char * pFileSpec ); extern Vec_Int_t * Gia_ManDeriveBoxMapping( Gia_Man_t * pGia ); /*=== giaTruth.c ===========================================================*/ extern word Gia_LutComputeTruth6( Gia_Man_t * p, int iObj, Vec_Wrd_t * vTruths ); diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c index cd35586ea..85b48b118 100644 --- a/src/aig/gia/giaAiger.c +++ b/src/aig/gia/giaAiger.c @@ -907,6 +907,25 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fGiaSi printf( "Cannot read extension \"w\" because AIG is rehashed. Use \"&r -s \".\n" ); Vec_IntFree( vPairs ); } + // read object ID mapping + else if ( *pCur == 'y' ) + { + pCur++; + int nInts = Gia_AigerReadInt(pCur)/4; pCur += 4; + if ( fSkipStrash ) { + pNew->vEquLitIds = Vec_IntStart( nInts ); + memcpy( Vec_IntArray(pNew->vEquLitIds), pCur, (size_t)4*nInts ); + if ( Vec_IntSize(pNew->vEquLitIds) != Gia_ManObjNum(pNew) ) { + printf( "Cannot read extension \"y\" because object count changed. Use \"&r -s \".\n" ); + Vec_IntFreeP( &pNew->vEquLitIds ); + } + else if ( fVerbose ) printf( "Finished reading extension \"y\".\n" ); + } + else { + if ( fVerbose ) printf( "Cannot read extension \"y\" because AIG is rehashed. Use \"&r -s \".\n" ); + } + pCur += 4*nInts; + } else break; } } @@ -1529,6 +1548,7 @@ void Gia_AigerWriteS( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, in Gia_FileWriteBufferSize( pFile, Vec_IntSize(p->vRegClasses) ); for ( i = 0; i < Vec_IntSize(p->vRegClasses); i++ ) Gia_FileWriteBufferSize( pFile, Vec_IntEntry(p->vRegClasses, i) ); + if ( fVerbose ) printf( "Finished writing extension \"r\".\n" ); } // write register inits if ( p->vRegInits ) @@ -1677,6 +1697,15 @@ void Gia_AigerWriteS( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, in assert( Vec_IntSize(p->vObjClasses) == Gia_ManObjNum(p) ); fwrite( Vec_IntArray(p->vObjClasses), 1, 4*Gia_ManObjNum(p), pFile ); } + // write object classes + if ( p->vEquLitIds ) + { + fprintf( pFile, "y" ); + Gia_FileWriteBufferSize( pFile, 4*Gia_ManObjNum(p) ); + assert( Vec_IntSize(p->vEquLitIds) == Gia_ManObjNum(p) ); + fwrite( Vec_IntArray(p->vEquLitIds), 1, 4*Gia_ManObjNum(p), pFile ); + if ( fVerbose ) printf( "Finished writing extension \"y\".\n" ); + } // write name if ( p->pName ) { @@ -1916,4 +1945,3 @@ int main( int argc, char ** argv ) ABC_NAMESPACE_IMPL_END - diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c index 72ec211ef..84a41d1dd 100644 --- a/src/aig/gia/giaMan.c +++ b/src/aig/gia/giaMan.c @@ -106,6 +106,7 @@ void Gia_ManStop( Gia_Man_t * p ) Vec_IntFreeP( &p->vCofVars ); Vec_IntFreeP( &p->vIdsOrig ); Vec_IntFreeP( &p->vIdsEquiv ); + Vec_IntFreeP( &p->vEquLitIds ); Vec_IntFreeP( &p->vLutConfigs ); Vec_IntFreeP( &p->vEdgeDelay ); Vec_IntFreeP( &p->vEdgeDelayR ); @@ -641,7 +642,7 @@ void Gia_ManPrintStats( Gia_Man_t * p, Gps_Par_t * pPars ) } if ( pPars && pPars->fSlacks ) Gia_ManDfsSlacksPrint( p ); - if ( Gia_ManHasMapping(p) && pPars->fMapOutStats ) + if ( Gia_ManHasMapping(p) && pPars && pPars->fMapOutStats ) Gia_ManPrintOutputLutStats( p ); } diff --git a/src/aig/gia/giaTim.c b/src/aig/gia/giaTim.c index 17f03aa4a..271c6d4ee 100644 --- a/src/aig/gia/giaTim.c +++ b/src/aig/gia/giaTim.c @@ -952,7 +952,114 @@ Gia_Man_t * Gia_ManDupCollapse( Gia_Man_t * p, Gia_Man_t * pBoxes, Vec_Int_t * v SeeAlso [] ***********************************************************************/ -int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, int nBTLimit, int nTimeLim, int fSeq, int fDumpFiles, int fVerbose, char * pFileSpec ) + +/* +› Please have a look at how name mapping is done in procedure Abc_FrameReadMiniLutNameMapping() in file "src/aig/gia/ + giaMini.c". The main idea is to map the object IDs in the design after synthesis (pAbc->pGiaMiniLut) into the object IDs in + the design before synthesis (pAbc->pGiaMiniAig). The computation is divided into three steps: (1) computing object + equivalences using Gia_ManComputeGiaEquivs(), which annotates the input AIG (pGia) containing both designs before and after + synthesis with equivalence class information; this information contains equivalence classes of objects from both designs; (2) + creating a map (pRes) of the resulting object IDs (in pAbc->pGiaMiniLut) into the original object IDs (in pAbc->pGiaMiniAig) + using procedure Gia_ManMapMiniLut2MiniAig(); this map is enabled by having two arrays (one of them is pAbc->vCopyMiniAig + mapping objects of pAbc->pGiaMiniAig in the original object IDs; the other one is pAbc->vCopyMiniLut mapping objects of + pAbc->pGiaMiniLut into the IDs of pAbc->pGiaMiniLut); (3) verification procedure (commented out by default) + Gia_ManNameMapVerify() which checks that the resulting mapping computed by Gia_ManMapMiniLut2MiniAig() is correct. Please + let me know if this computation is clear. +*/ + +Vec_Int_t * Gia_ManVerifyFindNameMapping( Gia_Man_t * p, Gia_Man_t * p1, Gia_Man_t * p2, Vec_Int_t * vMap1, Vec_Int_t * vMap2 ) +{ + Vec_Int_t * vRes = Vec_IntStartFull(Vec_IntSize(vMap2)); + Vec_Int_t * vMap = Vec_IntStartFull( Gia_ManObjNum(p) ); + int i, Entry, iRepr, fCompl, iLit; + Gia_Obj_t * pObj; + Gia_ManSetPhase( p1 ); + Gia_ManSetPhase( p2 ); + Vec_IntForEachEntry( vMap1, Entry, i ) + { + if ( Entry == -1 ) + continue; + pObj = Gia_ManObj( p1, Abc_Lit2Var(Entry) ); + if ( ~pObj->Value == 0 ) + continue; + fCompl = Abc_LitIsCompl(Entry) ^ pObj->fPhase; + iRepr = Gia_ObjReprSelf( p, Abc_Lit2Var(pObj->Value) ); + Vec_IntWriteEntry( vMap, iRepr, Abc_Var2Lit( i, fCompl ) ); + } + Vec_IntForEachEntry( vMap2, Entry, i ) + { + if ( Entry == -1 ) + continue; + pObj = Gia_ManObj( p2, Abc_Lit2Var(Entry) ); + if ( ~pObj->Value == 0 ) + continue; + fCompl = Abc_LitIsCompl(Entry) ^ pObj->fPhase; + iRepr = Gia_ObjReprSelf( p, Abc_Lit2Var(pObj->Value) ); + if ( (iLit = Vec_IntEntry(vMap, iRepr)) == -1 ) + continue; + Vec_IntWriteEntry( vRes, i, Abc_LitNotCond( iLit, fCompl ) ); + } + Vec_IntFill( vMap, Gia_ManCoNum(p1), -1 ); + Vec_IntForEachEntry( vMap1, Entry, i ) + { + if ( Entry == -1 ) + continue; + pObj = Gia_ManObj( p1, Abc_Lit2Var(Entry) ); + if ( !Gia_ObjIsCo(pObj) ) + continue; + Vec_IntWriteEntry( vMap, Gia_ObjCioId(pObj), i ); + } + Vec_IntForEachEntry( vMap2, Entry, i ) + { + if ( Entry == -1 ) + continue; + pObj = Gia_ManObj( p2, Abc_Lit2Var(Entry) ); + if ( !Gia_ObjIsCo(pObj) ) + continue; + + assert( Vec_IntEntry(vRes, i) == -1 ); + Vec_IntWriteEntry( vRes, i, Abc_Var2Lit( Vec_IntEntry(vMap, Gia_ObjCioId(pObj)), 0 ) ); + assert( Vec_IntEntry(vRes, i) != -1 ); + } + Vec_IntFree( vMap ); + return vRes; +} + +void Gia_ManVerifyVerifyNameMapping( Gia_Man_t * p, Gia_Man_t * p1, Gia_Man_t * p2, Vec_Int_t * vMap1, Vec_Int_t * vMap2, Vec_Int_t * vMapRes ) +{ + int iImpl, iReprSpec, iReprImpl, nSize = Vec_IntSize(vMap2); + Gia_Obj_t * pObjSpec, * pObjImpl; + if ( vMapRes == NULL || p == NULL || p->pReprs == NULL ) + return; + assert( Vec_IntSize(vMapRes) == nSize ); + Gia_ManSetPhase( p1 ); + Gia_ManSetPhase( p2 ); + for ( iImpl = 0; iImpl < nSize; iImpl++ ) + if ( Vec_IntEntry(vMapRes, iImpl) >= 0 ) + { + int Entry = Vec_IntEntry( vMapRes, iImpl ); + int iSpec = Abc_Lit2Var( Entry ); + int fCompl = Abc_LitIsCompl( Entry ); + int iLitSpec = Vec_IntEntry( vMap1, iSpec ); + int iLitImpl = Vec_IntEntry( vMap2, iImpl ); + pObjSpec = Gia_ManObj( p1, Abc_Lit2Var(iLitSpec) ); + if ( Gia_ObjIsCo(pObjSpec) ) + continue; + if ( ~pObjSpec->Value == 0 ) + continue; + pObjImpl = Gia_ManObj( p2, Abc_Lit2Var(iLitImpl) ); + if ( ~pObjImpl->Value == 0 ) + continue; + iReprSpec = Gia_ObjReprSelf( p, Abc_Lit2Var(pObjSpec->Value) ); + iReprImpl = Gia_ObjReprSelf( p, Abc_Lit2Var(pObjImpl->Value) ); + if ( iReprSpec != iReprImpl ) + printf( "Found functional mismatch for ImplId %d and SpecId %d.\n", iImpl, iSpec ); + if ( (pObjImpl->fPhase ^ Abc_LitIsCompl(iLitImpl)) != (pObjSpec->fPhase ^ Abc_LitIsCompl(iLitSpec) ^ fCompl) ) + printf( "Found phase mismatch for ImplId %d and SpecId %d.\n", iImpl, iSpec ); + } +} + +int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, int nBTLimit, int nTimeLim, int fSeq, int fObjIdMap, int fDumpFiles, int fVerbose, char * pFileSpec ) { int Status = -1; Gia_Man_t * pSpec, * pGia0, * pGia1, * pMiter; @@ -1052,12 +1159,30 @@ int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, int nBTLimit, int nTimeLim, int fS { Cec_ParCec_t ParsCec, * pPars = &ParsCec; Cec_ManCecSetDefaultParams( pPars ); - pPars->nBTLimit = nBTLimit; - pPars->TimeLimit = nTimeLim; - pPars->fVerbose = fVerbose; + pPars->nBTLimit = nBTLimit; + pPars->TimeLimit = nTimeLim; + pPars->fUseOrigIds = fObjIdMap; + pPars->fVerbose = fVerbose; Status = Cec_ManVerify( pMiter, pPars ); if ( pPars->iOutFail >= 0 ) Abc_Print( 1, "Verification failed for at least one output (%d).\n", pPars->iOutFail ); + if ( fObjIdMap ) { + Gia_Man_t * pReduced = Gia_ManOrigIdsReduce( pMiter, pMiter->vIdsEquiv ); + Gia_ManStop( pReduced ); + Gia_Obj_t * pObj; int i; + Vec_Int_t * vCopy0 = Vec_IntAlloc(Gia_ManObjNum(pSpec)); + Gia_ManForEachObj( pSpec, pObj, i ) + Vec_IntPush( vCopy0, pObj->Value ); + Vec_Int_t * vCopy1 = Vec_IntAlloc(Gia_ManObjNum(pGia)); + Gia_ManForEachObj( pGia, pObj, i ) + Vec_IntPush( vCopy1, pObj->Value ); + Vec_IntFreeP( &pGia->vEquLitIds ); + pGia->vEquLitIds = Gia_ManVerifyFindNameMapping( pMiter, pGia0, pGia1, vCopy0, vCopy1 ); + assert( Vec_IntSize(pGia->vEquLitIds) == Gia_ManObjNum(pGia) ); + Gia_ManVerifyVerifyNameMapping( pMiter, pGia0, pGia1, vCopy0, vCopy1, pGia->vEquLitIds ); + Vec_IntFree( vCopy0 ); + Vec_IntFree( vCopy1 ); + } Gia_ManStop( pMiter ); } } @@ -1094,4 +1219,3 @@ Vec_Int_t * Gia_ManDeriveBoxMapping( Gia_Man_t * pGia ) ABC_NAMESPACE_IMPL_END - diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 9ce0dc107..fd1c2c8b2 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -42227,9 +42227,9 @@ usage: int Abc_CommandAbc9Verify( Abc_Frame_t * pAbc, int argc, char ** argv ) { char * pFileSpec = NULL; - int c, nBTLimit = 1000, nTimeLim = 0, fSeq = 0, fDumpFiles = 0, fVerbose = 0; + int c, nBTLimit = 1000, nTimeLim = 0, fSeq = 0, fObjIdMap = 0, fDumpFiles = 0, fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "CTsdvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "CTsmdvh" ) ) != EOF ) { switch ( c ) { @@ -42258,6 +42258,9 @@ int Abc_CommandAbc9Verify( Abc_Frame_t * pAbc, int argc, char ** argv ) case 's': fSeq ^= 1; break; + case 'm': + fObjIdMap ^= 1; + break; case 'd': fDumpFiles ^= 1; break; @@ -42276,15 +42279,16 @@ int Abc_CommandAbc9Verify( Abc_Frame_t * pAbc, int argc, char ** argv ) Extra_FileNameCorrectPath( pFileSpec ); printf( "Taking spec from file \"%s\".\n", pFileSpec ); } - Gia_ManVerifyWithBoxes( pAbc->pGia, nBTLimit, nTimeLim, fSeq, fDumpFiles, fVerbose, pFileSpec ); + Gia_ManVerifyWithBoxes( pAbc->pGia, nBTLimit, nTimeLim, fSeq, fObjIdMap, fDumpFiles, fVerbose, pFileSpec ); return 0; usage: - Abc_Print( -2, "usage: &verify [-CT num] [-sdvh] \n" ); + Abc_Print( -2, "usage: &verify [-CT num] [-smdvh] \n" ); Abc_Print( -2, "\t performs verification of combinational design\n" ); Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", nBTLimit ); Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", nTimeLim ); Abc_Print( -2, "\t-s : toggle using sequential verification [default = %s]\n", fSeq? "yes":"no"); + Abc_Print( -2, "\t-m : toggle producing object ID mapping (CEC only) [default = %s]\n", fObjIdMap? "yes":"no"); Abc_Print( -2, "\t-d : toggle dumping AIGs to be compared [default = %s]\n", fDumpFiles? "yes":"no"); Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes":"no"); Abc_Print( -2, "\t-h : print the command usage\n"); diff --git a/src/proof/cec/cec.h b/src/proof/cec/cec.h index ca7eed5a7..a3fb06376 100644 --- a/src/proof/cec/cec.h +++ b/src/proof/cec/cec.h @@ -135,6 +135,7 @@ struct Cec_ParCec_t_ int fUseSmartCnf; // use smart CNF computation int fRewriting; // enables AIG rewriting int fNaive; // performs naive SAT-based checking + int fUseOrigIds; // enable recording of original IDs int fSilent; // print no messages int fVeryVerbose; // verbose stats int fVerbose; // verbose stats diff --git a/src/proof/cec/cecCec.c b/src/proof/cec/cecCec.c index f6a1ab527..e52258b9d 100644 --- a/src/proof/cec/cecCec.c +++ b/src/proof/cec/cecCec.c @@ -359,11 +359,13 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars ) pParsFra->nItersMax = 1000; pParsFra->nBTLimit = pPars->nBTLimit; pParsFra->TimeLimit = pPars->TimeLimit; + pParsFra->fUseOrigIds = pPars->fUseOrigIds; pParsFra->fVerbose = pPars->fVerbose; pParsFra->fVeryVerbose = pPars->fVeryVerbose; pParsFra->fCheckMiter = 1; pParsFra->fDualOut = 1; pNew = Cec_ManSatSweeping( p, pParsFra, pPars->fSilent ); + ABC_SWAP( Vec_Int_t *, pInit->vIdsEquiv, p->vIdsEquiv ); pPars->iOutFail = pParsFra->iOutFail; // update pInit->pCexComb = p->pCexComb; p->pCexComb = NULL; @@ -383,6 +385,7 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars ) } return 0; } + Vec_IntFreeP( &pInit->vIdsEquiv ); p = Gia_ManDup( pInit ); Gia_ManEquivFixOutputPairs( p ); p = Gia_ManCleanup( pNew = p ); From 5e58e34f6cc4c41568adc5136881f0ddf8e7d952 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 30 Nov 2025 19:51:05 -0800 Subject: [PATCH 8/9] Extending "lutexact -k" to work with larger functions. --- src/base/abci/abc.c | 36 ++++++++++++++++++++++++++++-------- src/sat/bmc/bmc.h | 1 + src/sat/bmc/bmcMaj8.c | 19 ++++++++++++------- 3 files changed, 41 insertions(+), 15 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index fd1c2c8b2..669632be2 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -10768,7 +10768,7 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv ) Bmc_EsPar_t Pars, * pPars = &Pars; Bmc_EsParSetDefault( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "NMKTFUSYPiaorfgckdsmvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "NMKTFUSYPiaorfgckdsmpvh" ) ) != EOF ) { switch ( c ) { @@ -10896,6 +10896,9 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'm': pPars->fMinNodes ^= 1; break; + case 'p': + pPars->fUsePerm ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -10945,15 +10948,31 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Function with %d variales cannot be implemented with %d %d-input LUTs.\n", pPars->nVars, pPars->nNodes, pPars->nLutSize ); return 1; } - if ( pPars->nVars > 12 ) + if ( pPars->fKissat ) { - Abc_Print( -1, "Function should not have more than 12 inputs.\n" ); - return 1; + if ( pPars->nVars > 14 ) + { + Abc_Print( -1, "Function should not have more than 14 inputs.\n" ); + return 1; + } + if ( pPars->nLutSize > 8 ) + { + Abc_Print( -1, "Node size should not be more than 8 inputs.\n" ); + return 1; + } } - if ( pPars->nLutSize > 6 ) + else { - Abc_Print( -1, "Node size should not be more than 6 inputs.\n" ); - return 1; + if ( pPars->nVars > 12 ) + { + Abc_Print( -1, "Function should not have more than 12 inputs.\n" ); + return 1; + } + if ( pPars->nLutSize > 6 ) + { + Abc_Print( -1, "Node size should not be more than 6 inputs.\n" ); + return 1; + } } if ( pPars->nRandFuncs ) { pPars->fGlucose = 1; @@ -10972,7 +10991,7 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: lutexact [-NMKTFUS ] [-Y string] [-P string] [-iaorfgckdsmvh] \n" ); + Abc_Print( -2, "usage: lutexact [-NMKTFUS ] [-Y string] [-P string] [-iaorfgckdsmpvh] \n" ); Abc_Print( -2, "\t exact synthesis of I-input function using N K-input gates\n" ); Abc_Print( -2, "\t-N : the number of input variables [default = %d]\n", pPars->nVars ); Abc_Print( -2, "\t-M : the number of K-input nodes [default = %d]\n", pPars->nNodes ); @@ -10994,6 +11013,7 @@ usage: Abc_Print( -2, "\t-d : toggle dumping decomposed networks into BLIF files [default = %s]\n", pPars->fDumpBlif ? "yes" : "no" ); Abc_Print( -2, "\t-s : toggle silent computation (no messages, except when a solution is found) [default = %s]\n", pPars->fSilent ? "yes" : "no" ); Abc_Print( -2, "\t-m : toggle minimum-node solution possibly smaller than \"-M \" [default = %s]\n", pPars->fMinNodes ? "yes" : "no" ); + Abc_Print( -2, "\t-p : toggle use specialized permutation when minimizing nodes [default = %s]\n", pPars->fUsePerm ? "yes" : "no" ); Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose ? "yes" : "no" ); Abc_Print( -2, "\t-h : print the command usage\n" ); Abc_Print( -2, "\t : truth table in hex notation\n" ); diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h index 374945039..3b591bb4e 100644 --- a/src/sat/bmc/bmc.h +++ b/src/sat/bmc/bmc.h @@ -68,6 +68,7 @@ struct Bmc_EsPar_t_ int fLutCascade; int fLutInFixed; int fMinNodes; + int fUsePerm; int RuntimeLim; int nRandFuncs; int nMintNum; diff --git a/src/sat/bmc/bmcMaj8.c b/src/sat/bmc/bmcMaj8.c index 4a96af84e..5f291c20a 100644 --- a/src/sat/bmc/bmcMaj8.c +++ b/src/sat/bmc/bmcMaj8.c @@ -47,6 +47,7 @@ ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// #define MAJ_NOBJS 64 // Const0 + Const1 + nVars + nNodes +#define MAJ_MAX_LUT 8 typedef struct Exa8_Man_t_ Exa8_Man_t; struct Exa8_Man_t_ @@ -63,7 +64,7 @@ struct Exa8_Man_t_ Vec_Wrd_t * vInfo; // nVars + nNodes + 1 Vec_Bit_t * vUsed2; // bit masks Vec_Bit_t * vUsed3; // bit masks - int VarMarks[MAJ_NOBJS][6][MAJ_NOBJS]; // variable marks + int VarMarks[MAJ_NOBJS][MAJ_MAX_LUT][MAJ_NOBJS]; // variable marks int VarVals[MAJ_NOBJS]; // values of the first nVars variables Vec_Wec_t * vOutLits; // output vars Vec_Wec_t * vInVars; // input vars @@ -214,6 +215,7 @@ static int Exa8_ManMarkup( Exa8_Man_t * p ) { int i, k, j; assert( p->nObjs <= MAJ_NOBJS ); + assert( p->nLutSize <= MAJ_MAX_LUT ); // assign functionality variables p->iVar = 1 + p->LutMask * p->nNodes; // assign connectivity variables @@ -347,7 +349,7 @@ static inline int Exa8_ManFindFanin( Exa8_Man_t * p, int i, int k ) static inline int Exa8_ManEval( Exa8_Man_t * p ) { static int Flag = 0; - int i, k, j, iMint; word * pFanins[6]; + int i, k, j, iMint; word * pFanins[MAJ_MAX_LUT]; for ( i = p->nVars; i < p->nObjs; i++ ) { int iVarStart = 1 + p->LutMask*(i - p->nVars); @@ -678,7 +680,11 @@ int Exa8_ManExactSynthesis( Bmc_EsPar_t * pPars ) abctime clkTotal = Abc_Clock(); Exa8_Man_t * p; int fCompl = 0; - word pTruth[64]; + assert( pPars->nVars <= 14 ); + assert( pPars->nLutSize <= 8 ); + int nTruthWords = Abc_TtWordNum( pPars->nVars ); + word * pTruth = ABC_CALLOC( word, nTruthWords ); + assert( pTruth ); if ( pPars->pSymStr ) { word * pFun = Abc_TtSymFunGenerate( pPars->pSymStr, pPars->nVars ); pPars->pTtStr = ABC_CALLOC( char, pPars->nVars > 2 ? (1 << (pPars->nVars-2)) + 1 : 2 ); @@ -689,8 +695,6 @@ int Exa8_ManExactSynthesis( Bmc_EsPar_t * pPars ) if ( pPars->pTtStr ) Abc_TtReadHex( pTruth, pPars->pTtStr ); else assert( 0 ); - assert( pPars->nVars <= 12 ); - assert( pPars->nLutSize <= 6 ); if ( pPars->fUseIncr && !pPars->fSilent ) printf( "Warning: Ignoring incremental option when using Kissat.\n" ); pPars->fUseIncr = 0; @@ -758,6 +762,7 @@ int Exa8_ManExactSynthesis( Bmc_EsPar_t * pPars ) if ( pPars->pSymStr ) ABC_FREE( pPars->pTtStr ); Exa8_ManFree( p ); + ABC_FREE( pTruth ); return Res; } @@ -770,7 +775,7 @@ int Exa8_ManExactSynthesisIter( Bmc_EsPar_t * pPars ) for ( int n = nNodeMin; n <= nNodeMax; n++ ) { printf( "\nTrying M = %d:\n", n ); pPars->nNodes = n; - if ( fGenPerm ) { + if ( !pPars->fUsePerm && fGenPerm ) { Vec_Str_t * vStr = Vec_StrAlloc( 100 ); for ( int v = 0; v < pPars->nLutSize; v++ ) Vec_StrPush( vStr, 'a'+v ); @@ -790,7 +795,7 @@ int Exa8_ManExactSynthesisIter( Bmc_EsPar_t * pPars ) pPars->pPermStr = Vec_StrReleaseArray(vStr); Vec_StrFree( vStr ); } - if ( 0 && fGenPerm ) { + else if ( pPars->fUsePerm && fGenPerm ) { Vec_Str_t * vStr = Vec_StrAlloc( 100 ); for ( int v = 0; v < pPars->nLutSize; v++ ) Vec_StrPush( vStr, 'a'+v ); From b7f8df09419b0070d6ba25e642f4d369ff606896 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 3 Dec 2025 13:39:13 -0800 Subject: [PATCH 9/9] Command "andexact". --- src/aig/gia/giaTim.c | 14 - src/base/abci/abc.c | 184 ++++++- src/sat/bmc/bmc.h | 3 +- src/sat/bmc/bmcMaj9.c | 1011 +++++++++++++++++++++++++++++++++++++++ src/sat/bmc/module.make | 1 + 5 files changed, 1197 insertions(+), 16 deletions(-) create mode 100644 src/sat/bmc/bmcMaj9.c diff --git a/src/aig/gia/giaTim.c b/src/aig/gia/giaTim.c index 271c6d4ee..54012bbde 100644 --- a/src/aig/gia/giaTim.c +++ b/src/aig/gia/giaTim.c @@ -953,20 +953,6 @@ Gia_Man_t * Gia_ManDupCollapse( Gia_Man_t * p, Gia_Man_t * pBoxes, Vec_Int_t * v ***********************************************************************/ -/* -› Please have a look at how name mapping is done in procedure Abc_FrameReadMiniLutNameMapping() in file "src/aig/gia/ - giaMini.c". The main idea is to map the object IDs in the design after synthesis (pAbc->pGiaMiniLut) into the object IDs in - the design before synthesis (pAbc->pGiaMiniAig). The computation is divided into three steps: (1) computing object - equivalences using Gia_ManComputeGiaEquivs(), which annotates the input AIG (pGia) containing both designs before and after - synthesis with equivalence class information; this information contains equivalence classes of objects from both designs; (2) - creating a map (pRes) of the resulting object IDs (in pAbc->pGiaMiniLut) into the original object IDs (in pAbc->pGiaMiniAig) - using procedure Gia_ManMapMiniLut2MiniAig(); this map is enabled by having two arrays (one of them is pAbc->vCopyMiniAig - mapping objects of pAbc->pGiaMiniAig in the original object IDs; the other one is pAbc->vCopyMiniLut mapping objects of - pAbc->pGiaMiniLut into the IDs of pAbc->pGiaMiniLut); (3) verification procedure (commented out by default) - Gia_ManNameMapVerify() which checks that the resulting mapping computed by Gia_ManMapMiniLut2MiniAig() is correct. Please - let me know if this computation is clear. -*/ - Vec_Int_t * Gia_ManVerifyFindNameMapping( Gia_Man_t * p, Gia_Man_t * p1, Gia_Man_t * p2, Vec_Int_t * vMap1, Vec_Int_t * vMap2 ) { Vec_Int_t * vRes = Vec_IntStartFull(Vec_IntSize(vMap2)); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 669632be2..d4ec89b41 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -172,6 +172,7 @@ static int Abc_CommandBmsPs ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandMajExact ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandTwoExact ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandLutExact ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAndExact ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAllExact ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandTestExact ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandMajGen ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -1002,6 +1003,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Exact synthesis", "majexact", Abc_CommandMajExact, 0 ); Cmd_CommandAdd( pAbc, "Exact synthesis", "twoexact", Abc_CommandTwoExact, 0 ); Cmd_CommandAdd( pAbc, "Exact synthesis", "lutexact", Abc_CommandLutExact, 0 ); + Cmd_CommandAdd( pAbc, "Exact synthesis", "andexact", Abc_CommandAndExact, 0 ); Cmd_CommandAdd( pAbc, "Exact synthesis", "allexact", Abc_CommandAllExact, 0 ); Cmd_CommandAdd( pAbc, "Exact synthesis", "testexact", Abc_CommandTestExact, 0 ); Cmd_CommandAdd( pAbc, "Exact synthesis", "majgen", Abc_CommandMajGen, 0 ); @@ -10992,7 +10994,7 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv ) usage: Abc_Print( -2, "usage: lutexact [-NMKTFUS ] [-Y string] [-P string] [-iaorfgckdsmpvh] \n" ); - Abc_Print( -2, "\t exact synthesis of I-input function using N K-input gates\n" ); + Abc_Print( -2, "\t exact synthesis of N-input function using M K-input lookup-tables\n" ); Abc_Print( -2, "\t-N : the number of input variables [default = %d]\n", pPars->nVars ); Abc_Print( -2, "\t-M : the number of K-input nodes [default = %d]\n", pPars->nNodes ); Abc_Print( -2, "\t-K : the number of node fanins [default = %d]\n", pPars->nLutSize ); @@ -11020,6 +11022,186 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAndExact( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern int Exa9_ManExactSynthesis( Bmc_EsPar_t * pPars ); + extern int Exa9_ManExactSynthesisIter( Bmc_EsPar_t * pPars ); + extern char * Abc_NtkReadTruth( Abc_Ntk_t * pNtk ); + int c; + Bmc_EsPar_t Pars, * pPars = &Pars; + Bmc_EsParSetDefault( pPars ); + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "NMTSHYiadsmvh" ) ) != EOF ) + { + switch ( c ) + { + case 'N': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nVars = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nVars < 0 ) + goto usage; + break; + case 'M': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nNodes = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nNodes < 0 ) + goto usage; + break; + case 'T': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" ); + goto usage; + } + pPars->RuntimeLim = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->RuntimeLim < 0 ) + goto usage; + break; + case 'S': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" ); + goto usage; + } + pPars->Seed = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->Seed < 0 ) + goto usage; + break; + case 'H': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-H\" should be followed by a string.\n" ); + goto usage; + } + pPars->n1HotAlgo = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + break; + case 'Y': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-Y\" should be followed by a string.\n" ); + goto usage; + } + pPars->pSymStr = argv[globalUtilOptind]; + globalUtilOptind++; + break; + case 'i': + pPars->fUseIncr ^= 1; + break; + case 'a': + pPars->fOnlyAnd ^= 1; + break; + case 'd': + pPars->fDumpBlif ^= 1; + break; + case 's': + pPars->fSilent ^= 1; + break; + case 'm': + pPars->fMinNodes ^= 1; + break; + case 'v': + pPars->fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( argc == globalUtilOptind + 1 ) + pPars->pTtStr = argv[globalUtilOptind]; + else if ( argc == globalUtilOptind && Abc_FrameReadNtk(pAbc) ) + { + pPars->pTtStr = Abc_NtkReadTruth( Abc_FrameReadNtk(pAbc) ); + if ( pPars->pTtStr ) + pPars->nVars = Abc_NtkCiNum(Abc_FrameReadNtk(pAbc)); + } + if ( pPars->pTtStr == NULL && pPars->pSymStr == NULL && pPars->nRandFuncs == 0 ) + { + Abc_Print( -1, "Truth table should be given on the command line.\n" ); + return 1; + } + if ( pPars->nVars == 0 && pPars->pTtStr ) + pPars->nVars = 2 + Abc_Base2Log((int)strlen(pPars->pTtStr)); + if ( pPars->pTtStr && (1 << (pPars->nVars-2)) != (int)strlen(pPars->pTtStr) ) + { + Abc_Print( -1, "Truth table is expected to have %d hex digits (instead of %d).\n", (1 << (pPars->nVars-2)), strlen(pPars->pTtStr) ); + return 1; + } + if ( pPars->nVars == 0 && pPars->pSymStr ) + pPars->nVars = (int)strlen(pPars->pSymStr) - 1; + if ( pPars->pSymStr && pPars->nVars+1 != strlen(pPars->pSymStr) ) + { + Abc_Print( -1, "The char string of the %d-variable symmetric function should have %d zeros and ones (instead of %d).\n", pPars->nVars, pPars->nVars+1, strlen(pPars->pSymStr) ); + return 1; + } + if ( pPars->nVars > pPars->nNodes + 1 ) + { + Abc_Print( -1, "Function with %d variales cannot be implemented with %d two-input nodes.\n", pPars->nVars, pPars->nNodes ); + return 1; + } + if ( pPars->nVars > 14 ) + { + Abc_Print( -1, "Function should not have more than 14 inputs.\n" ); + return 1; + } + if ( pPars->nNodes > 16 ) + { + Abc_Print( -1, "Node count cannot be more than 16 inputs.\n" ); + return 1; + } + if ( pPars->fMinNodes ) + Exa9_ManExactSynthesisIter( pPars ); + else + Exa9_ManExactSynthesis( pPars ); + if ( argc == globalUtilOptind && Abc_FrameReadNtk(pAbc) ) + ABC_FREE( pPars->pTtStr ); + return 0; + +usage: + Abc_Print( -2, "usage: andexact [-NMTSH ] [-Y str] [-iadmsvh] \n" ); + Abc_Print( -2, "\t exact synthesis of N-input function using two-input gates\n" ); + Abc_Print( -2, "\t-N : the number of input variables [default = %d]\n", pPars->nVars ); + Abc_Print( -2, "\t-M : the number of two-input nodes [default = %d]\n", pPars->nNodes ); + Abc_Print( -2, "\t-T : the runtime limit in seconds [default = %d]\n", pPars->RuntimeLim ); + Abc_Print( -2, "\t-S : the random seed for random function generation with -F [default = %d]\n", pPars->Seed ); + Abc_Print( -2, "\t-H : the 1-hotness algorithm used (0 = naive; 1 = seq; 2 = bim; 3 = cmd) [default = %d]\n", pPars->n1HotAlgo ); + Abc_Print( -2, "\t-Y : charasteristic string of a symmetric function [default = %s]\n", pPars->pSymStr ? pPars->pSymStr : "unused" ); + Abc_Print( -2, "\t-i : toggle using incremental SAT (CEGAR over minterms) [default = %s]\n", pPars->fUseIncr ? "yes" : "no" ); + Abc_Print( -2, "\t-a : toggle using only AND-gates when K = 2 [default = %s]\n", pPars->fOnlyAnd ? "yes" : "no" ); + Abc_Print( -2, "\t-m : toggle minimum-node solution possibly smaller than \"-M \" [default = %s]\n", pPars->fMinNodes ? "yes" : "no" ); + Abc_Print( -2, "\t-d : toggle dumping decomposed networks into BLIF files [default = %s]\n", pPars->fDumpBlif ? "yes" : "no" ); + Abc_Print( -2, "\t-s : toggle silent computation (no messages, except when a solution is found) [default = %s]\n", pPars->fSilent ? "yes" : "no" ); + Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose ? "yes" : "no" ); + Abc_Print( -2, "\t-h : print the command usage\n" ); + Abc_Print( -2, "\t : truth table in hex notation\n" ); + return 1; +} + /**Function************************************************************* Synopsis [] diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h index 3b591bb4e..93d3ea326 100644 --- a/src/sat/bmc/bmc.h +++ b/src/sat/bmc/bmc.h @@ -73,6 +73,7 @@ struct Bmc_EsPar_t_ int nRandFuncs; int nMintNum; int Seed; + int n1HotAlgo; int fDumpBlif; int fVerbose; int fSilent; @@ -102,6 +103,7 @@ static inline void Bmc_EsParSetDefault( Bmc_EsPar_t * pPars ) pPars->fUniqFans = 0; pPars->fLutCascade = 0; pPars->RuntimeLim = 0; + pPars->n1HotAlgo = 1; pPars->fVerbose = 0; } @@ -274,4 +276,3 @@ ABC_NAMESPACE_HEADER_END //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// - diff --git a/src/sat/bmc/bmcMaj9.c b/src/sat/bmc/bmcMaj9.c new file mode 100644 index 000000000..cc15c153a --- /dev/null +++ b/src/sat/bmc/bmcMaj9.c @@ -0,0 +1,1011 @@ +/**CFile**************************************************************** + + FileName [bmcMaj9.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [SAT-based bounded model checking.] + + Synopsis [Exact synthesis with majority gates.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - October 1, 2017.] + + Revision [$Id: bmcMaj9.c,v 1.00 2017/10/01 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "bmc.h" +#include "misc/extra/extra.h" +#include "misc/util/utilTruth.h" +#include "sat/kissat/kissat.h" +#include "aig/miniaig/miniaig.h" +#include "base/io/ioResub.h" +#include "base/main/main.h" +#include "base/cmd/cmd.h" + +#include +#include + +#define KISSAT_UNSAT 20 +#define KISSAT_SAT 10 +#define KISSAT_UNDEC 0 + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +#define MAJ_NOBJS 64 // Const0 + Const1 + nVars + nNodes + +typedef struct Exa9_Man_t_ Exa9_Man_t; +struct Exa9_Man_t_ +{ + Bmc_EsPar_t * pPars; // parameters + int nVars; // inputs + int nNodes; // internal nodes + int nObjs; // total objects (nVars inputs + nNodes internal nodes) + int nWords; // the truth table size in 64-bit words + int nMints; // number of input minterms + int nSelVars; // number of selection variables (fanin + output) + int nValVars; // number of value variables + int nVarAlloc; // total vars reserved in the solver + int nClausesStart; // clauses added in the structural part (excluding 1-hot) + int nClausesHot; // clauses added for 1-hot constraints + int nClausesMints; // clauses added per-minterm + int fCountStruct; // flag: counting structural clauses + int fCountHot; // flag: counting 1-hot clauses + word * pTruth; // truth table + Vec_Wrd_t * vTruths; // computed truth tables + kissat * pSat; // SAT solver + abctime timeStop; // runtime limit (0 = unlimited) +}; + +static inline int Exa9_LitToKissat( int Lit ) +{ + int v = Abc_Lit2Var( Lit ); + assert( v > 0 ); + return Abc_LitIsCompl( Lit ) ? -v : v; +} +static inline int Exa9_KissatAddClause( Exa9_Man_t * p, int * pLits, int nLits ) +{ + int i; + for ( i = 0; i < nLits; i++ ) + kissat_add( p->pSat, Exa9_LitToKissat( pLits[i] ) ); + kissat_add( p->pSat, 0 ); + if ( p->fCountStruct ) + { + if ( p->fCountHot ) + p->nClausesHot++; + else + p->nClausesStart++; + } + else + p->nClausesMints++; + return !kissat_is_inconsistent( p->pSat ); +} +static inline int Exa9_KissatVarValue( Exa9_Man_t * p, int v ) +{ + assert( v > 0 ); + return kissat_value( p->pSat, v ) > 0; +} +static int Exa9_KissatTerminate( void * pData ) +{ + Exa9_Man_t * p = (Exa9_Man_t *)pData; + return p && p->timeStop && Abc_Clock() > p->timeStop; +} + +static inline word * Exa9_ManTruth( Exa9_Man_t * p, int v ) { return Vec_WrdEntryP( p->vTruths, p->nWords * v ); } + +static inline int Exa9_ManSelVar( Exa9_Man_t * p, int iNode, int iFanin, int fCompl, int iObj ) +{ + return 1 + (((iNode * 2 + iFanin) * 2 + fCompl) * p->nObjs + (iObj - 1)); +} +static inline int Exa9_ManSelVarAux( Exa9_Man_t * p, int iNode, int iFanin, int fCompl, int iObj ) +{ + return 1 + p->nSelVars + (((iNode * 2 + iFanin) * 2 + fCompl) * p->nObjs + (iObj - 1)); +} +static inline int Exa9_ManSelVarOut( Exa9_Man_t * p, int fCompl, int iObj ) +{ + return 1 + 4 * p->nNodes * p->nObjs + fCompl * p->nObjs + (iObj - 1); +} +static inline int Exa9_ManSelVarOutAux( Exa9_Man_t * p, int fCompl, int iObj ) +{ + return 1 + p->nSelVars + 4 * p->nNodes * p->nObjs + fCompl * p->nObjs + (iObj - 1); +} +static inline int Exa9_ManValueVar( Exa9_Man_t * p, int iObj, int Place, int iMint ) +{ + int Base = 1 + 2 * p->nSelVars; + return Base + ((iObj - 1) * 3 + Place) * p->nMints + iMint; +} + +// return auxiliary vars actually used by a 1-hot of size nLits under the chosen encoding +static inline int Exa9_ManCountAuxOneHot( int nLits, int Algo ) +{ + if ( nLits <= 1 ) + return 0; + if ( Algo == 0 ) // naive pairwise + return 0; + if ( Algo == 1 ) // sequential + return nLits - 1; + if ( Algo == 2 ) // bimander + { + const int GroupSize = 6; + if ( nLits <= GroupSize ) + return 0; + { + int nGroups = (nLits + GroupSize - 1) / GroupSize; + int nBits = Abc_Base2Log( nGroups ); + return nBits; + } + } + if ( Algo == 3 ) // commander + { + const int GroupSize = 5; + if ( nLits <= GroupSize ) + return 0; + { + int nGroups = (nLits + GroupSize - 1) / GroupSize; + return nGroups; + } + } + return 0; +} + +static int Exa9_ManCountAuxTotal( Exa9_Man_t * p ) +{ + int Algo = p->pPars->n1HotAlgo; + int Total = 0; + int n; + // fanin selectors (two fanins * two polarities per node) + for ( n = 0; n < p->nNodes; n++ ) + { + int Obj = p->nVars + n + 1; + int nLits = Obj - 1; // choices for each polarity + int AuxPerGroup = Exa9_ManCountAuxOneHot( nLits, Algo ); + Total += 4 * AuxPerGroup; + } + // output selector (two polarities over all objects) + Total += Exa9_ManCountAuxOneHot( 2 * p->nObjs, Algo ); + return Total; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static int Exa9_ManVarReserve( Exa9_Man_t * p ) +{ + int64_t Count = 2 * (int64_t)p->nSelVars + (int64_t)p->nValVars; + if ( Count > INT_MAX ) + Count = INT_MAX; + return (int)Count; +} +static Exa9_Man_t * Exa9_ManAlloc( Bmc_EsPar_t * pPars, word * pTruth ) +{ + Exa9_Man_t * p = ABC_CALLOC( Exa9_Man_t, 1 ); + p->pPars = pPars; + p->nVars = pPars->nVars; + p->nNodes = pPars->nNodes; + p->nObjs = pPars->nVars + pPars->nNodes; + p->nWords = Abc_TtWordNum(pPars->nVars); + p->nMints = 1 << pPars->nVars; + p->nSelVars = p->nNodes * 4 * p->nObjs + 2 * p->nObjs; + p->nValVars = 3 * p->nObjs * p->nMints; + p->nVarAlloc = Exa9_ManVarReserve( p ); + p->nClausesStart = p->nClausesHot = p->nClausesMints = 0; + p->fCountStruct = 0; + p->fCountHot = 0; + p->pTruth = pTruth; + p->vTruths = Vec_WrdStart( p->nWords * (p->nObjs + 1) ); + p->pSat = kissat_init(); + { + int nBias = 0; // 0=neutral, 1=SAT bias, -1=UNSAT bias + if ( nBias > 0 ) + { + kissat_set_option( p->pSat, "target", 2 ); + kissat_set_option( p->pSat, "restartint", 50 ); + } + else if ( nBias < 0 ) + kissat_set_option( p->pSat, "stable", 0 ); + } + assert( Exa9_ManValueVar( p, p->nObjs, 2, p->nMints - 1 ) <= p->nVarAlloc ); + kissat_reserve( p->pSat, p->nVarAlloc ); + if ( pPars->Seed > 0 ) + kissat_set_option( p->pSat, "seed", pPars->Seed ); + p->timeStop = 0; + return p; +} +static void Exa9_ManFree( Exa9_Man_t * p ) +{ + kissat_release( p->pSat ); + Vec_WrdFree( p->vTruths ); + ABC_FREE( p ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Exa9_ManAddUnit( Exa9_Man_t * p, int Var, int fCompl ) +{ + int Lit = Abc_Var2Lit( Var, fCompl ); + return Exa9_KissatAddClause( p, &Lit, 1 ); +} +static inline int Exa9_ManAddEquality( Exa9_Man_t * p, int iSel, int iFan, int iOut, int fCompl ) +{ + int pLits[3]; + pLits[0] = Abc_Var2Lit( iSel, 1 ); + pLits[1] = Abc_Var2Lit( iFan, 1 ); + pLits[2] = Abc_Var2Lit( iOut, fCompl ); + if ( !Exa9_KissatAddClause( p, pLits, 3 ) ) + return 0; + pLits[1] = Abc_Var2Lit( iFan, 0 ); + pLits[2] = Abc_Var2Lit( iOut, !fCompl ); + return Exa9_KissatAddClause( p, pLits, 3 ); +} +static int Exa9_ManAddOneHotQuad( Exa9_Man_t * p, Vec_Int_t * vLits ) +{ + int * pArray = Vec_IntArray( vLits ); + int nLits = Vec_IntSize( vLits ); + int i, k; + assert( nLits > 0 ); + if ( !Exa9_KissatAddClause( p, pArray, nLits ) ) + return 0; + for ( i = 0; i < nLits; i++ ) + for ( k = i + 1; k < nLits; k++ ) + { + int pLits[2] = { Abc_LitNot(pArray[i]), Abc_LitNot(pArray[k]) }; + if ( !Exa9_KissatAddClause( p, pLits, 2 ) ) + return 0; + } + return 1; +} +static int Exa9_ManAddOneHotSeq( Exa9_Man_t * p, Vec_Int_t * vLits, Vec_Int_t * vAux ) +{ + int nLits = Vec_IntSize( vLits ); + int * x = Vec_IntArray( vLits ); + int * y = Vec_IntArray( vAux ); + int pLits[2], i; + assert( nLits > 0 ); + if ( !Exa9_KissatAddClause( p, x, nLits ) ) + return 0; + if ( nLits == 1 ) + return 1; + assert( Vec_IntSize(vAux) >= nLits - 1 ); + // (¬x1 ∨ y1) + pLits[0] = Abc_LitNot( x[0] ); + pLits[1] = Abc_Var2Lit( y[0], 0 ); + if ( !Exa9_KissatAddClause( p, pLits, 2 ) ) + return 0; + // middle constraints + for ( i = 1; i < nLits - 1; i++ ) + { + // (¬xi ∨ yi) + pLits[0] = Abc_LitNot( x[i] ); + pLits[1] = Abc_Var2Lit( y[i], 0 ); + if ( !Exa9_KissatAddClause( p, pLits, 2 ) ) + return 0; + // (¬yi-1 ∨ yi) + pLits[0] = Abc_LitNot( Abc_Var2Lit( y[i-1], 0 ) ); + pLits[1] = Abc_Var2Lit( y[i], 0 ); + if ( !Exa9_KissatAddClause( p, pLits, 2 ) ) + return 0; + // (¬xi ∨ ¬yi-1) + pLits[0] = Abc_LitNot( x[i] ); + pLits[1] = Abc_LitNot( Abc_Var2Lit( y[i-1], 0 ) ); + if ( !Exa9_KissatAddClause( p, pLits, 2 ) ) + return 0; + } + // (¬xn ∨ ¬y_{n-1}) + pLits[0] = Abc_LitNot( x[nLits-1] ); + pLits[1] = Abc_LitNot( Abc_Var2Lit( y[nLits-2], 0 ) ); + return Exa9_KissatAddClause( p, pLits, 2 ); +} +static inline int Exa9_ManAddAtMostOnePair( Exa9_Man_t * p, Vec_Int_t * vLits ) +{ + int nLits = Vec_IntSize( vLits ); + int * x = Vec_IntArray( vLits ); + int pLits[2], i, j; + for ( i = 0; i < nLits; i++ ) + for ( j = i + 1; j < nLits; j++ ) + { + pLits[0] = Abc_LitNot( x[i] ); + pLits[1] = Abc_LitNot( x[j] ); + if ( !Exa9_KissatAddClause( p, pLits, 2 ) ) + return 0; + } + return 1; +} +static int Exa9_ManAddOneHotBim( Exa9_Man_t * p, Vec_Int_t * vLits, Vec_Int_t * vAux ) +{ + int nLits = Vec_IntSize( vLits ); + int * x = Vec_IntArray( vLits ); + int * y = Vec_IntArray( vAux ); + int pLits[2], i, j, g; + int GroupSize = 6; + if ( nLits == 0 ) + return 0; + if ( !Exa9_KissatAddClause( p, x, nLits ) ) + return 0; + if ( nLits == 1 ) + return 1; + if ( nLits <= GroupSize ) + return Exa9_ManAddOneHotQuad( p, vLits ); + { + int nGroups = (nLits + GroupSize - 1) / GroupSize; + int nBits = Abc_Base2Log( nGroups ); + if ( nBits == 0 ) + return Exa9_ManAddOneHotQuad( p, vLits ); + assert( Vec_IntSize(vAux) >= nBits ); + // pairwise inside each group + for ( g = 0; g < nGroups; g++ ) + { + int iStart = g * GroupSize; + int iStop = Abc_MinInt( iStart + GroupSize, nLits ); + for ( i = iStart; i < iStop; i++ ) + for ( j = i + 1; j < iStop; j++ ) + { + pLits[0] = Abc_LitNot( x[i] ); + pLits[1] = Abc_LitNot( x[j] ); + if ( !Exa9_KissatAddClause( p, pLits, 2 ) ) + return 0; + } + // connect literals in the group to shared binary variables + for ( i = iStart; i < iStop; i++ ) + { + int Code = g; + int b; + for ( b = 0; b < nBits; b++, Code >>= 1 ) + { + pLits[0] = Abc_LitNot( x[i] ); + pLits[1] = (Code & 1) ? Abc_Var2Lit( y[b], 0 ) : Abc_LitNot( Abc_Var2Lit( y[b], 0 ) ); + if ( !Exa9_KissatAddClause( p, pLits, 2 ) ) + return 0; + } + } + } + } + return 1; +} +static int Exa9_ManAddOneHotCom( Exa9_Man_t * p, Vec_Int_t * vLits, Vec_Int_t * vAux ) +{ + int nLits = Vec_IntSize( vLits ); + int * x = Vec_IntArray( vLits ); + int * y = Vec_IntArray( vAux ); + int GroupSize = 4; + int i, j, g; + Vec_Int_t * vCmd; + if ( nLits == 0 ) + return 0; + if ( !Exa9_KissatAddClause( p, x, nLits ) ) + return 0; + if ( nLits == 1 ) + return 1; + if ( nLits <= GroupSize ) + return Exa9_ManAddOneHotQuad( p, vLits ); + vCmd = Vec_IntAlloc(16); + { + int nGroups = (nLits + GroupSize - 1) / GroupSize; + if ( nGroups > Vec_IntSize(vAux) ) + { + Vec_IntFree( vCmd ); + return Exa9_ManAddOneHotQuad( p, vLits ); + } + for ( g = 0; g < nGroups; g++ ) + { + int CmdVar = y[g]; + Vec_IntPush( vCmd, Abc_Var2Lit( CmdVar, 0 ) ); + int iStart = g * GroupSize; + int iStop = Abc_MinInt( iStart + GroupSize, nLits ); + // CmdVar => at least one literal in the group + { + int pLits[6]; // GroupSize <= 5 + int nCls = 0; + pLits[nCls++] = Abc_LitNot( Abc_Var2Lit( CmdVar, 0 ) ); + for ( i = iStart; i < iStop; i++ ) + pLits[nCls++] = x[i]; + assert( nCls <= 6 ); + if ( !Exa9_KissatAddClause( p, pLits, nCls ) ) + { + Vec_IntFree( vCmd ); + return 0; + } + } + for ( i = iStart; i < iStop; i++ ) + { + int pLits[2] = { Abc_LitNot( x[i] ), Abc_Var2Lit( CmdVar, 0 ) }; + if ( !Exa9_KissatAddClause( p, pLits, 2 ) ) + { + Vec_IntFree( vCmd ); + return 0; + } + } + for ( i = iStart; i < iStop; i++ ) + for ( j = i + 1; j < iStop; j++ ) + { + int pLits[2] = { Abc_LitNot( x[i] ), Abc_LitNot( x[j] ) }; + if ( !Exa9_KissatAddClause( p, pLits, 2 ) ) + { + Vec_IntFree( vCmd ); + return 0; + } + } + } + } + if ( !Exa9_ManAddAtMostOnePair( p, vCmd ) ) + { + Vec_IntFree( vCmd ); + return 0; + } + Vec_IntFree( vCmd ); + return 1; +} +static int Exa9_ManAddOneHot( Exa9_Man_t * p, Vec_Int_t * vLits, Vec_Int_t * vAux ) +{ + int Res = 0; + int fOldHot = p->fCountHot; + p->fCountHot = 1; + if ( Vec_IntSize(vLits) < 7 ) + Res = Exa9_ManAddOneHotQuad( p, vLits ); + else if ( p->pPars->n1HotAlgo == 1 ) + Res = Exa9_ManAddOneHotSeq( p, vLits, vAux ); + else if ( p->pPars->n1HotAlgo == 2 ) + Res = Exa9_ManAddOneHotBim( p, vLits, vAux ); + else if ( p->pPars->n1HotAlgo == 3 ) + Res = Exa9_ManAddOneHotCom( p, vLits, vAux ); + else + Res = Exa9_ManAddOneHotQuad( p, vLits ); + p->fCountHot = fOldHot; + return Res; +} +static int Exa9_ManAddCnfStart( Exa9_Man_t * p ) +{ + p->fCountStruct = 1; + Vec_Int_t * vLits = Vec_IntAlloc( 100 ); + Vec_Int_t * vAux = Vec_IntAlloc( 100 ); + Vec_Int_t * vUse = Vec_IntAlloc( 100 ); + int n, j, k, c, Var; + for ( n = 0; n < p->nNodes; n++ ) + { + int Obj = p->nVars + n + 1; + for ( k = 0; k < 2; k++ ) + { + Vec_IntClear( vLits ); + Vec_IntClear( vAux ); + for ( j = 1; j <= p->nObjs; j++ ) + for ( c = 0; c < 2; c++ ) + { + Var = Exa9_ManSelVar( p, n, k, c, j ); + if ( j >= Obj ) + { + if ( !Exa9_ManAddUnit( p, Var, 1 ) ) + { + Vec_IntFree( vLits ); + Vec_IntFree( vAux ); + return 0; + } + continue; + } + Vec_IntPush( vLits, Abc_Var2Lit( Var, 0 ) ); + Vec_IntPush( vAux, Exa9_ManSelVarAux( p, n, k, c, j ) ); + } + if ( Vec_IntSize(vLits) == 0 || !Exa9_ManAddOneHot( p, vLits, vAux ) ) + { + Vec_IntFree( vLits ); + Vec_IntFree( vAux ); + return 0; + } + } + // enforce first fanin index < second fanin index + for ( j = 1; j < Obj; j++ ) + for ( c = 0; c < 2; c++ ) + { + int Var0 = Exa9_ManSelVar( p, n, 0, c, j ); + int j2, c2; + for ( j2 = 1; j2 <= j; j2++ ) + for ( c2 = 0; c2 < 2; c2++ ) + { + int Var1 = Exa9_ManSelVar( p, n, 1, c2, j2 ); + int pLits[2] = { Abc_Var2Lit( Var0, 1 ), Abc_Var2Lit( Var1, 1 ) }; + if ( !Exa9_KissatAddClause( p, pLits, 2 ) ) + { + Vec_IntFree( vLits ); + Vec_IntFree( vAux ); + return 0; + } + } + } + /* + // order nodes by larger (second) fanin index + for ( j = 1; j < Obj; j++ ) + for ( c = 0; c < 2; c++ ) + { + int VarLargeThis = Exa9_ManSelVar( p, n, 1, c, j ); + int m, k, c3; + for ( m = 0; m < n; m++ ) + { + int ObjM = p->nVars + m + 1; + if ( j + 1 >= ObjM ) + continue; + for ( k = j + 1; k < ObjM; k++ ) + for ( c3 = 0; c3 < 2; c3++ ) + { + int VarLargePrev = Exa9_ManSelVar( p, m, 1, c3, k ); + int pLits[2] = { Abc_Var2Lit( VarLargeThis, 1 ), Abc_Var2Lit( VarLargePrev, 1 ) }; + if ( !Exa9_KissatAddClause( p, pLits, 2 ) ) + { + Vec_IntFree( vLits ); + Vec_IntFree( vAux ); + Vec_IntFree( vUse ); + return 0; + } + } + } + } + // forbid duplicate fanin pairs across nodes (respecting polarity) + for ( int m = 0; m < n; m++ ) + { + int j2, c2, ObjM = p->nVars + m + 1; + for ( j = 1; j + 1 < ObjM; j++ ) + for ( j2 = j + 1; j2 < ObjM; j2++ ) + for ( c = 0; c < 2; c++ ) + for ( c2 = 0; c2 < 2; c2++ ) + { + int VarN0 = Exa9_ManSelVar( p, n, 0, c, j ); + int VarN1 = Exa9_ManSelVar( p, n, 1, c2, j2 ); + int VarM0 = Exa9_ManSelVar( p, m, 0, c, j ); + int VarM1 = Exa9_ManSelVar( p, m, 1, c2, j2 ); + int pLits4[4] = { Abc_Var2Lit( VarN0, 1 ), Abc_Var2Lit( VarN1, 1 ), + Abc_Var2Lit( VarM0, 1 ), Abc_Var2Lit( VarM1, 1 ) }; + if ( !Exa9_KissatAddClause( p, pLits4, 4 ) ) + { + Vec_IntFree( vLits ); + Vec_IntFree( vAux ); + Vec_IntFree( vUse ); + return 0; + } + } + } + */ + } + // output connectivity (one-hot over all objects and two polarities) + Vec_IntClear( vLits ); + Vec_IntClear( vAux ); + for ( j = 1; j <= p->nObjs; j++ ) + for ( c = 0; c < 2; c++ ) + { + Vec_IntPush( vLits, Abc_Var2Lit( Exa9_ManSelVarOut(p, c, j), 0 ) ); + Vec_IntPush( vAux, Exa9_ManSelVarOutAux( p, c, j ) ); + } + if ( Vec_IntSize(vLits) == 0 || !Exa9_ManAddOneHot( p, vLits, vAux ) ) + { + Vec_IntFree( vLits ); + Vec_IntFree( vAux ); + Vec_IntFree( vUse ); + return 0; + } + // ensure each object (PI or internal) is used at least once as a fanin of some node/output + for ( j = 1; j <= p->nObjs; j++ ) + { + Vec_IntClear( vUse ); + for ( n = 0; n < p->nNodes; n++ ) + { + int Obj = p->nVars + n + 1; + if ( Obj <= j ) + continue; + for ( k = 0; k < 2; k++ ) + for ( c = 0; c < 2; c++ ) + Vec_IntPush( vUse, Abc_Var2Lit( Exa9_ManSelVar(p, n, k, c, j), 0 ) ); + } + for ( c = 0; c < 2; c++ ) + Vec_IntPush( vUse, Abc_Var2Lit( Exa9_ManSelVarOut(p, c, j), 0 ) ); + if ( Vec_IntSize(vUse) == 0 ) + continue; + if ( !Exa9_KissatAddClause( p, Vec_IntArray(vUse), Vec_IntSize(vUse) ) ) + { + Vec_IntFree( vLits ); + Vec_IntFree( vAux ); + Vec_IntFree( vUse ); + return 0; + } + } + Vec_IntFree( vLits ); + Vec_IntFree( vAux ); + Vec_IntFree( vUse ); + return 1; +} +static int Exa9_ManAddCnf( Exa9_Man_t * p, int iMint ) +{ + p->fCountStruct = 0; + int i, j, k, c; + // assign primary input values for this minterm + for ( i = 1; i <= p->nVars; i++ ) + { + int Value = (iMint >> (i-1)) & 1; + int VarOut = Exa9_ManValueVar( p, i, 2, iMint ); + if ( !Exa9_ManAddUnit( p, VarOut, !Value ) ) + return 0; + } + // internal nodes + for ( i = 0; i < p->nNodes; i++ ) + { + int Obj = p->nVars + i + 1; + int VarFan[2] = { Exa9_ManValueVar( p, Obj, 0, iMint ), Exa9_ManValueVar( p, Obj, 1, iMint ) }; + int VarOut = Exa9_ManValueVar( p, Obj, 2, iMint ); + for ( k = 0; k < 2; k++ ) + { + for ( j = 1; j < Obj; j++ ) + for ( c = 0; c < 2; c++ ) + { + int SelVar = Exa9_ManSelVar( p, i, k, c, j ); + int SrcVal = Exa9_ManValueVar( p, j, 2, iMint ); + if ( !Exa9_ManAddEquality( p, SelVar, VarFan[k], SrcVal, c ) ) + return 0; + } + } + // functionality clauses for a*b = out + { + int pLits1[2] = { Abc_Var2Lit( VarFan[0], 0 ), Abc_Var2Lit( VarOut, 1 ) }; + int pLits2[2] = { Abc_Var2Lit( VarFan[1], 0 ), Abc_Var2Lit( VarOut, 1 ) }; + int pLits3[3] = { Abc_Var2Lit( VarFan[0], 1 ), Abc_Var2Lit( VarFan[1], 1 ), Abc_Var2Lit( VarOut, 0 ) }; + if ( !Exa9_KissatAddClause( p, pLits1, 2 ) ) return 0; + if ( !Exa9_KissatAddClause( p, pLits2, 2 ) ) return 0; + if ( !Exa9_KissatAddClause( p, pLits3, 3 ) ) return 0; + } + } + // constrain the output to match the target function via selected source + { + int Value = Abc_TtGetBit( p->pTruth, iMint ); + for ( j = 1; j <= p->nObjs; j++ ) + for ( c = 0; c < 2; c++ ) + { + int SelVar = Exa9_ManSelVarOut( p, c, j ); + int SrcVal = Exa9_ManValueVar( p, j, 2, iMint ); + int pLits[2] = { Abc_Var2Lit( SelVar, 1 ), Abc_Var2Lit( SrcVal, (Value ^ c) ? 0 : 1 ) }; + if ( !Exa9_KissatAddClause( p, pLits, 2 ) ) + return 0; + } + } + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Exa9_ManFindFanin( Exa9_Man_t * p, int Obj, int k, int * pCompl ) +{ + int n = Obj - p->nVars - 1; + int j, c; + assert( Obj > p->nVars && n >= 0 && n < p->nNodes ); + for ( j = 1; j < Obj; j++ ) + for ( c = 0; c < 2; c++ ) + { + int Var = Exa9_ManSelVar( p, n, k, c, j ); + if ( Exa9_KissatVarValue(p, Var) ) + { + if ( pCompl ) + *pCompl = c; + return j; + } + } + assert( 0 ); + return -1; +} +static inline int Exa9_ManFindOutput( Exa9_Man_t * p, int * pCompl ) +{ + int j, c; + for ( j = 1; j <= p->nObjs; j++ ) + for ( c = 0; c < 2; c++ ) + if ( Exa9_KissatVarValue(p, Exa9_ManSelVarOut(p, c, j)) ) + { + if ( pCompl ) + *pCompl = c; + return j; + } + assert( 0 ); + return -1; +} +static int Exa9_ManEval( Exa9_Man_t * p ) +{ + int i, c0, c1, i0, i1; + int cOut, iOutObj; + for ( i = 1; i <= p->nVars; i++ ) + Abc_TtIthVar( Exa9_ManTruth(p, i), i-1, p->nVars ); + for ( i = p->nVars + 1; i <= p->nObjs; i++ ) + { + i0 = Exa9_ManFindFanin( p, i, 0, &c0 ); + i1 = Exa9_ManFindFanin( p, i, 1, &c1 ); + Abc_TtAndCompl( Exa9_ManTruth(p, i), Exa9_ManTruth(p, i0), c0, Exa9_ManTruth(p, i1), c1, p->nWords ); + } + iOutObj = Exa9_ManFindOutput( p, &cOut ); + if ( cOut ) + { + Abc_TtNot( Exa9_ManTruth(p, iOutObj), p->nWords ); + i0 = Abc_TtFindFirstDiffBit( Exa9_ManTruth(p, iOutObj), p->pTruth, p->nVars ); + Abc_TtNot( Exa9_ManTruth(p, iOutObj), p->nWords ); + return i0; + } + return Abc_TtFindFirstDiffBit( Exa9_ManTruth(p, iOutObj), p->pTruth, p->nVars ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static void Exa9_ManName( Exa9_Man_t * p, int Obj, char * pBuf, int fFinal ) +{ + if ( Obj <= p->nVars ) + sprintf( pBuf, "%c", 'a'+Obj-1 ); + else if ( fFinal ) + sprintf( pBuf, "F" ); + else + sprintf( pBuf, "%02d", Obj ); +} +static void Exa9_ManPrintSolution( Exa9_Man_t * p ) +{ + int i, c0, c1, i0, i1, cOut, iOutObj; + int nInv = 0; + char Buf0[16], Buf1[16]; + iOutObj = Exa9_ManFindOutput( p, &cOut ); + nInv += cOut; + for ( i = p->nVars + 1; i <= p->nObjs; i++ ) + { + Exa9_ManFindFanin( p, i, 0, &c0 ); + Exa9_ManFindFanin( p, i, 1, &c1 ); + nInv += c0 + c1; + } + printf( "Realization of given %d-input function using %d two-input and-nodes and %d inverters:\n", p->nVars, p->nNodes, nInv ); + if ( iOutObj <= p->nVars ) sprintf( Buf0, "%c", 'a'+iOutObj-1 ); + else sprintf( Buf0, "%c", 'A'+iOutObj-p->nVars-1 ); + printf( "F =%s%s\n", cOut ? " !" : " ", Buf0 ); + for ( i = p->nObjs; i > p->nVars; i-- ) + { + i0 = Exa9_ManFindFanin( p, i, 0, &c0 ); + i1 = Exa9_ManFindFanin( p, i, 1, &c1 ); + if ( i0 <= p->nVars ) sprintf( Buf0, "%c", 'a'+i0-1 ); + else sprintf( Buf0, "%c", 'A'+i0-p->nVars-1 ); + if ( i1 <= p->nVars ) sprintf( Buf1, "%c", 'a'+i1-1 ); + else sprintf( Buf1, "%c", 'A'+i1-p->nVars-1 ); + printf( "%c =%s%s & %s%s\n", 'A'+i-p->nVars-1, c0 ? " !" : " ", Buf0, c1 ? " !" : " ", Buf1 ); + } +} +static void Exa9_ManDumpBlif( Exa9_Man_t * p ) +{ + int i, c0, c1, i0, i1, cOut, iOutObj; + char pFileName[1000]; + char Buf0[16], Buf1[16], BufOut[16]; + char * pStr = Abc_UtilStrsav(p->pPars->pSymStr ? p->pPars->pSymStr : p->pPars->pTtStr); + if ( strlen(pStr) > 16 ) { + pStr[16] = '_'; + pStr[17] = '\0'; + } + sprintf( pFileName, "%s.blif", pStr ); + FILE * pFile = fopen( pFileName, "wb" ); + if ( pFile == NULL ) return; + fprintf( pFile, "# Realization of given %d-input function using %d two-input and-nodes synthesized by ABC on %s\n", p->nVars, p->nNodes, Extra_TimeStamp() ); + fprintf( pFile, ".model %s\n", pStr ); + fprintf( pFile, ".inputs" ); + for ( i = 0; i < p->nVars; i++ ) + fprintf( pFile, " %c", 'a'+i ); + fprintf( pFile, "\n.outputs F\n" ); + for ( i = p->nVars + 1; i <= p->nObjs; i++ ) + { + i0 = Exa9_ManFindFanin( p, i, 0, &c0 ); + i1 = Exa9_ManFindFanin( p, i, 1, &c1 ); + Exa9_ManName( p, i0, Buf0, 0 ); + Exa9_ManName( p, i1, Buf1, 0 ); + Exa9_ManName( p, i, BufOut, 0 ); + fprintf( pFile, ".names %s %s %s\n", Buf0, Buf1, BufOut ); + fprintf( pFile, "%d%d 1\n", !c0, !c1 ); + } + iOutObj = Exa9_ManFindOutput( p, &cOut ); + Exa9_ManName( p, iOutObj, Buf0, iOutObj == p->nObjs ); + fprintf( pFile, ".names %s F\n", Buf0 ); + fprintf( pFile, "%d 1\n", cOut ? 0 : 1 ); + fprintf( pFile, ".end\n\n" ); + fclose( pFile ); + if ( !p->pPars->fSilent ) printf( "Finished dumping the resulting network into file \"%s\".\n", pFileName ); + ABC_FREE( pStr ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Exa9_ManExactSynthesis( Bmc_EsPar_t * pPars ) +{ + extern int Exa9_ManExactSynthesisIter( Bmc_EsPar_t * pPars ); + if ( pPars->fMinNodes ) + return Exa9_ManExactSynthesisIter( pPars ); + if ( pPars->fVerbose && !pPars->fSilent ) + Abc_Print( 1, "Params: I = %d M = %d H = %d S = %d T = %d i = %d a = %d m = %d d = %d v = %d s = %d\n", + pPars->nVars, pPars->nNodes, pPars->n1HotAlgo, pPars->Seed, pPars->RuntimeLim, pPars->fUseIncr, pPars->fOnlyAnd, pPars->fMinNodes, pPars->fDumpBlif, pPars->fVerbose, pPars->fSilent ); + int status = KISSAT_UNDEC; + int Res = 0; + abctime clkTotal = Abc_Clock(); + Exa9_Man_t * p; + assert( pPars->nVars <= 14 ); + int nTruthWords = Abc_TtWordNum( pPars->nVars ); + word * pTruth = ABC_CALLOC( word, nTruthWords ); + assert( pTruth ); + if ( pPars->pSymStr ) { + word * pFun = Abc_TtSymFunGenerate( pPars->pSymStr, pPars->nVars ); + pPars->pTtStr = ABC_CALLOC( char, pPars->nVars > 2 ? (1 << (pPars->nVars-2)) + 1 : 2 ); + Extra_PrintHexadecimalString( pPars->pTtStr, (unsigned *)pFun, pPars->nVars ); + if ( !pPars->fSilent ) printf( "Generated symmetric function: %s\n", pPars->pTtStr ); + ABC_FREE( pFun ); + } + if ( pPars->pTtStr ) + Abc_TtReadHex( pTruth, pPars->pTtStr ); + else assert( 0 ); + if ( pPars->fUseIncr && !pPars->fSilent ) + printf( "Warning: Ignoring incremental option when using Kissat.\n" ); + pPars->fUseIncr = 0; + p = Exa9_ManAlloc( pPars, pTruth ); + if ( pPars->fVerbose && !pPars->fSilent ) { + int nStruct = p->nNodes * 4 * p->nObjs + 2 * p->nObjs; + int nAux = Exa9_ManCountAuxTotal( p ); + int nTotal = nStruct + nAux + p->nValVars; + const char * pAlgo = p->pPars->n1HotAlgo == 1 ? "seq" : (p->pPars->n1HotAlgo == 2 ? "bim" : (p->pPars->n1HotAlgo == 3 ? "cmd" : "naive")); + printf( "Variables: Structure = %6d. Uniqueness (%s) = %6d. Internal = %6d. Total = %6d.\n", + nStruct, pAlgo, nAux, p->nValVars, nTotal ); + //if ( pPars->Seed > 0 ) + // printf( "Kissat seed set to %d.\n", pPars->Seed ); + } + if ( Exa9_ManAddCnfStart( p ) ) + { + if ( pPars->fVerbose && !pPars->fSilent ) + { + int clausesPerMint = 0; + clausesPerMint += p->nVars; // PI assignments + for ( int i = 0; i < p->nNodes; i++ ) + { + int Obj = p->nVars + i + 1; + int choices = Obj - 1; + clausesPerMint += 2 /*fanins*/ * 2 /*polarity*/ * choices * 2; // two clauses per equality + clausesPerMint += 3; // functionality + } + clausesPerMint += 2 * p->nObjs; // output selector + const char * pAlgo = p->pPars->n1HotAlgo == 1 ? "seq" : (p->pPars->n1HotAlgo == 2 ? "bim" : (p->pPars->n1HotAlgo == 3 ? "cmd" : "naive")); + int internalTotal = clausesPerMint * p->nMints; + printf( "Clauses: Structure = %6d. Uniqueness (%s) = %6d. Internal = %6d. Total = %6d.\n", + p->nClausesStart, pAlgo, p->nClausesHot, internalTotal, p->nClausesStart + p->nClausesHot + internalTotal ); + } + if ( !pPars->fSilent ) + printf( "Running exact synthesis for %d-input function with %d two-input and-nodes...\n", p->nVars, p->nNodes ); + int iMint; + Vec_Int_t * vMints = Vec_IntAlloc( p->nMints ); + for ( iMint = 0; iMint < p->nMints; iMint++ ) + Vec_IntPush( vMints, iMint ); + if ( pPars->Seed > 0 ) + { + Abc_Random( pPars->Seed ); + for ( iMint = 1; iMint < p->nMints; iMint++ ) + { + int jMint = Abc_Random(0) % (iMint + 1); + int Temp = Vec_IntEntry( vMints, iMint ); + Vec_IntWriteEntry( vMints, iMint, Vec_IntEntry(vMints, jMint) ); + Vec_IntWriteEntry( vMints, jMint, Temp ); + } + } + status = KISSAT_UNSAT; + for ( iMint = 0; iMint < p->nMints; iMint++ ) + { + int Mint = Vec_IntEntry( vMints, iMint ); + if ( !Exa9_ManAddCnf( p, Mint ) ) + break; + } + Vec_IntFree( vMints ); + if ( iMint == p->nMints ) + { + if ( pPars->RuntimeLim ) + { + p->timeStop = Abc_Clock() + pPars->RuntimeLim * CLOCKS_PER_SEC; + kissat_set_terminate( p->pSat, p, Exa9_KissatTerminate ); + } + else + { + p->timeStop = 0; + kissat_set_terminate( p->pSat, NULL, NULL ); + } + status = kissat_solve( p->pSat ); + } + } + else + status = KISSAT_UNSAT; + + if ( status == KISSAT_SAT ) + { + int DiffMint = Exa9_ManEval( p ); + if ( DiffMint != -1 ) + printf( "******** Warning: Verification detected a mismatch at minterm %d.\n", DiffMint ); + Exa9_ManPrintSolution( p ); + if ( pPars->fDumpBlif ) + Exa9_ManDumpBlif( p ); + Res = 1; + } + else if ( status == KISSAT_UNSAT ) + { + if ( !p->pPars->fSilent ) + printf( "The problem has no solution.\n" ); + Res = 2; + } + else + { + Res = 0; + if ( pPars->RuntimeLim ) + printf( "The solver timed out after %d sec.\n", pPars->RuntimeLim ); + } + if ( !pPars->fSilent ) + Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal ); + if ( pPars->pSymStr ) + ABC_FREE( pPars->pTtStr ); + Exa9_ManFree( p ); + ABC_FREE( pTruth ); + return Res; +} + +int Exa9_ManExactSynthesisIter( Bmc_EsPar_t * pPars ) +{ + pPars->fMinNodes = 0; + int nNodeMin = pPars->nVars - 1; + int nNodeMax = pPars->nNodes, Result = 0; + for ( int n = nNodeMin; n <= nNodeMax; n++ ) { + //printf( "\nTrying M = %d:\n", n ); + printf( "\n" ); + pPars->nNodes = n; + Result = Exa9_ManExactSynthesis(pPars); + fflush( stdout ); + if ( Result == 1 ) + break; + } + return Result; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + +ABC_NAMESPACE_IMPL_END diff --git a/src/sat/bmc/module.make b/src/sat/bmc/module.make index e0e86212b..3bb7babf4 100644 --- a/src/sat/bmc/module.make +++ b/src/sat/bmc/module.make @@ -27,6 +27,7 @@ SRC += src/sat/bmc/bmcBCore.c \ src/sat/bmc/bmcMaj3.c \ src/sat/bmc/bmcMaj7.c \ src/sat/bmc/bmcMaj8.c \ + src/sat/bmc/bmcMaj9.c \ src/sat/bmc/bmcMaxi.c \ src/sat/bmc/bmcMesh.c \ src/sat/bmc/bmcMesh2.c \