mirror of https://github.com/YosysHQ/abc.git
Detecting properties of internal nodes.
This commit is contained in:
parent
a18da5c878
commit
0a1b6f8fcc
|
|
@ -7216,7 +7216,7 @@ usage:
|
||||||
***********************************************************************/
|
***********************************************************************/
|
||||||
int Abc_CommandDetect( Abc_Frame_t * pAbc, int argc, char ** argv )
|
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;
|
Abc_Ntk_t * pNtk;
|
||||||
int c, fVerbose = 0;
|
int c, fVerbose = 0;
|
||||||
pNtk = Abc_FrameReadNtk(pAbc);
|
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" );
|
Abc_Print( -1, "Only applicable to a logic network.\n" );
|
||||||
return 1;
|
return 1;
|
||||||
}
|
}
|
||||||
Abc_NtkDetectClassesTest( pNtk );
|
Abc_NtkDetectClassesTest( pNtk, fVerbose );
|
||||||
return 0;
|
return 0;
|
||||||
|
|
||||||
usage:
|
usage:
|
||||||
|
|
|
||||||
|
|
@ -8,7 +8,7 @@
|
||||||
|
|
||||||
Synopsis [Detect conditions.]
|
Synopsis [Detect conditions.]
|
||||||
|
|
||||||
Author [Alan Mishchenko]
|
Author [Alan Mishchenko, Dao Ai Quoc]
|
||||||
|
|
||||||
Affiliation [UC Berkeley]
|
Affiliation [UC Berkeley]
|
||||||
|
|
||||||
|
|
@ -21,10 +21,11 @@
|
||||||
#include "base/abc/abc.h"
|
#include "base/abc/abc.h"
|
||||||
#include "misc/vec/vecHsh.h"
|
#include "misc/vec/vecHsh.h"
|
||||||
#include "misc/util/utilNam.h"
|
#include "misc/util/utilNam.h"
|
||||||
|
#include "sat/cnf/cnf.h"
|
||||||
|
#include "sat/bsat/satStore.h"
|
||||||
|
|
||||||
ABC_NAMESPACE_IMPL_START
|
ABC_NAMESPACE_IMPL_START
|
||||||
|
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////
|
||||||
/// DECLARATIONS ///
|
/// DECLARATIONS ///
|
||||||
////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
@ -45,15 +46,6 @@ typedef enum {
|
||||||
ABC_FIN_RDOB_LAST // 12:
|
ABC_FIN_RDOB_LAST // 12:
|
||||||
} Abc_FinType_t;
|
} 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 ///
|
/// 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) );
|
assert( Vec_IntSize(vMap) == Abc_NamObjNumMax(pNam) );
|
||||||
// read file lines
|
// read file lines
|
||||||
vPairs = Vec_IntAlloc( 1000 );
|
vPairs = Vec_IntAlloc( 1000 );
|
||||||
|
Vec_IntPushTwo( vPairs, -1, -1 );
|
||||||
while ( fgets(Buffer, 1000, pFile) != NULL )
|
while ( fgets(Buffer, 1000, pFile) != NULL )
|
||||||
{
|
{
|
||||||
// read line number
|
// read line number
|
||||||
|
|
@ -168,17 +161,18 @@ Vec_Int_t * Io_ReadFins( Abc_Ntk_t * pNtk, char * pFileName, int fVerbose )
|
||||||
Type = Io_ReadFinType( pToken );
|
Type = Io_ReadFinType( pToken );
|
||||||
if ( Type == ABC_FIN_NONE )
|
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;
|
continue;
|
||||||
}
|
}
|
||||||
Vec_IntPushTwo( vPairs, Vec_IntEntry(vMap, iObj), Type );
|
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.\n", nLines - 1 );
|
||||||
|
|
||||||
// verify the reader by printing the results
|
// verify the reader by printing the results
|
||||||
if ( fVerbose )
|
if ( fVerbose )
|
||||||
Vec_IntForEachEntryDouble( vPairs, iObj, Type, i )
|
Vec_IntForEachEntryDoubleStart( vPairs, iObj, Type, i, 2 )
|
||||||
printf( "%-10d%-10s%-10s\n", i/2+1, Abc_ObjName(Abc_NtkObj(pNtk, iObj)), Io_WriteFinType(Type) );
|
printf( "%-10d%-10s%-10s\n", i/2, Abc_ObjName(Abc_NtkObj(pNtk, iObj)), Io_WriteFinType(Type) );
|
||||||
|
|
||||||
finish:
|
finish:
|
||||||
Vec_IntFree( vMap );
|
Vec_IntFree( vMap );
|
||||||
|
|
@ -190,138 +184,7 @@ finish:
|
||||||
|
|
||||||
/**Function*************************************************************
|
/**Function*************************************************************
|
||||||
|
|
||||||
Synopsis [Detect equivalence classes of nodes in terms of their TFO.]
|
Synopsis [Top-level procedure.]
|
||||||
|
|
||||||
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.]
|
|
||||||
|
|
||||||
Description []
|
Description []
|
||||||
|
|
||||||
|
|
@ -330,46 +193,12 @@ void Abc_NtkDetectClassesTest( Abc_Ntk_t * pNtk )
|
||||||
SeeAlso []
|
SeeAlso []
|
||||||
|
|
||||||
***********************************************************************/
|
***********************************************************************/
|
||||||
Vec_Int_t * Abc_NtkComputeObjects( Vec_Int_t * vPairs )
|
void Abc_NtkDetectClassesTest( Abc_Ntk_t * pNtk, int fVerbose )
|
||||||
{
|
{
|
||||||
int iObj, Type, i;
|
printf( "This procedure is currently not used.\n" );
|
||||||
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 );
|
|
||||||
}
|
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////
|
||||||
/// END OF FILE ///
|
/// END OF FILE ///
|
||||||
////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
|
||||||
|
|
@ -556,7 +556,7 @@ int Cba_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv )
|
||||||
Abc_FrameUpdateGia( pAbc, pNew );
|
Abc_FrameUpdateGia( pAbc, pNew );
|
||||||
return 0;
|
return 0;
|
||||||
usage:
|
usage:
|
||||||
Abc_Print( -2, "usage: %%blast [-svh]\n" );
|
Abc_Print( -2, "usage: @blast [-svh]\n" );
|
||||||
Abc_Print( -2, "\t performs bit-blasting of the word-level design\n" );
|
Abc_Print( -2, "\t performs bit-blasting of the word-level design\n" );
|
||||||
Abc_Print( -2, "\t-s : toggle blasting sequential elements [default = %s]\n", fSeq? "yes": "no" );
|
Abc_Print( -2, "\t-s : toggle blasting sequential elements [default = %s]\n", fSeq? "yes": "no" );
|
||||||
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
|
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue