Skip to content

A
abc
Commit c6afb9db by Alan Mishchenko
Options

Equivalent fault detection code.

parent 6cd66183
Showing with 1086 additions and 8 deletions
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;
}
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:
......@@ -52,6 +54,49 @@ typedef enum {
/**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.]
Description []
......@@ -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,6 +216,14 @@ Vec_Int_t * Io_ReadFins( Abc_Ntk_t * pNtk, char * pFileName, int fVerbose )
}
// read type
pToken = strtok( NULL, " \n\r\t" );
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 )
{
......@@ -184,6 +250,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.]
Description []
......@@ -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 );
}
......
src/map/mio/mio.h
......@@ -112,6 +112,7 @@ extern char * Mio_LibraryReadName ( Mio_Library_t * pLib );
extern int Mio_LibraryReadGateNum ( Mio_Library_t * pLib );
extern Mio_Gate_t * Mio_LibraryReadGates ( Mio_Library_t * pLib );
extern Mio_Gate_t ** Mio_LibraryReadGateArray ( Mio_Library_t * pLib );
extern Mio_Gate_t * Mio_LibraryReadGateById ( Mio_Library_t * pLib, int iD );
extern Mio_Gate_t * Mio_LibraryReadGateByName ( Mio_Library_t * pLib, char * pName, char * pOutName );
extern char * Mio_LibraryReadSopByName ( Mio_Library_t * pLib, char * pName );
extern Mio_Gate_t * Mio_LibraryReadGateByTruth( Mio_Library_t * pLib, word t );
......
src/map/mio/mioApi.c
......@@ -44,6 +44,7 @@ char * Mio_LibraryReadName ( Mio_Library_t * pLib ) { retur
int Mio_LibraryReadGateNum ( Mio_Library_t * pLib ) { return pLib->nGates; }
Mio_Gate_t * Mio_LibraryReadGates ( Mio_Library_t * pLib ) { return pLib->pGates; }
Mio_Gate_t ** Mio_LibraryReadGateArray ( Mio_Library_t * pLib ) { return pLib->ppGatesName;}
Mio_Gate_t * Mio_LibraryReadGateById ( Mio_Library_t * pLib, int Id ) { assert( pLib->ppGates0[Id]->Cell == Id ); return pLib->ppGates0[Id];}
Mio_Gate_t * Mio_LibraryReadBuf ( Mio_Library_t * pLib ) { return pLib->pGateBuf; }
Mio_Gate_t * Mio_LibraryReadInv ( Mio_Library_t * pLib ) { return pLib->pGateInv; }
Mio_Gate_t * Mio_LibraryReadConst0 ( Mio_Library_t * pLib ) { return pLib->pGate0; }
......
src/map/mio/mioRead.c
......@@ -586,7 +586,10 @@ void Mio_LibrarySortGates( Mio_Library_t * pLib )
int i = 0;
ppGates = ABC_ALLOC( Mio_Gate_t *, pLib->nGates );
Mio_LibraryForEachGate( pLib, pGate )
{
pGate->Cell = i;
ppGates[i++] = pGate;
}
assert( i == pLib->nGates );
// sort gates by name
pLib->ppGates0 = ABC_ALLOC( Mio_Gate_t *, pLib->nGates );
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment