dchChoice.c 17.6 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
/**CFile****************************************************************

  FileName    [dchChoice.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Choice computation for tech-mapping.]

  Synopsis    [Contrustion of choices.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - June 29, 2008.]

  Revision    [$Id: dchChoice.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]

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

#include "dchInt.h"

23 24 25
ABC_NAMESPACE_IMPL_START


Alan Mishchenko committed
26 27 28 29 30 31 32 33 34 35
////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////

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

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 61 62 63 64 65
  Synopsis    [Counts support nodes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Dch_ObjCountSupp_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
{
    int Count;
    if ( Aig_ObjIsTravIdCurrent( p, pObj ) )
        return 0;
    Aig_ObjSetTravIdCurrent( p, pObj );
    if ( Aig_ObjIsCi(pObj) )
        return 1;
    assert( Aig_ObjIsNode(pObj) );
    Count  = Dch_ObjCountSupp_rec( p, Aig_ObjFanin0(pObj) );
    Count += Dch_ObjCountSupp_rec( p, Aig_ObjFanin1(pObj) );
    return Count;
}
int Dch_ObjCountSupp( Aig_Man_t * p, Aig_Obj_t * pObj )
{
    Aig_ManIncrementTravId( p );
    return Dch_ObjCountSupp_rec( p, pObj );
}

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

Alan Mishchenko committed
66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88
  Synopsis    [Counts the number of representatives.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Dch_DeriveChoiceCountReprs( Aig_Man_t * pAig )
{
    Aig_Obj_t * pObj, * pRepr;
    int i, nReprs = 0;
    Aig_ManForEachObj( pAig, pObj, i )
    {
        pRepr = Aig_ObjRepr( pAig, pObj );
        if ( pRepr == NULL )
            continue;
        assert( pRepr->Id < pObj->Id );
        nReprs++;
    }
    return nReprs;
}
89 90 91 92 93 94 95 96 97
int Dch_DeriveChoiceCountEquivs( Aig_Man_t * pAig )
{
    Aig_Obj_t * pObj, * pEquiv;
    int i, nEquivs = 0;
    Aig_ManForEachObj( pAig, pObj, i )
    {
        pEquiv = Aig_ObjEquiv( pAig, pObj );
        if ( pEquiv == NULL )
            continue;
98
        assert( pEquiv->Id < pObj->Id );
99 100 101 102
        nEquivs++;
    }
    return nEquivs;
}
Alan Mishchenko committed
103 104 105

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

106
  Synopsis    [Marks the TFI of the node.]
Alan Mishchenko committed
107

108
  Description [Returns 1 if there is a CI not marked with previous ID.]
Alan Mishchenko committed
109 110 111 112 113 114
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
115
int Dch_ObjMarkTfi_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
Alan Mishchenko committed
116
{
117 118 119 120 121 122
    int RetValue;
    if ( pObj == NULL )
        return 0;
    if ( Aig_ObjIsTravIdCurrent( p, pObj ) )
        return 0;
    if ( Aig_ObjIsCi(pObj) )
Alan Mishchenko committed
123
    {
124 125 126
        RetValue = !Aig_ObjIsTravIdPrevious( p, pObj );
        Aig_ObjSetTravIdCurrent( p, pObj );
        return RetValue;
Alan Mishchenko committed
127
    }
128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149
    assert( Aig_ObjIsNode(pObj) );
    Aig_ObjSetTravIdCurrent( p, pObj );
    RetValue  = Dch_ObjMarkTfi_rec( p, Aig_ObjFanin0(pObj) );
    RetValue += Dch_ObjMarkTfi_rec( p, Aig_ObjFanin1(pObj) );
//    RetValue += Dch_ObjMarkTfi_rec( p, Aig_ObjEquiv(p, pObj) );
    return (RetValue > 0);
}
int Dch_ObjCheckSuppRed( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr )
{
    // mark support of the representative node (pRepr)
    Aig_ManIncrementTravId( p );
    Dch_ObjMarkTfi_rec( p, pRepr );
    // detect if the new node (pObj) depends on additional variables
    Aig_ManIncrementTravId( p );
    if ( Dch_ObjMarkTfi_rec( p, pObj ) )
        return 1;//, printf( "1" );
    // detect if the representative node (pRepr) depends on additional variables
    Aig_ManIncrementTravId( p );
    if ( Dch_ObjMarkTfi_rec( p, pRepr ) )
        return 1;//, printf( "2" );
    // skip the choice if this is what is happening
    return 0;
Alan Mishchenko committed
150 151 152 153
}

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

154
  Synopsis    [Make sure reprsentative nodes do not have representatives.]
Alan Mishchenko committed
155 156 157 158 159 160 161 162

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
163
void Aig_ManCheckReprs( Aig_Man_t * p )
Alan Mishchenko committed
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
    int fPrintConst = 0;
    Aig_Obj_t * pObj;
    int i, fProb = 0;
    int Class0 = 0, ClassCi = 0;
    Aig_ManForEachObj( p, pObj, i )
    {
        if ( Aig_ObjRepr(p, pObj) == NULL )
            continue;
        if ( !Aig_ObjIsNode(pObj) )
            printf( "Obj %d is not an AND but it has a repr %d.\n", i, Aig_ObjId(Aig_ObjRepr(p, pObj)) ), fProb = 1;
        else if ( Aig_ObjRepr(p, Aig_ObjRepr(p, pObj)) )
            printf( "Obj %d has repr %d with a repr %d.\n", i, Aig_ObjId(Aig_ObjRepr(p, pObj)), Aig_ObjId(Aig_ObjRepr(p, Aig_ObjRepr(p, pObj))) ), fProb = 1;
    }
    if ( !fProb )
        printf( "Representive verification successful.\n" );
    else
        printf( "Representive verification FAILED.\n" );
    if ( !fPrintConst )
        return;
    // count how many representatives are const0 or a CI
    Aig_ManForEachObj( p, pObj, i )
    {
        if ( Aig_ObjRepr(p, pObj) == Aig_ManConst1(p) )
            Class0++;
        if ( Aig_ObjRepr(p, pObj) && Aig_ObjIsCi(Aig_ObjRepr(p, pObj)) )
            ClassCi++;
    }
    printf( "Const0 nodes = %d.  ConstCI nodes = %d.\n", Class0, ClassCi );
Alan Mishchenko committed
193 194
}

195
/**Function*************************************************************
Alan Mishchenko committed
196

197
  Synopsis    [Verify correctness of choices.]
198

199 200 201
  Description []
               
  SideEffects []
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
  SeeAlso     []

***********************************************************************/
void Dch_CheckChoices( Aig_Man_t * p, int fSkipRedSupps )
{
    Aig_Obj_t * pObj;
    int i, fProb = 0;
    Aig_ManCleanMarkA( p );
    Aig_ManForEachNode( p, pObj, i )
    {
        if ( p->pEquivs[i] != NULL )
        {
            if ( pObj->fMarkA == 1 )
                printf( "node %d participates in more than one choice class\n", i ), fProb = 1;
            pObj->fMarkA = 1;
            // check redundancy
            if ( fSkipRedSupps && Dch_ObjCheckSuppRed( p, pObj, p->pEquivs[i]) )
                printf( "node %d and repr %d have diff supports\n", pObj->Id, p->pEquivs[i]->Id );
            // consider the next one
            pObj = p->pEquivs[i];
            if ( p->pEquivs[Aig_ObjId(pObj)] == NULL )
            {
                if ( pObj->fMarkA == 1 )
                    printf( "repr %d has final node %d participates in more than one choice class\n", i, pObj->Id ), fProb = 1;
                pObj->fMarkA = 1;
            }
            // consider the non-head ones
            if ( pObj->nRefs > 0 )
                printf( "node %d belonging to choice has fanout %d\n", pObj->Id, pObj->nRefs );
        }
        if ( p->pReprs && p->pReprs[i] != NULL )
        {
            if ( pObj->nRefs > 0 )
                printf( "node %d has representative %d and fanout count %d\n", pObj->Id, p->pReprs[i]->Id, pObj->nRefs ), fProb = 1;
        }
    }
    Aig_ManCleanMarkA( p );
    if ( !fProb )
        printf( "Verification of choice AIG succeeded.\n" );
    else
        printf( "Verification of choice AIG FAILED.\n" );
}
245 246 247

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

248 249 250 251 252 253 254 255 256 257 258 259 260
  Synopsis    [Checks for combinational loops in the AIG.]

  Description [Returns 1 if combinational loop is detected.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Aig_ManCheckAcyclic_rec( Aig_Man_t * p, Aig_Obj_t * pNode, int fVerbose )
{
    Aig_Obj_t * pFanin;
    int fAcyclic;
261
    if ( Aig_ObjIsCi(pNode) || Aig_ObjIsConst1(pNode) )
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 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343
        return 1;
    assert( Aig_ObjIsNode(pNode) );
    // make sure the node is not visited
    assert( !Aig_ObjIsTravIdPrevious(p, pNode) );
    // check if the node is part of the combinational loop
    if ( Aig_ObjIsTravIdCurrent(p, pNode) )
    {
        if ( fVerbose )
            Abc_Print( 1, "Network \"%s\" contains combinational loop!\n", p->pSpec? p->pSpec : NULL );
        if ( fVerbose )
        Abc_Print( 1, "Node \"%d\" is encountered twice on the following path to the COs:\n", Aig_ObjId(pNode) );
        return 0;
    }
    // mark this node as a node on the current path
    Aig_ObjSetTravIdCurrent( p, pNode );

    // visit the transitive fanin
    pFanin = Aig_ObjFanin0(pNode);
    // check if the fanin is visited
    if ( !Aig_ObjIsTravIdPrevious(p, pFanin) ) 
    {
        // traverse the fanin's cone searching for the loop
        if ( !(fAcyclic = Aig_ManCheckAcyclic_rec(p, pFanin, fVerbose)) )
        {
            // return as soon as the loop is detected
            if ( fVerbose )
            Abc_Print( 1, " %d ->", Aig_ObjId(pFanin) );
            return 0;
        }
    }

    // visit the transitive fanin
    pFanin = Aig_ObjFanin1(pNode);
    // check if the fanin is visited
    if ( !Aig_ObjIsTravIdPrevious(p, pFanin) ) 
    {
        // traverse the fanin's cone searching for the loop
        if ( !(fAcyclic = Aig_ManCheckAcyclic_rec(p, pFanin, fVerbose)) )
        {
            // return as soon as the loop is detected
            if ( fVerbose )
            Abc_Print( 1, " %d ->", Aig_ObjId(pFanin) );
            return 0;
        }
    }

    // visit choices
    if ( Aig_ObjRepr(p, pNode) == NULL && Aig_ObjEquiv(p, pNode) != NULL )
    {
        for ( pFanin = Aig_ObjEquiv(p, pNode); pFanin; pFanin = Aig_ObjEquiv(p, pFanin) )
        {
            // check if the fanin is visited
            if ( Aig_ObjIsTravIdPrevious(p, pFanin) ) 
                continue;
            // traverse the fanin's cone searching for the loop
            if ( (fAcyclic = Aig_ManCheckAcyclic_rec(p, pFanin, fVerbose)) )
                continue;
            // return as soon as the loop is detected
            if ( fVerbose )
            Abc_Print( 1, " %d", Aig_ObjId(pFanin) );
            if ( fVerbose )
            Abc_Print( 1, " (choice of %d) -> ", Aig_ObjId(pNode) );
            return 0;
        }
    }
    // mark this node as a visited node
    Aig_ObjSetTravIdPrevious( p, pNode );
    return 1;
}
int Aig_ManCheckAcyclic( Aig_Man_t * p, int fVerbose )
{
    Aig_Obj_t * pNode;
    int fAcyclic;
    int i;
    // set the traversal ID for this DFS ordering
    Aig_ManIncrementTravId( p );   
    Aig_ManIncrementTravId( p );   
    // pNode->TravId == pNet->nTravIds      means "pNode is on the path"
    // pNode->TravId == pNet->nTravIds - 1  means "pNode is visited but is not on the path"
    // pNode->TravId <  pNet->nTravIds - 1  means "pNode is not visited"
    // traverse the network to detect cycles
    fAcyclic = 1;
344
    Aig_ManForEachCo( p, pNode, i )
345 346 347 348 349 350 351 352 353 354 355 356 357 358 359
    {
        pNode = Aig_ObjFanin0(pNode);
        if ( Aig_ObjIsTravIdPrevious(p, pNode) )
            continue;
        // traverse the output logic cone
        if ( (fAcyclic = Aig_ManCheckAcyclic_rec(p, pNode, fVerbose)) )
            continue;
        // stop as soon as the first loop is detected
        if ( fVerbose )
        Abc_Print( 1, " CO %d\n", i );
        break;
    }
    return fAcyclic;
}

360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412

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

  Synopsis    [Returns 1 if the choice node of pRepr is in the TFI of pObj.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Dch_ObjCheckTfi_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
{
    // check the trivial cases
    if ( pObj == NULL )
        return 0;
    if ( Aig_ObjIsCi(pObj) )
        return 0;
    if ( pObj->fMarkA )
        return 1;
    // skip the visited node
    if ( Aig_ObjIsTravIdCurrent( p, pObj ) )
        return 0;
    Aig_ObjSetTravIdCurrent( p, pObj );
    // check the children
    if ( Dch_ObjCheckTfi_rec( p, Aig_ObjFanin0(pObj) ) )
        return 1;
    if ( Dch_ObjCheckTfi_rec( p, Aig_ObjFanin1(pObj) ) )
        return 1;
    // check equivalent nodes
    return Dch_ObjCheckTfi_rec( p, Aig_ObjEquiv(p, pObj) );
}
int Dch_ObjCheckTfi( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr )
{
    Aig_Obj_t * pTemp;
    int RetValue;
    assert( !Aig_IsComplement(pObj) );
    assert( !Aig_IsComplement(pRepr) );
    // mark nodes of the choice node
    for ( pTemp = pRepr; pTemp; pTemp = Aig_ObjEquiv(p, pTemp) )
        pTemp->fMarkA = 1;
    // traverse the new node
    Aig_ManIncrementTravId( p );
    RetValue = Dch_ObjCheckTfi_rec( p, pObj );
    // unmark nodes of the choice node
    for ( pTemp = pRepr; pTemp; pTemp = Aig_ObjEquiv(p, pTemp) )
        pTemp->fMarkA = 0;
    return RetValue;
}

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

413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433
  Synopsis    [Returns representatives of fanin in approapriate polarity.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline Aig_Obj_t * Aig_ObjGetRepr( Aig_Man_t * p, Aig_Obj_t * pObj )
{
    Aig_Obj_t * pRepr;
    if ( (pRepr = Aig_ObjRepr(p, Aig_Regular(pObj))) )
        return Aig_NotCond( pRepr, Aig_Regular(pObj)->fPhase ^ pRepr->fPhase ^ Aig_IsComplement(pObj) );
    return pObj;
}
static inline Aig_Obj_t * Aig_ObjChild0CopyRepr( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjGetRepr( p, Aig_ObjChild0Copy(pObj) ); }
static inline Aig_Obj_t * Aig_ObjChild1CopyRepr( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjGetRepr( p, Aig_ObjChild1Copy(pObj) ); }

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

434 435 436 437 438 439 440 441 442
  Synopsis    [Derives the AIG with choices from representatives.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
443 444 445
void Dch_DeriveChoiceAigNode( Aig_Man_t * pAigNew, Aig_Man_t * pAigOld, Aig_Obj_t * pObj, int fSkipRedSupps )
{
    Aig_Obj_t * pRepr, * pObjNew, * pReprNew;
446 447 448 449 450 451 452 453 454
    assert( !Aig_IsComplement(pObj) );
    // get the representative
    pRepr = Aig_ObjRepr( pAigOld, pObj );
    if ( pRepr != NULL && (Aig_ObjIsConst1(pRepr) || Aig_ObjIsCi(pRepr)) )
    {
        assert( pRepr->pData != NULL );
        pObj->pData = Aig_NotCond( (Aig_Obj_t *)pRepr->pData, pObj->fPhase ^ pRepr->fPhase );
        return;
    }
455
    // get the new node
456
    pObjNew = Aig_And( pAigNew, 
457 458
        Aig_ObjChild0CopyRepr(pAigNew, pObj), 
        Aig_ObjChild1CopyRepr(pAigNew, pObj) );
459
    pObjNew = Aig_ObjGetRepr( pAigNew, pObjNew );
460
//    assert( Aig_ObjRepr( pAigNew, pObjNew ) == NULL );
461 462 463 464
    // assign the copy
    assert( pObj->pData == NULL );
    pObj->pData = pObjNew;
    // skip those without reprs
465 466 467
    if ( pRepr == NULL )
        return;
    assert( pRepr->Id < pObj->Id );
468
    assert( Aig_ObjIsNode(pRepr) );
469 470 471
    // get the corresponding new nodes
    pObjNew  = Aig_Regular((Aig_Obj_t *)pObj->pData);
    pReprNew = Aig_Regular((Aig_Obj_t *)pRepr->pData);
472 473
    // skip earlier nodes
    if ( pReprNew->Id >= pObjNew->Id )
474 475 476 477 478 479 480 481
        return;
    assert( pReprNew->Id < pObjNew->Id );
    // set the representatives
    Aig_ObjSetRepr( pAigNew, pObjNew, pReprNew );
    // skip used nodes
    if ( pObjNew->nRefs > 0 )
        return;
    assert( pObjNew->nRefs == 0 );
482
    // skip choices that can lead to combo loops
483 484 485
    if ( Dch_ObjCheckTfi( pAigNew, pObjNew, pReprNew ) )
        return;
    // don't add choice if structural support of pObjNew and pReprNew differ
486 487 488 489 490 491
    if ( fSkipRedSupps && Dch_ObjCheckSuppRed(pAigNew, pObjNew, pReprNew) )
        return;
    // add choice to the end of the list
    while ( pAigNew->pEquivs[pReprNew->Id] != NULL )
        pReprNew = pAigNew->pEquivs[pReprNew->Id];
    assert( pAigNew->pEquivs[pReprNew->Id] == NULL );
492 493
    pAigNew->pEquivs[pReprNew->Id] = pObjNew;
}
494
Aig_Man_t * Dch_DeriveChoiceAigInt( Aig_Man_t * pAig, int fSkipRedSupps )
495 496 497 498 499 500 501 502 503 504 505
{
    Aig_Man_t * pChoices;
    Aig_Obj_t * pObj;
    int i;
    // start recording equivalences
    pChoices = Aig_ManStart( Aig_ManObjNumMax(pAig) );
    pChoices->pEquivs = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) );
    pChoices->pReprs  = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) );
    // map constants and PIs
    Aig_ManCleanData( pAig );
    Aig_ManConst1(pAig)->pData = Aig_ManConst1(pChoices);
506 507
    Aig_ManForEachCi( pAig, pObj, i )
        pObj->pData = Aig_ObjCreateCi( pChoices );
508 509
    // construct choices for the internal nodes
    assert( pAig->pReprs != NULL );
510
    Aig_ManForEachNode( pAig, pObj, i ) 
511
        Dch_DeriveChoiceAigNode( pChoices, pAig, pObj, fSkipRedSupps );
512 513
    Aig_ManForEachCo( pAig, pObj, i )
        Aig_ObjCreateCo( pChoices, Aig_ObjChild0CopyRepr(pChoices, pObj) );
514
    Aig_ManSetRegNum( pChoices, Aig_ManRegNum(pAig) );
515 516
    return pChoices;
}
517
Aig_Man_t * Dch_DeriveChoiceAig( Aig_Man_t * pAig, int fSkipRedSupps )
518
{
519
    int fCheck = 0;
520
    Aig_Man_t * pChoices, * pTemp;
521 522 523 524
    // verify
    if ( fCheck )
        Aig_ManCheckReprs( pAig ); 
    // compute choices
525
    pChoices = Dch_DeriveChoiceAigInt( pAig, fSkipRedSupps );
526
    ABC_FREE( pChoices->pReprs );
527 528 529 530
    // verify
    if ( fCheck )
        Dch_CheckChoices( pChoices, fSkipRedSupps ); 
    // find correct topo order with choices
531 532
    pChoices = Aig_ManDupDfs( pTemp = pChoices );
    Aig_ManStop( pTemp );
533 534 535
    // verify
    if ( fCheck )
        Dch_CheckChoices( pChoices, fSkipRedSupps ); 
536 537 538
    return pChoices;
}

Alan Mishchenko committed
539 540 541 542 543
////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////


544 545
ABC_NAMESPACE_IMPL_END