abcBm.c File Reference

#include "base/abc/abc.h"
#include "opt/sim/sim.h"
#include "sat/bsat/satSolver.h"

Include dependency graph for abcBm.c:

Go to the source code of this file.

Macros
#define	FALSE   0
#define	TRUE   1

Functions
int	match1by1 (Abc_Ntk_t *pNtk1, Vec_Ptr_t **nodesInLevel1, Vec_Int_t **iMatch1, Vec_Int_t **iDep1, Vec_Int_t *matchedInputs1, int *iGroup1, Vec_Int_t **oMatch1, int *oGroup1, Abc_Ntk_t *pNtk2, Vec_Ptr_t **nodesInLevel2, Vec_Int_t **iMatch2, Vec_Int_t **iDep2, Vec_Int_t *matchedInputs2, int *iGroup2, Vec_Int_t **oMatch2, int *oGroup2, Vec_Int_t *matchedOutputs1, Vec_Int_t *matchedOutputs2, Vec_Int_t *oMatchedGroups, Vec_Int_t *iNonSingleton, int ii, int idx)
int	Abc_NtkBmSat (Abc_Ntk_t *pNtk1, Abc_Ntk_t *pNtk2, Vec_Ptr_t *iMatchPairs, Vec_Ptr_t *oMatchPairs, Vec_Int_t *mismatch, int mode)
void	getDependencies (Abc_Ntk_t *pNtk, Vec_Int_t **iDep, Vec_Int_t **oDep)
void	initMatchList (Abc_Ntk_t *pNtk, Vec_Int_t **iDep, Vec_Int_t **oDep, Vec_Int_t **iMatch, int *iLastItem, Vec_Int_t **oMatch, int *oLastItem, int *iGroup, int *oGroup, int p_equivalence)
void	iSortDependencies (Abc_Ntk_t *pNtk, Vec_Int_t **iDep, int *oGroup)
void	oSortDependencies (Abc_Ntk_t *pNtk, Vec_Int_t **oDep, int *iGroup)
int	oSplitByDep (Abc_Ntk_t *pNtk, Vec_Int_t **oDep, Vec_Int_t **oMatch, int *oGroup, int *oLastItem, int *iGroup)
int	iSplitByDep (Abc_Ntk_t *pNtk, Vec_Int_t **iDep, Vec_Int_t **iMatch, int *iGroup, int *iLastItem, int *oGroup)
Vec_Ptr_t **	findTopologicalOrder (Abc_Ntk_t *pNtk)
int *	Abc_NtkSimulateOneNode (Abc_Ntk_t *pNtk, int *pModel, int input, Vec_Ptr_t **topOrder)
int	refineIOBySimulation (Abc_Ntk_t *pNtk, Vec_Int_t **iMatch, int *iLastItem, int *iGroup, Vec_Int_t **iDep, Vec_Int_t **oMatch, int *oLastItem, int *oGroup, Vec_Int_t **oDep, char *vPiValues, int *observability, Vec_Ptr_t **topOrder)
Abc_Ntk_t *	Abc_NtkMiterBm (Abc_Ntk_t *pNtk1, Abc_Ntk_t *pNtk2, Vec_Ptr_t *iCurrMatch, Vec_Ptr_t *oCurrMatch)
void	Abc_NtkVerifyReportError (Abc_Ntk_t *pNtk1, Abc_Ntk_t *pNtk2, int *pModel, Vec_Int_t *mismatch)
int	Abc_NtkMiterSatBm (Abc_Ntk_t *pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fVerbose, ABC_INT64_T *pNumConfs, ABC_INT64_T *pNumInspects)
int	checkEquivalence (Abc_Ntk_t *pNtk1, Vec_Int_t *matchedInputs1, Vec_Int_t *matchedOutputs1, Abc_Ntk_t *pNtk2, Vec_Int_t *matchedInputs2, Vec_Int_t *matchedOutputs2)
Abc_Ntk_t *	computeCofactor (Abc_Ntk_t *pNtk, Vec_Ptr_t **nodesInLevel, int *bitVector, Vec_Int_t *currInputs)
int	matchNonSingletonOutputs (Abc_Ntk_t *pNtk1, Vec_Ptr_t **nodesInLevel1, Vec_Int_t **iMatch1, Vec_Int_t **iDep1, Vec_Int_t *matchedInputs1, int *iGroup1, Vec_Int_t **oMatch1, int *oGroup1, Abc_Ntk_t *pNtk2, Vec_Ptr_t **nodesInLevel2, Vec_Int_t **iMatch2, Vec_Int_t **iDep2, Vec_Int_t *matchedInputs2, int *iGroup2, Vec_Int_t **oMatch2, int *oGroup2, Vec_Int_t *matchedOutputs1, Vec_Int_t *matchedOutputs2, Vec_Int_t *oMatchedGroups, Vec_Int_t *iNonSingleton, Abc_Ntk_t *subNtk1, Abc_Ntk_t *subNtk2, Vec_Ptr_t *oMatchPairs, Vec_Int_t *oNonSingleton, int oI, int idx, int ii, int iidx)
float	refineBySAT (Abc_Ntk_t *pNtk1, Vec_Int_t **iMatch1, int *iGroup1, Vec_Int_t **iDep1, int *iLastItem1, Vec_Int_t **oMatch1, int *oGroup1, Vec_Int_t **oDep1, int *oLastItem1, int *observability1, Abc_Ntk_t *pNtk2, Vec_Int_t **iMatch2, int *iGroup2, Vec_Int_t **iDep2, int *iLastItem2, Vec_Int_t **oMatch2, int *oGroup2, Vec_Int_t **oDep2, int *oLastItem2, int *observability2)
int	checkListConsistency (Vec_Int_t **iMatch1, Vec_Int_t **oMatch1, Vec_Int_t **iMatch2, Vec_Int_t **oMatch2, int iLastItem1, int oLastItem1, int iLastItem2, int oLastItem2)
void	bmGateWay (Abc_Ntk_t *pNtk1, Abc_Ntk_t *pNtk2, int p_equivalence)

Variables
int *	pValues1__
int *	pValues2__
FILE *	matchFile

Macro Definition Documentation

FALSE

#define FALSE   0

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

FileName [bm.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Boolean Matching package.]

Synopsis [Check P-equivalence and PP-equivalence of two circuits.]

Author [Hadi Katebi]

Affiliation [University of Michigan]

Date [Ver. 1.0. Started - January, 2009.]

Revision [No revisions so far]

Comments [This is the cleaned up version of the code I used for DATE 2010 publication.]
[If you have any question or if you find a bug, contact me at hadik.nosp@m.@umi.nosp@m.ch.ed.nosp@m.u.] [I don't guarantee that I can fix all the bugs, but I can definitely point you to the right direction so you can fix the bugs yourself].

Debugging [There are some part of the code that are commented out. Those parts mostly print the contents of the data structures to the standard output. Un-comment them if you find them useful for debugging.]

Definition at line 37 of file abcBm.c.

TRUE

#define TRUE   1

Definition at line 38 of file abcBm.c.

Function Documentation

Abc_NtkBmSat()

int Abc_NtkBmSat	(	Abc_Ntk_t *	pNtk1,
		Abc_Ntk_t *	pNtk2,
		Vec_Ptr_t *	iMatchPairs,
		Vec_Ptr_t *	oMatchPairs,
		Vec_Int_t *	mismatch,
		int	mode )

Definition at line 967 of file abcBm.c.

{    
    extern Abc_Ntk_t * Abc_NtkMulti( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple, int fFactor );    
 
    Abc_Ntk_t * pMiter = NULL;
    Abc_Ntk_t * pCnf;
    int RetValue = 0;
 
    // get the miter of the two networks
    if( mode == 0 )
    {
        //Abc_NtkDelete( pMiter );
        pMiter = Abc_NtkMiterBm( pNtk1, pNtk2, iMatchPairs, oMatchPairs );
    }
    else if( mode == 1 )        // add new outputs
    {        
        int i;
        Abc_Obj_t * pObj;
        Vec_Ptr_t * vPairs;
        Abc_Obj_t * pNtkMiter;        
 
        vPairs = Vec_PtrAlloc( 100 );
 
        Abc_NtkForEachCo( pMiter, pObj, i )            
            Abc_ObjRemoveFanins( pObj );
 
        for(i = 0; i < Vec_PtrSize( oMatchPairs ); i += 2)
        {
            Vec_PtrPush( vPairs, Abc_ObjChild0Copy((Abc_Obj_t *)Vec_PtrEntry(oMatchPairs, i)) );
            Vec_PtrPush( vPairs, Abc_ObjChild0Copy((Abc_Obj_t *)Vec_PtrEntry(oMatchPairs, i+1)) );
        }
        pNtkMiter = Abc_AigMiter( (Abc_Aig_t *)pMiter->pManFunc, vPairs, 0 );
        Abc_ObjAddFanin( Abc_NtkPo(pMiter,0), pNtkMiter );     
        Vec_PtrFree( vPairs);
    }
    else if( mode == 2 )        // add some outputs
    {
 
    }
    else if( mode == 3)            // remove all outputs
    {
    }
 
    if ( pMiter == NULL )
    {
        printf("Miter computation has failed.");        
        return -1;
    }
    RetValue = Abc_NtkMiterIsConstant( pMiter );
    if ( RetValue == 0)
    {        
        /*printf("Networks are NOT EQUIVALENT after structural hashing.");    */
        // report the error        
        if(mismatch != NULL)
        {
            pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, 1 );
            Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel, mismatch );
            ABC_FREE( pMiter->pModel );
        }        
        Abc_NtkDelete( pMiter );
        return RetValue;
    }
    if( RetValue == 1 )
    {        
        /*printf("Networks are equivalent after structural hashing.");    */
        Abc_NtkDelete( pMiter );
        return RetValue;
    }
 
    // convert the miter into a CNF
    //if(mode == 0)
    pCnf = Abc_NtkMulti( pMiter, 0, 100, 1, 0, 0, 0 );
    Abc_NtkDelete( pMiter );
    if ( pCnf == NULL )
    {        
        printf("Renoding for CNF has failed.");    
        return -1;
    }
 
    // solve the CNF using the SAT solver
    RetValue = Abc_NtkMiterSat( pCnf, (ABC_INT64_T)10000, (ABC_INT64_T)0, 0, NULL, NULL);
    /*if ( RetValue == -1 )
        printf("Networks are undecided (SAT solver timed out).");    
    else if ( RetValue == 0 )        
        printf("Networks are NOT EQUIVALENT after SAT.");    
    else
        printf("Networks are equivalent after SAT.");    */
    if ( mismatch != NULL && pCnf->pModel )
        Abc_NtkVerifyReportError( pNtk1, pNtk2, pCnf->pModel, mismatch );
 
    ABC_FREE( pCnf->pModel );
    Abc_NtkDelete( pCnf );
 
    return RetValue;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_NtkMiterBm()

Abc_Ntk_t * Abc_NtkMiterBm	(	Abc_Ntk_t *	pNtk1,
		Abc_Ntk_t *	pNtk2,
		Vec_Ptr_t *	iCurrMatch,
		Vec_Ptr_t *	oCurrMatch )

Definition at line 700 of file abcBm.c.

{
    char Buffer[1000];
    Abc_Ntk_t * pNtkMiter;
 
    pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
    sprintf( Buffer, "%s_%s_miter", pNtk1->pName, pNtk2->pName );
    pNtkMiter->pName = Extra_UtilStrsav(Buffer);
 
    //Abc_NtkMiterPrepare( pNtk1, pNtk2, pNtkMiter, fComb, nPartSize );
    {
        Abc_Obj_t * pObj, * pObjNew;
        int i;
 
        Abc_AigConst1(pNtk1)->pCopy = Abc_AigConst1(pNtkMiter);
        Abc_AigConst1(pNtk2)->pCopy = Abc_AigConst1(pNtkMiter);
 
        // create new PIs and remember them in the old PIs
        if(iCurrMatch == NULL)
        {
            Abc_NtkForEachCi( pNtk1, pObj, i )
            {
                pObjNew = Abc_NtkCreatePi( pNtkMiter );
                // remember this PI in the old PIs
                pObj->pCopy = pObjNew;
                pObj = Abc_NtkCi(pNtk2, i);  
                pObj->pCopy = pObjNew;
                // add name
                Abc_ObjAssignName( pObjNew, Abc_ObjName(pObj), NULL );
            }
        }
        else
        {
            for(i = 0; i < Vec_PtrSize( iCurrMatch ); i += 2)
            {
                pObjNew = Abc_NtkCreatePi( pNtkMiter );
                pObj = (Abc_Obj_t *)Vec_PtrEntry(iCurrMatch, i);
                pObj->pCopy = pObjNew;
                pObj = (Abc_Obj_t *)Vec_PtrEntry(iCurrMatch, i+1);
                pObj->pCopy = pObjNew;
                // add name
                Abc_ObjAssignName( pObjNew, Abc_ObjName(pObj), NULL );
            }
        }
 
        // create the only PO
        pObjNew = Abc_NtkCreatePo( pNtkMiter );
        // add the PO name
        Abc_ObjAssignName( pObjNew, "miter", NULL );
    }
 
    // Abc_NtkMiterAddOne( pNtk1, pNtkMiter );
    {
        Abc_Obj_t * pNode;
        int i;
        assert( Abc_NtkIsDfsOrdered(pNtk1) );
        Abc_AigForEachAnd( pNtk1, pNode, i )
            pNode->pCopy = Abc_AigAnd( (Abc_Aig_t *)pNtkMiter->pManFunc, Abc_ObjChild0Copy(pNode), Abc_ObjChild1Copy(pNode) );
    }
 
    // Abc_NtkMiterAddOne( pNtk2, pNtkMiter );
    {
        Abc_Obj_t * pNode;
        int i;
        assert( Abc_NtkIsDfsOrdered(pNtk2) );
        Abc_AigForEachAnd( pNtk2, pNode, i )
            pNode->pCopy = Abc_AigAnd( (Abc_Aig_t *)pNtkMiter->pManFunc, Abc_ObjChild0Copy(pNode), Abc_ObjChild1Copy(pNode) );
    }
    
    // Abc_NtkMiterFinalize( pNtk1, pNtk2, pNtkMiter, fComb, nPartSize );    
    {
        Vec_Ptr_t * vPairs;
        Abc_Obj_t * pMiter;
        int i;
 
        vPairs = Vec_PtrAlloc( 100 );
        
        // collect the CO nodes for the miter
        if(oCurrMatch != NULL)
        {
            for(i = 0; i < Vec_PtrSize( oCurrMatch ); i += 2)
            {
                Vec_PtrPush( vPairs, Abc_ObjChild0Copy((Abc_Obj_t *)Vec_PtrEntry(oCurrMatch, i)) );
                Vec_PtrPush( vPairs, Abc_ObjChild0Copy((Abc_Obj_t *)Vec_PtrEntry(oCurrMatch, i+1)) );
            }
        }
        else
        {
            Abc_Obj_t * pNode;
 
            Abc_NtkForEachCo( pNtk1, pNode, i )
            {
                Vec_PtrPush( vPairs, Abc_ObjChild0Copy(pNode) );
                pNode = Abc_NtkCo( pNtk2, i );
                Vec_PtrPush( vPairs, Abc_ObjChild0Copy(pNode) );
            }
        }
        
     pMiter = Abc_AigMiter( (Abc_Aig_t *)pNtkMiter->pManFunc, vPairs, 0 );
     Abc_ObjAddFanin( Abc_NtkPo(pNtkMiter,0), pMiter );
     Vec_PtrFree(vPairs);
    }
 
    //Abc_AigCleanup(pNtkMiter->pManFunc);
    
    return pNtkMiter;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_NtkMiterSatBm()

int Abc_NtkMiterSatBm	(	Abc_Ntk_t *	pNtk,
		ABC_INT64_T	nConfLimit,
		ABC_INT64_T	nInsLimit,
		int	fVerbose,
		ABC_INT64_T *	pNumConfs,
		ABC_INT64_T *	pNumInspects )

Definition at line 871 of file abcBm.c.

{
    static sat_solver * pSat = NULL;
    lbool   status;
    int RetValue = 0;
    abctime clk;    
 
    extern int Abc_NodeAddClausesTop( sat_solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars );
    extern Vec_Int_t * Abc_NtkGetCiSatVarNums( Abc_Ntk_t * pNtk );    
 
    if ( pNumConfs )
        *pNumConfs = 0;
    if ( pNumInspects )
        *pNumInspects = 0;
 
    assert( Abc_NtkLatchNum(pNtk) == 0 );
 
//    if ( Abc_NtkPoNum(pNtk) > 1 )
//        fprintf( stdout, "Warning: The miter has %d outputs. SAT will try to prove all of them.\n", Abc_NtkPoNum(pNtk) );
 
    // load clauses into the sat_solver
    clk = Abc_Clock();
 
            
        
    pSat = (sat_solver *)Abc_NtkMiterSatCreate( pNtk, 0 );
            
    if ( pSat == NULL )
        return 1;
//printf( "%d \n", pSat->clauses.size );
//sat_solver_delete( pSat );
//return 1;
 
//    printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
//    PRT( "Time", Abc_Clock() - clk );
 
    // simplify the problem
    clk = Abc_Clock();
    status = sat_solver_simplify(pSat);
//    printf( "Simplified the problem to %d variables and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
//    PRT( "Time", Abc_Clock() - clk );
    if ( status == 0 )
    {
        sat_solver_delete( pSat );
//        printf( "The problem is UNSATISFIABLE after simplification.\n" );
        return 1;
    }
 
    // solve the miter
    clk = Abc_Clock();
    if ( fVerbose )
        pSat->verbosity = 1;
    status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, (ABC_INT64_T)0, (ABC_INT64_T)0 );
    if ( status == l_Undef )
    {
//        printf( "The problem timed out.\n" );
        RetValue = -1;
    }
    else if ( status == l_True )
    {
//        printf( "The problem is SATISFIABLE.\n" );
        RetValue = 0;
    }
    else if ( status == l_False )
    {
//        printf( "The problem is UNSATISFIABLE.\n" );
        RetValue = 1;
    }
    else
        assert( 0 );
//    PRT( "SAT sat_solver time", Abc_Clock() - clk );
//    printf( "The number of conflicts = %d.\n", (int)pSat->sat_solver_stats.conflicts );
 
    // if the problem is SAT, get the counterexample
    if ( status == l_True )
    {
//        Vec_Int_t * vCiIds = Abc_NtkGetCiIds( pNtk );
        Vec_Int_t * vCiIds = Abc_NtkGetCiSatVarNums( pNtk );
        pNtk->pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize );
        Vec_IntFree( vCiIds );
    }
    // free the sat_solver
    if ( fVerbose )
        Sat_SolverPrintStats( stdout, pSat );
 
    if ( pNumConfs )
        *pNumConfs = (int)pSat->stats.conflicts;
    if ( pNumInspects )
        *pNumInspects = (int)pSat->stats.inspects;
 
//sat_solver_store_write( pSat, "trace.cnf" );    
    sat_solver_store_free( pSat );
    sat_solver_delete( pSat );
    return RetValue;
}

Here is the call graph for this function:

Abc_NtkSimulateOneNode()

int * Abc_NtkSimulateOneNode	(	Abc_Ntk_t *	pNtk,
		int *	pModel,
		int	input,
		Vec_Ptr_t **	topOrder )

Definition at line 449 of file abcBm.c.

{
    Abc_Obj_t * pNode;
    Vec_Ptr_t * vNodes;
    int * pValues, Value0, Value1, i;
   
    vNodes = Vec_PtrAlloc( 50 );
/*
    printf( "Counter example: " );
    Abc_NtkForEachCi( pNtk, pNode, i )
        printf( " %d", pModel[i] );
    printf( "\n" );
*/
    // increment the trav ID
    Abc_NtkIncrementTravId( pNtk );
    // set the CI values     
    Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)1;
    pNode = Abc_NtkCi(pNtk, input);
    pNode->iTemp = pModel[input];
    
    // simulate in the topological order    
    for(i = Vec_PtrSize(topOrder[input])-1; i >= 0; i--)
    {
        pNode = (Abc_Obj_t *)Vec_PtrEntry(topOrder[input], i);        
        
        Value0 = ((int)(ABC_PTRUINT_T)Abc_ObjFanin0(pNode)->pCopy) ^ Abc_ObjFaninC0(pNode);
        Value1 = ((int)(ABC_PTRUINT_T)Abc_ObjFanin1(pNode)->pCopy) ^ Abc_ObjFaninC1(pNode);
        
        if( pNode->iTemp != (Value0 & Value1))
        {
            pNode->iTemp = (Value0 & Value1);
            Vec_PtrPush(vNodes, pNode);
        }
    
    }    
    // fill the output values
    pValues = ABC_ALLOC( int, Abc_NtkCoNum(pNtk) );
    Abc_NtkForEachCo( pNtk, pNode, i )
        pValues[i] = ((int)(ABC_PTRUINT_T)Abc_ObjFanin0(pNode)->pCopy) ^ Abc_ObjFaninC0(pNode);
    
    pNode = Abc_NtkCi(pNtk, input);
    if(pNode->pCopy == (Abc_Obj_t *)1)
        pNode->pCopy = (Abc_Obj_t *)0;
    else
        pNode->pCopy = (Abc_Obj_t *)1;
 
    for(i = 0; i < Vec_PtrSize(vNodes); i++)
    {
        pNode = (Abc_Obj_t *)Vec_PtrEntry(vNodes, i);
 
        if(pNode->pCopy == (Abc_Obj_t *)1)
            pNode->pCopy = (Abc_Obj_t *)0;
        else
            pNode->pCopy = (Abc_Obj_t *)1;
    }
 
    Vec_PtrFree( vNodes );
 
    return pValues;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_NtkVerifyReportError()

void Abc_NtkVerifyReportError	(	Abc_Ntk_t *	pNtk1,
		Abc_Ntk_t *	pNtk2,
		int *	pModel,
		Vec_Int_t *	mismatch )

Definition at line 810 of file abcBm.c.

{
    Vec_Ptr_t * vNodes;
    Abc_Obj_t * pNode;    
    int nErrors, nPrinted, i, iNode = -1;
 
    assert( Abc_NtkCiNum(pNtk1) == Abc_NtkCiNum(pNtk2) );
    assert( Abc_NtkCoNum(pNtk1) == Abc_NtkCoNum(pNtk2) );
    // get the CO values under this model
    pValues1__ = Abc_NtkVerifySimulatePattern( pNtk1, pModel );
    pValues2__ = Abc_NtkVerifySimulatePattern( pNtk2, pModel );
    // count the mismatches
    nErrors = 0;
    for ( i = 0; i < Abc_NtkCoNum(pNtk1); i++ )
        nErrors += (int)( pValues1__[i] != pValues2__[i] );
    //printf( "Verification failed for at least %d outputs: ", nErrors );
    // print the first 3 outputs
    nPrinted = 0;
    for ( i = 0; i < Abc_NtkCoNum(pNtk1); i++ )
        if ( pValues1__[i] != pValues2__[i] )
        {
            if ( iNode == -1 )
                iNode = i;
            //printf( " %s", Abc_ObjName(Abc_NtkCo(pNtk1,i)) );
            if ( ++nPrinted == 3 )
                break;
        }
    /*if ( nPrinted != nErrors )
        printf( " ..." );
    printf( "\n" );*/
    // report mismatch for the first output
    if ( iNode >= 0 )
    {
        /*printf( "Output %s: Value in Network1 = %d. Value in Network2 = %d.\n", 
            Abc_ObjName(Abc_NtkCo(pNtk1,iNode)), pValues1[iNode], pValues2[iNode] );
        printf( "Input pattern: " );*/
        // collect PIs in the cone
        pNode = Abc_NtkCo(pNtk1,iNode);
        vNodes = Abc_NtkNodeSupport( pNtk1, &pNode, 1 );
        // set the PI numbers
        Abc_NtkForEachCi( pNtk1, pNode, i )
            pNode->iTemp = i;
        // print the model
        pNode = (Abc_Obj_t *)Vec_PtrEntry( vNodes, 0 );
        if ( Abc_ObjIsCi(pNode) )
        {
            Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
            {
                assert( Abc_ObjIsCi(pNode) );
                //printf( " %s=%d", Abc_ObjName(pNode), pModel[(int)pNode->pCopy] );
                Vec_IntPush(mismatch, Abc_ObjId(pNode)-1);
                Vec_IntPush(mismatch, pModel[(int)(size_t)pNode->pCopy]);
            }
        }
        //printf( "\n" );
        Vec_PtrFree( vNodes );
    }
    free( pValues1__ );
    free( pValues2__ );
}

Here is the call graph for this function:

Here is the caller graph for this function:

bmGateWay()

void bmGateWay	(	Abc_Ntk_t *	pNtk1,
		Abc_Ntk_t *	pNtk2,
		int	p_equivalence )

Definition at line 1779 of file abcBm.c.

{    
    Vec_Int_t ** iDep1, ** oDep1;
    Vec_Int_t ** iDep2, ** oDep2;
    Vec_Int_t ** iMatch1, ** oMatch1;
    Vec_Int_t ** iMatch2, ** oMatch2;        
    int * iGroup1, * oGroup1;
    int * iGroup2, * oGroup2;
    int iLastItem1, oLastItem1;
    int iLastItem2, oLastItem2;    
    int i, j;    
    
    char * vPiValues1, * vPiValues2;
    int * observability1, * observability2;
    abctime clk = Abc_Clock();
    float initTime;
    float simulTime;
    float satTime;
    Vec_Ptr_t ** topOrder1 = NULL, ** topOrder2 = NULL;
 
    extern void getDependencies(Abc_Ntk_t *pNtk, Vec_Int_t** iDep, Vec_Int_t** oDep);
    extern void initMatchList(Abc_Ntk_t *pNtk, Vec_Int_t** iDep, Vec_Int_t** oDep, Vec_Int_t** iMatch, int* iLastItem, Vec_Int_t** oMatch, int* oLastItem, int* iGroup, int* oGroup, int p_equivalence);        
    extern void iSortDependencies(Abc_Ntk_t *pNtk, Vec_Int_t** iDep, int* oGroup);
    extern void oSortDependencies(Abc_Ntk_t *pNtk, Vec_Int_t** oDep, int* iGroup);
    extern int iSplitByDep(Abc_Ntk_t *pNtk, Vec_Int_t** iDep, Vec_Int_t** iMatch, int* iGroup, int* iLastItem, int* oGroup);
    extern int oSplitByDep(Abc_Ntk_t *pNtk, Vec_Int_t** oDep, Vec_Int_t** oMatch, int* oGroup, int* oLastItem, int* iGroup);    
    extern Vec_Ptr_t ** findTopologicalOrder(Abc_Ntk_t * pNtk);
    extern int refineIOBySimulation(Abc_Ntk_t *pNtk, Vec_Int_t** iMatch, int* iLastItem, int * iGroup, Vec_Int_t** iDep, Vec_Int_t** oMatch, int* oLastItem, int * oGroup, Vec_Int_t** oDep, char * vPiValues, int * observability, Vec_Ptr_t ** topOrder);    
    extern float refineBySAT(Abc_Ntk_t * pNtk1, Vec_Int_t ** iMatch1, int * iGroup1, Vec_Int_t ** iDep1, int* iLastItem1, Vec_Int_t ** oMatch1, int * oGroup1, Vec_Int_t ** oDep1, int* oLastItem1, int * observability1,
                            Abc_Ntk_t * pNtk2, Vec_Int_t ** iMatch2, int * iGroup2, Vec_Int_t ** iDep2, int* iLastItem2, Vec_Int_t ** oMatch2, int * oGroup2, Vec_Int_t ** oDep2, int* oLastItem2, int * observability2);                
    int checkListConsistency(Vec_Int_t ** iMatch1, Vec_Int_t ** oMatch1, Vec_Int_t ** iMatch2, Vec_Int_t ** oMatch2, int iLastItem1, int oLastItem1, int iLastItem2, int oLastItem2);    
 
    iDep1 = ABC_ALLOC( Vec_Int_t*,  (unsigned)Abc_NtkPiNum(pNtk1) );
    oDep1 = ABC_ALLOC( Vec_Int_t*,  (unsigned)Abc_NtkPoNum(pNtk1) );
 
    iDep2 = ABC_ALLOC( Vec_Int_t*,  (unsigned)Abc_NtkPiNum(pNtk2) );
    oDep2 = ABC_ALLOC( Vec_Int_t*,  (unsigned)Abc_NtkPoNum(pNtk2) );
 
    iMatch1 = ABC_ALLOC( Vec_Int_t*,  (unsigned)Abc_NtkPiNum(pNtk1) );
    oMatch1 = ABC_ALLOC( Vec_Int_t*,  (unsigned)Abc_NtkPoNum(pNtk1) );
 
    iMatch2 = ABC_ALLOC( Vec_Int_t*,  (unsigned)Abc_NtkPiNum(pNtk2) );
    oMatch2 = ABC_ALLOC( Vec_Int_t*,  (unsigned)Abc_NtkPoNum(pNtk2) );        
 
    iGroup1 = ABC_ALLOC( int, Abc_NtkPiNum(pNtk1) );
    oGroup1 = ABC_ALLOC( int, Abc_NtkPoNum(pNtk1) );
 
    iGroup2 = ABC_ALLOC( int, Abc_NtkPiNum(pNtk2) );
    oGroup2 = ABC_ALLOC( int, Abc_NtkPoNum(pNtk2) );
 
    vPiValues1 = ABC_ALLOC( char,  Abc_NtkPiNum(pNtk1) + 1);
    vPiValues1[Abc_NtkPiNum(pNtk1)] = '\0';    
 
    vPiValues2 = ABC_ALLOC( char,  Abc_NtkPiNum(pNtk2) + 1);
    vPiValues2[Abc_NtkPiNum(pNtk2)] = '\0';    
 
    observability1 = ABC_ALLOC(int, (unsigned)Abc_NtkPiNum(pNtk1));
    observability2 = ABC_ALLOC(int, (unsigned)Abc_NtkPiNum(pNtk2));
 
    for(i = 0; i < Abc_NtkPiNum(pNtk1); i++)
    {        
        iDep1[i] = Vec_IntAlloc( 1 );
        iMatch1[i] = Vec_IntAlloc( 1 );
 
        iDep2[i] = Vec_IntAlloc( 1 );
        iMatch2[i] = Vec_IntAlloc( 1 );
 
        vPiValues1[i] = '0';
        vPiValues2[i] = '0';
 
        observability1[i] = 0;
        observability2[i] = 0;
    }
 
    for(i = 0; i < Abc_NtkPoNum(pNtk1); i++)
    {
        oDep1[i] = Vec_IntAlloc( 1 );
        oMatch1[i] = Vec_IntAlloc( 1 );
 
        oDep2[i] = Vec_IntAlloc( 1 );
        oMatch2[i] = Vec_IntAlloc( 1 );
    }    
    
    /************* Strashing ************/    
    pNtk1 = Abc_NtkStrash( pNtk1, 0, 0, 0 );    
    pNtk2 = Abc_NtkStrash( pNtk2, 0, 0, 0 );            
    printf("Network  strashing is done!\n");    
    /************************************/    
    
    /******* Getting Dependencies *******/    
    getDependencies(pNtk1, iDep1, oDep1);
    getDependencies(pNtk2, iDep2, oDep2);            
    printf("Getting dependencies is done!\n");    
    /************************************/
 
    /***** Intializing match lists ******/    
    initMatchList(pNtk1, iDep1, oDep1, iMatch1, &iLastItem1, oMatch1, &oLastItem1, iGroup1, oGroup1, p_equivalence);            
    initMatchList(pNtk2, iDep2, oDep2, iMatch2, &iLastItem2, oMatch2, &oLastItem2, iGroup2, oGroup2, p_equivalence);    
    printf("Initializing match lists is done!\n");        
    /************************************/
 
    if( !checkListConsistency(iMatch1, oMatch1, iMatch2, oMatch2, iLastItem1, oLastItem1, iLastItem2, oLastItem2) )
    {
        fprintf( stdout, "I/O dependencies of two circuits are different.\n");
        goto freeAndExit;
    }        
 
    printf("Refining IOs by dependencies ...");                
    // split match lists further by checking dependencies
    do
    {
        int iNumOfItemsAdded = 1, oNumOfItemsAdded = 1;        
 
        do
        {    
            if( oNumOfItemsAdded )
            {
                iSortDependencies(pNtk1, iDep1, oGroup1);
                iSortDependencies(pNtk2, iDep2, oGroup2);
            }
            
            if( iNumOfItemsAdded )
            {
                oSortDependencies(pNtk1, oDep1, iGroup1);
                oSortDependencies(pNtk2, oDep2, iGroup2);
            }
 
            if( iLastItem1 < Abc_NtkPiNum(pNtk1) )
            {                
                iSplitByDep(pNtk1, iDep1, iMatch1, iGroup1, &iLastItem1, oGroup1);
                if( oLastItem1 < Abc_NtkPoNum(pNtk1) )
                    oSplitByDep(pNtk1, oDep1, oMatch1, oGroup1, &oLastItem1, iGroup1);
            }                
 
            if( iLastItem2 < Abc_NtkPiNum(pNtk2) )
                iNumOfItemsAdded = iSplitByDep(pNtk2, iDep2, iMatch2, iGroup2, &iLastItem2, oGroup2);
            else
                iNumOfItemsAdded = 0;    
                
            if( oLastItem2 < Abc_NtkPoNum(pNtk2) )        
                oNumOfItemsAdded = oSplitByDep(pNtk2, oDep2, oMatch2, oGroup2, &oLastItem2, iGroup2);
            else
                oNumOfItemsAdded = 0;
            
            if(!checkListConsistency(iMatch1, oMatch1, iMatch2, oMatch2, iLastItem1, oLastItem1, iLastItem2, oLastItem2))
            {
                fprintf( stdout, "I/O dependencies of two circuits are different.\n");
                goto freeAndExit;
            }        
        }while(iNumOfItemsAdded != 0 || oNumOfItemsAdded != 0);
 
    }while(0);
 
    printf(" done!\n");
 
    initTime = ((float)(Abc_Clock() - clk)/(float)(CLOCKS_PER_SEC));    
    clk = Abc_Clock();
 
    topOrder1 = findTopologicalOrder(pNtk1);
    topOrder2 = findTopologicalOrder(pNtk2);
 
    printf("Refining IOs by simulation ...");                
 
    do
    {
        int counter = 0;
        int ioSuccess1, ioSuccess2;    
        
        do
        {
            for(i = 0; i < iLastItem1; i++)
            {
                int temp = (int)(SIM_RANDOM_UNSIGNED % 2);        
                
                if(Vec_IntSize(iMatch1[i]) != Vec_IntSize(iMatch2[i]))
                {
                    fprintf( stdout, "Input refinement by simulation finds two circuits different.\n");                
                    goto freeAndExit;
                }
                
                for(j = 0; j < Vec_IntSize(iMatch1[i]); j++)
                {
                    vPiValues1[Vec_IntEntry(iMatch1[i], j)] = temp + '0';
                    vPiValues2[Vec_IntEntry(iMatch2[i], j)] = temp + '0';    
                }            
            }                    
            
            ioSuccess1 = refineIOBySimulation(pNtk1, iMatch1, &iLastItem1, iGroup1, iDep1, oMatch1, &oLastItem1, oGroup1, oDep1, vPiValues1, observability1, topOrder1);                
            ioSuccess2 = refineIOBySimulation(pNtk2, iMatch2, &iLastItem2, iGroup2, iDep2, oMatch2, &oLastItem2, oGroup2, oDep2, vPiValues2, observability2, topOrder2);
            
            if(ioSuccess1 && ioSuccess2)
                counter = 0;
            else
                counter++;                        
            
            if(ioSuccess1 != ioSuccess2 ||
               !checkListConsistency(iMatch1, oMatch1, iMatch2, oMatch2, iLastItem1, oLastItem1, iLastItem2, oLastItem2))
            {
                fprintf( stdout, "Input refinement by simulation finds two circuits different.\n");                
                goto freeAndExit;
            }
        }while(counter <= 200);                
        
    }while(0);    
 
    printf(" done!\n");
    
    simulTime = (float)(Abc_Clock() - clk)/(float)(CLOCKS_PER_SEC);
    printf("SAT-based search started ...\n");
 
    satTime = refineBySAT(pNtk1, iMatch1, iGroup1, iDep1, &iLastItem1, oMatch1, oGroup1, oDep1, &oLastItem1, observability1,
                                  pNtk2, iMatch2, iGroup2, iDep2, &iLastItem2, oMatch2, oGroup2, oDep2, &oLastItem2, observability2);
 
    printf( "Init Time = %4.2f\n", initTime );    
    printf( "Simulation Time = %4.2f\n", simulTime );
    printf( "SAT Time = %4.2f\n", satTime );
    printf( "Overall Time = %4.2f\n", initTime + simulTime + satTime );
    
freeAndExit:
 
    for(i = 0; i < iLastItem1 ; i++)
    {            
        
        Vec_IntFree( iMatch1[i] );
        Vec_IntFree( iMatch2[i] );
    }
    
    for(i = 0; i < oLastItem1 ; i++)
    {            
        
        Vec_IntFree( oMatch1[i] );
        Vec_IntFree( oMatch2[i] );
    }
 
    for(i = 0; i < Abc_NtkPiNum(pNtk1); i++)
    {
        Vec_IntFree( iDep1[i] );
        Vec_IntFree( iDep2[i] );
        if(topOrder1 != NULL) {
            Vec_PtrFree( topOrder1[i] );
            Vec_PtrFree( topOrder2[i] );
        }
    }
 
    for(i = 0; i < Abc_NtkPoNum(pNtk1); i++)
    {
        Vec_IntFree( oDep1[i] );
        Vec_IntFree( oDep2[i] );
    }
 
    ABC_FREE( iMatch1 );
    ABC_FREE( iMatch2 );
    ABC_FREE( oMatch1 );
    ABC_FREE( oMatch2 );
    ABC_FREE( iDep1 );
    ABC_FREE( iDep2 );
    ABC_FREE( oDep1 );
    ABC_FREE( oDep2 );
    ABC_FREE( iGroup1 );
    ABC_FREE( iGroup2 );
    ABC_FREE( oGroup1 );
    ABC_FREE( oGroup2 );    
    ABC_FREE( vPiValues1 );
    ABC_FREE( vPiValues2 );
    ABC_FREE( observability1 );
    ABC_FREE( observability2 );
    if(topOrder1 != NULL) {
        ABC_FREE( topOrder1 );
        ABC_FREE( topOrder2 );
    }
}ABC_NAMESPACE_IMPL_END

Here is the call graph for this function:

checkEquivalence()

int checkEquivalence	(	Abc_Ntk_t *	pNtk1,
		Vec_Int_t *	matchedInputs1,
		Vec_Int_t *	matchedOutputs1,
		Abc_Ntk_t *	pNtk2,
		Vec_Int_t *	matchedInputs2,
		Vec_Int_t *	matchedOutputs2 )

Definition at line 1063 of file abcBm.c.

{    
    Vec_Ptr_t * iMatchPairs, * oMatchPairs;
    int i;
    int result;
 
    iMatchPairs = Vec_PtrAlloc( Abc_NtkPiNum( pNtk1 ) * 2);
    oMatchPairs = Vec_PtrAlloc( Abc_NtkPoNum( pNtk1 ) * 2);
 
    for(i = 0; i < Abc_NtkPiNum(pNtk1); i++)
    {    
        Vec_PtrPush(iMatchPairs, Abc_NtkPi(pNtk2, Vec_IntEntry(matchedInputs2, i)));
        Vec_PtrPush(iMatchPairs, Abc_NtkPi(pNtk1, Vec_IntEntry(matchedInputs1, i)));
    }
                
 
    for(i = 0; i < Abc_NtkPoNum(pNtk1); i++)        
    {
        Vec_PtrPush(oMatchPairs, Abc_NtkPo(pNtk2, Vec_IntEntry(matchedOutputs2, i)));
        Vec_PtrPush(oMatchPairs, Abc_NtkPo(pNtk1, Vec_IntEntry(matchedOutputs1, i)));
    }        
 
    result = Abc_NtkBmSat(pNtk1, pNtk2, iMatchPairs, oMatchPairs, NULL, 0);
 
    if( result )
        printf("*** Circuits are equivalent ***\n");
    else
        printf("*** Circuits are NOT equivalent ***\n");
 
    Vec_PtrFree( iMatchPairs );
    Vec_PtrFree( oMatchPairs );    
 
    return result;
}

Here is the call graph for this function:

Here is the caller graph for this function:

checkListConsistency()

int checkListConsistency	(	Vec_Int_t **	iMatch1,
		Vec_Int_t **	oMatch1,
		Vec_Int_t **	iMatch2,
		Vec_Int_t **	oMatch2,
		int	iLastItem1,
		int	oLastItem1,
		int	iLastItem2,
		int	oLastItem2 )

Definition at line 1758 of file abcBm.c.

{
    //int i;
 
    if(iLastItem1 != iLastItem2 || oLastItem1 != oLastItem2)
        return FALSE;
 
    /*for(i = 0; i < iLastItem1; i++) {
        if(Vec_IntSize(iMatch1[i]) != Vec_IntSize(iMatch2[i]))
            return FALSE;
    }
 
    for(i = 0; i < oLastItem1; i++) {
        if(Vec_IntSize(oMatch1[i]) != Vec_IntSize(oMatch2[i]))
            return FALSE;
    }*/
        
    return TRUE;
}

Here is the caller graph for this function:

computeCofactor()

Abc_Ntk_t * computeCofactor	(	Abc_Ntk_t *	pNtk,
		Vec_Ptr_t **	nodesInLevel,
		int *	bitVector,
		Vec_Int_t *	currInputs )

Definition at line 1099 of file abcBm.c.

{    
    Abc_Ntk_t * subNtk;    
    Abc_Obj_t * pObj, * pObjNew;
    int i, j, numOfLevels;        
 
    numOfLevels = Abc_AigLevel( pNtk );        // number of levels excludes PI/POs    
 
    // start a new network
    subNtk = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );    
    subNtk->pName = Extra_UtilStrsav("subNtk");
 
    Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(subNtk);    
 
    // clean the node copy fields and mark the nodes that need to be copied to the new network
    Abc_NtkCleanCopy( pNtk );
 
    if(bitVector != NULL)
    {
        for(i = 0; i < Abc_NtkPiNum(pNtk); i++)
            if(bitVector[i])
            {
                pObj = Abc_NtkPi(pNtk, i);
                pObj->pCopy = (Abc_Obj_t *)(1);
            }
    }
 
    for(i = 0; i < Vec_IntSize(currInputs); i++)
    {
        pObj = Abc_NtkPi(pNtk, Vec_IntEntry(currInputs, i));
        pObjNew = Abc_NtkDupObj( subNtk, pObj, 1 );
        pObj->pCopy = pObjNew;
    }
        
 
    // i = 0 are the inputs and the inputs are not added to the 2d array ( nodesInLevel )
    for( i = 0; i <= numOfLevels; i++ )    
        for( j = 0; j < Vec_PtrSize( nodesInLevel[i] ); j++)
        {
            pObj = (Abc_Obj_t *)Vec_PtrEntry( nodesInLevel[i], j );
 
            if(Abc_ObjChild0Copy(pObj) == NULL && Abc_ObjChild1Copy(pObj) == NULL)
                pObj->pCopy = NULL;
            else if(Abc_ObjChild0Copy(pObj) == NULL && Abc_ObjChild1Copy(pObj) == (void*)(1))
                pObj->pCopy = NULL;
            else if(Abc_ObjChild0Copy(pObj) == NULL && (Abc_ObjChild1Copy(pObj) != (NULL) && Abc_ObjChild1Copy(pObj) != (void*)(1)) )
                pObj->pCopy = NULL;
            else if(Abc_ObjChild0Copy(pObj) == (void*)(1) && Abc_ObjChild1Copy(pObj) == NULL)
                pObj->pCopy = NULL;
            else if(Abc_ObjChild0Copy(pObj) == (void*)(1) && Abc_ObjChild1Copy(pObj) == (void*)(1))
                pObj->pCopy = (Abc_Obj_t *)(1);
            else if(Abc_ObjChild0Copy(pObj) == (void*)(1) && (Abc_ObjChild1Copy(pObj) != (NULL) && Abc_ObjChild1Copy(pObj) != (void*)(1)) )
                pObj->pCopy = Abc_ObjChild1Copy(pObj);
            else if( (Abc_ObjChild0Copy(pObj) != (NULL) && Abc_ObjChild0Copy(pObj) != (void*)(1)) && Abc_ObjChild1Copy(pObj) == NULL )
                pObj->pCopy = NULL;
            else if( (Abc_ObjChild0Copy(pObj) != (NULL) && Abc_ObjChild0Copy(pObj) != (void*)(1)) && Abc_ObjChild1Copy(pObj) == (void*)(1) )
                pObj->pCopy = Abc_ObjChild0Copy(pObj);
            else if( (Abc_ObjChild0Copy(pObj) != (NULL) && Abc_ObjChild0Copy(pObj) != (void*)(1)) &&
                     (Abc_ObjChild1Copy(pObj) != (NULL) && Abc_ObjChild1Copy(pObj) != (void*)(1)) )
                pObj->pCopy = Abc_AigAnd( (Abc_Aig_t *)subNtk->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );                    
        }    
 
    for(i = 0; i < Abc_NtkPoNum(pNtk); i++)
    {
        pObj = Abc_NtkPo(pNtk, i);
        pObjNew = Abc_NtkDupObj( subNtk, pObj, 1 );
        
        if( Abc_ObjChild0Copy(pObj) == NULL)
        {
            Abc_ObjAddFanin( pObjNew, Abc_AigConst1(subNtk));
            pObjNew->fCompl0 = 1;
        }
        else if( Abc_ObjChild0Copy(pObj) == (void*)(1) )
        {
            Abc_ObjAddFanin( pObjNew, Abc_AigConst1(subNtk));
            pObjNew->fCompl0 = 0;
        }
        else
            Abc_ObjAddFanin( pObjNew, Abc_ObjChild0Copy(pObj) );
    }
 
    return subNtk;
}

Here is the call graph for this function:

Here is the caller graph for this function:

findTopologicalOrder()

static Vec_Ptr_t ** findTopologicalOrder

(

Abc_Ntk_t *

pNtk

)

Definition at line 422 of file abcBm.c.

{
    Vec_Ptr_t ** vNodes;
    Abc_Obj_t * pObj, * pFanout;
    int i, k;    
    
    extern void Abc_NtkDfsReverse_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes );
    
    // start the array of nodes
    vNodes = ABC_ALLOC(Vec_Ptr_t *, Abc_NtkPiNum(pNtk));
    for(i = 0; i < Abc_NtkPiNum(pNtk); i++)
        vNodes[i] = Vec_PtrAlloc(50);    
    
    Abc_NtkForEachCi( pNtk, pObj, i )
    {
        // set the traversal ID
        Abc_NtkIncrementTravId( pNtk );
        Abc_NodeSetTravIdCurrent( pObj );
        pObj = Abc_ObjFanout0Ntk(pObj);
        Abc_ObjForEachFanout( pObj, pFanout, k )
            Abc_NtkDfsReverse_rec( pFanout, vNodes[i] );
    }
   
    return vNodes;
}

Here is the call graph for this function:

Here is the caller graph for this function:

getDependencies()

static void getDependencies	(	Abc_Ntk_t *	pNtk,
		Vec_Int_t **	iDep,
		Vec_Int_t **	oDep )

Definition at line 46 of file abcBm.c.

{    
    Vec_Ptr_t * vSuppFun;
    int i, j;    
    
    vSuppFun = Sim_ComputeFunSupp(pNtk, 0);
    for(i = 0; i < Abc_NtkPoNum(pNtk); i++) {
        char * seg = (char *)vSuppFun->pArray[i];
        
        for(j = 0; j < Abc_NtkPiNum(pNtk); j+=8) {
            if(((*seg) & 0x01) == 0x01)
                Vec_IntPushOrder(oDep[i], j);
            if(((*seg) & 0x02) == 0x02)
                Vec_IntPushOrder(oDep[i], j+1);
            if(((*seg) & 0x04) == 0x04)
                Vec_IntPushOrder(oDep[i], j+2);
            if(((*seg) & 0x08) == 0x08)
                Vec_IntPushOrder(oDep[i], j+3);
            if(((*seg) & 0x10) == 0x10)
                Vec_IntPushOrder(oDep[i], j+4);
            if(((*seg) & 0x20) == 0x20)
                Vec_IntPushOrder(oDep[i], j+5);
            if(((*seg) & 0x40) == 0x40)
                Vec_IntPushOrder(oDep[i], j+6);
            if(((*seg) & 0x80) == 0x80)
                Vec_IntPushOrder(oDep[i], j+7);
 
            seg++;
        }
    }
 
    for(i = 0; i < Abc_NtkPoNum(pNtk); i++)
        for(j = 0; j < Vec_IntSize(oDep[i]); j++)
            Vec_IntPush(iDep[Vec_IntEntry(oDep[i], j)], i);    
    
 
    /*for(i = 0; i < Abc_NtkPoNum(pNtk); i++)
    {
        printf("Output %d: ", i);
        for(j = 0; j < Vec_IntSize(oDep[i]); j++)
            printf("%d ", Vec_IntEntry(oDep[i], j));
        printf("\n");
    }
 
    printf("\n");
 
    for(i = 0; i < Abc_NtkPiNum(pNtk); i++)
    {
        printf("Input %d: ", i);
        for(j = 0; j < Vec_IntSize(iDep[i]); j++)
            printf("%d ", Vec_IntEntry(iDep[i], j));
        printf("\n");
    }
 
    printf("\n");    */    
}

Here is the call graph for this function:

Here is the caller graph for this function:

initMatchList()

void initMatchList	(	Abc_Ntk_t *	pNtk,
		Vec_Int_t **	iDep,
		Vec_Int_t **	oDep,
		Vec_Int_t **	iMatch,
		int *	iLastItem,
		Vec_Int_t **	oMatch,
		int *	oLastItem,
		int *	iGroup,
		int *	oGroup,
		int	p_equivalence )

Definition at line 103 of file abcBm.c.

{
    int i, j, curr;
    Vec_Int_t** temp;
 
    if(!p_equivalence) {
        temp = ABC_ALLOC( Vec_Int_t*, Abc_NtkPiNum(pNtk)+1);
 
        for(i = 0; i < Abc_NtkPiNum(pNtk)+1; i++)    
            temp[i] = Vec_IntAlloc( 0 );    
 
        for(i = 0; i < Abc_NtkPoNum(pNtk); i++)        
            Vec_IntPush(temp[Vec_IntSize(oDep[i])], i);
 
        curr = 0;
        for(i = 0; i < Abc_NtkPiNum(pNtk)+1; i++)
        {
            if(Vec_IntSize(temp[i]) == 0)
                Vec_IntFree( temp[i] );
 
            else
            {
                oMatch[curr] = temp[i];
                
                for(j = 0; j < Vec_IntSize(temp[i]); j++)
                    oGroup[Vec_IntEntry(oMatch[curr], j)] = curr;
            
                curr++;
            }
        }
 
        *oLastItem = curr;
 
        ABC_FREE( temp );
    }
    else {
        // the else part fixes the outputs for P-equivalence checking
        for(i = 0; i < Abc_NtkPoNum(pNtk); i++)
        {
            Vec_IntPush(oMatch[i], i);
            oGroup[i] = i;
            (*oLastItem) = Abc_NtkPoNum(pNtk);
        }
    }
        
    /*for(j = 0; j < *oLastItem; j++)
    {
        printf("oMatch %d: ", j);
        for(i = 0; i < Vec_IntSize(oMatch[j]); i++)
            printf("%d ", Vec_IntEntry(oMatch[j], i));
        printf("\n");
    }
 
    for(i = 0; i < Abc_NtkPoNum(pNtk); i++)
        printf("%d: %d ", i, oGroup[i]);*/

 
    temp = ABC_ALLOC( Vec_Int_t*, Abc_NtkPoNum(pNtk)+1 );
 
    for(i = 0; i < Abc_NtkPoNum(pNtk)+1; i++)    
        temp[i] = Vec_IntAlloc( 0 );
 
    for(i = 0; i < Abc_NtkPiNum(pNtk); i++)        
        Vec_IntPush(temp[Vec_IntSize(iDep[i])], i);
 
    curr = 0;
    for(i = 0; i < Abc_NtkPoNum(pNtk)+1; i++)
    {
        if(Vec_IntSize(temp[i]) == 0)
            Vec_IntFree( temp[i] );
        else
        {
            iMatch[curr] = temp[i];
            for(j = 0; j < Vec_IntSize(iMatch[curr]); j++)
                iGroup[Vec_IntEntry(iMatch[curr], j)] = curr;
            curr++;
        }        
    }
 
    *iLastItem = curr;
 
    ABC_FREE( temp );        
 
    /*printf("\n");
    for(j = 0; j < *iLastItem; j++)
    {
        printf("iMatch %d: ", j);
        for(i = 0; i < Vec_IntSize(iMatch[j]); i++)
            printf("%d ", Vec_IntEntry(iMatch[j], i));
        printf("\n");
    }
 
    for(i = 0; i < Abc_NtkPiNum(pNtk); i++)
        printf("%d: %d ", i, iGroup[i]);
    printf("\n");*/
}

Here is the caller graph for this function:

iSortDependencies()

void iSortDependencies	(	Abc_Ntk_t *	pNtk,
		Vec_Int_t **	iDep,
		int *	oGroup )

Definition at line 201 of file abcBm.c.

{
    int i, j, k;    
    Vec_Int_t * temp;    
    Vec_Int_t * oGroupList;    
 
    oGroupList = Vec_IntAlloc( 10 );
 
    for(i = 0; i < Abc_NtkPiNum(pNtk); i++)
    {
        if(Vec_IntSize(iDep[i]) == 1)
            continue;
        
        temp = Vec_IntAlloc( Vec_IntSize(iDep[i]) );        
 
        for(j = 0; j < Vec_IntSize(iDep[i]); j++)
            Vec_IntPushUniqueOrder(oGroupList, oGroup[Vec_IntEntry(iDep[i], j)]);
 
        for(j = 0; j < Vec_IntSize(oGroupList); j++)
        {
            for(k = 0; k < Vec_IntSize(iDep[i]); k++)
                if(oGroup[Vec_IntEntry(iDep[i], k)] == Vec_IntEntry(oGroupList, j))
                {
                    Vec_IntPush( temp, Vec_IntEntry(iDep[i], k) );        
                    Vec_IntRemove( iDep[i], Vec_IntEntry(iDep[i], k) );
                    k--;
                }
        }        
 
        Vec_IntFree( iDep[i] );        
        iDep[i] = temp;
        Vec_IntClear( oGroupList );
 
        /*printf("Input %d: ", i);
        for(j = 0; j < Vec_IntSize(iDep[i]); j++)
            printf("%d ", Vec_IntEntry(iDep[i], j));
        printf("\n");*/
    }
    
    Vec_IntFree( oGroupList );
}

Here is the caller graph for this function:

iSplitByDep()

int iSplitByDep	(	Abc_Ntk_t *	pNtk,
		Vec_Int_t **	iDep,
		Vec_Int_t **	iMatch,
		int *	iGroup,
		int *	iLastItem,
		int *	oGroup )

Definition at line 356 of file abcBm.c.

{
    int i, j, k;    
    int numOfItemsAdded = 0;
    Vec_Int_t * array, * sortedArray;    
 
    for(i = 0; i < *iLastItem; i++)
    {
        if(Vec_IntSize(iMatch[i]) == 1)
            continue;
        
        array = Vec_IntAlloc( Vec_IntSize(iMatch[i]) );
        sortedArray = Vec_IntAlloc( Vec_IntSize(iMatch[i]) );
 
        for(j = 0; j < Vec_IntSize(iMatch[i]); j++)
        {        
            int factor, encode;
 
            encode = 0;
            factor = 1;    
            
            for(k = 0; k < Vec_IntSize(iDep[Vec_IntEntry(iMatch[i], j)]); k++)                            
                encode += oGroup[Vec_IntEntry(iDep[Vec_IntEntry(iMatch[i], j)], k)] * factor;                        
 
            Vec_IntPush(array, encode);
            Vec_IntPushUniqueOrder(sortedArray, encode);
            
            //printf("%d ", Vec_IntEntry(array, j));
        }            
                
        while( Vec_IntSize(sortedArray) > 1 )
        {            
            for(k = 0; k < Vec_IntSize(iMatch[i]); k++) 
            {
                if(Vec_IntEntry(array, k) == Vec_IntEntryLast(sortedArray))
                {
                    Vec_IntPush(iMatch[*iLastItem+numOfItemsAdded], Vec_IntEntry(iMatch[i], k));
                    iGroup[Vec_IntEntry(iMatch[i], k)] = *iLastItem+numOfItemsAdded;
                    Vec_IntRemove( iMatch[i], Vec_IntEntry(iMatch[i], k) );                            
                    Vec_IntRemove( array, Vec_IntEntry(array, k) );    
                    k--;
                }
            }
            numOfItemsAdded++;
            Vec_IntPop(sortedArray);    
        }
 
        Vec_IntFree( array );        
        Vec_IntFree( sortedArray );    
        //printf("\n");
    }    
 
    *iLastItem += numOfItemsAdded;
 
    /*printf("\n");
    for(j = 0; j < *iLastItem ; j++)
    {
        printf("iMatch %d: ", j);
        for(i = 0; i < Vec_IntSize(iMatch[j]); i++)
            printf("%d ", Vec_IntEntry(iMatch[j], i));
        printf("\n");
    }*/
 
    return numOfItemsAdded;    
}

Here is the caller graph for this function:

match1by1()

int match1by1	(	Abc_Ntk_t *	pNtk1,
		Vec_Ptr_t **	nodesInLevel1,
		Vec_Int_t **	iMatch1,
		Vec_Int_t **	iDep1,
		Vec_Int_t *	matchedInputs1,
		int *	iGroup1,
		Vec_Int_t **	oMatch1,
		int *	oGroup1,
		Abc_Ntk_t *	pNtk2,
		Vec_Ptr_t **	nodesInLevel2,
		Vec_Int_t **	iMatch2,
		Vec_Int_t **	iDep2,
		Vec_Int_t *	matchedInputs2,
		int *	iGroup2,
		Vec_Int_t **	oMatch2,
		int *	oGroup2,
		Vec_Int_t *	matchedOutputs1,
		Vec_Int_t *	matchedOutputs2,
		Vec_Int_t *	oMatchedGroups,
		Vec_Int_t *	iNonSingleton,
		int	ii,
		int	idx )

Definition at line 1331 of file abcBm.c.

{
    static int MATCH_FOUND = FALSE;
    Abc_Ntk_t * subNtk1, * subNtk2;
    Vec_Int_t * oNonSingleton;    
    Vec_Ptr_t * oMatchPairs;
    int * skipList;
    int j, m;    
    int i;        
    static int counter = 0;
 
    MATCH_FOUND = FALSE;
 
    if( ii == Vec_IntSize(iNonSingleton) )
    {
        MATCH_FOUND = TRUE;
        return TRUE;
    }
    
    i = Vec_IntEntry(iNonSingleton, ii);
 
    if( idx == Vec_IntSize(iMatch1[i]) )
    {        
        // call again with the next element in iNonSingleton
        return match1by1(pNtk1, nodesInLevel1, iMatch1, iDep1, matchedInputs1, iGroup1, oMatch1, oGroup1,
                         pNtk2, nodesInLevel2, iMatch2, iDep2, matchedInputs2, iGroup2, oMatch2, oGroup2,
                         matchedOutputs1, matchedOutputs2, oMatchedGroups, iNonSingleton, ii+1, 0);            
        
    }    
    
    oNonSingleton = Vec_IntAlloc(10);
    oMatchPairs = Vec_PtrAlloc(100);    
    skipList = ABC_ALLOC(int, Vec_IntSize(iMatch1[i]));
 
    for(j = 0; j < Vec_IntSize(iMatch1[i]); j++)
        skipList[j] = FALSE;
    
    Vec_IntPush(matchedInputs1, Vec_IntEntry(iMatch1[i], idx));
    idx++;
    
    if(idx == 1)
    {
        for(j = 0; j < Vec_IntSize(iDep1[Vec_IntEntryLast(iMatch1[i])]); j++)
        {
            if( Vec_IntSize(oMatch1[oGroup1[Vec_IntEntry(iDep1[Vec_IntEntryLast(iMatch1[i])], j)]]) == 1 ) 
                continue;
            if( Vec_IntFind( oMatchedGroups, oGroup1[Vec_IntEntry(iDep1[Vec_IntEntryLast(iMatch1[i])], j)]) != -1)
                continue;
            
            Vec_IntPushUnique(oNonSingleton,  oGroup1[Vec_IntEntry(iDep1[Vec_IntEntryLast(iMatch1[i])], j)]);
            Vec_IntPushUnique(oMatchedGroups, oGroup1[Vec_IntEntry(iDep1[Vec_IntEntryLast(iMatch1[i])], j)]);        
        }
    }
 
    subNtk1 = computeCofactor(pNtk1, nodesInLevel1, NULL, matchedInputs1);
 
    for(j = idx-1; j < Vec_IntSize(iMatch2[i]) && MATCH_FOUND == FALSE; j++)
    {
        int tempJ;
        Vec_Int_t * mismatch;
 
        if( skipList[j] )
            continue;
 
        mismatch = Vec_IntAlloc(10);
 
        Vec_IntPush(matchedInputs2, Vec_IntEntry(iMatch2[i], j));        
        
        subNtk2 = computeCofactor(pNtk2, nodesInLevel2, NULL, matchedInputs2);            
 
        for(m = 0; m < Vec_IntSize(matchedOutputs1); m++)
        {
            Vec_PtrPush(oMatchPairs, Abc_NtkPo(subNtk1, Vec_IntEntry(matchedOutputs1, m)));
            Vec_PtrPush(oMatchPairs, Abc_NtkPo(subNtk2, Vec_IntEntry(matchedOutputs2, m)));
        }
 
        counter++;
 
        if( Abc_NtkBmSat( subNtk2, subNtk1, NULL, oMatchPairs, mismatch, 0) )                
        {
            if(idx-1 != j)
            {
                tempJ = Vec_IntEntry(iMatch2[i], idx-1);
                Vec_IntWriteEntry(iMatch2[i], idx-1, Vec_IntEntry(iMatch2[i], j));
                Vec_IntWriteEntry(iMatch2[i], j, tempJ);
            }
 
            /*fprintf(matchFile, "%s matched to %s\n", Abc_ObjName(Abc_NtkPi(pNtk1, Vec_IntEntry(iMatch1[i], idx-1))), 
                                                      Abc_ObjName(Abc_NtkPi(pNtk2, Vec_IntEntry(iMatch2[i], j))));*/
 
            // we look for a match for outputs in oNonSingleton                                
            matchNonSingletonOutputs(pNtk1, nodesInLevel1, iMatch1, iDep1, matchedInputs1, iGroup1, oMatch1, oGroup1,
                                     pNtk2, nodesInLevel2, iMatch2, iDep2, matchedInputs2, iGroup2, oMatch2, oGroup2,
                                     matchedOutputs1, matchedOutputs2, oMatchedGroups, iNonSingleton,                         
                                     subNtk1, subNtk2, oMatchPairs, oNonSingleton, 0, 0, ii, idx);
            
            
            if(idx-1 != j)
            {
                tempJ = Vec_IntEntry(iMatch2[i], idx-1);
                Vec_IntWriteEntry(iMatch2[i], idx-1, Vec_IntEntry(iMatch2[i], j));
                Vec_IntWriteEntry(iMatch2[i], j, tempJ);
            }
        }
        else
        {
            Abc_Ntk_t * FpNtk1, * FpNtk2;
            int * bitVector1, * bitVector2;
            Vec_Int_t * currInputs1, * currInputs2;            
            Vec_Ptr_t * vSupp;    
            Abc_Obj_t * pObj;
            int suppNum1 = 0;
            int * suppNum2;            
            
            bitVector1 = ABC_ALLOC( int, Abc_NtkPiNum(pNtk1) );
            bitVector2 = ABC_ALLOC( int, Abc_NtkPiNum(pNtk2) );
 
            currInputs1 = Vec_IntAlloc(10);
            currInputs2 = Vec_IntAlloc(10);        
            
            suppNum2 = ABC_ALLOC(int, Vec_IntSize(iMatch2[i])-idx+1);
 
            for(m = 0; m < Abc_NtkPiNum(pNtk1); m++)
            {
                bitVector1[m] = 0;
                bitVector2[m] = 0;
            }
 
            for(m = 0; m < Vec_IntSize(iMatch2[i])-idx+1; m++)                        
                suppNum2[m]= 0;            
 
            // First of all set the value of the inputs that are already matched and are in mismatch
            for(m = 0; m < Vec_IntSize(mismatch); m += 2)
            {
                int n = Vec_IntEntry(mismatch, m);
                    
                bitVector1[Vec_IntEntry(matchedInputs1, n)] = Vec_IntEntry(mismatch, m+1);
                bitVector2[Vec_IntEntry(matchedInputs2, n)] = Vec_IntEntry(mismatch, m+1);
                
            }
            
            for(m = idx-1; m < Vec_IntSize(iMatch1[i]); m++)
            {
                Vec_IntPush(currInputs1, Vec_IntEntry(iMatch1[i], m));
                Vec_IntPush(currInputs2, Vec_IntEntry(iMatch2[i], m));
            }
 
            // Then add all the inputs that are not yet matched to the currInputs
            for(m = 0; m < Abc_NtkPiNum(pNtk1); m++)
            {
                if(Vec_IntFind( matchedInputs1, m ) == -1)
                    Vec_IntPushUnique(currInputs1, m);
 
                if(Vec_IntFind( matchedInputs2, m ) == -1)
                    Vec_IntPushUnique(currInputs2, m);
            }
 
            FpNtk1 = computeCofactor(pNtk1, nodesInLevel1, bitVector1, currInputs1);            
            FpNtk2 = computeCofactor(pNtk2, nodesInLevel2, bitVector2, currInputs2);    
 
            Abc_NtkForEachPo( FpNtk1, pObj, m )
            {        
                int n;
                vSupp  = Abc_NtkNodeSupport( FpNtk1, &pObj, 1 );                        
                
                for(n = 0; n < vSupp->nSize; n++)
                    if( Abc_ObjId((Abc_Obj_t *)vSupp->pArray[n]) == 1 )
                        suppNum1 += Vec_IntFind( matchedOutputs1, m) + 1;                
                        
                Vec_PtrFree( vSupp );
            }
            
            Abc_NtkForEachPo( FpNtk2, pObj, m )
            {        
                int n;
                vSupp  = Abc_NtkNodeSupport( FpNtk2, &pObj, 1 );                        
                
                for(n = 0; n < vSupp->nSize; n++)
                    if( (int)Abc_ObjId((Abc_Obj_t *)vSupp->pArray[n])-1 < (Vec_IntSize(iMatch2[i]))-idx+1 &&
                        (int)Abc_ObjId((Abc_Obj_t *)vSupp->pArray[n])-1 >= 0)
                        suppNum2[Abc_ObjId((Abc_Obj_t *)vSupp->pArray[n])-1] += Vec_IntFind( matchedOutputs2, m) + 1;                
                        
                Vec_PtrFree( vSupp );
            }
 
            /*if(suppNum1 != 0)            
                printf("Ntk1 is trigged");            
 
            if(suppNum2[0] != 0)
                printf("Ntk2 is trigged");*/
 
            for(m = 0; m < Vec_IntSize(iMatch2[i])-idx+1; m++)
                if(suppNum2[m] != suppNum1)
                {
                    skipList[m+idx-1] = TRUE;                    
                    /*printf("input is skipped");*/
                }
                
            Abc_NtkDelete( FpNtk1 );
            Abc_NtkDelete( FpNtk2 );
            ABC_FREE( bitVector1 );    
             ABC_FREE( bitVector2 );    
            Vec_IntFree( currInputs1 );
            Vec_IntFree( currInputs2 );            
            ABC_FREE( suppNum2 );
        }
        
        Vec_PtrClear(oMatchPairs);
        Abc_NtkDelete( subNtk2 );
        Vec_IntFree(mismatch);
 
        //Vec_IntWriteEntry(iMatch2[i], j, tempJ);        
        
        if( MATCH_FOUND == FALSE )
            Vec_IntPop(matchedInputs2);
    }
 
    if( MATCH_FOUND == FALSE )
    {
        Vec_IntPop(matchedInputs1);    
        
        if(idx == 1)
        {
            for(m = 0; m < Vec_IntSize(oNonSingleton); m++)
                Vec_IntPop( oMatchedGroups );
        }
    }
    
    Vec_IntFree( oNonSingleton );    
    Vec_PtrFree( oMatchPairs );    
    ABC_FREE( skipList );
    Abc_NtkDelete( subNtk1 );    
 
    if(MATCH_FOUND && counter != 0)
    {        
        /*printf("Number of INPUT SAT instances = %d\n", counter);*/
 
        counter = 0;
    }
 
    return MATCH_FOUND;
}

Here is the call graph for this function:

Here is the caller graph for this function:

matchNonSingletonOutputs()

int matchNonSingletonOutputs	(	Abc_Ntk_t *	pNtk1,
		Vec_Ptr_t **	nodesInLevel1,
		Vec_Int_t **	iMatch1,
		Vec_Int_t **	iDep1,
		Vec_Int_t *	matchedInputs1,
		int *	iGroup1,
		Vec_Int_t **	oMatch1,
		int *	oGroup1,
		Abc_Ntk_t *	pNtk2,
		Vec_Ptr_t **	nodesInLevel2,
		Vec_Int_t **	iMatch2,
		Vec_Int_t **	iDep2,
		Vec_Int_t *	matchedInputs2,
		int *	iGroup2,
		Vec_Int_t **	oMatch2,
		int *	oGroup2,
		Vec_Int_t *	matchedOutputs1,
		Vec_Int_t *	matchedOutputs2,
		Vec_Int_t *	oMatchedGroups,
		Vec_Int_t *	iNonSingleton,
		Abc_Ntk_t *	subNtk1,
		Abc_Ntk_t *	subNtk2,
		Vec_Ptr_t *	oMatchPairs,
		Vec_Int_t *	oNonSingleton,
		int	oI,
		int	idx,
		int	ii,
		int	iidx )

Definition at line 1185 of file abcBm.c.

{        
    static int MATCH_FOUND;
    int i;
    int j, temp;
    Vec_Int_t * mismatch;        
    int * skipList;    
    static int counter = 0;
 
    MATCH_FOUND = FALSE;
    
    if( oI == Vec_IntSize( oNonSingleton ) )
    {
        if( iNonSingleton != NULL)            
            if( match1by1(pNtk1, nodesInLevel1, iMatch1, iDep1, matchedInputs1, iGroup1, oMatch1, oGroup1,
                          pNtk2, nodesInLevel2, iMatch2, iDep2, matchedInputs2, iGroup2, oMatch2, oGroup2,
                           matchedOutputs1, matchedOutputs2, oMatchedGroups, iNonSingleton, ii, iidx) )
                MATCH_FOUND = TRUE;    
 
        if( iNonSingleton == NULL)
            MATCH_FOUND = TRUE;
 
        return MATCH_FOUND;
    }
 
    i = Vec_IntEntry(oNonSingleton, oI);
 
    mismatch = Vec_IntAlloc(10);
    
    skipList = ABC_ALLOC(int, Vec_IntSize(oMatch1[i]));
 
    for(j = 0; j < Vec_IntSize(oMatch1[i]); j++)
        skipList[j] = FALSE;
 
    Vec_PtrPush(oMatchPairs, Abc_NtkPo(subNtk1, Vec_IntEntry(oMatch1[i], idx)) );
    Vec_IntPush(matchedOutputs1, Vec_IntEntry(oMatch1[i], idx));
 
    for(j = 0; j < Vec_IntSize( oMatch2[i] ) && MATCH_FOUND == FALSE; j++)
    {
        if( Vec_IntEntry(oMatch2[i], j) == -1 || skipList[j] == TRUE)
            continue;
 
        Vec_PtrPush(oMatchPairs, Abc_NtkPo(subNtk2, Vec_IntEntry(oMatch2[i], j)));
        Vec_IntPush(matchedOutputs2, Vec_IntEntry(oMatch2[i], j));
 
        counter++;        
        if( Abc_NtkBmSat( subNtk1, subNtk2, NULL, oMatchPairs, mismatch, 0) )
        {
            /*fprintf(matchFile, "%s matched to %s\n", Abc_ObjName(Abc_NtkPo(pNtk1, Vec_IntEntry(oMatch1[i], idx))), 
                                         Abc_ObjName(Abc_NtkPo(pNtk2, Vec_IntEntry(oMatch2[i], j))));            */
 
            temp =  Vec_IntEntry(oMatch2[i], j);
            Vec_IntWriteEntry(oMatch2[i], j, -1);
            
            if(idx != Vec_IntSize( oMatch1[i] ) - 1)
                // call the same function with idx+1
                matchNonSingletonOutputs(pNtk1, nodesInLevel1, iMatch1, iDep1, matchedInputs1, iGroup1, oMatch1, oGroup1,
                                         pNtk2, nodesInLevel2, iMatch2, iDep2, matchedInputs2, iGroup2, oMatch2, oGroup2,
                                         matchedOutputs1, matchedOutputs2, oMatchedGroups, iNonSingleton,                         
                                         subNtk1, subNtk2, oMatchPairs,
                                         oNonSingleton, oI, idx+1, ii, iidx);
            else    
                // call the same function with idx = 0 and oI++
                matchNonSingletonOutputs(pNtk1, nodesInLevel1, iMatch1, iDep1, matchedInputs1, iGroup1, oMatch1, oGroup1,
                                         pNtk2, nodesInLevel2, iMatch2, iDep2, matchedInputs2, iGroup2, oMatch2, oGroup2,
                                         matchedOutputs1, matchedOutputs2, oMatchedGroups, iNonSingleton,                         
                                         subNtk1, subNtk2, oMatchPairs,
                                         oNonSingleton, oI+1, 0, ii, iidx);
 
            Vec_IntWriteEntry(oMatch2[i], j, temp);
        }        
        else
        {
            int * output1, * output2;
            int k;
            Abc_Obj_t * pObj;
            int * pModel;
            char * vPiValues;            
            
 
            vPiValues = ABC_ALLOC( char,  Abc_NtkPiNum(subNtk1) + 1);
            vPiValues[Abc_NtkPiNum(subNtk1)] = '\0';    
            
            for(k = 0; k < Abc_NtkPiNum(subNtk1); k++)
                vPiValues[k] = '0';
 
            for(k = 0; k < Vec_IntSize(mismatch); k += 2)            
                vPiValues[Vec_IntEntry(mismatch, k)] = Vec_IntEntry(mismatch, k+1);                        
 
            pModel = ABC_ALLOC( int, Abc_NtkCiNum(subNtk1) );    
 
            Abc_NtkForEachPi( subNtk1, pObj, k )
                pModel[k] = vPiValues[k] - '0';
            Abc_NtkForEachLatch( subNtk1, pObj, k )
                pModel[Abc_NtkPiNum(subNtk1)+k] = pObj->iData - 1;            
    
            output1 = Abc_NtkVerifySimulatePattern( subNtk1, pModel );
 
            Abc_NtkForEachLatch( subNtk2, pObj, k )
                pModel[Abc_NtkPiNum(subNtk2)+k] = pObj->iData - 1;
 
            output2 = Abc_NtkVerifySimulatePattern( subNtk2, pModel );
            
 
            for(k = 0; k < Vec_IntSize( oMatch1[i] ); k++)
                if(output1[Vec_IntEntry(oMatch1[i], idx)] != output2[Vec_IntEntry(oMatch2[i], k)])
                {
                    skipList[k] = TRUE;    
                    /*printf("Output is SKIPPED");*/
                }
                
            ABC_FREE( vPiValues );
            ABC_FREE( pModel );
            ABC_FREE( output1 );
            ABC_FREE( output2 );
        }
        
        if(MATCH_FOUND == FALSE )
        {
            Vec_PtrPop(oMatchPairs);
            Vec_IntPop(matchedOutputs2);
        }
    }
 
    if(MATCH_FOUND == FALSE )
    {
        Vec_PtrPop(oMatchPairs);
        Vec_IntPop(matchedOutputs1);
    }
 
    if(MATCH_FOUND && counter != 0)
    {        
        /*printf("Number of OUTPUT SAT instances = %d", counter);*/
        counter = 0;
    }
 
    ABC_FREE( mismatch );
    ABC_FREE( skipList );
 
    return MATCH_FOUND;
}

Here is the call graph for this function:

Here is the caller graph for this function:

oSortDependencies()

void oSortDependencies	(	Abc_Ntk_t *	pNtk,
		Vec_Int_t **	oDep,
		int *	iGroup )

Definition at line 243 of file abcBm.c.

{
    int i, j, k;    
    Vec_Int_t * temp;
    Vec_Int_t * iGroupList;    
    
    iGroupList = Vec_IntAlloc( 10 );
 
    for(i = 0; i < Abc_NtkPoNum(pNtk); i++)
    {
        if(Vec_IntSize(oDep[i]) == 1)
            continue;    
        
        temp = Vec_IntAlloc( Vec_IntSize(oDep[i]) );
 
        for(j = 0; j < Vec_IntSize(oDep[i]); j++)
            Vec_IntPushUniqueOrder(iGroupList, iGroup[Vec_IntEntry(oDep[i], j)]);        
 
        for(j = 0; j < Vec_IntSize(iGroupList); j++)
        {
            for(k = 0; k < Vec_IntSize(oDep[i]); k++)
                if(iGroup[Vec_IntEntry(oDep[i], k)] == Vec_IntEntry(iGroupList, j))
                {
                    Vec_IntPush( temp, Vec_IntEntry(oDep[i], k) );
                    Vec_IntRemove( oDep[i], Vec_IntEntry(oDep[i], k) );
                    k--;
                }
        }
 
        Vec_IntFree( oDep[i] );
        oDep[i] = temp;
        Vec_IntClear( iGroupList );
 
        /*printf("Output %d: ", i);
        for(j = 0; j < Vec_IntSize(oDep[i]); j++)
            printf("%d ", Vec_IntEntry(oDep[i], j));
        printf("\n");*/
    }
    
    Vec_IntFree( iGroupList );
}

Here is the caller graph for this function:

oSplitByDep()

int oSplitByDep	(	Abc_Ntk_t *	pNtk,
		Vec_Int_t **	oDep,
		Vec_Int_t **	oMatch,
		int *	oGroup,
		int *	oLastItem,
		int *	iGroup )

Definition at line 285 of file abcBm.c.

{
    int i, j, k;
    int numOfItemsAdded;
    Vec_Int_t * array, * sortedArray;    
 
    numOfItemsAdded = 0;
 
    for(i = 0; i < *oLastItem; i++)
    {
        if(Vec_IntSize(oMatch[i]) == 1)
            continue;
 
        array = Vec_IntAlloc( Vec_IntSize(oMatch[i]) );
        sortedArray = Vec_IntAlloc( Vec_IntSize(oMatch[i]) );
 
        for(j = 0; j < Vec_IntSize(oMatch[i]); j++)
        {
            int factor, encode;
 
            encode = 0;
            factor = 1;    
            
            for(k = 0; k < Vec_IntSize(oDep[Vec_IntEntry(oMatch[i], j)]); k++)                                        
                encode += iGroup[Vec_IntEntry(oDep[Vec_IntEntry(oMatch[i], j)], k)] * factor;                        
            
            Vec_IntPush(array, encode);
            Vec_IntPushUniqueOrder(sortedArray, encode);
 
            if( encode < 0)
                printf("WARNING! Integer overflow!");
 
            //printf("%d ", Vec_IntEntry(array, j));
        }                
        
        while( Vec_IntSize(sortedArray) > 1 )
        {            
            for(k = 0; k < Vec_IntSize(oMatch[i]); k++) 
            {
                if(Vec_IntEntry(array, k) == Vec_IntEntryLast(sortedArray))
                {
                    Vec_IntPush(oMatch[*oLastItem+numOfItemsAdded], Vec_IntEntry(oMatch[i], k));
                    oGroup[Vec_IntEntry(oMatch[i], k)] = *oLastItem+numOfItemsAdded;
                    Vec_IntRemove( oMatch[i], Vec_IntEntry(oMatch[i], k) );        
                    Vec_IntRemove( array, Vec_IntEntry(array, k) );            
                    k--;
                }    
            }            
            numOfItemsAdded++;
            Vec_IntPop(sortedArray);                        
        }
 
        Vec_IntFree( array );        
        Vec_IntFree( sortedArray );        
        //printf("\n");
    }    
 
    *oLastItem += numOfItemsAdded;
 
    /*printf("\n");
    for(j = 0; j < *oLastItem ; j++)
    {
        printf("oMatch %d: ", j);
        for(i = 0; i < Vec_IntSize(oMatch[j]); i++)
            printf("%d ", Vec_IntEntry(oMatch[j], i));
        printf("\n");
    }*/
 
    return numOfItemsAdded;
}

Here is the caller graph for this function:

refineBySAT()

float refineBySAT	(	Abc_Ntk_t *	pNtk1,
		Vec_Int_t **	iMatch1,
		int *	iGroup1,
		Vec_Int_t **	iDep1,
		int *	iLastItem1,
		Vec_Int_t **	oMatch1,
		int *	oGroup1,
		Vec_Int_t **	oDep1,
		int *	oLastItem1,
		int *	observability1,
		Abc_Ntk_t *	pNtk2,
		Vec_Int_t **	iMatch2,
		int *	iGroup2,
		Vec_Int_t **	iDep2,
		int *	iLastItem2,
		Vec_Int_t **	oMatch2,
		int *	oGroup2,
		Vec_Int_t **	oDep2,
		int *	oLastItem2,
		int *	observability2 )

Definition at line 1576 of file abcBm.c.

{
    int i, j;    
    Abc_Obj_t * pObj;
    Vec_Int_t * iNonSingleton;
    Vec_Int_t * matchedInputs1, * matchedInputs2;
    Vec_Int_t * matchedOutputs1, * matchedOutputs2;
    Vec_Ptr_t ** nodesInLevel1, ** nodesInLevel2;
    Vec_Int_t * oMatchedGroups;
    FILE *result;    
    int matchFound;
    abctime clk = Abc_Clock();
    float satTime = 0.0;
 
    /*matchFile = fopen("satmatch.txt", "w");*/
    
    iNonSingleton = Vec_IntAlloc(10);    
    
    matchedInputs1 = Vec_IntAlloc( Abc_NtkPiNum(pNtk1) );
    matchedInputs2 = Vec_IntAlloc( Abc_NtkPiNum(pNtk2) );
 
    matchedOutputs1 = Vec_IntAlloc( Abc_NtkPoNum(pNtk1) );
    matchedOutputs2 = Vec_IntAlloc( Abc_NtkPoNum(pNtk2) );
 
    nodesInLevel1 = ABC_ALLOC( Vec_Ptr_t *, Abc_AigLevel( pNtk1 ) + 1);    // why numOfLevels+1? because the inputs are in level 0
    for(i = 0; i <= Abc_AigLevel( pNtk1 ); i++)
        nodesInLevel1[i] = Vec_PtrAlloc( 20 );
 
    // bucket sort the objects based on their levels
    Abc_AigForEachAnd( pNtk1, pObj, i )    
        Vec_PtrPush(nodesInLevel1[Abc_ObjLevel(pObj)], pObj);
    
    nodesInLevel2 = ABC_ALLOC( Vec_Ptr_t *, Abc_AigLevel( pNtk2 ) + 1);    // why numOfLevels+1? because the inputs are in level 0
    for(i = 0; i <= Abc_AigLevel( pNtk2 ); i++)
        nodesInLevel2[i] = Vec_PtrAlloc( 20 );
 
    // bucket sort the objects based on their levels
    Abc_AigForEachAnd( pNtk2, pObj, i )    
        Vec_PtrPush(nodesInLevel2[Abc_ObjLevel(pObj)], pObj);    
 
    oMatchedGroups = Vec_IntAlloc( 10 );
 
    for(i = 0; i < *iLastItem1; i++)
    {
        if(Vec_IntSize(iMatch1[i]) == 1)
        {
            Vec_IntPush(matchedInputs1, Vec_IntEntryLast(iMatch1[i]));
            Vec_IntPush(matchedInputs2, Vec_IntEntryLast(iMatch2[i]));        
        }
        else
            Vec_IntPush(iNonSingleton, i);
    }
 
    for(i = 0; i < *oLastItem1; i++)
    {
        if(Vec_IntSize(oMatch1[i]) == 1)
        {
            Vec_IntPush(matchedOutputs1, Vec_IntEntryLast(oMatch1[i]));
            Vec_IntPush(matchedOutputs2, Vec_IntEntryLast(oMatch2[i]));
        }
    }
    
    for(i = 0; i < Vec_IntSize(iNonSingleton) - 1; i++)
    {
        for(j = i + 1; j < Vec_IntSize(iNonSingleton); j++)        
            if( observability2[Vec_IntEntry(iMatch2[Vec_IntEntry(iNonSingleton, j)], 0)] > 
                observability2[Vec_IntEntry(iMatch2[Vec_IntEntry(iNonSingleton, i)], 0)] )
            {                
                int temp = Vec_IntEntry(iNonSingleton, i);
                Vec_IntWriteEntry( iNonSingleton, i, Vec_IntEntry(iNonSingleton, j) );
                Vec_IntWriteEntry( iNonSingleton, j, temp );                
            }
            else if( observability2[Vec_IntEntry(iMatch2[Vec_IntEntry(iNonSingleton, j)], 0)] == 
                     observability2[Vec_IntEntry(iMatch2[Vec_IntEntry(iNonSingleton, i)], 0)] )
            {
                if( Vec_IntSize(iMatch2[Vec_IntEntry(iNonSingleton, j)]) < Vec_IntSize(iMatch2[Vec_IntEntry(iNonSingleton, i)]) )
                {
                    int temp = Vec_IntEntry(iNonSingleton, i);
                    Vec_IntWriteEntry( iNonSingleton, i, Vec_IntEntry(iNonSingleton, j) );
                    Vec_IntWriteEntry( iNonSingleton, j, temp );                
                }
            }
    }    
 
    /*for(i = 0; i < Vec_IntSize(iNonSingleton) - 1; i++)
    {
        for(j = i + 1; j < Vec_IntSize(iNonSingleton); j++)        
            if( Vec_IntSize(oDep2[oGroup2[Vec_IntEntryLast(iMatch2[Vec_IntEntry(iNonSingleton, j)])]]) > 
                Vec_IntSize(oDep2[oGroup2[Vec_IntEntryLast(iMatch2[Vec_IntEntry(iNonSingleton, i)])]]) )
            {                
                int temp = Vec_IntEntry(iNonSingleton, i);
                Vec_IntWriteEntry( iNonSingleton, i, Vec_IntEntry(iNonSingleton, j) );
                Vec_IntWriteEntry( iNonSingleton, j, temp );                
            }
            else if( Vec_IntSize(oDep2[oGroup2[Vec_IntEntryLast(iMatch2[Vec_IntEntry(iNonSingleton, j)])]]) == 
                Vec_IntSize(oDep2[oGroup2[Vec_IntEntryLast(iMatch2[Vec_IntEntry(iNonSingleton, i)])]]) )
            {
                if( observability2[Vec_IntEntry(iMatch2[Vec_IntEntry(iNonSingleton, j)], 0)] > 
                        observability2[Vec_IntEntry(iMatch2[Vec_IntEntry(iNonSingleton, i)], 0)] )
                {
                    int temp = Vec_IntEntry(iNonSingleton, i);
                    Vec_IntWriteEntry( iNonSingleton, i, Vec_IntEntry(iNonSingleton, j) );
                    Vec_IntWriteEntry( iNonSingleton, j, temp );                
                }
            }
    }*/
 
    matchFound = match1by1(pNtk1, nodesInLevel1, iMatch1, iDep1, matchedInputs1, iGroup1, oMatch1, oGroup1,
                           pNtk2, nodesInLevel2, iMatch2, iDep2, matchedInputs2, iGroup2, oMatch2, oGroup2,
                           matchedOutputs1, matchedOutputs2, oMatchedGroups, iNonSingleton, 0, 0);
 
    if( matchFound && Vec_IntSize(matchedOutputs1) != Abc_NtkPoNum(pNtk1) )
    {
        Vec_Int_t * oNonSingleton;
        Vec_Ptr_t * oMatchPairs;
        Abc_Ntk_t * subNtk1, * subNtk2;
 
        oNonSingleton = Vec_IntAlloc( 10 );
        
        oMatchPairs = Vec_PtrAlloc(Abc_NtkPoNum(pNtk1) * 2);    
 
        for(i = 0; i < *oLastItem1; i++)
            if( Vec_IntSize(oMatch1[i]) > 1 && Vec_IntFind( oMatchedGroups, i) == -1 )
                Vec_IntPush(oNonSingleton, i);
            
        subNtk1 = computeCofactor(pNtk1, nodesInLevel1, NULL, matchedInputs1);
        subNtk2 = computeCofactor(pNtk2, nodesInLevel2, NULL, matchedInputs2);
        
        matchFound = matchNonSingletonOutputs(pNtk1, nodesInLevel1, iMatch1, iDep1, matchedInputs1, iGroup1, oMatch1, oGroup1,
                                 pNtk2, nodesInLevel2, iMatch2, iDep2, matchedInputs2, iGroup1, oMatch2, oGroup2,
                                 matchedOutputs1, matchedOutputs2, oMatchedGroups, NULL,                         
                                 subNtk1, subNtk2, oMatchPairs, oNonSingleton, 0, 0, 0, 0);
 
        Vec_IntFree( oNonSingleton );        
        Vec_PtrFree( oMatchPairs );
 
        Abc_NtkDelete(subNtk1);
        Abc_NtkDelete(subNtk2);
    }
 
    satTime = (float)(Abc_Clock() - clk)/(float)(CLOCKS_PER_SEC);    
 
    if( matchFound )
    {
          checkEquivalence( pNtk1, matchedInputs1, matchedOutputs1, pNtk2, matchedInputs2, matchedOutputs2);
 
        result = fopen("IOmatch.txt", "w");
 
        fprintf(result, "I/O = %d / %d \n\n", Abc_NtkPiNum(pNtk1), Abc_NtkPoNum(pNtk1));
        
        for(i = 0; i < Vec_IntSize(matchedInputs1) ; i++)
              fprintf(result, "{%s}\t{%s}\n", Abc_ObjName(Abc_NtkPi(pNtk1, Vec_IntEntry(matchedInputs1, i))), Abc_ObjName(Abc_NtkPi(pNtk2, Vec_IntEntry(matchedInputs2, i))) );                                    
 
        fprintf(result, "\n-----------------------------------------\n");
 
        for(i = 0; i < Vec_IntSize(matchedOutputs1) ; i++)
            fprintf(result, "{%s}\t{%s}\n", Abc_ObjName(Abc_NtkPo(pNtk1, Vec_IntEntry(matchedOutputs1, i))), Abc_ObjName(Abc_NtkPo(pNtk2, Vec_IntEntry(matchedOutputs2, i))) );                                    
 
        fclose( result );    
    }
 
    Vec_IntFree( matchedInputs1 );
    Vec_IntFree( matchedInputs2 );
    Vec_IntFree( matchedOutputs1 );
    Vec_IntFree( matchedOutputs2 );
    Vec_IntFree( iNonSingleton );
    Vec_IntFree( oMatchedGroups );
    
    for(i = 0; i <= Abc_AigLevel( pNtk1 ); i++)    
        Vec_PtrFree( nodesInLevel1[i] );
    for(i = 0; i <= Abc_AigLevel( pNtk2 ); i++)    
        Vec_PtrFree( nodesInLevel2[i] );
    
 
    ABC_FREE( nodesInLevel1 );
    ABC_FREE( nodesInLevel2 );
    /*fclose(matchFile);*/
    
    return satTime;
}

Here is the call graph for this function:

Here is the caller graph for this function:

refineIOBySimulation()

int refineIOBySimulation	(	Abc_Ntk_t *	pNtk,
		Vec_Int_t **	iMatch,
		int *	iLastItem,
		int *	iGroup,
		Vec_Int_t **	iDep,
		Vec_Int_t **	oMatch,
		int *	oLastItem,
		int *	oGroup,
		Vec_Int_t **	oDep,
		char *	vPiValues,
		int *	observability,
		Vec_Ptr_t **	topOrder )

Definition at line 510 of file abcBm.c.

{
    Abc_Obj_t * pObj;
    int * pModel;//, ** pModel2;
    int * output, * output2;
    int lastItem;
    int i, j, k;
    Vec_Int_t * iComputedNum, * iComputedNumSorted;    
    Vec_Int_t * oComputedNum;                // encoding the number of flips        
    int factor;    
    int isRefined = FALSE;    
 
    pModel = ABC_ALLOC( int, Abc_NtkCiNum(pNtk) );    
 
    Abc_NtkForEachPi( pNtk, pObj, i )
        pModel[i] = vPiValues[i] - '0';
    Abc_NtkForEachLatch( pNtk, pObj, i )
        pModel[Abc_NtkPiNum(pNtk)+i] = pObj->iData - 1;
 
    output = Abc_NtkVerifySimulatePattern( pNtk, pModel );    
 
    oComputedNum = Vec_IntAlloc( Abc_NtkPoNum(pNtk) );
    for(i = 0; i < Abc_NtkPoNum(pNtk); i++)
        Vec_IntPush(oComputedNum, 0);
    
    /****************************************************************************************/
    /********** group outputs that produce 1 and outputs that produce 0 together ************/    
    
    lastItem = *oLastItem;
    for(i = 0; i < lastItem && (*oLastItem) != Abc_NtkPoNum(pNtk); i++)
    {
        int flag = FALSE;
 
        if(Vec_IntSize(oMatch[i]) == 1)
            continue;
 
        for(j = 1; j < Vec_IntSize(oMatch[i]); j++)
            if(output[Vec_IntEntry(oMatch[i], 0)] != output[Vec_IntEntry(oMatch[i], j)])
            {
                flag = TRUE;
                break;
            }
 
        if(flag)
        {
            for(j = 0; j < Vec_IntSize(oMatch[i]); j++)
                if(output[Vec_IntEntry(oMatch[i], j)])
                {
                    Vec_IntPush(oMatch[*oLastItem], Vec_IntEntry(oMatch[i], j));
                    oGroup[Vec_IntEntry(oMatch[i], j)] = *oLastItem;    
                    Vec_IntRemove(oMatch[i], Vec_IntEntry(oMatch[i], j));    
                    j--;
                }
 
            (*oLastItem)++;
        }
    }
 
    if( (*oLastItem) > lastItem )
    {
        isRefined = TRUE;
        iSortDependencies(pNtk, iDep, oGroup);    
    }
 
    /****************************************************************************************/
    /************* group inputs that make the same number of flips in outpus ****************/        
 
    lastItem = *iLastItem;
    for(i = 0; i < lastItem && (*iLastItem) != Abc_NtkPiNum(pNtk); i++)
    {
        int num;
 
        if(Vec_IntSize(iMatch[i]) == 1)
            continue;
 
        iComputedNum = Vec_IntAlloc( Vec_IntSize(iMatch[i]) );
        iComputedNumSorted = Vec_IntAlloc( Vec_IntSize(iMatch[i]) );    
        
        for(j = 0; j < Vec_IntSize(iMatch[i]); j++)
        {
            if( vPiValues[Vec_IntEntry(iMatch[i], j)] == '0' )                
                pModel[Vec_IntEntry(iMatch[i], j)] = 1;
            else                 
                pModel[Vec_IntEntry(iMatch[i], j)] = 0;        
            
            //output2 = Abc_NtkVerifySimulatePattern( pNtk, pModel );    
            output2 = Abc_NtkSimulateOneNode( pNtk, pModel, Vec_IntEntry(iMatch[i], j), topOrder );
            
            num = 0;
            factor = 1;    
            for(k = 0; k < Vec_IntSize(iDep[Vec_IntEntry(iMatch[i], j)]); k++)
            {
                int outputIndex = Vec_IntEntry(iDep[Vec_IntEntry(iMatch[i], j)], k);        
 
                if(output2[outputIndex])
                    num += (oGroup[outputIndex] + 1) * factor;                
            
                if(output[outputIndex] != output2[outputIndex])
                {
                    int temp = Vec_IntEntry(oComputedNum, outputIndex) + i + 1;
                    Vec_IntWriteEntry(oComputedNum, outputIndex, temp);    
                    observability[Vec_IntEntry(iMatch[i], j)]++;
                }
            }
 
            Vec_IntPush(iComputedNum, num);
            Vec_IntPushUniqueOrder(iComputedNumSorted, num);            
 
            pModel[Vec_IntEntry(iMatch[i], j)] = vPiValues[Vec_IntEntry(iMatch[i], j)] - '0';
            ABC_FREE( output2 );
        }    
 
        while( Vec_IntSize( iComputedNumSorted ) > 1 )
        {
            for(k = 0; k < Vec_IntSize(iMatch[i]); k++)
            {                            
                if(Vec_IntEntry(iComputedNum, k) == Vec_IntEntryLast(iComputedNumSorted) )
                {
                    Vec_IntPush(iMatch[*iLastItem], Vec_IntEntry(iMatch[i], k));
                    iGroup[Vec_IntEntry(iMatch[i], k)] = *iLastItem;
                    Vec_IntRemove( iMatch[i], Vec_IntEntry(iMatch[i], k) );
                    Vec_IntRemove( iComputedNum, Vec_IntEntry(iComputedNum, k) );        
                    k--;
                }                
            }
            (*iLastItem)++;    
            Vec_IntPop( iComputedNumSorted );
        }    
 
        Vec_IntFree( iComputedNum );
        Vec_IntFree( iComputedNumSorted );
    }
 
    if( (*iLastItem) > lastItem )
    {
        isRefined = TRUE;
        oSortDependencies(pNtk, oDep, iGroup);
    }
 
    /****************************************************************************************/
    /********** encode the number of flips in each output by flipping the outputs ***********/
    /********** and group all the outputs that have the same encoding         ***********/    
 
    lastItem = *oLastItem;
    for(i = 0; i < lastItem && (*oLastItem) != Abc_NtkPoNum(pNtk); i++)
    {
        Vec_Int_t * encode, * sortedEncode;                // encoding the number of flips                    
 
        if(Vec_IntSize(oMatch[i]) == 1)
            continue;
            
        encode = Vec_IntAlloc( Vec_IntSize(oMatch[i]) );
        sortedEncode = Vec_IntAlloc( Vec_IntSize(oMatch[i]) );                    
    
        for(j = 0; j < Vec_IntSize(oMatch[i]); j++)
        {
            Vec_IntPush(encode, Vec_IntEntry(oComputedNum, Vec_IntEntry(oMatch[i], j)) );
            Vec_IntPushUniqueOrder( sortedEncode, Vec_IntEntry(encode, j) );
        }
 
        while( Vec_IntSize(sortedEncode) > 1 )
        {
            for(j = 0; j < Vec_IntSize(oMatch[i]); j++)
                if(Vec_IntEntry(encode, j) == Vec_IntEntryLast(sortedEncode))
                {
                    Vec_IntPush(oMatch[*oLastItem], Vec_IntEntry(oMatch[i], j));
                    oGroup[Vec_IntEntry(oMatch[i], j)] = *oLastItem;
                    Vec_IntRemove( oMatch[i], Vec_IntEntry(oMatch[i], j) );
                    Vec_IntRemove( encode, Vec_IntEntry(encode, j) );
                    j --;
                }                
            
            (*oLastItem)++;
            Vec_IntPop( sortedEncode );
        }
 
        Vec_IntFree( encode );
        Vec_IntFree( sortedEncode );
    }
 
    if( (*oLastItem) > lastItem )
        isRefined = TRUE;    
 
    ABC_FREE( pModel );
    ABC_FREE( output );
    Vec_IntFree( oComputedNum );
 
    return isRefined;    
}

Here is the call graph for this function:

Here is the caller graph for this function:

Variable Documentation

matchFile

FILE* matchFile

Definition at line 1183 of file abcBm.c.

pValues1__

int* pValues1__

Definition at line 808 of file abcBm.c.

pValues2__

int * pValues2__

Definition at line 808 of file abcBm.c.