From 1485e63ae3cc36d2840b5c2d1d7da38a88ee8928 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 7 Jan 2020 01:36:06 +0200 Subject: Allowing nodes and boxes to have more than 6 inputs in mfs2 and &mfs. --- src/aig/gia/giaMfs.c | 77 +++++++++++++++++++++------ src/base/abc/abcSop.c | 21 +++++--- src/base/abci/abc.c | 4 +- src/base/abci/abcMfs.c | 142 +++++++++++++++++++++++++++++++++++++++++++------ src/misc/tim/timMan.c | 2 +- src/opt/sfm/sfm.h | 2 +- src/opt/sfm/sfmCnf.c | 61 +++++++++++++++++---- src/opt/sfm/sfmInt.h | 4 +- src/opt/sfm/sfmLib.c | 2 +- src/opt/sfm/sfmNtk.c | 11 ++-- src/opt/sfm/sfmSat.c | 1 + 11 files changed, 270 insertions(+), 57 deletions(-) diff --git a/src/aig/gia/giaMfs.c b/src/aig/gia/giaMfs.c index 2d9d09e8..69f6ee7a 100644 --- a/src/aig/gia/giaMfs.c +++ b/src/aig/gia/giaMfs.c @@ -46,7 +46,7 @@ ABC_NAMESPACE_IMPL_START ***********************************************************************/ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p ) { - word uTruth, uTruths6[6] = { + word uTruth, * pTruth, uTruths6[6] = { ABC_CONST(0xAAAAAAAAAAAAAAAA), ABC_CONST(0xCCCCCCCCCCCCCCCC), ABC_CONST(0xF0F0F0F0F0F0F0F0), @@ -60,6 +60,8 @@ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p ) Vec_Str_t * vEmpty; // mfs data Vec_Wrd_t * vTruths; // mfs data Vec_Int_t * vArray; + Vec_Int_t * vStarts; + Vec_Wrd_t * vTruths2; Vec_Int_t * vLeaves; Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime; int nBoxes = Gia_ManBoxNum(p), nVars; @@ -67,6 +69,9 @@ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p ) int nRealPos = nBoxes ? Tim_ManPoNum(pManTime) : Gia_ManPoNum(p); int i, j, k, curCi, curCo, nBoxIns, nBoxOuts; int Id, iFan, nMfsVars, nBbIns = 0, nBbOuts = 0, Counter = 0; + int nLutSizeMax = Gia_ManLutSizeMax( p ); + nLutSizeMax = Abc_MaxInt( nLutSizeMax, 6 ); + assert( nLutSizeMax < 16 ); //assert( !p->pAigExtra || Gia_ManPiNum(p->pAigExtra) <= 6 ); if ( pManTime ) Tim_ManBlackBoxIoNum( pManTime, &nBbIns, &nBbOuts ); // skip PIs due to box outputs @@ -77,6 +82,8 @@ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p ) vFixed = Vec_StrStart( nMfsVars ); vEmpty = Vec_StrStart( nMfsVars ); vTruths = Vec_WrdStart( nMfsVars ); + vStarts = Vec_IntStart( nMfsVars ); + vTruths2 = Vec_WrdAlloc( 10000 ); // set internal PIs Gia_ManCleanCopyArray( p ); Gia_ManForEachCiId( p, Id, i ) @@ -86,8 +93,8 @@ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p ) Vec_WrdWriteEntry( vTruths, Counter, (word)0 ); Gia_ObjSetCopyArray( p, 0, Counter++ ); // set internal LUTs - vLeaves = Vec_IntAlloc( 6 ); - Gia_ObjComputeTruthTableStart( p, 6 ); + vLeaves = Vec_IntAlloc( nLutSizeMax ); + Gia_ObjComputeTruthTableStart( p, nLutSizeMax ); Gia_ManForEachLut( p, Id ) { Vec_IntClear( vLeaves ); @@ -99,12 +106,22 @@ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p ) Vec_IntPush( vArray, Gia_ObjCopyArray(p, iFan) ); Vec_IntPush( vLeaves, iFan ); } - assert( Vec_IntSize(vLeaves) <= 6 ); + assert( Vec_IntSize(vLeaves) < 16 ); assert( Vec_IntSize(vLeaves) == Gia_ObjLutSize(p, Id) ); - uTruth = *Gia_ObjComputeTruthTableCut( p, Gia_ManObj(p, Id), vLeaves ); - nVars = Abc_Tt6MinBase( &uTruth, Vec_IntArray(vArray), Vec_IntSize(vArray) ); +// uTruth = *Gia_ObjComputeTruthTableCut( p, Gia_ManObj(p, Id), vLeaves ); +// nVars = Abc_Tt6MinBase( &uTruth, Vec_IntArray(vArray), Vec_IntSize(vArray) ); + pTruth = Gia_ObjComputeTruthTableCut( p, Gia_ManObj(p, Id), vLeaves ); + nVars = Abc_TtMinBase( pTruth, Vec_IntArray(vArray), Vec_IntSize(vArray), Vec_IntSize(vLeaves) ); Vec_IntShrink( vArray, nVars ); - Vec_WrdWriteEntry( vTruths, Counter, uTruth ); + if ( nVars <= 6 ) + Vec_WrdWriteEntry( vTruths, Counter, pTruth[0] ); + else + { + int w, nWords = Abc_Truth6WordNum( nVars ); + Vec_IntWriteEntry( vStarts, Counter, Vec_WrdSize(vTruths2) ); + for ( w = 0; w < nWords; w++ ) + Vec_WrdPush( vTruths2, pTruth[w] ); + } if ( Gia_ObjLutIsMux(p, Id) ) { Vec_StrWriteEntry( vFixed, Counter, (char)1 ); @@ -136,7 +153,8 @@ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p ) if ( p->pAigExtra ) { int iBbIn = 0, iBbOut = 0; - Gia_ObjComputeTruthTableStart( p->pAigExtra, 6 ); + assert( Gia_ManCiNum(p->pAigExtra) < 16 ); + Gia_ObjComputeTruthTableStart( p->pAigExtra, Gia_ManCiNum(p->pAigExtra) ); curCi = nRealPis; curCo = 0; for ( k = 0; k < nBoxes; k++ ) @@ -148,7 +166,7 @@ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p ) for ( i = 0; i < nBoxIns; i++ ) Vec_IntPush( vLeaves, Gia_ObjId(p->pAigExtra, Gia_ManCi(p->pAigExtra, i)) ); // iterate through box outputs - if ( !Tim_ManBoxIsBlack(pManTime, k) && Tim_ManBoxInputNum(pManTime, k) <= 6 ) + if ( !Tim_ManBoxIsBlack(pManTime, k) ) //&& Tim_ManBoxInputNum(pManTime, k) <= 6 ) { for ( j = 0; j < nBoxOuts; j++ ) { @@ -168,17 +186,39 @@ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p ) // box output in the extra manager pObjExtra = Gia_ManCo( p->pAigExtra, curCi - nRealPis + j ); // compute truth table + pTruth = NULL; if ( Gia_ObjFaninId0p(p->pAigExtra, pObjExtra) == 0 ) + { uTruth = 0; + uTruth = Gia_ObjFaninC0(pObjExtra) ? ~uTruth : uTruth; + pTruth = &uTruth; + } else if ( Gia_ObjIsCi(Gia_ObjFanin0(pObjExtra)) ) + { uTruth = uTruths6[Gia_ObjCioId(Gia_ObjFanin0(pObjExtra))]; + uTruth = Gia_ObjFaninC0(pObjExtra) ? ~uTruth : uTruth; + pTruth = &uTruth; + } else - uTruth = *Gia_ObjComputeTruthTableCut( p->pAigExtra, Gia_ObjFanin0(pObjExtra), vLeaves ); - uTruth = Gia_ObjFaninC0(pObjExtra) ? ~uTruth : uTruth; + { + pTruth = Gia_ObjComputeTruthTableCut( p->pAigExtra, Gia_ObjFanin0(pObjExtra), vLeaves ); + if ( Gia_ObjFaninC0(pObjExtra) ) + Abc_TtNot( pTruth, Abc_Truth6WordNum(Vec_IntSize(vLeaves)) ); + } + //uTruth = Gia_ObjFaninC0(pObjExtra) ? ~uTruth : uTruth; //Dau_DsdPrintFromTruth( &uTruth, Vec_IntSize(vArray) ); - nVars = Abc_Tt6MinBase( &uTruth, Vec_IntArray(vArray), Vec_IntSize(vArray) ); + //nVars = Abc_Tt6MinBase( &uTruth, Vec_IntArray(vArray), Vec_IntSize(vArray) ); + nVars = Abc_TtMinBase( pTruth, Vec_IntArray(vArray), Vec_IntSize(vArray), Vec_IntSize(vLeaves) ); Vec_IntShrink( vArray, nVars ); - Vec_WrdWriteEntry( vTruths, Counter, uTruth ); + if ( nVars <= 6 ) + Vec_WrdWriteEntry( vTruths, Counter, pTruth[0] ); + else + { + int w, nWords = Abc_Truth6WordNum( nVars ); + Vec_IntWriteEntry( vStarts, Counter, Vec_WrdSize(vTruths2) ); + for ( w = 0; w < nWords; w++ ) + Vec_WrdPush( vTruths2, pTruth[w] ); + } } } else // create buffers for black box inputs and outputs @@ -230,7 +270,7 @@ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p ) } // finalize Vec_IntFree( vLeaves ); - return Sfm_NtkConstruct( vFanins, nBbOuts + nRealPis, nRealPos + nBbIns, vFixed, vEmpty, vTruths ); + return Sfm_NtkConstruct( vFanins, nBbOuts + nRealPis, nRealPos + nBbIns, vFixed, vEmpty, vTruths, vStarts, vTruths2 ); } /**Function************************************************************* @@ -464,11 +504,16 @@ Gia_Man_t * Gia_ManPerformMfs( Gia_Man_t * p, Sfm_Par_t * pPars ) Abc_Print( 1, "Timing manager is given but there is no GIA of boxes.\n" ); return NULL; } + if ( p->pManTime != NULL && p->pAigExtra != NULL && Gia_ManCiNum(p->pAigExtra) > 15 ) + { + Abc_Print( 1, "Currently \"&mfs\" cannot process the network containing white-boxes with more than 15 inputs.\n" ); + return NULL; + } // count fanouts nFaninMax = Gia_ManLutSizeMax( p ); - if ( nFaninMax > 6 ) + if ( nFaninMax > 15 ) { - Abc_Print( 1, "Currently \"&mfs\" cannot process the network containing nodes with more than 6 fanins.\n" ); + Abc_Print( 1, "Currently \"&mfs\" cannot process the network containing nodes with more than 15 fanins.\n" ); return NULL; } // collect information diff --git a/src/base/abc/abcSop.c b/src/base/abc/abcSop.c index b0ce2ab7..b91214af 100644 --- a/src/base/abc/abcSop.c +++ b/src/base/abc/abcSop.c @@ -457,12 +457,21 @@ char * Abc_SopCreateFromIsop( Mem_Flex_t * pMan, int nVars, Vec_Int_t * vCover ) char * Abc_SopCreateFromTruthIsop( Mem_Flex_t * pMan, int nVars, word * pTruth, Vec_Int_t * vCover ) { char * pSop = NULL; - assert( nVars <= 6 ); - if ( pTruth[0] == 0 ) - pSop = Abc_SopRegister( pMan, " 0\n" ); - else if ( ~pTruth[0] == 0 ) - pSop = Abc_SopRegister( pMan, " 1\n" ); - else + int w, nWords = Abc_Truth6WordNum( nVars ); + assert( nVars < 16 ); + + for ( w = 0; w < nWords; w++ ) + if ( pTruth[w] ) + break; + if ( w == nWords ) + return Abc_SopRegister( pMan, " 0\n" ); + + for ( w = 0; w < nWords; w++ ) + if ( ~pTruth[w] ) + break; + if ( w == nWords ) + return Abc_SopRegister( pMan, " 1\n" ); + { int RetValue = Kit_TruthIsop( (unsigned *)pTruth, nVars, vCover, 1 ); assert( nVars > 0 ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 3dba557c..5df604cc 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -44822,9 +44822,9 @@ int Abc_CommandAbc9Mfs( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9Mfs(): The current AIG has no mapping.\n" ); return 0; } - if ( Gia_ManLutSizeMax(pAbc->pGia) > 6 ) + if ( Gia_ManLutSizeMax(pAbc->pGia) > 15 ) { - Abc_Print( -1, "Abc_CommandAbc9Mfs(): The current mapping has nodes with more than 6 inputs. Cannot use \"mfs\".\n" ); + Abc_Print( -1, "Abc_CommandAbc9Mfs(): The current mapping has nodes with more than 15 inputs. Cannot use \"mfs\".\n" ); return 0; } /* diff --git a/src/base/abci/abcMfs.c b/src/base/abci/abcMfs.c index 5c566074..d91bda66 100644 --- a/src/base/abci/abcMfs.c +++ b/src/base/abci/abcMfs.c @@ -80,6 +80,55 @@ Vec_Ptr_t * Abc_NtkAssignIDs2( Abc_Ntk_t * pNtk ) return vNodes; } +/**Function************************************************************* + + Synopsis [Assign truth table sizes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Abc_NtkAssignStarts( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, int * pnTotal ) +{ + Abc_Obj_t * pObj; int i, Counter = 0; + Vec_Int_t * vStarts = Vec_IntStart( Abc_NtkObjNum(pNtk) ); + Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i ) + { + Vec_IntWriteEntry( vStarts, pObj->iTemp, Counter ); + Counter += Abc_Truth6WordNum( Abc_ObjFaninNum(pObj) ); + } + *pnTotal = Counter; + return vStarts; +} + +void Abc_NtkFillTruthStore( word TruthStore[16][1<<10] ) +{ + if ( TruthStore[0][0] == 0 ) + { + static word Truth6[6] = { + 0xAAAAAAAAAAAAAAAA, + 0xCCCCCCCCCCCCCCCC, + 0xF0F0F0F0F0F0F0F0, + 0xFF00FF00FF00FF00, + 0xFFFF0000FFFF0000, + 0xFFFFFFFF00000000 + }; + int nVarsMax = 16; + int nWordsMax = (1 << 10); + int i, k; + assert( nVarsMax <= 16 ); + for ( i = 0; i < 6; i++ ) + for ( k = 0; k < nWordsMax; k++ ) + TruthStore[i][k] = Truth6[i]; + for ( i = 6; i < nVarsMax; i++ ) + for ( k = 0; k < nWordsMax; k++ ) + TruthStore[i][k] = ((k >> (i-6)) & 1) ? ~(word)0 : 0; + } +} + /**Function************************************************************* Synopsis [Extracts information about the network.] @@ -93,28 +142,59 @@ Vec_Ptr_t * Abc_NtkAssignIDs2( Abc_Ntk_t * pNtk ) ***********************************************************************/ Sfm_Ntk_t * Abc_NtkExtractMfs( Abc_Ntk_t * pNtk, int nFirstFixed ) { + word TruthStore[16][1<<10] = {{0}}, * pTruths[16] = {NULL}, pCube[1<<10] = {0}; Vec_Ptr_t * vNodes; Vec_Wec_t * vFanins; Vec_Str_t * vFixed; Vec_Wrd_t * vTruths; Vec_Int_t * vArray; + Vec_Int_t * vStarts; + Vec_Wrd_t * vTruths2; Abc_Obj_t * pObj, * pFanin; - int i, k, nObjs; + int i, k, nObjs, nTotal = 0; vNodes = nFirstFixed ? Abc_NtkAssignIDs2(pNtk) : Abc_NtkAssignIDs(pNtk); nObjs = Abc_NtkCiNum(pNtk) + Vec_PtrSize(vNodes) + Abc_NtkCoNum(pNtk); vFanins = Vec_WecStart( nObjs ); vFixed = Vec_StrStart( nObjs ); vTruths = Vec_WrdStart( nObjs ); + vStarts = Abc_NtkAssignStarts( pNtk, vNodes, &nTotal ); + vTruths2= Vec_WrdStart( nTotal ); + Abc_NtkFillTruthStore( TruthStore ); + for ( i = 0; i < 16; i++ ) + pTruths[i] = TruthStore[i]; Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i ) { - word uTruth = Abc_SopToTruth((char *)pObj->pData, Abc_ObjFaninNum(pObj)); - Vec_WrdWriteEntry( vTruths, pObj->iTemp, uTruth ); - if ( uTruth == 0 || ~uTruth == 0 ) - continue; + if ( Abc_ObjFaninNum(pObj) <= 6 ) + { + word uTruth = Abc_SopToTruth((char *)pObj->pData, Abc_ObjFaninNum(pObj)); + Vec_WrdWriteEntry( vTruths, pObj->iTemp, uTruth ); + if ( uTruth == 0 || ~uTruth == 0 ) + continue; + } + else + { + int nWords = Abc_Truth6WordNum( Abc_ObjFaninNum(pObj) ); + int Offset = Vec_IntEntry( vStarts, pObj->iTemp ); + word * pRes = Vec_WrdEntryP( vTruths2, Offset ); + Abc_SopToTruthBig( (char *)pObj->pData, Abc_ObjFaninNum(pObj), pTruths, pCube, pRes ); + // check const0 + for ( k = 0; k < nWords; k++ ) + if ( pRes[k] ) + break; + if ( k == nWords ) + continue; + // check const1 + for ( k = 0; k < nWords; k++ ) + if ( ~pRes[k] ) + break; + if ( k == nWords ) + continue; + } vArray = Vec_WecEntry( vFanins, pObj->iTemp ); Vec_IntGrow( vArray, Abc_ObjFaninNum(pObj) ); Abc_ObjForEachFanin( pObj, pFanin, k ) Vec_IntPush( vArray, pFanin->iTemp ); + //Vec_IntPrint( vArray ); } Abc_NtkForEachCo( pNtk, pObj, i ) { @@ -131,28 +211,58 @@ Sfm_Ntk_t * Abc_NtkExtractMfs( Abc_Ntk_t * pNtk, int nFirstFixed ) // for ( i = Abc_NtkCiNum(pNtk); i + Abc_NtkCoNum(pNtk) < Abc_NtkObjNum(pNtk); i++ ) // if ( rand() % 10 == 0 ) // Vec_StrWriteEntry( vFixed, i, (char)1 ); - return Sfm_NtkConstruct( vFanins, Abc_NtkCiNum(pNtk), Abc_NtkCoNum(pNtk), vFixed, NULL, vTruths ); + return Sfm_NtkConstruct( vFanins, Abc_NtkCiNum(pNtk), Abc_NtkCoNum(pNtk), vFixed, NULL, vTruths, vStarts, vTruths2 ); } Sfm_Ntk_t * Abc_NtkExtractMfs2( Abc_Ntk_t * pNtk, int iPivot ) { + word TruthStore[16][1<<10] = {{0}}, * pTruths[16] = {NULL}, pCube[1<<10] = {0}; Vec_Ptr_t * vNodes; Vec_Wec_t * vFanins; Vec_Str_t * vFixed; Vec_Wrd_t * vTruths; Vec_Int_t * vArray; + Vec_Int_t * vStarts; + Vec_Wrd_t * vTruths2; Abc_Obj_t * pObj, * pFanin; - int i, k, nObjs; + int i, k, nObjs, nTotal = 0; vNodes = Abc_NtkAssignIDs2(pNtk); nObjs = Abc_NtkCiNum(pNtk) + Vec_PtrSize(vNodes) + Abc_NtkCoNum(pNtk); vFanins = Vec_WecStart( nObjs ); vFixed = Vec_StrStart( nObjs ); vTruths = Vec_WrdStart( nObjs ); + vStarts = Abc_NtkAssignStarts( pNtk, vNodes, &nTotal ); + vTruths2= Vec_WrdAlloc( nTotal ); + Abc_NtkFillTruthStore( TruthStore ); + for ( i = 0; i < 16; i++ ) + pTruths[i] = TruthStore[i]; Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i ) { - word uTruth = Abc_SopToTruth((char *)pObj->pData, Abc_ObjFaninNum(pObj)); - Vec_WrdWriteEntry( vTruths, pObj->iTemp, uTruth ); - if ( uTruth == 0 || ~uTruth == 0 ) - continue; + if ( Abc_ObjFaninNum(pObj) <= 6 ) + { + word uTruth = Abc_SopToTruth((char *)pObj->pData, Abc_ObjFaninNum(pObj)); + Vec_WrdWriteEntry( vTruths, pObj->iTemp, uTruth ); + if ( uTruth == 0 || ~uTruth == 0 ) + continue; + } + else + { + int nWords = Abc_Truth6WordNum( Abc_ObjFaninNum(pObj) ); + int Offset = Vec_IntEntry( vStarts, pObj->iTemp ); + word * pRes = Vec_WrdEntryP( vTruths2, Offset ); + Abc_SopToTruthBig( (char *)pObj->pData, Abc_ObjFaninNum(pObj), pTruths, pCube, pRes ); + // check const0 + for ( k = 0; k < nWords; k++ ) + if ( pRes[k] ) + break; + if ( k == nWords ) + continue; + // check const1 + for ( k = 0; k < nWords; k++ ) + if ( ~pRes[k] ) + break; + if ( k == nWords ) + continue; + } vArray = Vec_WecEntry( vFanins, pObj->iTemp ); Vec_IntGrow( vArray, Abc_ObjFaninNum(pObj) ); Abc_ObjForEachFanin( pObj, pFanin, k ) @@ -170,7 +280,7 @@ Sfm_Ntk_t * Abc_NtkExtractMfs2( Abc_Ntk_t * pNtk, int iPivot ) Abc_NtkForEachNode( pNtk, pObj, i ) if ( i >= iPivot ) Vec_StrWriteEntry( vFixed, pObj->iTemp, (char)1 ); - return Sfm_NtkConstruct( vFanins, Abc_NtkCiNum(pNtk), Abc_NtkCoNum(pNtk), vFixed, NULL, vTruths ); + return Sfm_NtkConstruct( vFanins, Abc_NtkCiNum(pNtk), Abc_NtkCoNum(pNtk), vFixed, NULL, vTruths, vStarts, vTruths2 ); } /**Function************************************************************* @@ -243,9 +353,9 @@ int Abc_NtkPerformMfs( Abc_Ntk_t * pNtk, Sfm_Par_t * pPars ) Abc_NtkSweep( pNtk, 0 ); // count fanouts nFaninMax = Abc_NtkGetFaninMax( pNtk ); - if ( nFaninMax > 6 ) + if ( nFaninMax > 15 ) { - Abc_Print( 1, "Currently \"mfs\" cannot process the network containing nodes with more than 6 fanins.\n" ); + Abc_Print( 1, "Currently \"mfs\" cannot process the network containing nodes with more than 15 fanins.\n" ); return 1; } if ( !Abc_NtkHasSop(pNtk) ) @@ -424,9 +534,9 @@ int Abc_NtkMfsAfterICheck( Abc_Ntk_t * p, int nFrames, int nFramesAdd, Vec_Int_t assert( Abc_NtkIsLogic(p) ); // count fanouts nFaninMax = Abc_NtkGetFaninMax( p ); - if ( nFaninMax > 6 ) + if ( nFaninMax > 15 ) { - Abc_Print( 1, "Currently \"mfs\" cannot process the network containing nodes with more than 6 fanins.\n" ); + Abc_Print( 1, "Currently \"mfs\" cannot process the network containing nodes with more than 15 fanins.\n" ); return 0; } if ( !Abc_NtkHasSop(p) ) diff --git a/src/misc/tim/timMan.c b/src/misc/tim/timMan.c index 2b6ba6dc..151bf91d 100644 --- a/src/misc/tim/timMan.c +++ b/src/misc/tim/timMan.c @@ -738,7 +738,7 @@ void Tim_ManBlackBoxIoNum( Tim_Man_t * p, int * pnBbIns, int * pnBbOuts ) if ( Tim_ManBoxNum(p) ) Tim_ManForEachBox( p, pBox, i ) { - if ( !pBox->fBlack && pBox->nInputs <= 6 ) + if ( !pBox->fBlack )//&& pBox->nInputs <= 6 ) continue; *pnBbIns += Tim_ManBoxInputNum( p, i ); *pnBbOuts += Tim_ManBoxOutputNum( p, i ); diff --git a/src/opt/sfm/sfm.h b/src/opt/sfm/sfm.h index 002778dc..1aa8b7d0 100644 --- a/src/opt/sfm/sfm.h +++ b/src/opt/sfm/sfm.h @@ -87,7 +87,7 @@ struct Sfm_Par_t_ extern void Sfm_ParSetDefault( Sfm_Par_t * pPars ); extern int Sfm_NtkPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars ); /*=== sfmNtk.c ==========================================================*/ -extern Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t * vFixed, Vec_Str_t * vEmpty, Vec_Wrd_t * vTruths ); +extern Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t * vFixed, Vec_Str_t * vEmpty, Vec_Wrd_t * vTruths, Vec_Int_t * vStarts, Vec_Wrd_t * vTruths2 ); extern void Sfm_NtkFree( Sfm_Ntk_t * p ); extern Vec_Int_t * Sfm_NodeReadFanins( Sfm_Ntk_t * p, int i ); extern word * Sfm_NodeReadTruth( Sfm_Ntk_t * p, int i ); diff --git a/src/opt/sfm/sfmCnf.c b/src/opt/sfm/sfmCnf.c index ce2f34b8..f6d434f8 100644 --- a/src/opt/sfm/sfmCnf.c +++ b/src/opt/sfm/sfmCnf.c @@ -68,24 +68,63 @@ void Sfm_PrintCnf( Vec_Str_t * vCnf ) SeeAlso [] ***********************************************************************/ -int Sfm_TruthToCnf( word Truth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vCnf ) +int Sfm_TruthToCnf( word Truth, word * pTruth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vCnf ) { + int w, nWords = Abc_Truth6WordNum( nVars ); Vec_StrClear( vCnf ); - if ( Truth == 0 || ~Truth == 0 ) + if ( nVars <= 6 ) { -// assert( nVars == 0 ); - Vec_StrPush( vCnf, (char)(Truth == 0) ); - Vec_StrPush( vCnf, (char)-1 ); - return 1; + if ( Truth == 0 || ~Truth == 0 ) + { + //assert( nVars == 0 ); + Vec_StrPush( vCnf, (char)(Truth == 0) ); + Vec_StrPush( vCnf, (char)-1 ); + return 1; + } + } + else + { + // const0 + for ( w = 0; w < nWords; w++ ) + if ( pTruth[w] ) + break; + if ( w == nWords ) + { + Vec_StrPush( vCnf, (char)1 ); + Vec_StrPush( vCnf, (char)-1 ); + return 1; + } + // const1 + for ( w = 0; w < nWords; w++ ) + if ( ~pTruth[w] ) + break; + if ( w == nWords ) + { + Vec_StrPush( vCnf, (char)0 ); + Vec_StrPush( vCnf, (char)-1 ); + return 1; + } } - else { int i, k, c, RetValue, Literal, Cube, nCubes = 0; assert( nVars > 0 ); for ( c = 0; c < 2; c ++ ) { - Truth = c ? ~Truth : Truth; - RetValue = Kit_TruthIsop( (unsigned *)&Truth, nVars, vCover, 0 ); + if ( nVars <= 6 ) + { + Truth = c ? ~Truth : Truth; + RetValue = Kit_TruthIsop( (unsigned *)&Truth, nVars, vCover, 0 ); + } + else + { + if ( c ) + for ( k = 0; k < nWords; k++ ) + pTruth[k] = ~pTruth[k]; + RetValue = Kit_TruthIsop( (unsigned *)pTruth, nVars, vCover, 0 ); + if ( c ) + for ( k = 0; k < nWords; k++ ) + pTruth[k] = ~pTruth[k]; + } assert( RetValue == 0 ); nCubes += Vec_IntSize( vCover ); Vec_IntForEachEntry( vCover, Cube, i ) @@ -129,7 +168,9 @@ Vec_Wec_t * Sfm_CreateCnf( Sfm_Ntk_t * p ) vCnfs = Vec_WecStart( p->nObjs ); Vec_WrdForEachEntryStartStop( p->vTruths, uTruth, i, p->nPis, Vec_WrdSize(p->vTruths)-p->nPos ) { - nCubes = Sfm_TruthToCnf( uTruth, Sfm_ObjFaninNum(p, i), p->vCover, vCnf ); + int Offset = Vec_IntEntry( p->vStarts, i ); + word * pRes = Vec_WrdSize(p->vTruths2) ? Vec_WrdEntryP( p->vTruths2, Offset ) : NULL; + nCubes = Sfm_TruthToCnf( uTruth, pRes, Sfm_ObjFaninNum(p, i), p->vCover, vCnf ); vCnfBase = (Vec_Str_t *)Vec_WecEntry( vCnfs, i ); Vec_StrGrow( vCnfBase, Vec_StrSize(vCnf) ); memcpy( Vec_StrArray(vCnfBase), Vec_StrArray(vCnf), (size_t)Vec_StrSize(vCnf) ); diff --git a/src/opt/sfm/sfmInt.h b/src/opt/sfm/sfmInt.h index 2b96d4bd..80edd54d 100644 --- a/src/opt/sfm/sfmInt.h +++ b/src/opt/sfm/sfmInt.h @@ -81,6 +81,8 @@ struct Sfm_Ntk_t_ Vec_Str_t * vEmpty; // transparent objects Vec_Wrd_t * vTruths; // truth tables Vec_Wec_t vFanins; // fanins + Vec_Int_t * vStarts; // offsets + Vec_Wrd_t * vTruths2; // truth tables (large) // attributes Vec_Wec_t vFanouts; // fanouts Vec_Int_t vLevels; // logic level @@ -195,7 +197,7 @@ extern void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars ); /*=== sfmCnf.c ==========================================================*/ extern void Sfm_PrintCnf( Vec_Str_t * vCnf ); -extern int Sfm_TruthToCnf( word Truth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vCnf ); +extern int Sfm_TruthToCnf( word Truth, word * pTruth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vCnf ); extern Vec_Wec_t * Sfm_CreateCnf( Sfm_Ntk_t * p ); extern void Sfm_TranslateCnf( Vec_Wec_t * vRes, Vec_Str_t * vCnf, Vec_Int_t * vFaninMap, int iPivotVar ); /*=== sfmCore.c ==========================================================*/ diff --git a/src/opt/sfm/sfmLib.c b/src/opt/sfm/sfmLib.c index afb4a48d..18ba0971 100644 --- a/src/opt/sfm/sfmLib.c +++ b/src/opt/sfm/sfmLib.c @@ -107,7 +107,7 @@ void Sfm_DecCreateCnf( Vec_Int_t * vGateSizes, Vec_Wrd_t * vGateFuncs, Vec_Wec_t vCover = Vec_IntAlloc( 100 ); Vec_WrdForEachEntry( vGateFuncs, uTruth, i ) { - nCubes = Sfm_TruthToCnf( uTruth, Vec_IntEntry(vGateSizes, i), vCover, vCnf ); + nCubes = Sfm_TruthToCnf( uTruth, NULL, Vec_IntEntry(vGateSizes, i), vCover, vCnf ); vCnfBase = (Vec_Str_t *)Vec_WecEntry( vGateCnfs, i ); Vec_StrGrow( vCnfBase, Vec_StrSize(vCnf) ); memcpy( Vec_StrArray(vCnfBase), Vec_StrArray(vCnf), (size_t)Vec_StrSize(vCnf) ); diff --git a/src/opt/sfm/sfmNtk.c b/src/opt/sfm/sfmNtk.c index 1ded0ede..d410aa0b 100644 --- a/src/opt/sfm/sfmNtk.c +++ b/src/opt/sfm/sfmNtk.c @@ -164,7 +164,7 @@ void Sfm_CreateLevelR( Vec_Wec_t * vFanouts, Vec_Int_t * vLevelsR, Vec_Str_t * v SeeAlso [] ***********************************************************************/ -Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t * vFixed, Vec_Str_t * vEmpty, Vec_Wrd_t * vTruths ) +Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t * vFixed, Vec_Str_t * vEmpty, Vec_Wrd_t * vTruths, Vec_Int_t * vStarts, Vec_Wrd_t * vTruths2 ) { Sfm_Ntk_t * p; Sfm_CheckConsistency( vFanins, nPis, nPos, vFixed ); @@ -178,6 +178,8 @@ Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t p->vEmpty = vEmpty; p->vTruths = vTruths; p->vFanins = *vFanins; + p->vStarts = vStarts; + p->vTruths2 = vTruths2; ABC_FREE( vFanins ); // attributes Sfm_CreateFanout( &p->vFanins, &p->vFanouts ); @@ -217,6 +219,8 @@ void Sfm_NtkFree( Sfm_Ntk_t * p ) Vec_StrFreeP( &p->vEmpty ); Vec_WrdFree( p->vTruths ); Vec_WecErase( &p->vFanins ); + Vec_IntFree( p->vStarts ); + Vec_WrdFree( p->vTruths2 ); // attributes Vec_WecErase( &p->vFanouts ); ABC_FREE( p->vLevels.pArray ); @@ -316,6 +320,7 @@ void Sfm_NtkUpdate( Sfm_Ntk_t * p, int iNode, int f, int iFaninNew, word uTruth int iFanin = Sfm_ObjFanin( p, iNode, f ); assert( Sfm_ObjIsNode(p, iNode) ); assert( iFanin != iFaninNew ); + assert( Sfm_ObjFaninNum(p, iNode) <= 6 ); if ( uTruth == 0 || ~uTruth == 0 ) { Sfm_ObjForEachFanin( p, iNode, iFanin, f ) @@ -341,7 +346,7 @@ void Sfm_NtkUpdate( Sfm_Ntk_t * p, int iNode, int f, int iFaninNew, word uTruth Sfm_NtkUpdateLevelR_rec( p, iFanin ); // update truth table Vec_WrdWriteEntry( p->vTruths, iNode, uTruth ); - Sfm_TruthToCnf( uTruth, Sfm_ObjFaninNum(p, iNode), p->vCover, (Vec_Str_t *)Vec_WecEntry(p->vCnfs, iNode) ); + Sfm_TruthToCnf( uTruth, NULL, Sfm_ObjFaninNum(p, iNode), p->vCover, (Vec_Str_t *)Vec_WecEntry(p->vCnfs, iNode) ); } /**Function************************************************************* @@ -361,7 +366,7 @@ Vec_Int_t * Sfm_NodeReadFanins( Sfm_Ntk_t * p, int i ) } word * Sfm_NodeReadTruth( Sfm_Ntk_t * p, int i ) { - return Vec_WrdEntryP( p->vTruths, i ); + return Sfm_ObjFaninNum(p, i) <= 6 ? Vec_WrdEntryP( p->vTruths, i ) : Vec_WrdEntryP( p->vTruths2, Vec_IntEntry(p->vStarts, i) ); } int Sfm_NodeReadFixed( Sfm_Ntk_t * p, int i ) { diff --git a/src/opt/sfm/sfmSat.c b/src/opt/sfm/sfmSat.c index 8bcb7f8a..6ccdd903 100644 --- a/src/opt/sfm/sfmSat.c +++ b/src/opt/sfm/sfmSat.c @@ -167,6 +167,7 @@ word Sfm_ComputeInterpolant( Sfm_Ntk_t * p ) sat_solver_setnvars( p->pSat, nVars + 1 ); pLits[0] = Abc_Var2Lit( Sfm_ObjSatVar(p, p->iPivotNode), 0 ); // F = 1 pLits[1] = Abc_Var2Lit( nVars, 0 ); // iNewLit + assert( Vec_IntSize(p->vDivIds) <= 6 ); while ( 1 ) { // find onset minterm -- cgit v1.2.3