From 0a1b6f8fcc72d24e11171a31dc1aeced322ea4bf Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 14 Jun 2016 15:37:59 -0700 Subject: Detecting properties of internal nodes. --- src/base/abci/abc.c | 4 +- src/base/abci/abcDetect.c | 195 +++------------------------------------------- 2 files changed, 14 insertions(+), 185 deletions(-) (limited to 'src/base/abci') diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index a5b96c24..5ac2cd09 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -7216,7 +7216,7 @@ usage: ***********************************************************************/ int Abc_CommandDetect( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern void Abc_NtkDetectClassesTest( Abc_Ntk_t * pNtk ); + extern void Abc_NtkDetectClassesTest( Abc_Ntk_t * pNtk, int fVerbose ); Abc_Ntk_t * pNtk; int c, fVerbose = 0; pNtk = Abc_FrameReadNtk(pAbc); @@ -7244,7 +7244,7 @@ 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 ); + Abc_NtkDetectClassesTest( pNtk, fVerbose ); return 0; usage: diff --git a/src/base/abci/abcDetect.c b/src/base/abci/abcDetect.c index 91fa2d9f..8fa395e8 100644 --- a/src/base/abci/abcDetect.c +++ b/src/base/abci/abcDetect.c @@ -8,7 +8,7 @@ Synopsis [Detect conditions.] - Author [Alan Mishchenko] + Author [Alan Mishchenko, Dao Ai Quoc] Affiliation [UC Berkeley] @@ -21,10 +21,11 @@ #include "base/abc/abc.h" #include "misc/vec/vecHsh.h" #include "misc/util/utilNam.h" +#include "sat/cnf/cnf.h" +#include "sat/bsat/satStore.h" ABC_NAMESPACE_IMPL_START - //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -45,15 +46,6 @@ typedef enum { ABC_FIN_RDOB_LAST // 12: } Abc_FinType_t; -typedef struct Fin_Info_t_ -{ - Vec_Int_t * vPairs; // original info as a set of pairs (ObjId, TypeId) - Vec_Int_t * vObjs; // all those objects that have some info - Vec_Wec_t * vMap; // for each object, the set of types - Vec_Wec_t * vClasses; // classes of objects - -} Abc_FinInfo_t; - //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -145,6 +137,7 @@ Vec_Int_t * Io_ReadFins( Abc_Ntk_t * pNtk, char * pFileName, int fVerbose ) assert( Vec_IntSize(vMap) == Abc_NamObjNumMax(pNam) ); // read file lines vPairs = Vec_IntAlloc( 1000 ); + Vec_IntPushTwo( vPairs, -1, -1 ); while ( fgets(Buffer, 1000, pFile) != NULL ) { // read line number @@ -168,17 +161,18 @@ Vec_Int_t * Io_ReadFins( Abc_Ntk_t * pNtk, char * pFileName, int fVerbose ) Type = Io_ReadFinType( pToken ); if ( Type == ABC_FIN_NONE ) { - printf( "Cannot read type \"%s\" of object \"%s\".\n", pToken, Abc_ObjName(pObj) ); + printf( "Cannot read type \"%s\" of object \"%s\".\n", pToken, Abc_ObjName(Abc_NtkObj(pNtk, iObj)) ); continue; } Vec_IntPushTwo( vPairs, Vec_IntEntry(vMap, iObj), Type ); } + assert( Vec_IntSize(vPairs) == 2 * nLines ); printf( "Finished reading %d lines.\n", nLines - 1 ); // verify the reader by printing the results if ( fVerbose ) - Vec_IntForEachEntryDouble( vPairs, iObj, Type, i ) - printf( "%-10d%-10s%-10s\n", i/2+1, Abc_ObjName(Abc_NtkObj(pNtk, iObj)), Io_WriteFinType(Type) ); + Vec_IntForEachEntryDoubleStart( vPairs, iObj, Type, i, 2 ) + printf( "%-10d%-10s%-10s\n", i/2, Abc_ObjName(Abc_NtkObj(pNtk, iObj)), Io_WriteFinType(Type) ); finish: Vec_IntFree( vMap ); @@ -190,138 +184,7 @@ finish: /**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_NtkDetectClasses_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_NtkDetectClasses_rec( Abc_ObjFanout0(pObj), vMap, pHash, vTemp ); - if ( Abc_ObjFanoutNum(pObj) == 1 ) - 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_NtkDetectClasses_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_NtkDetectClasses( Abc_Ntk_t * pNtk, Vec_Int_t * vObjs ) -{ - 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, i ); - 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_NtkDetectClasses_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 ) - { - // 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) ); - } - Hsh_VecManStop( pHash ); - Vec_IntFree( vClassMap ); - Vec_IntFree( vMap ); - return vClasses; -} -void Abc_NtkDetectClassesTest( Abc_Ntk_t * pNtk ) -{ - Vec_Int_t * vObjs; - Vec_Wec_t * vRes; - // 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_NtkDetectClasses( pNtk, vObjs ); - Vec_WecPrint( vRes, 0 ); - // clean up - Vec_IntFree( vObjs ); - Vec_WecFree( vRes ); -} - -/**Function************************************************************* - - Synopsis [Miter construction.] + Synopsis [Top-level procedure.] Description [] @@ -330,46 +193,12 @@ void Abc_NtkDetectClassesTest( Abc_Ntk_t * pNtk ) SeeAlso [] ***********************************************************************/ -Vec_Int_t * Abc_NtkComputeObjects( Vec_Int_t * vPairs ) +void Abc_NtkDetectClassesTest( Abc_Ntk_t * pNtk, int fVerbose ) { - int iObj, Type, i; - Vec_Int_t * vObjs = Vec_IntAlloc( 100 ); - Vec_IntForEachEntryDouble( vPairs, iObj, Type, i ) - Vec_IntPush( vObjs, iObj ); - Vec_IntUniqify( vObjs ); - return vObjs; -} -Vec_Wec_t * Abc_NtkComputeObjInfo( Vec_Int_t * vPairs, int nObjs ) -{ - int iObj, Type, i; - Vec_Wec_t * vInfo = Vec_WecStart( nObjs ); - Vec_IntForEachEntryDouble( vPairs, iObj, Type, i ) - Vec_WecPush( vInfo, iObj, Type ); - return vInfo; -} -void Abc_NtkSolveClassesTest( Abc_Ntk_t * pNtk ) -{ - Abc_FinInfo_t * p; - if ( pNtk->vFins == NULL ) - { - printf( "Current network does not have the required info.\n" ); - return; - } - // collect data - p = ABC_CALLOC( Abc_FinInfo_t, 1 ); - p->vPairs = pNtk->vFins; - p->vObjs = Abc_NtkComputeObjects( p->vPairs ); - p->vMap = Abc_NtkComputeObjInfo( p->vPairs, Abc_NtkObjNumMax(pNtk) ); - p->vClasses = Abc_NtkDetectClasses( pNtk, p->vObjs ); - - - // cleanup - Vec_WecFree( p->vClasses ); - Vec_WecFree( p->vMap ); - Vec_IntFree( p->vObjs ); - ABC_FREE( p ); + printf( "This procedure is currently not used.\n" ); } + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -- cgit v1.2.3