abcUnreach.c 12.4 KB
Newer Older
Alan Mishchenko committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32
/**CFile****************************************************************

  FileName    [abcUnreach.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Network and node package.]

  Synopsis    [Computes unreachable states for small benchmarks.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - June 20, 2005.]

  Revision    [$Id: abcUnreach.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]

***********************************************************************/

#include "abc.h"

////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

static DdNode *    Abc_NtkTransitionRelation( DdManager * dd, Abc_Ntk_t * pNtk, int fVerbose );
static DdNode *    Abc_NtkInitStateAndVarMap( DdManager * dd, Abc_Ntk_t * pNtk, int fVerbose );
static DdNode *    Abc_NtkComputeUnreachable( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bRelation, DdNode * bInitial, bool fVerbose );
static Abc_Ntk_t * Abc_NtkConstructExdc     ( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUnreach );

////////////////////////////////////////////////////////////////////////
Alan Mishchenko committed
33
///                     FUNCTION DEFINITIONS                         ///
Alan Mishchenko committed
34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60
////////////////////////////////////////////////////////////////////////

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

  Synopsis    [Extracts sequential DCs of the network.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_NtkExtractSequentialDcs( Abc_Ntk_t * pNtk, bool fVerbose )
{
    int fReorder = 1;
    DdManager * dd;
    DdNode * bRelation, * bInitial, * bUnreach;

    // remove EXDC network if present
    if ( pNtk->pExdc )
    {
        Abc_NtkDelete( pNtk->pExdc );
        pNtk->pExdc = NULL; 
    }

    // compute the global BDDs of the latches
Alan Mishchenko committed
61
    dd = Abc_NtkGlobalBdds( pNtk, 10000000, 1, 1, fVerbose );    
Alan Mishchenko committed
62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89
    if ( dd == NULL )
        return 0;
    if ( fVerbose )
        printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );

    // create the transition relation (dereferenced global BDDs)
    bRelation = Abc_NtkTransitionRelation( dd, pNtk, fVerbose );              Cudd_Ref( bRelation );
    // create the initial state and the variable map
    bInitial  = Abc_NtkInitStateAndVarMap( dd, pNtk, fVerbose );              Cudd_Ref( bInitial );
    // compute the unreachable states
    bUnreach  = Abc_NtkComputeUnreachable( dd, pNtk, bRelation, bInitial, fVerbose );   Cudd_Ref( bUnreach );
    Cudd_RecursiveDeref( dd, bRelation );
    Cudd_RecursiveDeref( dd, bInitial );

    // reorder and disable reordering
    if ( fReorder )
    {
        if ( fVerbose )
            fprintf( stdout, "BDD nodes in the unreachable states before reordering %d.\n", Cudd_DagSize(bUnreach) );
        Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 1 );
        Cudd_AutodynDisable( dd );
        if ( fVerbose )
            fprintf( stdout, "BDD nodes in the unreachable states after reordering %d.\n", Cudd_DagSize(bUnreach) );
    }

    // allocate ZDD variables
    Cudd_zddVarsFromBddVars( dd, 2 );
    // create the EXDC network representing the unreachable states
Alan Mishchenko committed
90 91
    if ( pNtk->pExdc )
        Abc_NtkDelete( pNtk->pExdc );
Alan Mishchenko committed
92 93 94
    pNtk->pExdc = Abc_NtkConstructExdc( dd, pNtk, bUnreach );
    Cudd_RecursiveDeref( dd, bUnreach );
    Extra_StopManager( dd );
Alan Mishchenko committed
95
    pNtk->pManGlob = NULL;
Alan Mishchenko committed
96 97

    // make sure that everything is okay
Alan Mishchenko committed
98
    if ( !Abc_NtkCheck( pNtk->pExdc ) )
Alan Mishchenko committed
99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139
    {
        printf( "Abc_NtkExtractSequentialDcs: The network check has failed.\n" );
        Abc_NtkDelete( pNtk->pExdc );
        return 0;
    }
    return 1;
}

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

  Synopsis    [Computes the transition relation of the network.]

  Description [Assumes that the global BDDs are computed.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
DdNode * Abc_NtkTransitionRelation( DdManager * dd, Abc_Ntk_t * pNtk, int fVerbose )
{
    DdNode * bRel, * bTemp, * bProd, * bVar, * bInputs;
    Abc_Obj_t * pNode;
    int fReorder = 1;
    int i;

    // extand the BDD manager to represent NS variables
    assert( dd->size == Abc_NtkCiNum(pNtk) );
    Cudd_bddIthVar( dd, Abc_NtkCiNum(pNtk) + Abc_NtkLatchNum(pNtk) - 1 );

    // enable reordering
    if ( fReorder )
        Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
    else
        Cudd_AutodynDisable( dd );

    // compute the transition relation
    bRel = b1;   Cudd_Ref( bRel );
    Abc_NtkForEachLatch( pNtk, pNode, i )
    {
        bVar  = Cudd_bddIthVar( dd, Abc_NtkCiNum(pNtk) + i );
Alan Mishchenko committed
140 141
        bProd = Cudd_bddXnor( dd, bVar, pNtk->vFuncsGlob->pArray[i] );  Cudd_Ref( bProd );
        bRel  = Cudd_bddAnd( dd, bTemp = bRel, bProd );                 Cudd_Ref( bRel );
Alan Mishchenko committed
142 143 144 145
        Cudd_RecursiveDeref( dd, bTemp ); 
        Cudd_RecursiveDeref( dd, bProd ); 
    }
    // free the global BDDs
Alan Mishchenko committed
146
    Abc_NtkFreeGlobalBdds( pNtk );
Alan Mishchenko committed
147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194

    // quantify the PI variables
    bInputs = Extra_bddComputeRangeCube( dd, 0, Abc_NtkPiNum(pNtk) );    Cudd_Ref( bInputs );
    bRel    = Cudd_bddExistAbstract( dd, bTemp = bRel, bInputs );    Cudd_Ref( bRel );
    Cudd_RecursiveDeref( dd, bTemp ); 
    Cudd_RecursiveDeref( dd, bInputs ); 

    // reorder and disable reordering
    if ( fReorder )
    {
        if ( fVerbose )
            fprintf( stdout, "BDD nodes in the transition relation before reordering %d.\n", Cudd_DagSize(bRel) );
        Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
        Cudd_AutodynDisable( dd );
        if ( fVerbose )
            fprintf( stdout, "BDD nodes in the transition relation after reordering %d.\n", Cudd_DagSize(bRel) );
    }
    Cudd_Deref( bRel );
    return bRel;
}

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

  Synopsis    [Computes the initial state and sets up the variable map.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
DdNode * Abc_NtkInitStateAndVarMap( DdManager * dd, Abc_Ntk_t * pNtk, int fVerbose )
{
    DdNode ** pbVarsX, ** pbVarsY;
    DdNode * bTemp, * bProd, * bVar;
    Abc_Obj_t * pLatch;
    int i;

    // set the variable mapping for Cudd_bddVarMap()
    pbVarsX = ALLOC( DdNode *, dd->size );
    pbVarsY = ALLOC( DdNode *, dd->size );
    bProd = b1;         Cudd_Ref( bProd );
    Abc_NtkForEachLatch( pNtk, pLatch, i )
    {
        pbVarsX[i] = dd->vars[ Abc_NtkPiNum(pNtk) + i ];
        pbVarsY[i] = dd->vars[ Abc_NtkCiNum(pNtk) + i ];
        // get the initial value of the latch
Alan Mishchenko committed
195
        bVar  = Cudd_NotCond( pbVarsX[i], !Abc_LatchIsInit1(pLatch) );
Alan Mishchenko committed
196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286
        bProd = Cudd_bddAnd( dd, bTemp = bProd, bVar );      Cudd_Ref( bProd );
        Cudd_RecursiveDeref( dd, bTemp ); 
    }
    Cudd_SetVarMap( dd, pbVarsX, pbVarsY, Abc_NtkLatchNum(pNtk) );
    FREE( pbVarsX );
    FREE( pbVarsY );

    Cudd_Deref( bProd );
    return bProd;
}

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

  Synopsis    [Computes the set of unreachable states.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
DdNode * Abc_NtkComputeUnreachable( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bTrans, DdNode * bInitial, bool fVerbose )
{
    DdNode * bRelation, * bReached, * bCubeCs;
    DdNode * bCurrent, * bNext, * bTemp;
    int nIters;

    // perform reachability analisys
    bCurrent  = bInitial;   Cudd_Ref( bCurrent );
    bReached  = bInitial;   Cudd_Ref( bReached );
    bRelation = bTrans;     Cudd_Ref( bRelation );
    bCubeCs   = Extra_bddComputeRangeCube( dd, Abc_NtkPiNum(pNtk), Abc_NtkCiNum(pNtk) );    Cudd_Ref( bCubeCs );
    for ( nIters = 1; ; nIters++ )
    {
        // compute the next states
        bNext = Cudd_bddAndAbstract( dd, bRelation, bCurrent, bCubeCs );  Cudd_Ref( bNext );
        Cudd_RecursiveDeref( dd, bCurrent );
        // remap these states into the current state vars
        bNext = Cudd_bddVarMap( dd, bTemp = bNext );                      Cudd_Ref( bNext );
        Cudd_RecursiveDeref( dd, bTemp );
        // check if there are any new states
        if ( Cudd_bddLeq( dd, bNext, bReached ) )
            break;
        // get the new states
        bCurrent = Cudd_bddAnd( dd, bNext, Cudd_Not(bReached) );          Cudd_Ref( bCurrent );
        // minimize the new states with the reached states
//        bCurrent = Cudd_bddConstrain( dd, bTemp = bCurrent, Cudd_Not(bReached) ); Cudd_Ref( bCurrent );
//        Cudd_RecursiveDeref( dd, bTemp );
        // add to the reached states
        bReached = Cudd_bddOr( dd, bTemp = bReached, bNext );             Cudd_Ref( bReached );
        Cudd_RecursiveDeref( dd, bTemp );
        Cudd_RecursiveDeref( dd, bNext );
        // minimize the transition relation
//        bRelation = Cudd_bddConstrain( dd, bTemp = bRelation, Cudd_Not(bReached) ); Cudd_Ref( bRelation );
//        Cudd_RecursiveDeref( dd, bTemp );
    }
    Cudd_RecursiveDeref( dd, bRelation );
    Cudd_RecursiveDeref( dd, bCubeCs );
    Cudd_RecursiveDeref( dd, bNext );
    // report the stats
    if ( fVerbose )
    {
    fprintf( stdout, "Reachability analysis completed in %d iterations.\n", nIters );
    fprintf( stdout, "The number of minterms in the reachable state set = %d.\n", 
                        (int)Cudd_CountMinterm(dd, bReached, Abc_NtkLatchNum(pNtk) ) ); 
    }
//PRB( dd, bReached );
    Cudd_Deref( bReached );
    return Cudd_Not( bReached );
}

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

  Synopsis    [Creates the EXDC network.]

  Description [The set of unreachable states depends on CS variables.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUnreach )
{
    Abc_Ntk_t * pNtkNew;
    Abc_Obj_t * pNode, * pNodeNew;
    int * pPermute;
    int i;

    // start the new network
Alan Mishchenko committed
287
    pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_BDD );
Alan Mishchenko committed
288
    pNtkNew->pName = Extra_UtilStrsav( "exdc" );
Alan Mishchenko committed
289 290
    pNtkNew->pSpec = NULL;

Alan Mishchenko committed
291 292
    // create PIs corresponding to LOs
    Abc_NtkForEachLatch( pNtk, pNode, i )
Alan Mishchenko committed
293 294
        Abc_NtkLogicStoreName( pNode->pCopy = Abc_NtkCreatePi(pNtkNew), Abc_ObjName(pNode) );
    // cannot ADD POs here because pLatch->pCopy point to the PIs
Alan Mishchenko committed
295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312

    // create a new node
    pNodeNew = Abc_NtkCreateNode(pNtkNew);
    // add the fanins corresponding to latch outputs
    Abc_NtkForEachLatch( pNtk, pNode, i )
        Abc_ObjAddFanin( pNodeNew, pNode->pCopy );

    // create the logic function
    pPermute = ALLOC( int, dd->size );
    for ( i = 0; i < dd->size; i++ )
        pPermute[i] = -1;
    Abc_NtkForEachLatch( pNtk, pNode, i )
        pPermute[Abc_NtkPiNum(pNtk) + i] = i;
    // remap the functions
    pNodeNew->pData = Extra_TransferPermute( dd, pNtkNew->pManFunc, bUnreach, pPermute );   Cudd_Ref( pNodeNew->pData );
    free( pPermute );
    Abc_NodeMinimumBase( pNodeNew );

Alan Mishchenko committed
313 314 315 316
    // for each CO, create PO (skip POs equal to CIs because of name conflict)
    Abc_NtkForEachPo( pNtk, pNode, i )
        if ( !Abc_ObjIsCi(Abc_ObjFanin0(pNode)) )
            Abc_NtkLogicStoreName( pNode->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjName(pNode) );
Alan Mishchenko committed
317
    Abc_NtkForEachLatch( pNtk, pNode, i )
Alan Mishchenko committed
318 319 320
        Abc_NtkLogicStoreName( pNode->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjNameSuffix(pNode, "_in") );

    // link to the POs of the network 
Alan Mishchenko committed
321
    Abc_NtkForEachPo( pNtk, pNode, i )
Alan Mishchenko committed
322 323
        if ( !Abc_ObjIsCi(Abc_ObjFanin0(pNode)) )
            Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
Alan Mishchenko committed
324
    Abc_NtkForEachLatch( pNtk, pNode, i )
Alan Mishchenko committed
325
        Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
Alan Mishchenko committed
326

Alan Mishchenko committed
327 328
    // remove the extra nodes
    Abc_AigCleanup( pNtkNew->pManFunc );
Alan Mishchenko committed
329 330 331

    // fix the problem with complemented and duplicated CO edges
    Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
Alan Mishchenko committed
332 333

    // transform the network to the SOP representation
Alan Mishchenko committed
334 335
    if ( !Abc_NtkBddToSop( pNtkNew, 0 ) )
    {
Alan Mishchenko committed
336
        printf( "Abc_NtkConstructExdc(): Converting to SOPs has failed.\n" );
Alan Mishchenko committed
337 338
        return NULL;
    }
Alan Mishchenko committed
339 340 341 342 343 344 345 346
    return pNtkNew;
}

////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////