simSupp.c File Reference

#include "base/abc/abc.h"
#include "proof/fraig/fraig.h"
#include "sim.h"

Include dependency graph for simSupp.c:

Go to the source code of this file.

Functions
Vec_Ptr_t *	Sim_ComputeStrSupp (Abc_Ntk_t *pNtk)
	FUNCTION DEFINITIONS ///.
Vec_Ptr_t *	Sim_ComputeFunSupp (Abc_Ntk_t *pNtk, int fVerbose)
int	Sim_NtkSimTwoPats_rec (Abc_Obj_t *pNode)

Function Documentation

Sim_ComputeFunSupp()

Vec_Ptr_t * Sim_ComputeFunSupp	(	Abc_Ntk_t *	pNtk,
		int	fVerbose )

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

Synopsis [Compute functional supports.]

Description [Supports are returned as an array of bit strings, one for each CO.]

SideEffects []

SeeAlso []

Definition at line 103 of file simSupp.c.

{
    Sim_Man_t * p;
    Vec_Ptr_t * vResult;
    int nSolved, i;
    abctime clk = Abc_Clock();
 
    srand( 0xABC );
 
    // start the simulation manager
    p = Sim_ManStart( pNtk, 0 );
 
    // compute functional support using one round of random simulation
    Sim_UtilAssignRandom( p );
    Sim_ComputeSuppRound( p, 0 );
 
    // set the support targets 
    Sim_ComputeSuppSetTargets( p );
    if ( fVerbose )
        printf( "Number of support targets after simulation = %5d.\n", Vec_VecSizeSize(p->vSuppTargs) );
    if ( Vec_VecSizeSize(p->vSuppTargs) == 0 )
        goto exit;
 
    for ( i = 0; i < 1; i++ )
    {
        // compute patterns using one round of random simulation
        Sim_UtilAssignRandom( p );
        nSolved = Sim_ComputeSuppRound( p, 1 );
        if ( Vec_VecSizeSize(p->vSuppTargs) == 0 )
            goto exit;
 
        if ( fVerbose )
            printf( "Targets = %5d.   Solved = %5d.  Fifo = %5d.\n",
                Vec_VecSizeSize(p->vSuppTargs), nSolved, Vec_PtrSize(p->vFifo) );
    }
 
    // try to solve the support targets
    while ( Vec_VecSizeSize(p->vSuppTargs) > 0 )
    {
        // solve targets until the first disproved one (which gives counter-example)
        Sim_SolveTargetsUsingSat( p, p->nSimWords/p->nSuppWords );
        // compute additional functional support
        Sim_UtilAssignFromFifo( p );
        nSolved = Sim_ComputeSuppRound( p, 1 );
 
if ( fVerbose )
    printf( "Targets = %5d.   Solved = %5d.  Fifo = %5d.  SAT runs = %3d.\n", 
            Vec_VecSizeSize(p->vSuppTargs), nSolved, Vec_PtrSize(p->vFifo), p->nSatRuns );
    }
 
exit:
p->timeTotal = Abc_Clock() - clk;
    vResult = p->vSuppFun;  
    //  p->vSuppFun = NULL;
    Sim_ManStop( p );
    return vResult;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Sim_ComputeStrSupp()

Vec_Ptr_t * Sim_ComputeStrSupp

(

Abc_Ntk_t *

pNtk

)

FUNCTION DEFINITIONS ///.

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

Synopsis [Computes structural supports.]

Description [Supports are returned as an array of bit strings, one for each CO.]

SideEffects []

SeeAlso []

Definition at line 57 of file simSupp.c.

{
    Vec_Ptr_t * vSuppStr;
    Abc_Obj_t * pNode;
    unsigned * pSimmNode, * pSimmNode1, * pSimmNode2;
    int nSuppWords, i, k;
    // allocate room for structural supports
    nSuppWords = SIM_NUM_WORDS( Abc_NtkCiNum(pNtk) );
    vSuppStr   = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), nSuppWords, 1 );
    // assign the structural support to the PIs
    Abc_NtkForEachCi( pNtk, pNode, i )
        Sim_SuppStrSetVar( vSuppStr, pNode, i );
    // derive the structural supports of the internal nodes
    Abc_NtkForEachNode( pNtk, pNode, i )
    {
//        if ( Abc_NodeIsConst(pNode) )
//            continue;
        pSimmNode  = (unsigned *)vSuppStr->pArray[ pNode->Id ];
        pSimmNode1 = (unsigned *)vSuppStr->pArray[ Abc_ObjFaninId0(pNode) ];
        pSimmNode2 = (unsigned *)vSuppStr->pArray[ Abc_ObjFaninId1(pNode) ];
        for ( k = 0; k < nSuppWords; k++ )
            pSimmNode[k] = pSimmNode1[k] | pSimmNode2[k];
    }
    // set the structural supports of the PO nodes
    Abc_NtkForEachCo( pNtk, pNode, i )
    {
        pSimmNode  = (unsigned *)vSuppStr->pArray[ pNode->Id ];
        pSimmNode1 = (unsigned *)vSuppStr->pArray[ Abc_ObjFaninId0(pNode) ];
        for ( k = 0; k < nSuppWords; k++ )
            pSimmNode[k] = pSimmNode1[k];
    }
    return vSuppStr;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Sim_NtkSimTwoPats_rec()

int Sim_NtkSimTwoPats_rec

(

Abc_Obj_t *

pNode

)

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

Synopsis [Saves the counter example.]

Description []

SideEffects []

SeeAlso []

Definition at line 548 of file simSupp.c.

{
    int Value0, Value1;
    if ( Abc_NodeIsTravIdCurrent( pNode ) )
        return (int)(ABC_PTRUINT_T)pNode->pCopy;
    Abc_NodeSetTravIdCurrent( pNode );
    Value0 = Sim_NtkSimTwoPats_rec( Abc_ObjFanin0(pNode) );
    Value1 = Sim_NtkSimTwoPats_rec( Abc_ObjFanin1(pNode) );
    if ( Abc_ObjFaninC0(pNode) )
        Value0 = ~Value0;
    if ( Abc_ObjFaninC1(pNode) )
        Value1 = ~Value1;
    pNode->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)(Value0 & Value1);
    return Value0 & Value1;
}

Here is the call graph for this function:

Here is the caller graph for this function: