From faf8d6ecea8e7b7030a13531b834522f9821ff30 Mon Sep 17 00:00:00 2001 From: Vinicius Callegaro Date: Tue, 8 Nov 2016 17:00:35 -0200 Subject: Disjoint-support decomposition with cofactoring and boolean difference analysis from V. Callegaro, F. S. Marranghello, M. G. A. Martins, R. P. Ribas and A. I. Reis, entitled "Bottom-up disjoint-support decomposition based on cofactor and boolean difference analysis" presented in ICCD'15. --- src/base/abci/abc.c | 3 +++ src/base/abci/abcDec.c | 22 +++++++++++++++++++++- 2 files changed, 24 insertions(+), 1 deletion(-) (limited to 'src/base/abci') diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 953a6c6a..ffcd5054 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -6212,6 +6212,9 @@ usage: Abc_Print( -2, "\t 3: disjoint-support decomposition with cofactoring\n" ); Abc_Print( -2, "\t 4: updated disjoint-support decomposition with cofactoring\n" ); Abc_Print( -2, "\t 5: enumerating decomposable variable sets\n" ); + Abc_Print( -2, "\t 6: disjoint-support decomposition with cofactoring and boolean difference analysis\n" ); + Abc_Print( -2, "\t from V. Callegaro, F. S. Marranghello, M. G. A. Martins, R. P. Ribas and A. I. Reis,\n"); + Abc_Print( -2, "\t \"Bottom-up disjoint-support decomposition based on cofactor and boolean difference analysis,\" ICCD'15.\n" ); Abc_Print( -2, "\t-N : the number of support variables (binary files only) [default = unused]\n" ); Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); diff --git a/src/base/abci/abcDec.c b/src/base/abci/abcDec.c index 919a46de..8bb04f16 100644 --- a/src/base/abci/abcDec.c +++ b/src/base/abci/abcDec.c @@ -26,6 +26,7 @@ #include "bool/kit/kit.h" #include "opt/dau/dau.h" #include "misc/util/utilTruth.h" +#include "opt/dsc/dsc.h" ABC_NAMESPACE_IMPL_START @@ -484,6 +485,8 @@ void Abc_TruthDecPerform( Abc_TtStore_t * p, int DecType, int fVerbose ) pAlgoName = "fast DSD"; else if ( DecType == 5 ) pAlgoName = "analysis"; + else if ( DecType == 6 ) + pAlgoName = "DSD ICCD'15"; if ( pAlgoName ) printf( "Applying %-10s to %8d func%s of %2d vars... ", @@ -577,6 +580,23 @@ void Abc_TruthDecPerform( Abc_TtStore_t * p, int DecType, int fVerbose ) if ( fVerbose ) printf( "\n" ); } + } else if ( DecType == 6 ) + { + char pDsd[DSC_MAX_STR]; + /* memory pool with a capacity of storing 3*nVars + truth-tables for negative and positive cofactors and + the boolean difference for each input variable */ + word *mem_pool = Dsc_alloc_pool(p->nVars); + for ( i = 0; i < p->nFuncs; i++ ) + { + if ( fVerbose ) + printf( "%7d : ", i ); + Dsc_Decompose(p->pFuncs[i], p->nVars, pDsd, mem_pool); + if ( fVerbose ) + printf( "%s\n", pDsd[0] ? pDsd : "NULL"); + nNodes += Dsc_CountAnds( pDsd ); + } + Dsc_free_pool(mem_pool); } else assert( 0 ); @@ -629,7 +649,7 @@ int Abc_DecTest( char * pFileName, int DecType, int nVarNum, int fVerbose ) printf( "Using truth tables from file \"%s\"...\n", pFileName ); if ( DecType == 0 ) { if ( nVarNum < 0 ) Abc_TtStoreTest( pFileName ); } - else if ( DecType >= 1 && DecType <= 5 ) + else if ( DecType >= 1 && DecType <= 6 ) Abc_TruthDecTest( pFileName, DecType, nVarNum, fVerbose ); else printf( "Unknown decomposition type value (%d).\n", DecType ); -- cgit v1.2.3 From c6afb9db639b7ce0ac714e4e63e629b4c8bf1ac1 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 9 Nov 2016 21:17:44 -0800 Subject: Equivalent fault detection code. --- src/base/abci/abc.c | 25 +- src/base/abci/abcDetect.c | 1066 ++++++++++++++++++++++++++++++++++++++++++++- 2 files changed, 1082 insertions(+), 9 deletions(-) (limited to 'src/base/abci') diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 953a6c6a..b1c81cd5 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -7237,21 +7237,28 @@ usage: ***********************************************************************/ int Abc_CommandDetect( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern void Abc_NtkDetectClassesTest( Abc_Ntk_t * pNtk, int fSeq, int fVerbose ); + extern void Abc_NtkDetectClassesTest( Abc_Ntk_t * pNtk, int fSeq, int fVerbose, int fVeryVerbose ); + extern void Abc_NtkGenFaultList( Abc_Ntk_t * pNtk, char * pFileName ); Abc_Ntk_t * pNtk; - int c, fSeq = 0, fVerbose = 0; + int c, fGen = 0, fSeq = 0, fVerbose = 0, fVeryVerbose = 0; pNtk = Abc_FrameReadNtk(pAbc); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "svh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "gsvwh" ) ) != EOF ) { switch ( c ) { + case 'g': + fGen ^= 1; + break; case 's': fSeq ^= 1; break; case 'v': fVerbose ^= 1; break; + case 'w': + fVeryVerbose ^= 1; + break; case 'h': goto usage; default: @@ -7268,14 +7275,22 @@ int Abc_CommandDetect( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Only applicable to a logic network.\n" ); return 1; } - Abc_NtkDetectClassesTest( pNtk, fSeq, fVerbose ); + if ( fGen ) + { + char * pFileName = Extra_FileNameGenericAppend(Abc_NtkSpec(pNtk), "_faults.txt"); + Abc_NtkGenFaultList( pNtk, pFileName ); + } + else + Abc_NtkDetectClassesTest( pNtk, fSeq, fVerbose, fVeryVerbose ); return 0; usage: - Abc_Print( -2, "usage: detect [-svh]\n" ); + Abc_Print( -2, "usage: detect [-gsvwh]\n" ); Abc_Print( -2, "\t detects properties of internal nodes\n" ); + Abc_Print( -2, "\t-g : toggle generating fault list for the given network [default = %s]\n", fGen? "yes": "no" ); Abc_Print( -2, "\t-s : toggle using sequential circuit information [default = %s]\n", fSeq? "yes": "no" ); Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-w : toggle printing equivalence classes [default = %s]\n", fVeryVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; } diff --git a/src/base/abci/abcDetect.c b/src/base/abci/abcDetect.c index c87169b5..b1a598cd 100644 --- a/src/base/abci/abcDetect.c +++ b/src/base/abci/abcDetect.c @@ -23,6 +23,8 @@ #include "misc/util/utilNam.h" #include "sat/cnf/cnf.h" #include "sat/bsat/satStore.h" +#include "map/mio/mio.h" +#include "map/mio/exp.h" ABC_NAMESPACE_IMPL_START @@ -31,7 +33,7 @@ ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// typedef enum { - ABC_FIN_NONE = 0, // 0: unknown + ABC_FIN_NONE = -100, // 0: unknown ABC_FIN_SA0, // 1: ABC_FIN_SA1, // 2: ABC_FIN_NEG, // 3: @@ -50,6 +52,49 @@ typedef enum { /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +/**Function************************************************************* + + Synopsis [Generates fault list for the given mapped network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkGenFaultList( Abc_Ntk_t * pNtk, char * pFileName ) +{ + Mio_Library_t * pLib = (Mio_Library_t *)pNtk->pManFunc; + Mio_Gate_t * pGate; + Abc_Obj_t * pObj; + int i, Count = 1; + FILE * pFile = fopen( pFileName, "wb" ); + if ( pFile == NULL ) + { + printf( "Cannot open file \"%s\" for writing.\n", pFileName ); + return; + } + assert( Abc_NtkIsMappedLogic(pNtk) ); + Abc_NtkForEachNode( pNtk, pObj, i ) + { + Mio_Gate_t * pGateObj = (Mio_Gate_t *)pObj->pData; + int nInputs = Mio_GateReadPinNum(pGateObj); + // add basic faults (SA0, SA1, NEG) + fprintf( pFile, "%d %s %s\n", Count, Abc_ObjName(pObj), "SA0" ), Count++; + fprintf( pFile, "%d %s %s\n", Count, Abc_ObjName(pObj), "SA1" ), Count++; + fprintf( pFile, "%d %s %s\n", Count, Abc_ObjName(pObj), "NEG" ), Count++; + // add other faults, which correspond to changing the given gate + // by another gate with the same support-size from the same library + Mio_LibraryForEachGate( pLib, pGate ) + if ( pGate != pGateObj && Mio_GateReadPinNum(pGate) == nInputs ) + fprintf( pFile, "%d %s %s\n", Count, Abc_ObjName(pObj), Mio_GateReadName(pGate) ), Count++; + } + printf( "Generated fault list \"%s\" for network \"%s\" with %d nodes and %d faults.\n", + pFileName, Abc_NtkName(pNtk), Abc_NtkNodeNum(pNtk), Count-1 ); + fclose( pFile ); +} + /**Function************************************************************* Synopsis [Recognize type.] @@ -61,6 +106,16 @@ typedef enum { SeeAlso [] ***********************************************************************/ +int Io_ReadFinTypeMapped( Mio_Library_t * pLib, char * pThis ) +{ + Mio_Gate_t * pGate = Mio_LibraryReadGateByName( pLib, pThis, NULL ); + if ( pGate == NULL ) + { + printf( "Cannot find gate \"%s\" in the current library.\n", pThis ); + return ABC_FIN_NONE; + } + return Mio_GateReadCell( pGate ); +} int Io_ReadFinType( char * pThis ) { if ( !strcmp(pThis, "SA0") ) return ABC_FIN_SA0; @@ -106,6 +161,7 @@ char * Io_WriteFinType( int Type ) ***********************************************************************/ Vec_Int_t * Io_ReadFins( Abc_Ntk_t * pNtk, char * pFileName, int fVerbose ) { + Mio_Library_t * pLib = (Mio_Library_t *)pNtk->pManFunc; char Buffer[1000]; Abc_Obj_t * pObj; Abc_Nam_t * pNam; @@ -142,6 +198,8 @@ Vec_Int_t * Io_ReadFins( Abc_Ntk_t * pNtk, char * pFileName, int fVerbose ) { // read line number char * pToken = strtok( Buffer, " \n\r\t" ); + if ( pToken == NULL ) + break; if ( nLines++ != atoi(pToken) ) { printf( "Line numbers are not consecutive. Quitting.\n" ); @@ -158,7 +216,15 @@ Vec_Int_t * Io_ReadFins( Abc_Ntk_t * pNtk, char * pFileName, int fVerbose ) } // read type pToken = strtok( NULL, " \n\r\t" ); - Type = Io_ReadFinType( pToken ); + if ( Abc_NtkIsMappedLogic(pNtk) ) + { + if ( !strcmp(pToken, "SA0") || !strcmp(pToken, "SA1") || !strcmp(pToken, "NEG") ) + Type = Io_ReadFinType( pToken ); + else + Type = Io_ReadFinTypeMapped( pLib, pToken ); + } + else + Type = Io_ReadFinType( pToken ); if ( Type == ABC_FIN_NONE ) { printf( "Cannot read type \"%s\" of object \"%s\".\n", pToken, Abc_ObjName(Abc_NtkObj(pNtk, iObj)) ); @@ -182,6 +248,987 @@ finish: } +/**Function************************************************************* + + Synopsis [Extend the network by adding second timeframe.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkFrameExtend( Abc_Ntk_t * pNtk ) +{ + Vec_Ptr_t * vFanins, * vNodes; + Abc_Obj_t * pObj, * pFanin, * pReset, * pEnable, * pSignal; + Abc_Obj_t * pResetN, * pEnableN, * pAnd0, * pAnd1, * pMux; + int i, k, iStartPo, nPisOld = Abc_NtkPiNum(pNtk), nPosOld = Abc_NtkPoNum(pNtk); + // skip if there are no flops + if ( pNtk->nConstrs == 0 ) + return; + assert( Abc_NtkPiNum(pNtk) >= pNtk->nConstrs ); + assert( Abc_NtkPoNum(pNtk) >= pNtk->nConstrs * 4 ); + // collect nodes + vNodes = Vec_PtrAlloc( Abc_NtkNodeNum(pNtk) ); + Abc_NtkForEachNode( pNtk, pObj, i ) + Vec_PtrPush( vNodes, pObj ); + // duplicate PIs + vFanins = Vec_PtrAlloc( 2 ); + Abc_NtkForEachPi( pNtk, pObj, i ) + { + if ( i == nPisOld ) + break; + if ( i < nPisOld - pNtk->nConstrs ) + { + Abc_NtkDupObj( pNtk, pObj, 0 ); + Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(pObj), "_frame1" ); + continue; + } + // create flop input + iStartPo = nPosOld + 4 * (i - nPisOld); + pReset = Abc_ObjFanin0( Abc_NtkPo( pNtk, iStartPo + 1 ) ); + pEnable = Abc_ObjFanin0( Abc_NtkPo( pNtk, iStartPo + 2 ) ); + pSignal = Abc_ObjFanin0( Abc_NtkPo( pNtk, iStartPo + 3 ) ); + pResetN = Abc_NtkCreateNodeInv( pNtk, pReset ); + pEnableN = Abc_NtkCreateNodeInv( pNtk, pEnable ); + Vec_PtrFillTwo( vFanins, 2, pEnableN, pObj ); + pAnd0 = Abc_NtkCreateNodeAnd( pNtk, vFanins ); + Vec_PtrFillTwo( vFanins, 2, pEnable, pSignal ); + pAnd1 = Abc_NtkCreateNodeAnd( pNtk, vFanins ); + Vec_PtrFillTwo( vFanins, 2, pAnd0, pAnd1 ); + pMux = Abc_NtkCreateNodeOr( pNtk, vFanins ); + Vec_PtrFillTwo( vFanins, 2, pResetN, pMux ); + pObj->pCopy = Abc_NtkCreateNodeAnd( pNtk, vFanins ); + } + // duplicate internal nodes + Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i ) + Abc_NtkDupObj( pNtk, pObj, 0 ); + // connect objects + Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i ) + Abc_ObjForEachFanin( pObj, pFanin, k ) + Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy ); + // create new POs and reconnect flop inputs + Abc_NtkForEachPo( pNtk, pObj, i ) + { + if ( i == nPosOld ) + break; + if ( i < nPosOld - 4 * pNtk->nConstrs ) + { + Abc_NtkDupObj( pNtk, pObj, 0 ); + Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(pObj), "_frame1" ); + Abc_ObjAddFanin( pObj->pCopy, Abc_ObjFanin0(pObj)->pCopy ); + continue; + } + Abc_ObjPatchFanin( pObj, Abc_ObjFanin0(pObj), Abc_ObjFanin0(pObj)->pCopy ); + } + Vec_PtrFree( vFanins ); + Vec_PtrFree( vNodes ); +} + +/**Function************************************************************* + + Synopsis [Detect equivalence classes of nodes in terms of their TFO.] + + Description [Given is the logic network (pNtk) and the set of objects + (primary inputs or internal nodes) to be considered (vObjs), this function + returns a set of equivalence classes of these objects in terms of their + transitive fanout (TFO). Two objects belong to the same class if the set + of COs they feed into are the same.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkDetectObjClasses_rec( Abc_Obj_t * pObj, Vec_Int_t * vMap, Hsh_VecMan_t * pHash, Vec_Int_t * vTemp ) +{ + Vec_Int_t * vArray, * vSet; + Abc_Obj_t * pNext; int i; + // get the CO set for this object + int Entry = Vec_IntEntry(vMap, Abc_ObjId(pObj)); + if ( Entry != -1 ) // the set is already computed + return Entry; + // compute a new CO set + assert( Abc_ObjIsCi(pObj) || Abc_ObjIsNode(pObj) ); + // if there is no fanouts, the set of COs is empty + if ( Abc_ObjFanoutNum(pObj) == 0 ) + { + Vec_IntWriteEntry( vMap, Abc_ObjId(pObj), 0 ); + return 0; + } + // compute the set for the first fanout + Entry = Abc_NtkDetectObjClasses_rec( Abc_ObjFanout0(pObj), vMap, pHash, vTemp ); + if ( Abc_ObjFanoutNum(pObj) == 1 ) + { + Vec_IntWriteEntry( vMap, Abc_ObjId(pObj), Entry ); + return Entry; + } + vSet = Vec_IntAlloc( 16 ); + // initialize the set with that of first fanout + vArray = Hsh_VecReadEntry( pHash, Entry ); + Vec_IntClear( vSet ); + Vec_IntAppend( vSet, vArray ); + // iteratively add sets of other fanouts + Abc_ObjForEachFanout( pObj, pNext, i ) + { + if ( i == 0 ) + continue; + Entry = Abc_NtkDetectObjClasses_rec( pNext, vMap, pHash, vTemp ); + vArray = Hsh_VecReadEntry( pHash, Entry ); + Vec_IntTwoMerge2( vSet, vArray, vTemp ); + ABC_SWAP( Vec_Int_t, *vSet, *vTemp ); + } + // create or find new set and map the object into it + Entry = Hsh_VecManAdd( pHash, vSet ); + Vec_IntWriteEntry( vMap, Abc_ObjId(pObj), Entry ); + Vec_IntFree( vSet ); + return Entry; +} +Vec_Wec_t * Abc_NtkDetectObjClasses( Abc_Ntk_t * pNtk, Vec_Int_t * vObjs, Vec_Wec_t ** pvCos ) +{ + Vec_Wec_t * vClasses; // classes of equivalence objects from vObjs + Vec_Int_t * vClassMap; // mapping of each CO set into its class in vClasses + Vec_Int_t * vClass; // one equivalence class + Abc_Obj_t * pObj; + int i, iObj, SetId, ClassId; + // create hash table to hash sets of CO indexes + Hsh_VecMan_t * pHash = Hsh_VecManStart( 1000 ); + // create elementary sets (each composed of one CO) and map COs into them + Vec_Int_t * vMap = Vec_IntStartFull( Abc_NtkObjNumMax(pNtk) ); + Vec_Int_t * vSet = Vec_IntAlloc( 16 ); + assert( Abc_NtkIsLogic(pNtk) ); + // compute empty set + SetId = Hsh_VecManAdd( pHash, vSet ); + assert( SetId == 0 ); + Abc_NtkForEachCo( pNtk, pObj, i ) + { + Vec_IntFill( vSet, 1, Abc_ObjId(pObj) ); + SetId = Hsh_VecManAdd( pHash, vSet ); + Vec_IntWriteEntry( vMap, Abc_ObjId(pObj), SetId ); + } + // make sure the array of objects is sorted + Vec_IntSort( vObjs, 0 ); + // begin from the objects and map their IDs into sets of COs + Abc_NtkForEachObjVec( vObjs, pNtk, pObj, i ) + Abc_NtkDetectObjClasses_rec( pObj, vMap, pHash, vSet ); + Vec_IntFree( vSet ); + // create map for mapping CO set its their classes + vClassMap = Vec_IntStartFull( Hsh_VecSize(pHash) + 1 ); + // collect classes of objects + vClasses = Vec_WecAlloc( 1000 ); + Vec_IntForEachEntry( vObjs, iObj, i ) + { + //char * pName = Abc_ObjName( Abc_NtkObj(pNtk, iObj) ); + // for a given object (iObj), find the ID of its COs set + SetId = Vec_IntEntry( vMap, iObj ); + assert( SetId >= 0 ); + // for the given CO set, finds its equivalence class + ClassId = Vec_IntEntry( vClassMap, SetId ); + if ( ClassId == -1 ) // there is no equivalence class + { + // map this CO set into a new equivalence class + Vec_IntWriteEntry( vClassMap, SetId, Vec_WecSize(vClasses) ); + vClass = Vec_WecPushLevel( vClasses ); + } + else // get hold of the equivalence class + vClass = Vec_WecEntry( vClasses, ClassId ); + // add objects to the class + Vec_IntPush( vClass, iObj ); + // print the set for this object + //printf( "Object %5d : ", iObj ); + //Vec_IntPrint( Hsh_VecReadEntry(pHash, SetId) ); + } + // collect arrays of COs for each class + *pvCos = Vec_WecStart( Vec_WecSize(vClasses) ); + Vec_WecForEachLevel( vClasses, vClass, i ) + { + iObj = Vec_IntEntry( vClass, 0 ); + // for a given object (iObj), find the ID of its COs set + SetId = Vec_IntEntry( vMap, iObj ); + assert( SetId >= 0 ); + // for the given CO set ID, find the set + vSet = Hsh_VecReadEntry( pHash, SetId ); + Vec_IntAppend( Vec_WecEntry(*pvCos, i), vSet ); + } + Hsh_VecManStop( pHash ); + Vec_IntFree( vClassMap ); + Vec_IntFree( vMap ); + return vClasses; +} +void Abc_NtkDetectClassesTest2( Abc_Ntk_t * pNtk, int fVerbose, int fVeryVerbose ) +{ + Vec_Int_t * vObjs; + Vec_Wec_t * vRes, * vCos; + // for testing, create the set of object IDs for all combinational inputs (CIs) + Abc_Obj_t * pObj; int i; + vObjs = Vec_IntAlloc( Abc_NtkCiNum(pNtk) ); + Abc_NtkForEachCi( pNtk, pObj, i ) + Vec_IntPush( vObjs, Abc_ObjId(pObj) ); + // compute equivalence classes of CIs and print them + vRes = Abc_NtkDetectObjClasses( pNtk, vObjs, &vCos ); + Vec_WecPrint( vRes, 0 ); + Vec_WecPrint( vCos, 0 ); + // clean up + Vec_IntFree( vObjs ); + Vec_WecFree( vRes ); + Vec_WecFree( vCos ); +} + +/**Function************************************************************* + + Synopsis [Collecting objects.] + + Description [Collects combinational inputs (vCIs) and internal nodes (vNodes) + reachable from the given set of combinational outputs (vCOs).] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkFinMiterCollect_rec( Abc_Obj_t * pObj, Vec_Int_t * vCis, Vec_Int_t * vNodes ) +{ + if ( Abc_NodeIsTravIdCurrent(pObj) ) + return; + Abc_NodeSetTravIdCurrent(pObj); + if ( Abc_ObjIsCi(pObj) ) + Vec_IntPush( vCis, Abc_ObjId(pObj) ); + else + { + Abc_Obj_t * pFanin; int i; + assert( Abc_ObjIsNode( pObj ) ); + Abc_ObjForEachFanin( pObj, pFanin, i ) + Abc_NtkFinMiterCollect_rec( pFanin, vCis, vNodes ); + Vec_IntPush( vNodes, Abc_ObjId(pObj) ); + } +} +void Abc_NtkFinMiterCollect( Abc_Ntk_t * pNtk, Vec_Int_t * vCos, Vec_Int_t * vCis, Vec_Int_t * vNodes ) +{ + Abc_Obj_t * pObj; int i; + Vec_IntClear( vCis ); + Vec_IntClear( vNodes ); + Abc_NtkIncrementTravId( pNtk ); + Abc_NtkForEachObjVec( vCos, pNtk, pObj, i ) + Abc_NtkFinMiterCollect_rec( Abc_ObjFanin0(pObj), vCis, vNodes ); +} + +/**Function************************************************************* + + Synopsis [Simulates expression using given simulation info.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Mio_LibGateSimulate( Mio_Gate_t * pGate, word * ppFaninSims[6], int nWords, word * pObjSim ) +{ + int i, w, nVars = Mio_GateReadPinNum(pGate); + Vec_Int_t * vExpr = Mio_GateReadExpr( pGate ); + assert( nVars <= 6 ); + for ( w = 0; w < nWords; w++ ) + { + word uFanins[6]; + for ( i = 0; i < nVars; i++ ) + uFanins[i] = ppFaninSims[i][w]; + pObjSim[w] = Exp_Truth6( nVars, vExpr, uFanins ); + } +} + +/**Function************************************************************* + + Synopsis [Simulates expression for one simulation pattern.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Mio_LibGateSimulateOne( Mio_Gate_t * pGate, int iBits[6] ) +{ + int nVars = Mio_GateReadPinNum(pGate); + int i, iMint = 0; + for ( i = 0; i < nVars; i++ ) + if ( iBits[i] ) + iMint |= (1 << i); + return Abc_InfoHasBit( (unsigned *)Mio_GateReadTruthP(pGate), iMint ); +} + +/**Function************************************************************* + + Synopsis [Simulated expression with one bit.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Mio_LibGateSimulateGia( Gia_Man_t * pGia, Mio_Gate_t * pGate, int iLits[6], Vec_Int_t * vLits ) +{ + int i, nVars = Mio_GateReadPinNum(pGate); + Vec_Int_t * vExpr = Mio_GateReadExpr( pGate ); + if ( Exp_IsConst0(vExpr) ) + return 0; + if ( Exp_IsConst1(vExpr) ) + return 1; + if ( Exp_IsLit(vExpr) ) + { + int Index0 = Vec_IntEntry(vExpr,0) >> 1; + int fCompl0 = Vec_IntEntry(vExpr,0) & 1; + assert( Index0 < nVars ); + return Abc_LitNotCond( iLits[Index0], fCompl0 ); + } + Vec_IntClear( vLits ); + for ( i = 0; i < nVars; i++ ) + Vec_IntPush( vLits, iLits[i] ); + for ( i = 0; i < Exp_NodeNum(vExpr); i++ ) + { + int Index0 = Vec_IntEntry( vExpr, 2*i+0 ) >> 1; + int Index1 = Vec_IntEntry( vExpr, 2*i+1 ) >> 1; + int fCompl0 = Vec_IntEntry( vExpr, 2*i+0 ) & 1; + int fCompl1 = Vec_IntEntry( vExpr, 2*i+1 ) & 1; + Vec_IntPush( vLits, Gia_ManHashAnd( pGia, Abc_LitNotCond(Vec_IntEntry(vLits, Index0), fCompl0), Abc_LitNotCond(Vec_IntEntry(vLits, Index1), fCompl1) ) ); + } + return Abc_LitNotCond( Vec_IntEntryLast(vLits), Vec_IntEntryLast(vExpr) & 1 ); +} + +/**Function************************************************************* + + Synopsis [AIG construction and simulation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Abc_NtkFinSimOneLit( Gia_Man_t * pNew, Abc_Obj_t * pObj, int Type, Vec_Int_t * vMap, int n, Vec_Int_t * vTemp ) +{ + if ( Abc_NtkIsMappedLogic(pObj->pNtk) && Type >= 0 ) + { + extern int Mio_LibGateSimulateGia( Gia_Man_t * pGia, Mio_Gate_t * pGate, int iLits[6], Vec_Int_t * vLits ); + Mio_Library_t * pLib = (Mio_Library_t *)pObj->pNtk->pManFunc; + int i, Lits[6]; + for ( i = 0; i < Abc_ObjFaninNum(pObj); i++ ) + Lits[i] = Vec_IntEntry( vMap, Abc_Var2Lit(Abc_ObjFaninId(pObj, i), n) ); + return Mio_LibGateSimulateGia( pNew, Mio_LibraryReadGateById(pLib, Type), Lits, vTemp ); + } + else + { + int iLit0 = Abc_ObjFaninNum(pObj) > 0 ? Vec_IntEntry( vMap, Abc_Var2Lit(Abc_ObjFaninId0(pObj), n) ) : -1; + int iLit1 = Abc_ObjFaninNum(pObj) > 1 ? Vec_IntEntry( vMap, Abc_Var2Lit(Abc_ObjFaninId1(pObj), n) ) : -1; + assert( Type != ABC_FIN_NEG ); + if ( Type == ABC_FIN_SA0 ) return 0; + if ( Type == ABC_FIN_SA1 ) return 1; + if ( Type == ABC_FIN_RDOB_BUFF ) return iLit0; + if ( Type == ABC_FIN_RDOB_NOT ) return Abc_LitNot( iLit0 ); + if ( Type == ABC_FIN_RDOB_AND ) return Gia_ManHashAnd( pNew, iLit0, iLit1 ); + if ( Type == ABC_FIN_RDOB_OR ) return Gia_ManHashOr( pNew, iLit0, iLit1 ); + if ( Type == ABC_FIN_RDOB_XOR ) return Gia_ManHashXor( pNew, iLit0, iLit1 ); + if ( Type == ABC_FIN_RDOB_NAND ) return Abc_LitNot(Gia_ManHashAnd( pNew, iLit0, iLit1 )); + if ( Type == ABC_FIN_RDOB_NOR ) return Abc_LitNot(Gia_ManHashOr( pNew, iLit0, iLit1 )); + if ( Type == ABC_FIN_RDOB_NXOR ) return Abc_LitNot(Gia_ManHashXor( pNew, iLit0, iLit1 )); + assert( 0 ); + return -1; + } +} +static inline int Abc_NtkFinSimOneBit( Abc_Obj_t * pObj, int Type, Vec_Wrd_t * vSims, int nWords, int iBit ) +{ + if ( Abc_NtkIsMappedLogic(pObj->pNtk) && Type >= 0 ) + { + extern int Mio_LibGateSimulateOne( Mio_Gate_t * pGate, int iBits[6] ); + Mio_Library_t * pLib = (Mio_Library_t *)pObj->pNtk->pManFunc; + int i, iBits[6]; + for ( i = 0; i < Abc_ObjFaninNum(pObj); i++ ) + { + word * pSim0 = Vec_WrdEntryP( vSims, nWords * Abc_ObjFaninId(pObj, i) ); + iBits[i] = Abc_InfoHasBit( (unsigned*)pSim0, iBit ); + } + return Mio_LibGateSimulateOne( Mio_LibraryReadGateById(pLib, Type), iBits ); + } + else + { + word * pSim0 = Abc_ObjFaninNum(pObj) > 0 ? Vec_WrdEntryP( vSims, nWords * Abc_ObjFaninId0(pObj) ) : NULL; + word * pSim1 = Abc_ObjFaninNum(pObj) > 1 ? Vec_WrdEntryP( vSims, nWords * Abc_ObjFaninId1(pObj) ) : NULL; + int iBit0 = Abc_ObjFaninNum(pObj) > 0 ? Abc_InfoHasBit( (unsigned*)pSim0, iBit ) : -1; + int iBit1 = Abc_ObjFaninNum(pObj) > 1 ? Abc_InfoHasBit( (unsigned*)pSim1, iBit ) : -1; + assert( Type != ABC_FIN_NEG ); + if ( Type == ABC_FIN_SA0 ) return 0; + if ( Type == ABC_FIN_SA1 ) return 1; + if ( Type == ABC_FIN_RDOB_BUFF ) return iBit0; + if ( Type == ABC_FIN_RDOB_NOT ) return !iBit0; + if ( Type == ABC_FIN_RDOB_AND ) return iBit0 & iBit1; + if ( Type == ABC_FIN_RDOB_OR ) return iBit0 | iBit1; + if ( Type == ABC_FIN_RDOB_XOR ) return iBit0 ^ iBit1; + if ( Type == ABC_FIN_RDOB_NAND ) return !(iBit0 & iBit1); + if ( Type == ABC_FIN_RDOB_NOR ) return !(iBit0 | iBit1); + if ( Type == ABC_FIN_RDOB_NXOR ) return !(iBit0 ^ iBit1); + assert( 0 ); + return -1; + } +} +static inline void Abc_NtkFinSimOneWord( Abc_Obj_t * pObj, int Type, Vec_Wrd_t * vSims, int nWords ) +{ + if ( Abc_NtkIsMappedLogic(pObj->pNtk) ) + { + extern void Mio_LibGateSimulate( Mio_Gate_t * pGate, word * ppFaninSims[6], int nWords, word * pObjSim ); + word * ppSims[6]; int i; + word * pSim = Vec_WrdEntryP( vSims, nWords * Abc_ObjId(pObj) ); + assert( Type == -1 ); + for ( i = 0; i < Abc_ObjFaninNum(pObj); i++ ) + ppSims[i] = Vec_WrdEntryP( vSims, nWords * Abc_ObjFaninId(pObj, i) ); + Mio_LibGateSimulate( (Mio_Gate_t *)pObj->pData, ppSims, nWords, pSim ); + } + else + { + word * pSim = Vec_WrdEntryP( vSims, nWords * Abc_ObjId(pObj) ); int w; + word * pSim0 = Abc_ObjFaninNum(pObj) > 0 ? Vec_WrdEntryP( vSims, nWords * Abc_ObjFaninId0(pObj) ) : NULL; + word * pSim1 = Abc_ObjFaninNum(pObj) > 1 ? Vec_WrdEntryP( vSims, nWords * Abc_ObjFaninId1(pObj) ) : NULL; + assert( Type != ABC_FIN_NEG ); + if ( Type == ABC_FIN_SA0 ) for ( w = 0; w < nWords; w++ ) pSim[w] = 0; + else if ( Type == ABC_FIN_SA1 ) for ( w = 0; w < nWords; w++ ) pSim[w] = ~((word)0); + else if ( Type == ABC_FIN_RDOB_BUFF ) for ( w = 0; w < nWords; w++ ) pSim[w] = pSim0[w]; + else if ( Type == ABC_FIN_RDOB_NOT ) for ( w = 0; w < nWords; w++ ) pSim[w] = ~pSim0[w]; + else if ( Type == ABC_FIN_RDOB_AND ) for ( w = 0; w < nWords; w++ ) pSim[w] = pSim0[w] & pSim1[w]; + else if ( Type == ABC_FIN_RDOB_OR ) for ( w = 0; w < nWords; w++ ) pSim[w] = pSim0[w] | pSim1[w]; + else if ( Type == ABC_FIN_RDOB_XOR ) for ( w = 0; w < nWords; w++ ) pSim[w] = pSim0[w] ^ pSim1[w]; + else if ( Type == ABC_FIN_RDOB_NAND ) for ( w = 0; w < nWords; w++ ) pSim[w] = ~(pSim0[w] & pSim1[w]); + else if ( Type == ABC_FIN_RDOB_NOR ) for ( w = 0; w < nWords; w++ ) pSim[w] = ~(pSim0[w] | pSim1[w]); + else if ( Type == ABC_FIN_RDOB_NXOR ) for ( w = 0; w < nWords; w++ ) pSim[w] = ~(pSim0[w] ^ pSim1[w]); + else assert( 0 ); + } +} + + +// returns 1 if the functionality with indexes i1 and i2 is the same +static inline int Abc_NtkFinCompareSimTwo( Abc_Ntk_t * pNtk, Vec_Int_t * vCos, Vec_Wrd_t * vSims, int nWords, int i1, int i2 ) +{ + Abc_Obj_t * pObj; int i; + assert( i1 != i2 ); + Abc_NtkForEachObjVec( vCos, pNtk, pObj, i ) + { + word * pSim0 = Vec_WrdEntryP( vSims, nWords * Abc_ObjFaninId0(pObj) ); + if ( Abc_InfoHasBit((unsigned*)pSim0, i1) != Abc_InfoHasBit((unsigned*)pSim0, i2) ) + return 0; + } + return 1; +} + +Gia_Man_t * Abc_NtkFinMiterToGia( Abc_Ntk_t * pNtk, Vec_Int_t * vTypes, Vec_Int_t * vCos, Vec_Int_t * vCis, Vec_Int_t * vNodes, + int iObjs[2], int Types[2], Vec_Int_t * vLits ) +{ + Gia_Man_t * pNew = NULL, * pTemp; + Abc_Obj_t * pObj; + Vec_Int_t * vTemp = Vec_IntAlloc( 100 ); + int n, i, Type, iMiter, iLit, * pLits; + // create AIG manager + pNew = Gia_ManStart( 1000 ); + pNew->pName = Abc_UtilStrsav( pNtk->pName ); + pNew->pSpec = Abc_UtilStrsav( pNtk->pSpec ); + Gia_ManHashStart( pNew ); + // create inputs + Abc_NtkForEachObjVec( vCis, pNtk, pObj, i ) + { + iLit = Gia_ManAppendCi(pNew); + for ( n = 0; n < 2; n++ ) + { + if ( iObjs[n] != (int)Abc_ObjId(pObj) ) + Vec_IntWriteEntry( vLits, Abc_Var2Lit(Abc_ObjId(pObj), n), iLit ); + else if ( Types[n] != ABC_FIN_NEG ) + Vec_IntWriteEntry( vLits, Abc_Var2Lit(Abc_ObjId(pObj), n), Abc_NtkFinSimOneLit(pNew, pObj, Types[n], vLits, n, vTemp) ); + else // if ( iObjs[n] == (int)Abc_ObjId(pObj) && Types[n] == ABC_FIN_NEG ) + Vec_IntWriteEntry( vLits, Abc_Var2Lit(Abc_ObjId(pObj), n), Abc_LitNot(iLit) ); + } + } + // create internal nodes + Abc_NtkForEachObjVec( vNodes, pNtk, pObj, i ) + { + Type = Abc_NtkIsMappedLogic(pNtk) ? Mio_GateReadCell((Mio_Gate_t *)pObj->pData) : Vec_IntEntry(vTypes, Abc_ObjId(pObj)); + for ( n = 0; n < 2; n++ ) + { + if ( iObjs[n] != (int)Abc_ObjId(pObj) ) + Vec_IntWriteEntry( vLits, Abc_Var2Lit(Abc_ObjId(pObj), n), Abc_NtkFinSimOneLit(pNew, pObj, Type, vLits, n, vTemp) ); + else if ( Types[n] != ABC_FIN_NEG ) + Vec_IntWriteEntry( vLits, Abc_Var2Lit(Abc_ObjId(pObj), n), Abc_NtkFinSimOneLit(pNew, pObj, Types[n], vLits, n, vTemp) ); + else // if ( iObjs[n] == (int)Abc_ObjId(pObj) && Types[n] == ABC_FIN_NEG ) + Vec_IntWriteEntry( vLits, Abc_Var2Lit(Abc_ObjId(pObj), n), Abc_LitNot(Abc_NtkFinSimOneLit(pNew, pObj, Type, vLits, n, vTemp)) ); + } + } + // create comparator + iMiter = 0; + Abc_NtkForEachObjVec( vCos, pNtk, pObj, i ) + { + pLits = Vec_IntEntryP( vLits, Abc_Var2Lit(Abc_ObjFaninId0(pObj), 0) ); + iLit = Gia_ManHashXor( pNew, pLits[0], pLits[1] ); + iMiter = Gia_ManHashOr( pNew, iMiter, iLit ); + } + Gia_ManAppendCo( pNew, iMiter ); + // perform cleanup + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + Vec_IntFree( vTemp ); + return pNew; +} +void Abc_NtkFinSimulateOne( Abc_Ntk_t * pNtk, Vec_Int_t * vTypes, Vec_Int_t * vCos, Vec_Int_t * vCis, Vec_Int_t * vNodes, + Vec_Wec_t * vMap2, Vec_Int_t * vPat, Vec_Wrd_t * vSims, int nWords, Vec_Int_t * vPairs, Vec_Wec_t * vRes, int iLevel, int iItem ) +{ + Abc_Obj_t * pObj; + Vec_Int_t * vClass, * vArray; + int i, Counter = 0; + int nItems = Vec_WecSizeSize(vRes); + assert( nItems == Vec_WecSizeSize(vMap2) ); + assert( nItems <= 128 * nWords ); + // assign inputs + assert( Vec_IntSize(vPat) == Vec_IntSize(vCis) ); + Abc_NtkForEachObjVec( vCis, pNtk, pObj, i ) + { + int w, iObj = Abc_ObjId( pObj ); + word Init = Vec_IntEntry(vPat, i) ? ~((word)0) : 0; + word * pSim = Vec_WrdEntryP( vSims, nWords * Abc_ObjId(pObj) ); + for ( w = 0; w < nWords; w++ ) + pSim[w] = Init; + vArray = Vec_WecEntry(vMap2, iObj); + if ( Vec_IntSize(vArray) > 0 ) + { + int k, iFin, Index, iObj, Type; + Vec_IntForEachEntryDouble( vArray, iFin, Index, k ) + { + assert( Index < 64 ); + iObj = Vec_IntEntry( vPairs, 2*iFin ); + assert( iObj == (int)Abc_ObjId(pObj) ); + Type = Vec_IntEntry( vPairs, 2*iFin+1 ); + assert( Type == ABC_FIN_NEG || Type == ABC_FIN_SA0 || Type == ABC_FIN_SA1 ); + if ( Type == ABC_FIN_NEG || Abc_InfoHasBit((unsigned *)pSim, Index) != Abc_NtkFinSimOneBit(pObj, Type, vSims, nWords, Index) ) + Abc_InfoXorBit( (unsigned *)pSim, Index ); + Counter++; + } + } + } + // simulate internal nodes + Abc_NtkForEachObjVec( vNodes, pNtk, pObj, i ) + { + int iObj = Abc_ObjId( pObj ); + int Type = Abc_NtkIsMappedLogic(pNtk) ? -1 : Vec_IntEntry( vTypes, iObj ); + word * pSim = Vec_WrdEntryP( vSims, nWords * Abc_ObjId(pObj) ); + Abc_NtkFinSimOneWord( pObj, Type, vSims, nWords ); + vArray = Vec_WecEntry(vMap2, iObj); + if ( Vec_IntSize(vArray) > 0 ) + { + int k, iFin, Index, iObj, Type; + Vec_IntForEachEntryDouble( vArray, iFin, Index, k ) + { + assert( Index < 64 * nWords ); + iObj = Vec_IntEntry( vPairs, 2*iFin ); + assert( iObj == (int)Abc_ObjId(pObj) ); + Type = Vec_IntEntry( vPairs, 2*iFin+1 ); + if ( Type == ABC_FIN_NEG || Abc_InfoHasBit((unsigned *)pSim, Index) != Abc_NtkFinSimOneBit(pObj, Type, vSims, nWords, Index) ) + Abc_InfoXorBit( (unsigned *)pSim, Index ); + Counter++; + } + } + } + assert( nItems == 2*Counter ); + + // confirm no refinement + Vec_WecForEachLevelStop( vRes, vClass, i, iLevel+1 ) + { + int k, iFin, Index, Value; + int iFin0 = Vec_IntEntry( vClass, 0 ); + int Index0 = Vec_IntEntry( vClass, 1 ); + Vec_IntForEachEntryDoubleStart( vClass, iFin, Index, k, 2 ) + { + if ( i == iLevel && k/2 >= iItem ) + break; + //printf( "Double-checking pair %d and %d\n", iFin0, iFin ); + Value = Abc_NtkFinCompareSimTwo( pNtk, vCos, vSims, nWords, Index0, Index ); + assert( Value ); // the same value + } + } + + // check refinement + Vec_WecForEachLevelStart( vRes, vClass, i, iLevel ) + { + int k, iFin, Index, Value, Index0 = Vec_IntEntry(vClass, 1); + int j = (i == iLevel) ? 2*iItem : 2; + Vec_Int_t * vNewClass = NULL; + Vec_IntForEachEntryDoubleStart( vClass, iFin, Index, k, j ) + { + Value = Abc_NtkFinCompareSimTwo( pNtk, vCos, vSims, nWords, Index0, Index ); + if ( Value ) // the same value + { + Vec_IntWriteEntry( vClass, j++, iFin ); + Vec_IntWriteEntry( vClass, j++, Index ); + continue; + } + // create new class + vNewClass = vNewClass ? vNewClass : Vec_WecPushLevel( vRes ); + Vec_IntPushTwo( vNewClass, iFin, Index ); // index and first entry + vClass = Vec_WecEntry( vRes, i ); + } + Vec_IntShrink( vClass, j ); + } +} + +/**Function************************************************************* + + Synopsis [Check equivalence using SAT solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Abc_NtkFinCheckPair( Abc_Ntk_t * pNtk, Vec_Int_t * vTypes, Vec_Int_t * vCos, Vec_Int_t * vCis, Vec_Int_t * vNodes, int iObjs[2], int Types[2], Vec_Int_t * vLits ) +{ + Gia_Man_t * pGia = Abc_NtkFinMiterToGia( pNtk, vTypes, vCos, vCis, vNodes, iObjs, Types, vLits ); + if ( Gia_ManAndNum(pGia) == 0 && Gia_ObjIsConst0(Gia_ObjFanin0(Gia_ManCo(pGia, 0))) ) + { + Vec_Int_t * vPat = Gia_ObjFaninC0(Gia_ManCo(pGia, 0)) ? Vec_IntStart(Vec_IntSize(vCis)) : NULL; + Gia_ManStop( pGia ); + return vPat; + } + else + { + extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose ); + Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( pGia, 8, 0, 1, 0 ); + sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); + if ( pSat == NULL ) + { + Gia_ManStop( pGia ); + Cnf_DataFree( pCnf ); + return NULL; + } + else + { + int i, nConfLimit = 10000; + Vec_Int_t * vPat = NULL; + int status, iVarBeg = pCnf->nVars - Gia_ManPiNum(pGia);// - 1; + //Gia_AigerWrite( pGia, "temp_detect.aig", 0, 0 ); + Gia_ManStop( pGia ); + Cnf_DataFree( pCnf ); + status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, 0, 0, 0 ); + if ( status == l_Undef ) + vPat = Vec_IntAlloc(0); + else if ( status == l_True ) + { + vPat = Vec_IntAlloc( Vec_IntSize(vCis) ); + for ( i = 0; i < Vec_IntSize(vCis); i++ ) + Vec_IntPush( vPat, sat_solver_var_value(pSat, iVarBeg+i) ); + } + //printf( "%d ", sat_solver_nconflicts(pSat) ); + sat_solver_delete( pSat ); + return vPat; + } + } +} + + +/**Function************************************************************* + + Synopsis [Refinement of equivalence classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkFinLocalSetup( Vec_Int_t * vPairs, Vec_Int_t * vList, Vec_Wec_t * vMap2, Vec_Int_t * vResArray ) +{ + int i, iFin; + Vec_IntClear( vResArray ); + Vec_IntForEachEntry( vList, iFin, i ) + { + int iObj = Vec_IntEntry( vPairs, 2*iFin ); + int Type = Vec_IntEntry( vPairs, 2*iFin+1 ); + Vec_Int_t * vArray = Vec_WecEntry( vMap2, iObj ); + Vec_IntPushTwo( vArray, iFin, i ); + Vec_IntPushTwo( vResArray, iFin, i ); + } +} +void Abc_NtkFinLocalSetdown( Vec_Int_t * vPairs, Vec_Int_t * vList, Vec_Wec_t * vMap2 ) +{ + int i, iFin; + Vec_IntForEachEntry( vList, iFin, i ) + { + int iObj = Vec_IntEntry( vPairs, 2*iFin ); + Vec_Int_t * vArray = Vec_WecEntry( vMap2, iObj ); + Vec_IntClear( vArray ); + } +} +int Abc_NtkFinRefinement( Abc_Ntk_t * pNtk, Vec_Int_t * vTypes, Vec_Int_t * vCos, Vec_Int_t * vCis, Vec_Int_t * vNodes, + Vec_Int_t * vPairs, Vec_Int_t * vList, Vec_Wec_t * vMap2, Vec_Wec_t * vResult ) +{ + Vec_Wec_t * vRes = Vec_WecAlloc( 100 ); + int nWords = Abc_Bit6WordNum( Vec_IntSize(vList) ); + Vec_Wrd_t * vSims = Vec_WrdStart( nWords * Abc_NtkObjNumMax(pNtk) ); // simulation info for each object + Vec_Int_t * vLits = Vec_IntStart( 2*Abc_NtkObjNumMax(pNtk) ); // two literals for each object + Vec_Int_t * vPat, * vClass, * vArray; + int i, k, iFin, Index, nCalls = 0; + // prepare + vArray = Vec_WecPushLevel( vRes ); + Abc_NtkFinLocalSetup( vPairs, vList, vMap2, vArray ); + // try all-0/all-1 pattern + for ( i = 0; i < 2; i++ ) + { + vPat = Vec_IntAlloc( Vec_IntSize(vCis) ); + Vec_IntFill( vPat, Vec_IntSize(vCis), i ); + Abc_NtkFinSimulateOne( pNtk, vTypes, vCos, vCis, vNodes, vMap2, vPat, vSims, nWords, vPairs, vRes, 0, 1 ); + Vec_IntFree( vPat ); + } + // explore the classes + //Vec_WecPrint( vRes, 0 ); + Vec_WecForEachLevel( vRes, vClass, i ) + { + int iFin0 = Vec_IntEntry( vClass, 0 ); + int Index0 = Vec_IntEntry( vClass, 1 ); + Vec_IntForEachEntryDoubleStart( vClass, iFin, Index, k, 2 ) + { + int Objs[2] = { Vec_IntEntry(vPairs, 2*iFin0), Vec_IntEntry(vPairs, 2*iFin) }; + int Types[2] = { Vec_IntEntry(vPairs, 2*iFin0+1), Vec_IntEntry(vPairs, 2*iFin+1) }; + nCalls++; + //printf( "Checking pair %d and %d.\n", iFin0, iFin ); + vPat = Abc_NtkFinCheckPair( pNtk, vTypes, vCos, vCis, vNodes, Objs, Types, vLits ); + if ( vPat == NULL ) // proved + continue; + assert( Vec_IntEntry(vClass, k) == iFin ); + if ( Vec_IntSize(vPat) == 0 ) + { + Vec_Int_t * vNewClass = Vec_WecPushLevel( vRes ); + Vec_IntPushTwo( vNewClass, iFin, Index ); // index and first entry + vClass = Vec_WecEntry( vRes, i ); + Vec_IntDrop( vClass, k+1 ); + Vec_IntDrop( vClass, k ); + } + else // resimulate and refine + Abc_NtkFinSimulateOne( pNtk, vTypes, vCos, vCis, vNodes, vMap2, vPat, vSims, nWords, vPairs, vRes, i, k/2 ); + Vec_IntFree( vPat ); + // make sure refinement happened (k'th entry is now absent or different) + vClass = Vec_WecEntry( vRes, i ); + assert( Vec_IntSize(vClass) <= k || Vec_IntEntry(vClass, k) != iFin ); + k -= 2; + //Vec_WecPrint( vRes, 0 ); + } + } + // unprepare + Abc_NtkFinLocalSetdown( vPairs, vList, vMap2 ); + // reload proved equivs into the final array + Vec_WecForEachLevel( vRes, vArray, i ) + { + assert( Vec_IntSize(vArray) % 2 == 0 ); + if ( Vec_IntSize(vArray) <= 2 ) + continue; + vClass = Vec_WecPushLevel( vResult ); + Vec_IntForEachEntryDouble( vArray, iFin, Index, k ) + Vec_IntPush( vClass, iFin ); + } + Vec_WecFree( vRes ); + Vec_WrdFree( vSims ); + Vec_IntFree( vLits ); + return nCalls; +} + +/**Function************************************************************* + + Synopsis [Detecting classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Abc_ObjFinGateType( Abc_Obj_t * pNode ) +{ + char * pSop = (char *)pNode->pData; + if ( !strcmp(pSop, "1 1\n") ) return ABC_FIN_RDOB_BUFF; + if ( !strcmp(pSop, "0 1\n") ) return ABC_FIN_RDOB_NOT; + if ( !strcmp(pSop, "11 1\n") ) return ABC_FIN_RDOB_AND; + if ( !strcmp(pSop, "11 0\n") ) return ABC_FIN_RDOB_NAND; + if ( !strcmp(pSop, "00 0\n") ) return ABC_FIN_RDOB_OR; + if ( !strcmp(pSop, "00 1\n") ) return ABC_FIN_RDOB_NOR; + if ( !strcmp(pSop, "01 1\n10 1\n") ) return ABC_FIN_RDOB_XOR; + if ( !strcmp(pSop, "11 1\n00 1\n") ) return ABC_FIN_RDOB_NXOR; + return ABC_FIN_NONE; +} +int Abc_NtkFinCheckTypesOk( Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pObj; int i; + Abc_NtkForEachNode( pNtk, pObj, i ) + if ( Abc_ObjFinGateType(pObj) == ABC_FIN_NONE ) + return i; + return 0; +} +int Abc_NtkFinCheckTypesOk2( Abc_Ntk_t * pNtk ) +{ + Mio_Library_t * pLib = (Mio_Library_t *)pNtk->pManFunc; + int i, iObj, Type; + Vec_IntForEachEntryDoubleStart( pNtk->vFins, iObj, Type, i, 2 ) + { + Abc_Obj_t * pObj = Abc_NtkObj( pNtk, iObj ); + Mio_Gate_t * pGateFlt, * pGateObj = (Mio_Gate_t *)pObj->pData; + if ( Type < 0 ) // SA0, SA1, NEG + continue; + pGateFlt = Mio_LibraryReadGateById( pLib, Type ); + if ( Mio_GateReadPinNum(pGateFlt) < 1 ) + continue; + if ( Mio_GateReadPinNum(pGateObj) != Mio_GateReadPinNum(pGateFlt) ) + return iObj; + } + return 0; +} +Vec_Int_t * Abc_NtkFinComputeTypes( Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pObj; int i; + Vec_Int_t * vObjs = Vec_IntStart( Abc_NtkObjNumMax(pNtk) ); + Abc_NtkForEachNode( pNtk, pObj, i ) + Vec_IntWriteEntry( vObjs, Abc_ObjId(pObj), Abc_ObjFinGateType(pObj) ); + return vObjs; +} +Vec_Int_t * Abc_NtkFinComputeObjects( Vec_Int_t * vPairs, Vec_Wec_t ** pvMap, int nObjs ) +{ + int i, iObj, Type; + Vec_Int_t * vObjs = Vec_IntAlloc( 100 ); + *pvMap = Vec_WecStart( nObjs ); + Vec_IntForEachEntryDoubleStart( vPairs, iObj, Type, i, 2 ) + { + Vec_IntPush( vObjs, iObj ); + Vec_WecPush( *pvMap, iObj, i/2 ); + } + Vec_IntUniqify( vObjs ); + return vObjs; +} +Vec_Int_t * Abc_NtkFinCreateList( Vec_Wec_t * vMap, Vec_Int_t * vClass ) +{ + int i, iObj; + Vec_Int_t * vList = Vec_IntAlloc( 100 ); + Vec_IntForEachEntry( vClass, iObj, i ) + Vec_IntAppend( vList, Vec_WecEntry(vMap, iObj) ); + return vList; +} +int Abc_NtkFinCountPairs( Vec_Wec_t * vClasses ) +{ + int i, Counter = 0; + Vec_Int_t * vLevel; + Vec_WecForEachLevel( vClasses, vLevel, i ) + Counter += Vec_IntSize(vLevel) - 1; + return Counter; +} +Vec_Wec_t * Abc_NtkDetectFinClasses( Abc_Ntk_t * pNtk, int fVerbose ) +{ + Vec_Int_t * vTypes = NULL; // gate types + Vec_Int_t * vPairs; // original info as a set of pairs (ObjId, TypeId) + Vec_Int_t * vObjs; // all those objects that have some fin + Vec_Wec_t * vMap; // for each object, the set of fins + Vec_Wec_t * vMap2; // for each local object, the set of pairs (Info, Index) + Vec_Wec_t * vClasses; // classes of objects + Vec_Wec_t * vCoSets; // corresponding CO sets + Vec_Int_t * vClass; // one class + Vec_Int_t * vCoSet; // one set of COs + Vec_Int_t * vCiSet; // one set of CIs + Vec_Int_t * vNodeSet; // one set of nodes + Vec_Int_t * vList; // one info list + Vec_Wec_t * vResult; // resulting equivalences + int i, iObj, nCalls; + if ( pNtk->vFins == NULL ) + { + printf( "Current network does not have the required info.\n" ); + return NULL; + } + assert( Abc_NtkIsSopLogic(pNtk) || Abc_NtkIsMappedLogic(pNtk) ); + if ( Abc_NtkIsSopLogic(pNtk) ) + { + iObj = Abc_NtkFinCheckTypesOk(pNtk); + if ( iObj ) + { + printf( "Current network contains unsupported gate types (for example, see node \"%s\").\n", Abc_ObjName(Abc_NtkObj(pNtk, iObj)) ); + return NULL; + } + vTypes = Abc_NtkFinComputeTypes( pNtk ); + } + else if ( Abc_NtkIsMappedLogic(pNtk) ) + { + iObj = Abc_NtkFinCheckTypesOk2(pNtk); + if ( iObj ) + { + printf( "Current network has mismatch between mapped gate size and fault gate size (for example, see node \"%s\").\n", Abc_ObjName(Abc_NtkObj(pNtk, iObj)) ); + return NULL; + } + } + else assert( 0 ); + //Abc_NtkFrameExtend( pNtk ); + // collect data + vPairs = pNtk->vFins; + vObjs = Abc_NtkFinComputeObjects( vPairs, &vMap, Abc_NtkObjNumMax(pNtk) ); + vClasses = Abc_NtkDetectObjClasses( pNtk, vObjs, &vCoSets ); + // refine classes + vCiSet = Vec_IntAlloc( 1000 ); + vNodeSet = Vec_IntAlloc( 1000 ); + vMap2 = Vec_WecStart( Abc_NtkObjNumMax(pNtk) ); + vResult = Vec_WecAlloc( 1000 ); + Vec_WecForEachLevel( vClasses, vClass, i ) + { + // extract one window + vCoSet = Vec_WecEntry( vCoSets, i ); + Abc_NtkFinMiterCollect( pNtk, vCoSet, vCiSet, vNodeSet ); + // refine one class + vList = Abc_NtkFinCreateList( vMap, vClass ); + nCalls = Abc_NtkFinRefinement( pNtk, vTypes, vCoSet, vCiSet, vNodeSet, vPairs, vList, vMap2, vResult ); + if ( fVerbose ) + printf( "Group %4d : Obj =%4d. Fins =%4d. CI =%5d. CO =%5d. Node =%6d. SAT calls =%5d.\n", + i, Vec_IntSize(vClass), Vec_IntSize(vList), Vec_IntSize(vCiSet), Vec_IntSize(vCoSet), Vec_IntSize(vNodeSet), nCalls ); + Vec_IntFree( vList ); + } + // sort entries in each array + Vec_WecForEachLevel( vResult, vClass, i ) + Vec_IntSort( vClass, 0 ); + // sort by the index of the first entry + Vec_WecSortByFirstInt( vResult, 0 ); + // cleanup + Vec_IntFreeP( & vTypes ); + Vec_IntFree( vObjs ); + Vec_WecFree( vClasses ); + Vec_WecFree( vMap ); + Vec_WecFree( vMap2 ); + Vec_WecFree( vCoSets ); + Vec_IntFree( vCiSet ); + Vec_IntFree( vNodeSet ); + return vResult; +} + +/**Function************************************************************* + + Synopsis [Print results.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkPrintFinResults( Vec_Wec_t * vClasses ) +{ + Vec_Int_t * vClass; + int i, k, Entry; + Vec_WecForEachLevel( vClasses, vClass, i ) + Vec_IntForEachEntryStart( vClass, Entry, k, 1 ) + printf( "%d %d\n", Vec_IntEntry(vClass, 0), Entry ); +} + /**Function************************************************************* Synopsis [Top-level procedure.] @@ -193,9 +1240,20 @@ finish: SeeAlso [] ***********************************************************************/ -void Abc_NtkDetectClassesTest( Abc_Ntk_t * pNtk, int fSeq, int fVerbose ) +void Abc_NtkDetectClassesTest( Abc_Ntk_t * pNtk, int fSeq, int fVerbose, int fVeryVerbose ) { - printf( "This procedure is currently not used.\n" ); + Vec_Wec_t * vResult; + abctime clk = Abc_Clock(); + if ( fSeq ) + Abc_NtkFrameExtend( pNtk ); + vResult = Abc_NtkDetectFinClasses( pNtk, fVerbose ); + printf( "Computed %d equivalence classes with %d item pairs. ", Vec_WecSize(vResult), Abc_NtkFinCountPairs(vResult) ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + if ( fVeryVerbose ) + Vec_WecPrint( vResult, 1 ); +// if ( fVerbose ) +// Abc_NtkPrintFinResults( vResult ); + Vec_WecFree( vResult ); } -- cgit v1.2.3 From 460a5700a5369a0cb46ae5c6d5bbc001deaf8ab4 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 9 Nov 2016 21:19:52 -0800 Subject: Compiler warnings. --- src/base/abci/abcDetect.c | 3 --- 1 file changed, 3 deletions(-) (limited to 'src/base/abci') diff --git a/src/base/abci/abcDetect.c b/src/base/abci/abcDetect.c index b1a598cd..0125a67e 100644 --- a/src/base/abci/abcDetect.c +++ b/src/base/abci/abcDetect.c @@ -842,7 +842,6 @@ void Abc_NtkFinSimulateOne( Abc_Ntk_t * pNtk, Vec_Int_t * vTypes, Vec_Int_t * vC Vec_WecForEachLevelStop( vRes, vClass, i, iLevel+1 ) { int k, iFin, Index, Value; - int iFin0 = Vec_IntEntry( vClass, 0 ); int Index0 = Vec_IntEntry( vClass, 1 ); Vec_IntForEachEntryDoubleStart( vClass, iFin, Index, k, 2 ) { @@ -952,7 +951,6 @@ void Abc_NtkFinLocalSetup( Vec_Int_t * vPairs, Vec_Int_t * vList, Vec_Wec_t * vM Vec_IntForEachEntry( vList, iFin, i ) { int iObj = Vec_IntEntry( vPairs, 2*iFin ); - int Type = Vec_IntEntry( vPairs, 2*iFin+1 ); Vec_Int_t * vArray = Vec_WecEntry( vMap2, iObj ); Vec_IntPushTwo( vArray, iFin, i ); Vec_IntPushTwo( vResArray, iFin, i ); @@ -993,7 +991,6 @@ int Abc_NtkFinRefinement( Abc_Ntk_t * pNtk, Vec_Int_t * vTypes, Vec_Int_t * vCos Vec_WecForEachLevel( vRes, vClass, i ) { int iFin0 = Vec_IntEntry( vClass, 0 ); - int Index0 = Vec_IntEntry( vClass, 1 ); Vec_IntForEachEntryDoubleStart( vClass, iFin, Index, k, 2 ) { int Objs[2] = { Vec_IntEntry(vPairs, 2*iFin0), Vec_IntEntry(vPairs, 2*iFin) }; -- cgit v1.2.3 From 71a52ae9e5e0572f93df9eb14cba8c7567d3e676 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 10 Nov 2016 09:38:07 -0800 Subject: Renaming command 'detect' to be 'faultclasses'. --- src/base/abci/abc.c | 20 +++++++++++--------- src/base/abci/abcDetect.c | 2 +- 2 files changed, 12 insertions(+), 10 deletions(-) (limited to 'src/base/abci') diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index b1c81cd5..07ea78b2 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -134,7 +134,7 @@ static int Abc_CommandRr ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandCascade ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandExtract ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandVarMin ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandDetect ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandFaultClasses ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandExact ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandBmsStart ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandBmsStop ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -778,7 +778,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Synthesis", "cascade", Abc_CommandCascade, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "extract", Abc_CommandExtract, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "varmin", Abc_CommandVarMin, 0 ); - Cmd_CommandAdd( pAbc, "Synthesis", "detect", Abc_CommandDetect, 0 ); + Cmd_CommandAdd( pAbc, "Synthesis", "faultclasses", Abc_CommandFaultClasses, 0 ); Cmd_CommandAdd( pAbc, "Synthesis", "exact", Abc_CommandExact, 1 ); Cmd_CommandAdd( pAbc, "Exact synthesis", "bms_start", Abc_CommandBmsStart, 0 ); @@ -7235,7 +7235,7 @@ usage: SeeAlso [] ***********************************************************************/ -int Abc_CommandDetect( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandFaultClasses( Abc_Frame_t * pAbc, int argc, char ** argv ) { extern void Abc_NtkDetectClassesTest( Abc_Ntk_t * pNtk, int fSeq, int fVerbose, int fVeryVerbose ); extern void Abc_NtkGenFaultList( Abc_Ntk_t * pNtk, char * pFileName ); @@ -7285,12 +7285,14 @@ int Abc_CommandDetect( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: detect [-gsvwh]\n" ); - Abc_Print( -2, "\t detects properties of internal nodes\n" ); - Abc_Print( -2, "\t-g : toggle generating fault list for the given network [default = %s]\n", fGen? "yes": "no" ); - Abc_Print( -2, "\t-s : toggle using sequential circuit information [default = %s]\n", fSeq? "yes": "no" ); - Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" ); - Abc_Print( -2, "\t-w : toggle printing equivalence classes [default = %s]\n", fVeryVerbose? "yes": "no" ); + Abc_Print( -2, "usage: faultclasses [-gsvwh]\n" ); + Abc_Print( -2, "\t computes equivalence classes of faults in the given mapped netlist;\n" ); + Abc_Print( -2, "\t the fault list with faults in the format: \n" ); + Abc_Print( -2, "\t should be read by command \"read_fins\" before calling this command\n" ); + Abc_Print( -2, "\t-g : toggle generating a fault list for the current mapped network [default = %s]\n", fGen? "yes": "no" ); + Abc_Print( -2, "\t-s : toggle detecting sequential equivalence classes [default = %s]\n", fSeq? "yes": "no" ); + Abc_Print( -2, "\t-v : toggle verbose printout during computation [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-w : toggle printing of resulting fault equivalence classes [default = %s]\n", fVeryVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; } diff --git a/src/base/abci/abcDetect.c b/src/base/abci/abcDetect.c index 0125a67e..4325f49c 100644 --- a/src/base/abci/abcDetect.c +++ b/src/base/abci/abcDetect.c @@ -233,7 +233,7 @@ Vec_Int_t * Io_ReadFins( Abc_Ntk_t * pNtk, char * pFileName, int fVerbose ) Vec_IntPushTwo( vPairs, Vec_IntEntry(vMap, iObj), Type ); } assert( Vec_IntSize(vPairs) == 2 * nLines ); - printf( "Finished reading %d lines.\n", nLines - 1 ); + printf( "Finished reading %d lines from the fault list file \"%s\".\n", nLines - 1, pFileName ); // verify the reader by printing the results if ( fVerbose ) -- cgit v1.2.3 From b483c97fdd6e1fe6d52158d1b0231678073ace5e Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 21 Nov 2016 11:52:50 -0800 Subject: Minor bug fixes. --- src/base/abci/abc.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/base/abci') diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 689c21b5..3efc41c9 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -7463,7 +7463,7 @@ usage: Abc_Print( -2, "\t finds optimum networks using SAT-based exact synthesis for hex truth tables ...\n" ); Abc_Print( -2, "\t-D : constrain maximum depth (if too low, algorithm may not terminate)\n" ); Abc_Print( -2, "\t-A : input arrival times (comma separated list)\n" ); - Abc_Print( -2, "\t-S : number of start gates in search [default = %s]\n", nStartGates ); + Abc_Print( -2, "\t-S : number of start gates in search [default = %d]\n", nStartGates ); Abc_Print( -2, "\t-C : the limit on the number of conflicts; turn off with 0 [default = %d]\n", nBTLimit ); Abc_Print( -2, "\t-a : toggle create AIG [default = %s]\n", fMakeAIG ? "yes" : "no" ); Abc_Print( -2, "\t-t : run test suite\n" ); -- cgit v1.2.3 From 64bdbe1a74fcf6343e06caa0dc4f6dae0e621e76 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 22 Nov 2016 20:09:25 -0800 Subject: Adding switch '-c' to generate only stuck-at faults in 'faultclasses -g'. --- src/base/abci/abc.c | 14 +++++++++----- src/base/abci/abcDetect.c | 8 +++++--- 2 files changed, 14 insertions(+), 8 deletions(-) (limited to 'src/base/abci') diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 3efc41c9..4dcea33a 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -7241,18 +7241,21 @@ usage: int Abc_CommandFaultClasses( Abc_Frame_t * pAbc, int argc, char ** argv ) { extern void Abc_NtkDetectClassesTest( Abc_Ntk_t * pNtk, int fSeq, int fVerbose, int fVeryVerbose ); - extern void Abc_NtkGenFaultList( Abc_Ntk_t * pNtk, char * pFileName ); + extern void Abc_NtkGenFaultList( Abc_Ntk_t * pNtk, char * pFileName, int fStuckAt ); Abc_Ntk_t * pNtk; - int c, fGen = 0, fSeq = 0, fVerbose = 0, fVeryVerbose = 0; + int c, fGen = 0, fStuckAt = 0, fSeq = 0, fVerbose = 0, fVeryVerbose = 0; pNtk = Abc_FrameReadNtk(pAbc); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "gsvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "gcsvwh" ) ) != EOF ) { switch ( c ) { case 'g': fGen ^= 1; break; + case 'c': + fStuckAt ^= 1; + break; case 's': fSeq ^= 1; break; @@ -7281,18 +7284,19 @@ int Abc_CommandFaultClasses( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( fGen ) { char * pFileName = Extra_FileNameGenericAppend(Abc_NtkSpec(pNtk), "_faults.txt"); - Abc_NtkGenFaultList( pNtk, pFileName ); + Abc_NtkGenFaultList( pNtk, pFileName, fStuckAt ); } else Abc_NtkDetectClassesTest( pNtk, fSeq, fVerbose, fVeryVerbose ); return 0; usage: - Abc_Print( -2, "usage: faultclasses [-gsvwh]\n" ); + Abc_Print( -2, "usage: faultclasses [-gcsvwh]\n" ); Abc_Print( -2, "\t computes equivalence classes of faults in the given mapped netlist;\n" ); Abc_Print( -2, "\t the fault list with faults in the format: \n" ); Abc_Print( -2, "\t should be read by command \"read_fins\" before calling this command\n" ); Abc_Print( -2, "\t-g : toggle generating a fault list for the current mapped network [default = %s]\n", fGen? "yes": "no" ); + Abc_Print( -2, "\t-c : toggle using only stuck-at faults in the generated fault list [default = %s]\n", fStuckAt? "yes": "no" ); Abc_Print( -2, "\t-s : toggle detecting sequential equivalence classes [default = %s]\n", fSeq? "yes": "no" ); Abc_Print( -2, "\t-v : toggle verbose printout during computation [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-w : toggle printing of resulting fault equivalence classes [default = %s]\n", fVeryVerbose? "yes": "no" ); diff --git a/src/base/abci/abcDetect.c b/src/base/abci/abcDetect.c index 4325f49c..8b8bba64 100644 --- a/src/base/abci/abcDetect.c +++ b/src/base/abci/abcDetect.c @@ -63,7 +63,7 @@ typedef enum { SeeAlso [] ***********************************************************************/ -void Abc_NtkGenFaultList( Abc_Ntk_t * pNtk, char * pFileName ) +void Abc_NtkGenFaultList( Abc_Ntk_t * pNtk, char * pFileName, int fStuckAt ) { Mio_Library_t * pLib = (Mio_Library_t *)pNtk->pManFunc; Mio_Gate_t * pGate; @@ -84,14 +84,16 @@ void Abc_NtkGenFaultList( Abc_Ntk_t * pNtk, char * pFileName ) fprintf( pFile, "%d %s %s\n", Count, Abc_ObjName(pObj), "SA0" ), Count++; fprintf( pFile, "%d %s %s\n", Count, Abc_ObjName(pObj), "SA1" ), Count++; fprintf( pFile, "%d %s %s\n", Count, Abc_ObjName(pObj), "NEG" ), Count++; + if ( fStuckAt ) + continue; // add other faults, which correspond to changing the given gate // by another gate with the same support-size from the same library Mio_LibraryForEachGate( pLib, pGate ) if ( pGate != pGateObj && Mio_GateReadPinNum(pGate) == nInputs ) fprintf( pFile, "%d %s %s\n", Count, Abc_ObjName(pObj), Mio_GateReadName(pGate) ), Count++; } - printf( "Generated fault list \"%s\" for network \"%s\" with %d nodes and %d faults.\n", - pFileName, Abc_NtkName(pNtk), Abc_NtkNodeNum(pNtk), Count-1 ); + printf( "Generated fault list \"%s\" for network \"%s\" with %d nodes and %d %sfaults.\n", + pFileName, Abc_NtkName(pNtk), Abc_NtkNodeNum(pNtk), Count-1, fStuckAt ? "stuck-at ":"" ); fclose( pFile ); } -- cgit v1.2.3 From 6b55bf0205f414ca711d92baea115a808fff3dc9 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 26 Nov 2016 14:28:12 -0800 Subject: New SAT-based optimization package. --- src/base/abci/abc.c | 129 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 129 insertions(+) (limited to 'src/base/abci') diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 4dcea33a..25bcc306 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -55,6 +55,7 @@ #include "sat/bmc/bmc.h" #include "proof/ssc/ssc.h" #include "opt/sfm/sfm.h" +#include "opt/sbd/sbd.h" #include "bool/rpo/rpo.h" #include "map/mpm/mpm.h" #include "opt/fret/fretime.h" @@ -481,6 +482,7 @@ static int Abc_CommandAbc9Acec ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9Esop ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Exorcism ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Mfs ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Mfsd ( Abc_Frame_t * pAbc, int argc, char ** argv ); //static int Abc_CommandAbc9PoPart2 ( Abc_Frame_t * pAbc, int argc, char ** argv ); //static int Abc_CommandAbc9CexCut ( Abc_Frame_t * pAbc, int argc, char ** argv ); //static int Abc_CommandAbc9CexMerge ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -1122,6 +1124,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&esop", Abc_CommandAbc9Esop, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&exorcism", Abc_CommandAbc9Exorcism, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&mfs", Abc_CommandAbc9Mfs, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&mfsd", Abc_CommandAbc9Mfsd, 0 ); // Cmd_CommandAdd( pAbc, "ABC9", "&popart2", Abc_CommandAbc9PoPart2, 0 ); // Cmd_CommandAdd( pAbc, "ABC9", "&cexcut", Abc_CommandAbc9CexCut, 0 ); // Cmd_CommandAdd( pAbc, "ABC9", "&cexmerge", Abc_CommandAbc9CexMerge, 0 ); @@ -40824,6 +40827,132 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc9Mfsd( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * pGia, Sbd_Par_t * pPars ); + Gia_Man_t * pTemp; int c; + Sbd_Par_t Pars, * pPars = &Pars; + Sbd_ParSetDefault( pPars ); + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "KWFMCavwh" ) ) != EOF ) + { + switch ( c ) + { + case 'K': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-K\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nLutSize = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nLutSize < 0 ) + goto usage; + break; + case 'W': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-W\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nTfoLevels = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nTfoLevels < 0 ) + goto usage; + break; + case 'F': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nTfoFanMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nTfoFanMax < 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->nWinSizeMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nWinSizeMax < 0 ) + goto usage; + break; + case 'C': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nBTLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nBTLimit < 0 ) + goto usage; + break; + case 'a': + pPars->fArea ^= 1; + break; + case 'v': + pPars->fVerbose ^= 1; + break; + case 'w': + pPars->fVeryVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9Mfs(): There is no AIG.\n" ); + return 0; + } + if ( Gia_ManBufNum(pAbc->pGia) ) + { + Abc_Print( -1, "Abc_CommandAbc9Mfs(): This command does not work with barrier buffers.\n" ); + return 1; + } + if ( Gia_ManHasMapping(pAbc->pGia) ) + { + Abc_Print( -1, "Abc_CommandAbc9Mfs(): The current AIG has mapping (run &st to unmap).\n" ); + return 0; + } + pTemp = Sbd_NtkPerform( pAbc->pGia, pPars ); + Abc_FrameUpdateGia( pAbc, pTemp ); + return 0; + +usage: + Abc_Print( -2, "usage: &mfsd [-KWFMC ] [-avwh]\n" ); + Abc_Print( -2, "\t performs SAT-based delay-oriented AIG optimization\n" ); + Abc_Print( -2, "\t-K : the LUT size for delay minimization (2 <= num <= 6) [default = %d]\n", pPars->nLutSize ); + Abc_Print( -2, "\t-W : the number of levels in the TFO cone (0 <= num) [default = %d]\n", pPars->nTfoLevels ); + Abc_Print( -2, "\t-F : the max number of fanouts to skip (1 <= num) [default = %d]\n", pPars->nTfoFanMax ); + Abc_Print( -2, "\t-M : the max node count of windows to consider (0 = no limit) [default = %d]\n", pPars->nWinSizeMax ); + Abc_Print( -2, "\t-C : the max number of conflicts in one SAT run (0 = no limit) [default = %d]\n", pPars->nBTLimit ); + Abc_Print( -2, "\t-a : toggle minimizing area or area+edges [default = %s]\n", pPars->fArea? "area": "area+edges" ); + Abc_Print( -2, "\t-v : toggle printing optimization summary [default = %s]\n", pPars->fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-w : toggle printing detailed stats for each node [default = %s]\n", pPars->fVeryVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + /**Function************************************************************* Synopsis [] -- cgit v1.2.3 From 91aab10757add03dc29e5b7d0d966f5784625949 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 4 Dec 2016 13:05:51 -0800 Subject: Analysis of arithmetic logic cones. --- src/base/abci/abc.c | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) (limited to 'src/base/abci') diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 25bcc306..ba4d37b3 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -28220,9 +28220,10 @@ int Abc_CommandAbc9MuxProfile( Abc_Frame_t * pAbc, int argc, char ** argv ) extern void Gia_ManMuxProfiling( Gia_Man_t * p ); extern void Gia_ManProfileStructures( Gia_Man_t * p, int nLimit, int fVerbose ); extern void Acec_StatsCollect( Gia_Man_t * p, int fVerbose ); - int c, fNpn = 0, fMuxes = 0, nLimit = 0, fVerbose = 0; + extern void Acec_ManProfile( Gia_Man_t * p, int fVerbose ); + int c, fNpn = 0, fMuxes = 0, fAdders = 0, nLimit = 0, fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Nnmvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Nnmavh" ) ) != EOF ) { switch ( c ) { @@ -28243,6 +28244,9 @@ int Abc_CommandAbc9MuxProfile( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'm': fMuxes ^= 1; break; + case 'a': + fAdders ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -28268,16 +28272,19 @@ int Abc_CommandAbc9MuxProfile( Abc_Frame_t * pAbc, int argc, char ** argv ) } else if ( fMuxes ) Gia_ManMuxProfiling( pAbc->pGia ); + else if ( fAdders ) + Acec_ManProfile( pAbc->pGia, fVerbose ); else Gia_ManProfileStructures( pAbc->pGia, nLimit, fVerbose ); return 0; usage: - Abc_Print( -2, "usage: &profile [-N num] [-nmvh]\n" ); + Abc_Print( -2, "usage: &profile [-N num] [-nmavh]\n" ); Abc_Print( -2, "\t profile gate structures appearing in the AIG\n" ); Abc_Print( -2, "\t-N num : limit on class size to show [default = %d]\n", nLimit ); Abc_Print( -2, "\t-n : toggle profiling NPN-classes (for 3-LUT mapped AIGs) [default = %s]\n", fNpn? "yes": "no" ); Abc_Print( -2, "\t-m : toggle profiling MUX structures [default = %s]\n", fMuxes? "yes": "no" ); + Abc_Print( -2, "\t-a : toggle profiling adder structures [default = %s]\n", fAdders? "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"); return 1; -- cgit v1.2.3 From 8ba6071a76b2f25995c4048567eb0b3780130ece Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 4 Dec 2016 21:59:10 -0800 Subject: New SAT-based optimization package. --- src/base/abci/abc.c | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) (limited to 'src/base/abci') diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index ba4d37b3..1fdffd77 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -27643,6 +27643,7 @@ static inline int Gia_ManCompareWithBest( Gia_Man_t * pBest, Gia_Man_t * p, int *pnBestLuts = nCurLuts; *pnBestEdges = nCurEdges; *pnBestLevels = nCurLevels; + //printf( "\nUpdating best (%d %d %d).\n\n", nCurLuts, nCurEdges, nCurLevels ); return 1; } return 0; @@ -31023,7 +31024,7 @@ usage: Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit ); Abc_Print( -2, "\t-S num : the max number of SAT variables [default = %d]\n", pPars->nSatVarMax ); Abc_Print( -2, "\t-K num : the target LUT size for downstream mapping [default = %d]\n", nLutSize ); - Abc_Print( -2, "\t-R num : the delay relaxation ratio (num >= 0) [default = %d]\n", nRelaxRatio ); + Abc_Print( -2, "\t-R num : the delay relaxation ratio (num >= 0) [default = %d]\n", nRelaxRatio ); Abc_Print( -2, "\t-f : toggle using lighter logic synthesis [default = %s]\n", pPars->fLightSynth? "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"); @@ -40852,7 +40853,7 @@ int Abc_CommandAbc9Mfsd( Abc_Frame_t * pAbc, int argc, char ** argv ) Sbd_Par_t Pars, * pPars = &Pars; Sbd_ParSetDefault( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "KWFMCavwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "KWFMCacvwh" ) ) != EOF ) { switch ( c ) { @@ -40914,6 +40915,9 @@ int Abc_CommandAbc9Mfsd( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'a': pPars->fArea ^= 1; break; + case 'c': + pPars->fCover ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -40946,7 +40950,7 @@ int Abc_CommandAbc9Mfsd( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &mfsd [-KWFMC ] [-avwh]\n" ); + Abc_Print( -2, "usage: &mfsd [-KWFMC ] [-acvwh]\n" ); Abc_Print( -2, "\t performs SAT-based delay-oriented AIG optimization\n" ); Abc_Print( -2, "\t-K : the LUT size for delay minimization (2 <= num <= 6) [default = %d]\n", pPars->nLutSize ); Abc_Print( -2, "\t-W : the number of levels in the TFO cone (0 <= num) [default = %d]\n", pPars->nTfoLevels ); @@ -40954,6 +40958,7 @@ usage: Abc_Print( -2, "\t-M : the max node count of windows to consider (0 = no limit) [default = %d]\n", pPars->nWinSizeMax ); Abc_Print( -2, "\t-C : the max number of conflicts in one SAT run (0 = no limit) [default = %d]\n", pPars->nBTLimit ); Abc_Print( -2, "\t-a : toggle minimizing area or area+edges [default = %s]\n", pPars->fArea? "area": "area+edges" ); + Abc_Print( -2, "\t-c : toggle using complete slow covering procedure [default = %s]\n", pPars->fCover? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing optimization summary [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-w : toggle printing detailed stats for each node [default = %s]\n", pPars->fVeryVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); -- cgit v1.2.3 From 6a351c4dc0d4da86d2a82efdecd09021a2e6280f Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 5 Dec 2016 17:45:15 -0800 Subject: Adding support for minimalistic representation of LUT mapping. --- src/base/abci/abc.c | 32 ++++++++++++++++++++++---------- 1 file changed, 22 insertions(+), 10 deletions(-) (limited to 'src/base/abci') diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 1fdffd77..9f04926d 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -12074,8 +12074,6 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) { // extern void Cba_PrsReadBlifTest(); // Cba_PrsReadBlifTest(); - extern void Sfm_TimTest( Abc_Ntk_t * pNtk ); - Sfm_TimTest( pNtk ); } return 0; usage: @@ -26998,12 +26996,13 @@ int Abc_CommandAbc9Read( Abc_Frame_t * pAbc, int argc, char ** argv ) char ** pArgvNew; char * FileName, * pTemp; int c, nArgcNew; - int fUseMini = 0; + int fMiniAig = 0; + int fMiniLut = 0; int fVerbose = 0; int fGiaSimple = 0; int fSkipStrash = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "csmvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "csmlvh" ) ) != EOF ) { switch ( c ) { @@ -27014,7 +27013,10 @@ int Abc_CommandAbc9Read( Abc_Frame_t * pAbc, int argc, char ** argv ) fSkipStrash ^= 1; break; case 'm': - fUseMini ^= 1; + fMiniAig ^= 1; + break; + case 'l': + fMiniLut ^= 1; break; case 'v': fVerbose ^= 1; @@ -27047,8 +27049,10 @@ int Abc_CommandAbc9Read( Abc_Frame_t * pAbc, int argc, char ** argv ) } fclose( pFile ); - if ( fUseMini ) + if ( fMiniAig ) pAig = Gia_ManReadMiniAig( FileName ); + else if ( fMiniLut ) + pAig = Gia_ManReadMiniLut( FileName ); // else if ( Extra_FileIsType( FileName, ".v", NULL, NULL ) ) // Abc3_ReadShowHie( FileName, fSkipStrash ); else @@ -27058,11 +27062,12 @@ int Abc_CommandAbc9Read( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &r [-csmvh] \n" ); + Abc_Print( -2, "usage: &r [-csmlvh] \n" ); Abc_Print( -2, "\t reads the current AIG from the AIGER file\n" ); Abc_Print( -2, "\t-c : toggles reading simple AIG [default = %s]\n", fGiaSimple? "yes": "no" ); Abc_Print( -2, "\t-s : toggles structural hashing while reading [default = %s]\n", !fSkipStrash? "yes": "no" ); - Abc_Print( -2, "\t-m : toggles reading MiniAIG rather than AIGER file [default = %s]\n", fUseMini? "yes": "no" ); + Abc_Print( -2, "\t-m : toggles reading MiniAIG rather than AIGER file [default = %s]\n", fMiniAig? "yes": "no" ); + Abc_Print( -2, "\t-l : toggles reading MiniLUT rather than AIGER file [default = %s]\n", fMiniLut? "yes": "no" ); Abc_Print( -2, "\t-v : toggles additional verbose output [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); Abc_Print( -2, "\t : the file name\n"); @@ -27843,9 +27848,10 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv ) int c, nArgcNew; int fUnique = 0; int fMiniAig = 0; + int fMiniLut = 0; int fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "umvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "umlvh" ) ) != EOF ) { switch ( c ) { @@ -27855,6 +27861,9 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'm': fMiniAig ^= 1; break; + case 'l': + fMiniLut ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -27885,15 +27894,18 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv ) } else if ( fMiniAig ) Gia_ManWriteMiniAig( pAbc->pGia, pFileName ); + else if ( fMiniLut ) + Gia_ManWriteMiniLut( pAbc->pGia, pFileName ); else Gia_AigerWrite( pAbc->pGia, pFileName, 0, 0 ); return 0; usage: - Abc_Print( -2, "usage: &w [-umvh] \n" ); + Abc_Print( -2, "usage: &w [-umlvh] \n" ); Abc_Print( -2, "\t writes the current AIG into the AIGER file\n" ); Abc_Print( -2, "\t-u : toggle writing canonical AIG structure [default = %s]\n", fUnique? "yes" : "no" ); Abc_Print( -2, "\t-m : toggle writing MiniAIG rather than AIGER [default = %s]\n", fMiniAig? "yes" : "no" ); + Abc_Print( -2, "\t-l : toggle writing MiniLUT rather than AIGER [default = %s]\n", fMiniLut? "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"); Abc_Print( -2, "\t : the file name\n"); -- cgit v1.2.3 From 3169bd96b784cbc86bb523cb6de094580299fdb6 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 5 Dec 2016 17:48:21 -0800 Subject: Compiler warnings. --- src/base/abci/abc.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/base/abci') diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 9f04926d..7da88d3c 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -11867,7 +11867,7 @@ int Abc_CommandTestColor( Abc_Frame_t * pAbc, int argc, char ** argv ) ***********************************************************************/ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) { - Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc); + //Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc); int nCutMax = 1; int nLeafMax = 4; int nDivMax = 2; -- cgit v1.2.3