abcDetect.c File Reference

#include "base/abc/abc.h"
#include "misc/vec/vecHsh.h"
#include "misc/util/utilNam.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satStore.h"
#include "map/mio/mio.h"
#include "map/mio/exp.h"

Include dependency graph for abcDetect.c:

Go to the source code of this file.

Enumerations
enum	Abc_FinType_t {   ABC_FIN_NONE = -100 , ABC_FIN_SA0 , ABC_FIN_SA1 , ABC_FIN_NEG ,   ABC_FIN_RDOB_AND , ABC_FIN_RDOB_NAND , ABC_FIN_RDOB_OR , ABC_FIN_RDOB_NOR ,   ABC_FIN_RDOB_XOR , ABC_FIN_RDOB_NXOR , ABC_FIN_RDOB_NOT , ABC_FIN_RDOB_BUFF ,   ABC_FIN_RDOB_LAST }
	DECLARATIONS ///. More...

Functions
void	Abc_NtkGenFaultList (Abc_Ntk_t *pNtk, char *pFileName, int fStuckAt)
	FUNCTION DEFINITIONS ///.
int	Io_ReadFinTypeMapped (Mio_Library_t *pLib, char *pThis)
int	Io_ReadFinType (char *pThis)
char *	Io_WriteFinType (int Type)
Vec_Int_t *	Io_ReadFins (Abc_Ntk_t *pNtk, char *pFileName, int fVerbose)
void	Abc_NtkFrameExtend (Abc_Ntk_t *pNtk)
int	Abc_NtkDetectObjClasses_rec (Abc_Obj_t *pObj, Vec_Int_t *vMap, Hsh_VecMan_t *pHash, Vec_Int_t *vTemp)
Vec_Wec_t *	Abc_NtkDetectObjClasses (Abc_Ntk_t *pNtk, Vec_Int_t *vObjs, Vec_Wec_t **pvCos)
void	Abc_NtkDetectClassesTest2 (Abc_Ntk_t *pNtk, int fVerbose, int fVeryVerbose)
void	Abc_NtkFinMiterCollect_rec (Abc_Obj_t *pObj, Vec_Int_t *vCis, Vec_Int_t *vNodes)
void	Abc_NtkFinMiterCollect (Abc_Ntk_t *pNtk, Vec_Int_t *vCos, Vec_Int_t *vCis, Vec_Int_t *vNodes)
void	Mio_LibGateSimulate (Mio_Gate_t *pGate, word *ppFaninSims[6], int nWords, word *pObjSim)
int	Mio_LibGateSimulateOne (Mio_Gate_t *pGate, int iBits[6])
int	Mio_LibGateSimulateGia (Gia_Man_t *pGia, Mio_Gate_t *pGate, int iLits[6], Vec_Int_t *vLits)
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)
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)
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)
void	Abc_NtkFinLocalSetup (Vec_Int_t *vPairs, Vec_Int_t *vList, Vec_Wec_t *vMap2, Vec_Int_t *vResArray)
void	Abc_NtkFinLocalSetdown (Vec_Int_t *vPairs, Vec_Int_t *vList, Vec_Wec_t *vMap2)
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)
int	Abc_NtkFinCheckTypesOk (Abc_Ntk_t *pNtk)
int	Abc_NtkFinCheckTypesOk2 (Abc_Ntk_t *pNtk)
Vec_Int_t *	Abc_NtkFinComputeTypes (Abc_Ntk_t *pNtk)
Vec_Int_t *	Abc_NtkFinComputeObjects (Vec_Int_t *vPairs, Vec_Wec_t **pvMap, int nObjs)
Vec_Int_t *	Abc_NtkFinCreateList (Vec_Wec_t *vMap, Vec_Int_t *vClass)
int	Abc_NtkFinCountPairs (Vec_Wec_t *vClasses)
Vec_Wec_t *	Abc_NtkDetectFinClasses (Abc_Ntk_t *pNtk, int fVerbose)
void	Abc_NtkPrintFinResults (Vec_Wec_t *vClasses)
void	Abc_NtkDetectClassesTest (Abc_Ntk_t *pNtk, int fSeq, int fVerbose, int fVeryVerbose)

Enumeration Type Documentation

Abc_FinType_t

enum Abc_FinType_t

DECLARATIONS ///.

CFile****************************************************************

FileName [abcDetect.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Network and node package.]

Synopsis [Detect conditions.]

Author [Alan Mishchenko, Dao Ai Quoc]

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

]

Enumerator
ABC_FIN_NONE
ABC_FIN_SA0
ABC_FIN_SA1
ABC_FIN_NEG
ABC_FIN_RDOB_AND
ABC_FIN_RDOB_NAND
ABC_FIN_RDOB_OR
ABC_FIN_RDOB_NOR
ABC_FIN_RDOB_XOR
ABC_FIN_RDOB_NXOR
ABC_FIN_RDOB_NOT
ABC_FIN_RDOB_BUFF
ABC_FIN_RDOB_LAST

Definition at line 35 of file abcDetect.c.

             { 
    ABC_FIN_NONE = -100,   //  0:  unknown
    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;

Function Documentation

Abc_NtkDetectClassesTest()

void Abc_NtkDetectClassesTest	(	Abc_Ntk_t *	pNtk,
		int	fSeq,
		int	fVerbose,
		int	fVeryVerbose )

Function*************************************************************

Synopsis [Top-level procedure.]

Description []

SideEffects []

SeeAlso []

Definition at line 1241 of file abcDetect.c.

{
    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 );
}

Here is the call graph for this function:

Abc_NtkDetectClassesTest2()

void Abc_NtkDetectClassesTest2	(	Abc_Ntk_t *	pNtk,
		int	fVerbose,
		int	fVeryVerbose )

Definition at line 462 of file abcDetect.c.

{
    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 );
}

Here is the call graph for this function:

Abc_NtkDetectFinClasses()

Vec_Wec_t * Abc_NtkDetectFinClasses	(	Abc_Ntk_t *	pNtk,
		int	fVerbose )

Definition at line 1128 of file abcDetect.c.

{
    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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_NtkDetectObjClasses()

Vec_Wec_t * Abc_NtkDetectObjClasses	(	Abc_Ntk_t *	pNtk,
		Vec_Int_t *	vObjs,
		Vec_Wec_t **	pvCos )

Definition at line 391 of file abcDetect.c.

{
    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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_NtkDetectObjClasses_rec()

int Abc_NtkDetectObjClasses_rec	(	Abc_Obj_t *	pObj,
		Vec_Int_t *	vMap,
		Hsh_VecMan_t *	pHash,
		Vec_Int_t *	vTemp )

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 []

Definition at line 347 of file abcDetect.c.

{
    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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_NtkFinCheckPair()

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 )

Function*************************************************************

Synopsis [Check equivalence using SAT solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 893 of file abcDetect.c.

{
    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
    {
        Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( pGia, 8, 0, 1, 0, 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, 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;
        }
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_NtkFinCheckTypesOk()

int Abc_NtkFinCheckTypesOk

(

Abc_Ntk_t *

pNtk

)

Definition at line 1065 of file abcDetect.c.

{
    Abc_Obj_t * pObj; int i;
    Abc_NtkForEachNode( pNtk, pObj, i )
        if ( Abc_ObjFinGateType(pObj) == ABC_FIN_NONE )
            return i;
    return 0;
}

Here is the caller graph for this function:

Abc_NtkFinCheckTypesOk2()

int Abc_NtkFinCheckTypesOk2

(

Abc_Ntk_t *

pNtk

)

Definition at line 1073 of file abcDetect.c.

{
    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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_NtkFinComputeObjects()

Vec_Int_t * Abc_NtkFinComputeObjects	(	Vec_Int_t *	vPairs,
		Vec_Wec_t **	pvMap,
		int	nObjs )

Definition at line 1099 of file abcDetect.c.

{
    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;
}

Here is the caller graph for this function:

Abc_NtkFinComputeTypes()

Vec_Int_t * Abc_NtkFinComputeTypes

(

Abc_Ntk_t *

pNtk

)

Definition at line 1091 of file abcDetect.c.

{
    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;
}

Here is the caller graph for this function:

Abc_NtkFinCountPairs()

int Abc_NtkFinCountPairs

(

Vec_Wec_t *

vClasses

)

Definition at line 1120 of file abcDetect.c.

{
    int i, Counter = 0;
    Vec_Int_t * vLevel;
    Vec_WecForEachLevel( vClasses, vLevel, i )
        Counter += Vec_IntSize(vLevel) - 1;
    return Counter;
}

Here is the caller graph for this function:

Abc_NtkFinCreateList()

Vec_Int_t * Abc_NtkFinCreateList	(	Vec_Wec_t *	vMap,
		Vec_Int_t *	vClass )

Definition at line 1112 of file abcDetect.c.

{
    int i, iObj;
    Vec_Int_t * vList = Vec_IntAlloc( 100 );
    Vec_IntForEachEntry( vClass, iObj, i )
        Vec_IntAppend( vList, Vec_WecEntry(vMap, iObj) );
    return vList;
}

Here is the caller graph for this function:

Abc_NtkFinLocalSetdown()

void Abc_NtkFinLocalSetdown	(	Vec_Int_t *	vPairs,
		Vec_Int_t *	vList,
		Vec_Wec_t *	vMap2 )

Definition at line 960 of file abcDetect.c.

{
    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 );
    }
}

Here is the caller graph for this function:

Abc_NtkFinLocalSetup()

void Abc_NtkFinLocalSetup	(	Vec_Int_t *	vPairs,
		Vec_Int_t *	vList,
		Vec_Wec_t *	vMap2,
		Vec_Int_t *	vResArray )

Function*************************************************************

Synopsis [Refinement of equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 948 of file abcDetect.c.

{
    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 );
    }
}

Here is the caller graph for this function:

Abc_NtkFinMiterCollect()

void Abc_NtkFinMiterCollect	(	Abc_Ntk_t *	pNtk,
		Vec_Int_t *	vCos,
		Vec_Int_t *	vCis,
		Vec_Int_t *	vNodes )

Definition at line 509 of file abcDetect.c.

{
    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 );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_NtkFinMiterCollect_rec()

void Abc_NtkFinMiterCollect_rec	(	Abc_Obj_t *	pObj,
		Vec_Int_t *	vCis,
		Vec_Int_t *	vNodes )

Function*************************************************************

Synopsis [Collecting objects.]

Description [Collects combinational inputs (vCIs) and internal nodes (vNodes) reachable from the given set of combinational outputs (vCOs).]

SideEffects []

SeeAlso []

Definition at line 493 of file abcDetect.c.

{
    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) );
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_NtkFinMiterToGia()

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 )

Definition at line 728 of file abcDetect.c.

{
    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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_NtkFinRefinement()

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 )

Definition at line 970 of file abcDetect.c.

{
    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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_NtkFinSimulateOne()

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 )

Definition at line 783 of file abcDetect.c.

{
    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 );
    }
}

Here is the caller graph for this function:

Abc_NtkFrameExtend()

void Abc_NtkFrameExtend

(

Abc_Ntk_t *

pNtk

)

Function*************************************************************

Synopsis [Extend the network by adding second timeframe.]

Description []

SideEffects []

SeeAlso []

Definition at line 264 of file abcDetect.c.

{
    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 );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_NtkGenFaultList()

void Abc_NtkGenFaultList	(	Abc_Ntk_t *	pNtk,
		char *	pFileName,
		int	fStuckAt )

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis [Generates fault list for the given mapped network.]

Description []

SideEffects []

SeeAlso []

Definition at line 66 of file abcDetect.c.

{
    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++;
        if ( fStuckAt )
            continue;
        // add other faults, which correspond to changing the given gate
        // by another gate with the same support-size from the same library
        Mio_LibraryForEachGate( pLib, pGate )
            if ( pGate != pGateObj && Mio_GateReadPinNum(pGate) == nInputs )
                fprintf( pFile, "%d %s %s\n", Count, Abc_ObjName(pObj), Mio_GateReadName(pGate) ), Count++;
    }
    printf( "Generated fault list \"%s\" for network \"%s\" with %d nodes and %d %sfaults.\n", 
        pFileName, Abc_NtkName(pNtk), Abc_NtkNodeNum(pNtk), Count-1, fStuckAt ? "stuck-at ":"" );
    fclose( pFile );
}

Here is the call graph for this function:

Abc_NtkPrintFinResults()

void Abc_NtkPrintFinResults

(

Vec_Wec_t *

vClasses

)

Function*************************************************************

Synopsis [Print results.]

Description []

SideEffects []

SeeAlso []

Definition at line 1221 of file abcDetect.c.

{
    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 );
}

Io_ReadFins()

Vec_Int_t * Io_ReadFins	(	Abc_Ntk_t *	pNtk,
		char *	pFileName,
		int	fVerbose )

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 []

Definition at line 164 of file abcDetect.c.

{
    Mio_Library_t * pLib = (Mio_Library_t *)pNtk->pManFunc;
    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 );
    Vec_IntPushTwo( vPairs, -1, -1 );
    while ( fgets(Buffer, 1000, pFile) != NULL )
    {
        // 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" );
            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" );
        if ( Abc_NtkIsMappedLogic(pNtk) )
        {
            if ( !strcmp(pToken, "SA0") || !strcmp(pToken, "SA1") || !strcmp(pToken, "NEG") )
                Type = Io_ReadFinType( pToken );
            else
                Type = Io_ReadFinTypeMapped( pLib, pToken );
        }
        else
            Type = Io_ReadFinType( pToken );
        if ( Type == ABC_FIN_NONE )
        {
            printf( "Cannot read type \"%s\" of object \"%s\".\n", pToken, Abc_ObjName(Abc_NtkObj(pNtk, iObj)) );
            continue;
        }
        Vec_IntPushTwo( vPairs, Vec_IntEntry(vMap, iObj), Type );
    }
    assert( Vec_IntSize(vPairs) == 2 * nLines );
    printf( "Finished reading %d lines from the fault list file \"%s\".\n", nLines - 1, pFileName );
 
    // verify the reader by printing the results
    if ( fVerbose )
        Vec_IntForEachEntryDoubleStart( vPairs, iObj, Type, i, 2 )
            printf( "%-10d%-10s%-10s\n", i/2, Abc_ObjName(Abc_NtkObj(pNtk, iObj)), Io_WriteFinType(Type) );
 
finish:
    Vec_IntFree( vMap );
    Abc_NamDeref( pNam );
    fclose( pFile );
    return vPairs;
}

Here is the call graph for this function:

Io_ReadFinType()

int Io_ReadFinType

(

char *

pThis

)

Definition at line 121 of file abcDetect.c.

{
    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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Io_ReadFinTypeMapped()

int Io_ReadFinTypeMapped	(	Mio_Library_t *	pLib,
		char *	pThis )

Function*************************************************************

Synopsis [Recognize type.]

Description []

SideEffects []

SeeAlso []

Definition at line 111 of file abcDetect.c.

{
    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 );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Io_WriteFinType()

char * Io_WriteFinType

(

int

Type

)

Definition at line 136 of file abcDetect.c.

{
    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";
}

Here is the caller graph for this function:

Mio_LibGateSimulate()

void Mio_LibGateSimulate	(	Mio_Gate_t *	pGate,
		word *	ppFaninSims[6],
		int	nWords,
		word *	pObjSim )

Function*************************************************************

Synopsis [Simulates expression using given simulation info.]

Description []

SideEffects []

SeeAlso []

Definition at line 530 of file abcDetect.c.

{
    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 );
    }
}

Here is the call graph for this function:

Mio_LibGateSimulateGia()

int Mio_LibGateSimulateGia	(	Gia_Man_t *	pGia,
		Mio_Gate_t *	pGate,
		int	iLits[6],
		Vec_Int_t *	vLits )

Function*************************************************************

Synopsis [Simulated expression with one bit.]

Description []

SideEffects []

SeeAlso []

Definition at line 576 of file abcDetect.c.

{
    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 );
}

Here is the call graph for this function:

Mio_LibGateSimulateOne()

int Mio_LibGateSimulateOne	(	Mio_Gate_t *	pGate,
		int	iBits[6] )

Function*************************************************************

Synopsis [Simulates expression for one simulation pattern.]

Description []

SideEffects []

SeeAlso []

Definition at line 555 of file abcDetect.c.

{
    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 );
}

Here is the call graph for this function: