luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity
abc/src/base/abci/abcDetect.c

1266 lines
48 KiB
C
Raw Normal View History

Detecting properties of internal nodes.
2016-06-07 23:32:38 +02:00
/**CFile****************************************************************
FileName [abcDetect.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Network and node package.]
Synopsis [Detect conditions.]
Detecting properties of internal nodes.
2016-06-15 00:37:59 +02:00
Author [Alan Mishchenko, Dao Ai Quoc]
Detecting properties of internal nodes.
2016-06-07 23:32:38 +02:00
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 7, 2016.]
Revision [$Id: abcDetect.c,v 1.00 2016/06/07 00:00:00 alanmi Exp $]
***********************************************************************/
#include "base/abc/abc.h"
#include "misc/vec/vecHsh.h"
Detecting properties of internal nodes.
2016-06-13 04:07:46 +02:00
#include "misc/util/utilNam.h"
Detecting properties of internal nodes.
2016-06-15 00:37:59 +02:00
#include "sat/cnf/cnf.h"
#include "sat/bsat/satStore.h"
Equivalent fault detection code.
2016-11-10 06:17:44 +01:00
#include "map/mio/mio.h"
#include "map/mio/exp.h"
Detecting properties of internal nodes.
2016-06-07 23:32:38 +02:00
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
Detecting properties of internal nodes.
2016-06-13 04:07:46 +02:00
typedef enum {
Equivalent fault detection code.
2016-11-10 06:17:44 +01:00
ABC_FIN_NONE = -100, // 0: unknown
Detecting properties of internal nodes.
2016-06-13 04:07:46 +02:00
ABC_FIN_SA0, // 1:
ABC_FIN_SA1, // 2:
ABC_FIN_NEG, // 3:
ABC_FIN_RDOB_AND, // 4:
ABC_FIN_RDOB_NAND, // 5:
ABC_FIN_RDOB_OR, // 6:
ABC_FIN_RDOB_NOR, // 7:
ABC_FIN_RDOB_XOR, // 8:
ABC_FIN_RDOB_NXOR, // 9:
ABC_FIN_RDOB_NOT, // 10:
ABC_FIN_RDOB_BUFF, // 11:
ABC_FIN_RDOB_LAST // 12:
} Abc_FinType_t;
Detecting properties of internal nodes.
2016-06-07 23:32:38 +02:00
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
Equivalent fault detection code.
2016-11-10 06:17:44 +01:00
/**Function*************************************************************
Synopsis [Generates fault list for the given mapped network.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Adding switch '-c' to generate only stuck-at faults in 'faultclasses -g'.
2016-11-23 05:09:25 +01:00
void Abc_NtkGenFaultList( Abc_Ntk_t * pNtk, char * pFileName, int fStuckAt )
Equivalent fault detection code.
2016-11-10 06:17:44 +01:00
{
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++;
Adding switch '-c' to generate only stuck-at faults in 'faultclasses -g'.
2016-11-23 05:09:25 +01:00
if ( fStuckAt )
continue;
Equivalent fault detection code.
2016-11-10 06:17:44 +01:00
// 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++;
}
Adding switch '-c' to generate only stuck-at faults in 'faultclasses -g'.
2016-11-23 05:09:25 +01:00
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 ":"" );
Equivalent fault detection code.
2016-11-10 06:17:44 +01:00
fclose( pFile );
}
Detecting properties of internal nodes.
2016-06-13 04:07:46 +02:00
/**Function*************************************************************
Synopsis [Recognize type.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Equivalent fault detection code.
2016-11-10 06:17:44 +01:00
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 );
}
Detecting properties of internal nodes.
2016-06-13 04:07:46 +02:00
int Io_ReadFinType( char * pThis )
{
if ( !strcmp(pThis, "SA0") ) return ABC_FIN_SA0;
if ( !strcmp(pThis, "SA1") ) return ABC_FIN_SA1;
if ( !strcmp(pThis, "NEG") ) return ABC_FIN_NEG;
if ( !strcmp(pThis, "RDOB_AND") ) return ABC_FIN_RDOB_AND;
if ( !strcmp(pThis, "RDOB_NAND") ) return ABC_FIN_RDOB_NAND;
if ( !strcmp(pThis, "RDOB_OR") ) return ABC_FIN_RDOB_OR;
if ( !strcmp(pThis, "RDOB_NOR") ) return ABC_FIN_RDOB_NOR;
if ( !strcmp(pThis, "RDOB_XOR") ) return ABC_FIN_RDOB_XOR;
if ( !strcmp(pThis, "RDOB_NXOR") ) return ABC_FIN_RDOB_NXOR;
if ( !strcmp(pThis, "RDOB_NOT") ) return ABC_FIN_RDOB_NOT;
if ( !strcmp(pThis, "RDOB_BUFF") ) return ABC_FIN_RDOB_BUFF;
return ABC_FIN_NONE;
}
char * Io_WriteFinType( int Type )
{
if ( Type == ABC_FIN_SA0 ) return "SA0";
if ( Type == ABC_FIN_SA1 ) return "SA1";
if ( Type == ABC_FIN_NEG ) return "NEG";
if ( Type == ABC_FIN_RDOB_AND ) return "RDOB_AND" ;
if ( Type == ABC_FIN_RDOB_NAND ) return "RDOB_NAND";
if ( Type == ABC_FIN_RDOB_OR ) return "RDOB_OR" ;
if ( Type == ABC_FIN_RDOB_NOR ) return "RDOB_NOR" ;
if ( Type == ABC_FIN_RDOB_XOR ) return "RDOB_XOR" ;
if ( Type == ABC_FIN_RDOB_NXOR ) return "RDOB_NXOR";
if ( Type == ABC_FIN_RDOB_NOT ) return "RDOB_NOT" ;
if ( Type == ABC_FIN_RDOB_BUFF ) return "RDOB_BUFF";
return "Unknown";
}
/**Function*************************************************************
Synopsis [Read information from file.]
Description [Returns information as a set of pairs: (ObjId, TypeId).
Uses the current network to map ObjName given in the file into ObjId.]
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Io_ReadFins( Abc_Ntk_t * pNtk, char * pFileName, int fVerbose )
{
Equivalent fault detection code.
2016-11-10 06:17:44 +01:00
Mio_Library_t * pLib = (Mio_Library_t *)pNtk->pManFunc;
Detecting properties of internal nodes.
2016-06-13 04:07:46 +02:00
char Buffer[1000];
Abc_Obj_t * pObj;
Abc_Nam_t * pNam;
Vec_Int_t * vMap;
Vec_Int_t * vPairs = NULL;
int i, Type, iObj, fFound, nLines = 1;
FILE * pFile = fopen( pFileName, "r" );
if ( pFile == NULL )
{
printf( "Cannot open input file \"%s\" for reading.\n", pFileName );
return NULL;
}
// map CI/node names into their IDs
pNam = Abc_NamStart( 1000, 10 );
vMap = Vec_IntAlloc( 1000 );
Vec_IntPush( vMap, -1 );
Abc_NtkForEachObj( pNtk, pObj, i )
{
if ( !Abc_ObjIsCi(pObj) && !Abc_ObjIsNode(pObj) )
continue;
Abc_NamStrFindOrAdd( pNam, Abc_ObjName(pObj), &fFound );
if ( fFound )
{
printf( "The same name \"%s\" appears twice among CIs and internal nodes.\n", Abc_ObjName(pObj) );
goto finish;
}
Vec_IntPush( vMap, Abc_ObjId(pObj) );
}
assert( Vec_IntSize(vMap) == Abc_NamObjNumMax(pNam) );
// read file lines
vPairs = Vec_IntAlloc( 1000 );
Detecting properties of internal nodes.
2016-06-15 00:37:59 +02:00
Vec_IntPushTwo( vPairs, -1, -1 );
Detecting properties of internal nodes.
2016-06-13 04:07:46 +02:00
while ( fgets(Buffer, 1000, pFile) != NULL )
{
// read line number
char * pToken = strtok( Buffer, " \n\r\t" );
Equivalent fault detection code.
2016-11-10 06:17:44 +01:00
if ( pToken == NULL )
break;
Detecting properties of internal nodes.
2016-06-13 04:07:46 +02:00
if ( nLines++ != atoi(pToken) )
{
printf( "Line numbers are not consecutive. Quitting.\n" );
Vec_IntFreeP( &vPairs );
goto finish;
}
// read object name and find its ID
pToken = strtok( NULL, " \n\r\t" );
iObj = Abc_NamStrFind( pNam, pToken );
if ( !iObj )
{
printf( "Cannot find object with name \"%s\".\n", pToken );
continue;
}
// read type
pToken = strtok( NULL, " \n\r\t" );
Equivalent fault detection code.
2016-11-10 06:17:44 +01:00
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 );
Detecting properties of internal nodes.
2016-06-13 04:07:46 +02:00
if ( Type == ABC_FIN_NONE )
{
Detecting properties of internal nodes.
2016-06-15 00:37:59 +02:00
printf( "Cannot read type \"%s\" of object \"%s\".\n", pToken, Abc_ObjName(Abc_NtkObj(pNtk, iObj)) );
Detecting properties of internal nodes.
2016-06-13 04:07:46 +02:00
continue;
}
Vec_IntPushTwo( vPairs, Vec_IntEntry(vMap, iObj), Type );
}
Detecting properties of internal nodes.
2016-06-15 00:37:59 +02:00
assert( Vec_IntSize(vPairs) == 2 * nLines );
Renaming command 'detect' to be 'faultclasses'.
2016-11-10 18:38:07 +01:00
printf( "Finished reading %d lines from the fault list file \"%s\".\n", nLines - 1, pFileName );
Detecting properties of internal nodes.
2016-06-13 04:07:46 +02:00
// verify the reader by printing the results
if ( fVerbose )
Detecting properties of internal nodes.
2016-06-15 00:37:59 +02:00
Vec_IntForEachEntryDoubleStart( vPairs, iObj, Type, i, 2 )
printf( "%-10d%-10s%-10s\n", i/2, Abc_ObjName(Abc_NtkObj(pNtk, iObj)), Io_WriteFinType(Type) );
Detecting properties of internal nodes.
2016-06-13 04:07:46 +02:00
finish:
Vec_IntFree( vMap );
Abc_NamDeref( pNam );
fclose( pFile );
return vPairs;
}
Equivalent fault detection code.
2016-11-10 06:17:44 +01:00
/**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 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 );
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 );
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 );
}
Detecting properties of internal nodes.
2016-06-07 23:32:38 +02:00
/**Function*************************************************************
Detecting properties of internal nodes.
2016-06-15 00:37:59 +02:00
Synopsis [Top-level procedure.]
Detecting properties of internal nodes.
2016-06-13 04:07:46 +02:00
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Equivalent fault detection code.
2016-11-10 06:17:44 +01:00
void Abc_NtkDetectClassesTest( Abc_Ntk_t * pNtk, int fSeq, int fVerbose, int fVeryVerbose )
Detecting properties of internal nodes.
2016-06-13 04:07:46 +02:00
{
Equivalent fault detection code.
2016-11-10 06:17:44 +01:00
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 );
Detecting properties of internal nodes.
2016-06-13 04:07:46 +02:00
}
Detecting properties of internal nodes.
2016-06-15 00:37:59 +02:00
Detecting properties of internal nodes.
2016-06-07 23:32:38 +02:00
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END