simpimage.c

主要进行大规模的电路综合

    DdNode     *bCare)
{
    int i,k,nValues, nFanins;
    sarray_t       *aFuncs, *aNodes;
    Mva_Func_t     *pMva;
    
    Ntk_Node_t     *pResult, *pFanin;
    Ntk_Pin_t      *pPin;
    Simp_Node_t    *simp_data;
    Mvc_Cover_t    *pMvcCare;
    Mvc_Data_t     *pMvcData;
    Vm_VarMap_t    *pVm;
    DdNode         **pbGlo, *bTemp;
    DdManager      *mg;
    
    mg = pInfo->ddmg;
    
    /* compute output cofactors */
    nFanins = Ntk_NodeReadFaninNum(pNode);
    aFuncs = sarray_alloc( Mva_Func_t *, nFanins );
    aNodes = sarray_alloc( Ntk_Node_t *, nFanins );
    Ntk_NodeReadFanins(pNode, (Ntk_Node_t **)(aNodes->space));
    aNodes->num = nFanins;
    
    Ntk_NodeForEachFaninWithIndex( pNode, pPin, pFanin, i ) {
        
        simp_data = Simp_DaemonGetNodeData(pFanin);
        nValues   = Ntk_NodeReadValueNum( pFanin );
        pMva      = Mva_FuncAlloc( mg, nValues );
        
        /* have to use global function here */
        pbGlo = Ntk_NodeGetFuncGlo(pFanin);
        
        for (k=0; k<nValues; ++k) {
            bTemp = Cudd_bddConstrain(mg, pbGlo[k], bCare);
            Cudd_Ref(bTemp);
            Mva_FuncReplaceIset( pMva, k, bTemp );
        }
        
        sarray_insert_last( Mva_Func_t *, aFuncs, pMva );
    }
    
    /* reset the start time */
    SimpTimeOutStartNode(pInfo, pInfo->time_left_node);
    
    /* allocate cover information (var mask etc.) */
    pVm = Ntk_NodeReadFuncVm( pNode );
    pMvcData = SimpAllocateMvcData( pNode );
    
    /* start recursive range computation */
    pMvcCare = SimpComputeRangeRecur(pInfo, &aFuncs, &aNodes, pVm, pMvcData, 0);
    
    /* de-allocate cover information */
    SimpFreeMvcData( pNode, pMvcData );
    
    
    /* NULL means full image */
    if (pMvcCare == NULL) {
        pResult = NULL;
    }
    else {
        pResult = SimpNodeCreateFromFanins(Ntk_NodeReadNetwork(pNode),aNodes);
        SimpNodeAssignMvc( pResult, pMvcCare );
    }
    
    sarray_free(aNodes);
    if (aFuncs != NIL(sarray_t)) {
        SimpMvaArrayFree( aFuncs, 0 );
    }
    
    return pResult;
}


/**Function********************************************************************

  Synopsis    [Recursive range computation.]

  Description [Recursive range computation. The function list and node list
  are given in terms of addresses of the pointers, because the pointer may get
  freed or changed.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
Mvc_Cover_t *
SimpComputeRangeRecur(
    Simp_Info_t   *pInfo,
    sarray_t     **func_list,
    sarray_t     **local_base,
    Vm_VarMap_t   *pVm,
    Mvc_Data_t    *pMvcData,
    int            start_index)
{
    DdManager       *mg;
    Mvc_Cover_t     *pImage, *pSuper, *pLit, *pTemp, *pTemp1;
    Mva_Func_t      *pMva;
    sarray_t        *listFuncs, *listNodes, *listSupp;
    var_set_t       *vsSupp;
    int             i, k, nConst, thisone, count, iSet;
    
    if (SimpTimeOutCheckNode(pInfo)) {
        return NULL;
    }

    mg = pInfo->ddmg;
    listFuncs = *func_list;
    listNodes = *local_base;
    
    /* Constant functions are removed from the list;
     * the corresponding mv variable is ANDed to the image cube.
     */
    pImage  = NULL;
    thisone = -1;
    count   = 0;
    
    for (i=start_index; i<sarray_n(listFuncs); ++i) {
        
        pMva = sarray_fetch( Mva_Func_t *, listFuncs, i);
        if ( pMva == NULL )
            continue;
        
        if ( Mva_FuncIsConstant( pMva, &nConst ) ) {
            
            Mva_FuncFree( pMva );
            sarray_insert( Mva_Func_t *, listFuncs, i, NULL );
            pLit  = SimpCubeLiteral( pInfo->pMvcMem, pVm, i, nConst );
            if (pImage==NULL) {
                pImage = pLit;
            }
            else {
                pTemp = Mvc_CoverBooleanAnd( pMvcData, pImage, pLit );
                Mvc_CoverFree(pImage);
                Mvc_CoverFree(pLit);
                pImage = pTemp;
            }
            continue;
        }
        count++;
        if (thisone == -1 ) {
            thisone = i; /* the first non-NIL function */
        }
    }
    
    /* if only one function left and not constant,
     * terminate the recursion and return the full image
     */
    if (count <= 1) {
        if (thisone>=0) {
            
            /* compute actual set of values, may not be whole set */
            pMva = sarray_fetch( Mva_Func_t *, listFuncs, thisone);
            pLit = SimpCubeLiteralImage ( pInfo->pMvcMem, pVm, mg, thisone, pMva);
            
            if (pLit) { /* Null means fullset and no need to intersect */
                pTemp = Mvc_CoverBooleanAnd( pMvcData, pImage, pLit );
                Mvc_CoverFree( pImage );
                Mvc_CoverFree( pLit );
                pImage = pTemp;
            }
            Mva_FuncFree( pMva ); pMva = NULL;
        }
        /* if nothing is left then return empty set */
        
        sarray_free(listFuncs); /* recursively generated */
        *func_list = NIL(sarray_t);
        return pImage;
    }
    
    /* partition the list of functions into disjoint supports;
       If there is only one function, no need to process; if there are two
       functions, call a special routine; else do output cofactoring with
       respect to the first function and recurse.
    */
    
    listSupp = SimpDisjointSupports(listNodes, listFuncs, start_index, pInfo);
    
    pSuper = NULL;
    for (iSet=0; iSet<sarray_n(listSupp); ++iSet) {
        
        vsSupp = sarray_fetch(var_set_t *, listSupp, iSet);
        k = var_set_n_elts(vsSupp);
        if (k==1) {
            /* stand alone node:
             *  still need to check if all phases of this node are reachable;
             *  if not, apply restrictions to the super_image.
             */
            pTemp = SimpRangeOne( pInfo, pVm, start_index, vsSupp, listFuncs);
        }
        else if (k==2) {
            pTemp = SimpRangeTwo( pInfo, pVm, pMvcData, start_index, vsSupp, listFuncs);
        }
        else {
            pTemp = SimpRangeCofact(pInfo, pVm, pMvcData, start_index, vsSupp,
                                    listFuncs, local_base );
        }
        var_set_free(vsSupp);
        if (pTemp) {
            if (pSuper) {
                pTemp1 = Mvc_CoverBooleanAnd( pMvcData, pSuper, pTemp );
                Mvc_CoverFree(pSuper);
                Mvc_CoverFree(pTemp);
                pSuper = pTemp1;
            } else {
                pSuper = pTemp;
            }
        }
    }
    sarray_free(listSupp);
    
    /* quick simplification to avoid huge image */
    if ( pSuper && Mvc_CoverReadCubeNum(pSuper) >= 300 ) {
        
        //printf("warning: image size larger than 300 cubes.\n");
        Mvc_CoverDist1Merge( pMvcData, pSuper );
    }
    
    if (pImage) {
        if (pSuper) {
            pTemp = Mvc_CoverBooleanAnd( pMvcData, pSuper, pImage );
            Mvc_CoverFree(pSuper);
            Mvc_CoverFree(pImage);
            pSuper = pTemp;
        }
        else {
            pSuper = pImage;
        }
    }
    
    return pSuper;
}


/**Function********************************************************************

  Synopsis    [Return the range of one function.]

  Description [Return the range of one function. The support set contains
  disjoint functional supports, in which only one function is left. Check if
  all output values of this node are reachable; if not, apply restrictions to
  the super_image]

  SideEffects []
  SeeAlso     []

******************************************************************************/
Mvc_Cover_t *
SimpRangeOne(
    Simp_Info_t *pInfo,
    Vm_VarMap_t *pVm,
    int         start_index,
    var_set_t   *supset,
    sarray_t     *listFuncs )
{
    int i;
    Mva_Func_t  *pMva = NULL;
    
    /* retrieve the one and only left */
    for ( i = start_index; i < sarray_n(listFuncs); ++i ) {
        if (!var_set_get_elt(supset,i)) continue;
        pMva = sarray_fetch( Mva_Func_t *, listFuncs, i );
        break;
    }
    
    assert( pMva );
    return ( SimpCubeLiteralImage ( pInfo->pMvcMem, pVm, pInfo->ddmg, i, pMva ) );
    /* NULL means full-set here */
}

/**Function********************************************************************

  Synopsis    [Return the range of two function.]

  Description [Return the range of two function. The support set contains
  disjoint functional supports, in which only two functions are left. Perform
  output cofactoring on these two functions.]

  SideEffects []
  SeeAlso     []

******************************************************************************/
Mvc_Cover_t *
SimpRangeTwo(
    Simp_Info_t *pInfo,
    Vm_VarMap_t *pVm,
    Mvc_Data_t  *pMvcData,
    int         start_index,
    var_set_t   *supset,
    sarray_t    *listFuncs )
{
    int i, flag;
    int iVar1, iVar2, iValue, count;
    Mva_Func_t  *pMva, *pFun1, *pFun2, *pCof;
    DdNode      *bFunc;
    DdManager   *mg;
    Mvc_Cover_t *lit1, *lit2;
    Mvc_Cover_t *temp, *temp2, *image;
    
    flag = -1;
    pFun1 = NULL;
    pFun2 = NULL;
    iVar1 = iVar2 = 0;
    mg = pInfo->ddmg;
    
    /* retrieve the two functions according to var_set */
    for (i=start_index; i<sarray_n(listFuncs); ++i) {
        if (!var_set_get_elt(supset, i)) continue;
        
        pMva = sarray_fetch( Mva_Func_t *, listFuncs, i);
        if (pMva == NULL) continue;
        if (flag==-1) {
            pFun1=pMva; iVar1=i; flag=i;
        } else {
            pFun2=pMva; iVar2=i;
        }
    }
    
    /* do output cofactoring of f2 wrt. f1 */
    count = Mva_FuncReadIsetNum( pFun1 );
    image = NULL;
    
    for ( iValue=0; iValue<count; ++iValue ) {
        
        /* iVar1'th var taking iValue'th value */
        bFunc = pFun1->pbFuncs[iValue];
        
        /* if this component is Null, it means this value is
           not reachable and no need to explore further */
        if ( bFunc == NULL || bFunc == Cudd_ReadLogicZero(mg) ) {
            continue;
        }
        
        lit1 = SimpCubeLiteral( pInfo->pMvcMem, pVm, iVar1, iValue );
        pCof = Mva_FuncCofactor( pFun2, bFunc );
        
        /* in case of non-constant, need to test multiple values */
        lit2 = SimpCubeLiteralImage ( pInfo->pMvcMem, pVm, mg, iVar2, pCof );
        
        if (lit2) {
            temp = Mvc_CoverBooleanAnd( pMvcData, lit1, lit2 );
            Mvc_CoverFree(lit1);
            Mvc_CoverFree(lit2);