abcFraig.c 27.2 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
/**CFile****************************************************************

  FileName    [abcFraig.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Network and node package.]

  Synopsis    [Procedures interfacing with the FRAIG package.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

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

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

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

21 22 23
#include "base/abc/abc.h"
#include "proof/fraig/fraig.h"
#include "base/main/main.h"
Alan Mishchenko committed
24

25 26 27
ABC_NAMESPACE_IMPL_START


Alan Mishchenko committed
28 29 30 31
////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

Alan Mishchenko committed
32 33 34 35 36 37 38 39 40 41
extern Abc_Ntk_t *    Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk );
static Abc_Ntk_t *    Abc_NtkFromFraig2( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk );
static Abc_Obj_t *    Abc_NodeFromFraig_rec( Abc_Ntk_t * pNtkNew, Fraig_Node_t * pNodeFraig );
static void           Abc_NtkFromFraig2_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, Vec_Ptr_t * vNodeReprs );
extern Fraig_Node_t * Abc_NtkToFraigExdc( Fraig_Man_t * pMan, Abc_Ntk_t * pNtkMain, Abc_Ntk_t * pNtkExdc );
static void           Abc_NtkFraigRemapUsingExdc( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk );

static int            Abc_NtkFraigTrustCheck( Abc_Ntk_t * pNtk );
static void           Abc_NtkFraigTrustOne( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
static Abc_Obj_t *    Abc_NodeFraigTrust( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode );
Alan Mishchenko committed
42 43
 
////////////////////////////////////////////////////////////////////////
Alan Mishchenko committed
44
///                     FUNCTION DEFINITIONS                         ///
Alan Mishchenko committed
45 46 47 48 49 50 51 52 53 54 55 56 57
////////////////////////////////////////////////////////////////////////

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

  Synopsis    [Interfaces the network with the FRAIG package.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
58
Abc_Ntk_t * Abc_NtkFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes, int fExdc )
Alan Mishchenko committed
59
{
60
    Fraig_Params_t * pPars = (Fraig_Params_t *)pParams;
Alan Mishchenko committed
61
    Abc_Ntk_t * pNtkNew;
Alan Mishchenko committed
62 63 64 65
    Fraig_Man_t * pMan; 
    // check if EXDC is present
    if ( fExdc && pNtk->pExdc == NULL )
        fExdc = 0, printf( "Warning: Networks has no EXDC.\n" );
Alan Mishchenko committed
66
    // perform fraiging
67
    pMan = (Fraig_Man_t *)Abc_NtkToFraig( pNtk, pParams, fAllNodes, fExdc ); 
Alan Mishchenko committed
68 69 70
    // add algebraic choices
//    if ( pPars->fChoicing )
//        Fraig_ManAddChoices( pMan, 0, 6 );
Alan Mishchenko committed
71
    // prove the miter if asked to
Alan Mishchenko committed
72
    if ( pPars->fTryProve )
Alan Mishchenko committed
73 74
        Fraig_ManProveMiter( pMan );
    // reconstruct FRAIG in the new network
Alan Mishchenko committed
75 76 77 78
    if ( fExdc ) 
        pNtkNew = Abc_NtkFromFraig2( pMan, pNtk );
    else
        pNtkNew = Abc_NtkFromFraig( pMan, pNtk );
Alan Mishchenko committed
79
    Fraig_ManFree( pMan );
Alan Mishchenko committed
80 81
    if ( pNtk->pExdc )
        pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
Alan Mishchenko committed
82
    // make sure that everything is okay
Alan Mishchenko committed
83
    if ( !Abc_NtkCheck( pNtkNew ) )
Alan Mishchenko committed
84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102
    {
        printf( "Abc_NtkFraig: The network check has failed.\n" );
        Abc_NtkDelete( pNtkNew );
        return NULL;
    }
    return pNtkNew;
}

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

  Synopsis    [Transforms the strashed network into FRAIG.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
103
void * Abc_NtkToFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes, int fExdc )
Alan Mishchenko committed
104
{
Alan Mishchenko committed
105
    int fInternal = ((Fraig_Params_t *)pParams)->fInternal;
Alan Mishchenko committed
106
    Fraig_Man_t * pMan;
Alan Mishchenko committed
107
    ProgressBar * pProgress = NULL;
Alan Mishchenko committed
108
    Vec_Ptr_t * vNodes;
Alan Mishchenko committed
109
    Abc_Obj_t * pNode;
Alan Mishchenko committed
110 111
    int i;

Alan Mishchenko committed
112
    assert( Abc_NtkIsStrash(pNtk) );
Alan Mishchenko committed
113 114

    // create the FRAIG manager
115
    pMan = Fraig_ManCreate( (Fraig_Params_t *)pParams );
Alan Mishchenko committed
116

Alan Mishchenko committed
117
    // map the constant node
Alan Mishchenko committed
118
    Abc_NtkCleanCopy( pNtk );
Alan Mishchenko committed
119 120
    Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Fraig_ManReadConst1(pMan);
    // create PIs and remember them in the old nodes
Alan Mishchenko committed
121 122
    Abc_NtkForEachCi( pNtk, pNode, i )
        pNode->pCopy = (Abc_Obj_t *)Fraig_ManReadIthVar(pMan, i);
Alan Mishchenko committed
123
 
Alan Mishchenko committed
124
    // perform strashing
Alan Mishchenko committed
125
    vNodes = Abc_AigDfs( pNtk, fAllNodes, 0 );
Alan Mishchenko committed
126
    if ( !fInternal )
Alan Mishchenko committed
127
        pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize );
128
    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
Alan Mishchenko committed
129
    {
Alan Mishchenko committed
130
        if ( Abc_ObjFaninNum(pNode) == 0 )
Alan Mishchenko committed
131
            continue;
132
        if ( pProgress ) 
Alan Mishchenko committed
133 134
            Extra_ProgressBarUpdate( pProgress, i, NULL );
        pNode->pCopy = (Abc_Obj_t *)Fraig_NodeAnd( pMan, 
135 136
                Fraig_NotCond( Abc_ObjFanin0(pNode)->pCopy, (int)Abc_ObjFaninC0(pNode) ),
                Fraig_NotCond( Abc_ObjFanin1(pNode)->pCopy, (int)Abc_ObjFaninC1(pNode) ) );
Alan Mishchenko committed
137
    }
138
    if ( pProgress )
Alan Mishchenko committed
139
        Extra_ProgressBarStop( pProgress );
Alan Mishchenko committed
140 141
    Vec_PtrFree( vNodes );

Alan Mishchenko committed
142 143 144 145
    // use EXDC to change the mapping of nodes into FRAIG nodes
    if ( fExdc )
        Abc_NtkFraigRemapUsingExdc( pMan, pNtk );

Alan Mishchenko committed
146 147
    // set the primary outputs
    Abc_NtkForEachCo( pNtk, pNode, i )
Alan Mishchenko committed
148
        Fraig_ManSetPo( pMan, (Fraig_Node_t *)Abc_ObjNotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ) );
Alan Mishchenko committed
149 150 151 152 153
    return pMan;
}

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

Alan Mishchenko committed
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
  Synopsis    [Derives EXDC node for the given network.]

  Description [Assumes that EXDCs of all POs are the same.
  Returns the EXDC of the first PO.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Fraig_Node_t * Abc_NtkToFraigExdc( Fraig_Man_t * pMan, Abc_Ntk_t * pNtkMain, Abc_Ntk_t * pNtkExdc )
{
    Abc_Ntk_t * pNtkStrash;
    Abc_Obj_t * pObj;
    Fraig_Node_t * gResult;
    char ** ppNames;
    int i, k;
    // strash the EXDC network
    pNtkStrash = Abc_NtkStrash( pNtkExdc, 0, 0, 0 );
    Abc_NtkCleanCopy( pNtkStrash );
    Abc_AigConst1(pNtkStrash)->pCopy = (Abc_Obj_t *)Fraig_ManReadConst1(pMan);
    // set the mapping of the PI nodes
    ppNames = Abc_NtkCollectCioNames( pNtkMain, 0 );
    Abc_NtkForEachCi( pNtkStrash, pObj, i )
    {
        for ( k = 0; k < Abc_NtkCiNum(pNtkMain); k++ )
            if ( strcmp( Abc_ObjName(pObj), ppNames[k] ) == 0 )
            {
                pObj->pCopy = (Abc_Obj_t *)Fraig_ManReadIthVar(pMan, k);
                break;
            }
        assert( pObj->pCopy != NULL );
    }
Alan Mishchenko committed
187
    ABC_FREE( ppNames );
Alan Mishchenko committed
188 189 190
    // build FRAIG for each node
    Abc_AigForEachAnd( pNtkStrash, pObj, i )
        pObj->pCopy = (Abc_Obj_t *)Fraig_NodeAnd( pMan, 
191 192
                Fraig_NotCond( Abc_ObjFanin0(pObj)->pCopy, (int)Abc_ObjFaninC0(pObj) ),
                Fraig_NotCond( Abc_ObjFanin1(pObj)->pCopy, (int)Abc_ObjFaninC1(pObj) ) );
Alan Mishchenko committed
193 194
    // get the EXDC to be returned
    pObj = Abc_NtkPo( pNtkStrash, 0 );
195
    gResult = Fraig_NotCond( Abc_ObjFanin0(pObj)->pCopy, (int)Abc_ObjFaninC0(pObj) );
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
    Abc_NtkDelete( pNtkStrash );
    return gResult;
}


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

  Synopsis    [Changes mapping of the old nodes into FRAIG nodes using EXDC.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_NtkFraigRemapUsingExdc( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk )
{
    Fraig_Node_t * gNodeNew, * gNodeExdc;
    stmm_table * tTable;
    stmm_generator * gen;
    Abc_Obj_t * pNode, * pNodeBest;
    Abc_Obj_t * pClass, ** ppSlot;
    Vec_Ptr_t * vNexts;
    int i;

    // get the global don't-cares
    assert( pNtk->pExdc );
    gNodeExdc = Abc_NtkToFraigExdc( pMan, pNtk, pNtk->pExdc );

    // save the next pointers
    vNexts = Vec_PtrStart( Abc_NtkObjNumMax(pNtk) );
    Abc_NtkForEachNode( pNtk, pNode, i )
        Vec_PtrWriteEntry( vNexts, pNode->Id, pNode->pNext );

    // find the classes of AIG nodes which have FRAIG nodes assigned
    Abc_NtkCleanNext( pNtk );
    tTable = stmm_init_table(stmm_ptrcmp,stmm_ptrhash);
    Abc_NtkForEachNode( pNtk, pNode, i )
        if ( pNode->pCopy )
        {
            gNodeNew = Fraig_NodeAnd( pMan, (Fraig_Node_t *)pNode->pCopy, Fraig_Not(gNodeExdc) );
            if ( !stmm_find_or_add( tTable, (char *)Fraig_Regular(gNodeNew), (char ***)&ppSlot ) )
                *ppSlot = NULL;
            pNode->pNext = *ppSlot;
            *ppSlot = pNode;
        }

    // for reach non-trival class, find the node with minimum level, and replace other nodes by it
    Abc_AigSetNodePhases( pNtk );
    stmm_foreach_item( tTable, gen, (char **)&gNodeNew, (char **)&pClass )
    {
        if ( pClass->pNext == NULL )
            continue;
        // find the node with minimum level
        pNodeBest = pClass;
        for ( pNode = pClass->pNext; pNode; pNode = pNode->pNext )
            if ( pNodeBest->Level > pNode->Level )
                 pNodeBest = pNode;
        // remap the class nodes
        for ( pNode = pClass; pNode; pNode = pNode->pNext )
            pNode->pCopy = Abc_ObjNotCond( pNodeBest->pCopy, pNode->fPhase ^ pNodeBest->fPhase );
    }
    stmm_free_table( tTable );

    // restore the next pointers
    Abc_NtkCleanNext( pNtk );
    Abc_NtkForEachNode( pNtk, pNode, i )
264
        pNode->pNext = (Abc_Obj_t *)Vec_PtrEntry( vNexts, pNode->Id );
Alan Mishchenko committed
265 266 267 268 269 270
    Vec_PtrFree( vNexts );
}

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

  Synopsis    [Transforms FRAIG into strashed network with choices.]
Alan Mishchenko committed
271 272 273 274 275 276 277 278 279 280

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Abc_Ntk_t * Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk )
{
Alan Mishchenko committed
281
    ProgressBar * pProgress;
Alan Mishchenko committed
282
    Abc_Ntk_t * pNtkNew;
Alan Mishchenko committed
283
    Abc_Obj_t * pNode, * pNodeNew;
Alan Mishchenko committed
284 285
    int i;
    // create the new network
Alan Mishchenko committed
286
    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
Alan Mishchenko committed
287 288 289 290
    // make the mapper point to the new network
    Abc_NtkForEachCi( pNtk, pNode, i )
        Fraig_NodeSetData1( Fraig_ManReadIthVar(pMan, i), (Fraig_Node_t *)pNode->pCopy );
    // set the constant node
Alan Mishchenko committed
291
    Fraig_NodeSetData1( Fraig_ManReadConst1(pMan), (Fraig_Node_t *)Abc_AigConst1(pNtkNew) );
Alan Mishchenko committed
292
    // process the nodes in topological order
Alan Mishchenko committed
293
    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) );
Alan Mishchenko committed
294 295
    Abc_NtkForEachCo( pNtk, pNode, i )
    {
Alan Mishchenko committed
296
        Extra_ProgressBarUpdate( pProgress, i, NULL );
Alan Mishchenko committed
297 298
        pNodeNew = Abc_NodeFromFraig_rec( pNtkNew, Fraig_ManReadOutputs(pMan)[i] );
        Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
Alan Mishchenko committed
299
    }
Alan Mishchenko committed
300 301
    Extra_ProgressBarStop( pProgress );
    Abc_NtkReassignIds( pNtkNew );
Alan Mishchenko committed
302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321
    return pNtkNew;
}

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

  Synopsis    [Transforms into AIG one node.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Abc_Obj_t * Abc_NodeFromFraig_rec( Abc_Ntk_t * pNtkNew, Fraig_Node_t * pNodeFraig )
{
    Abc_Obj_t * pRes, * pRes0, * pRes1, * pResMin, * pResCur;
    Fraig_Node_t * pNodeTemp, * pNodeFraigR = Fraig_Regular(pNodeFraig);
    void ** ppTail;
    // check if the node was already considered
Alan Mishchenko committed
322
    if ( (pRes = (Abc_Obj_t *)Fraig_NodeReadData1(pNodeFraigR)) )
Alan Mishchenko committed
323 324 325 326 327
        return Abc_ObjNotCond( pRes, Fraig_IsComplement(pNodeFraig) );
    // solve the children
    pRes0 = Abc_NodeFromFraig_rec( pNtkNew, Fraig_NodeReadOne(pNodeFraigR) );
    pRes1 = Abc_NodeFromFraig_rec( pNtkNew, Fraig_NodeReadTwo(pNodeFraigR) );
    // derive the new node
328
    pRes = Abc_AigAnd( (Abc_Aig_t *)pNtkNew->pManFunc, pRes0, pRes1 );
Alan Mishchenko committed
329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367
    pRes->fPhase = Fraig_NodeReadSimInv( pNodeFraigR );
    // if the node has an equivalence class, find its representative
    if ( Fraig_NodeReadRepr(pNodeFraigR) == NULL && Fraig_NodeReadNextE(pNodeFraigR) != NULL )
    {
        // go through the FRAIG nodes belonging to this equivalence class
        // and find the representative node (the node with the smallest level)
        pResMin = pRes;
        for ( pNodeTemp = Fraig_NodeReadNextE(pNodeFraigR); pNodeTemp; pNodeTemp = Fraig_NodeReadNextE(pNodeTemp) )
        {
            assert( Fraig_NodeReadData1(pNodeTemp) == NULL );
            pResCur = Abc_NodeFromFraig_rec( pNtkNew, pNodeTemp );
            if ( pResMin->Level > pResCur->Level )
                pResMin = pResCur;
        }
        // link the nodes in such a way that representative goes first
        ppTail = &pResMin->pData;
        if ( pRes != pResMin )
        {
            *ppTail = pRes;
            ppTail = &pRes->pData;
        }
        for ( pNodeTemp = Fraig_NodeReadNextE(pNodeFraigR); pNodeTemp; pNodeTemp = Fraig_NodeReadNextE(pNodeTemp) )
        {
            pResCur = (Abc_Obj_t *)Fraig_NodeReadData1(pNodeTemp);
            assert( pResCur );
            if ( pResMin == pResCur )
                continue;
            *ppTail = pResCur;
            ppTail = &pResCur->pData;
        }
        assert( *ppTail == NULL );

        // update the phase of the node
        pRes = Abc_ObjNotCond( pResMin, (pRes->fPhase ^ pResMin->fPhase) );
    }
    Fraig_NodeSetData1( pNodeFraigR, (Fraig_Node_t *)pRes );
    return Abc_ObjNotCond( pRes, Fraig_IsComplement(pNodeFraig) );
}

Alan Mishchenko committed
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 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460
/**Function*************************************************************

  Synopsis    [Transforms FRAIG into strashed network without choices.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Abc_Ntk_t * Abc_NtkFromFraig2( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk )
{
    ProgressBar * pProgress;
    stmm_table * tTable;
    Vec_Ptr_t * vNodeReprs;
    Abc_Ntk_t * pNtkNew;
    Abc_Obj_t * pNode, * pRepr, ** ppSlot;
    int i;

    // map the nodes into their lowest level representives
    tTable = stmm_init_table(stmm_ptrcmp,stmm_ptrhash);
    pNode = Abc_AigConst1(pNtk);
    if ( !stmm_find_or_add( tTable, (char *)Fraig_Regular(pNode->pCopy), (char ***)&ppSlot ) )
        *ppSlot = pNode;
    Abc_NtkForEachCi( pNtk, pNode, i )
        if ( !stmm_find_or_add( tTable, (char *)Fraig_Regular(pNode->pCopy), (char ***)&ppSlot ) )
            *ppSlot = pNode;
    Abc_NtkForEachNode( pNtk, pNode, i )
        if ( pNode->pCopy )
        {
            if ( !stmm_find_or_add( tTable, (char *)Fraig_Regular(pNode->pCopy), (char ***)&ppSlot ) )
                *ppSlot = pNode;
            else if ( (*ppSlot)->Level > pNode->Level )
                *ppSlot = pNode;
        }
    // save representatives for each node
    vNodeReprs = Vec_PtrStart( Abc_NtkObjNumMax(pNtk) );
    Abc_NtkForEachNode( pNtk, pNode, i )
        if ( pNode->pCopy )
        {           
            if ( !stmm_lookup( tTable, (char *)Fraig_Regular(pNode->pCopy), (char **)&pRepr ) )
                assert( 0 );
            if ( pNode != pRepr )
                Vec_PtrWriteEntry( vNodeReprs, pNode->Id, pRepr );
        }
    stmm_free_table( tTable );

    // create the new network
    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );

    // perform strashing
    Abc_AigSetNodePhases( pNtk );
    Abc_NtkIncrementTravId( pNtk );
    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) );
    Abc_NtkForEachCo( pNtk, pNode, i )
    {
        Extra_ProgressBarUpdate( pProgress, i, NULL );
        Abc_NtkFromFraig2_rec( pNtkNew, Abc_ObjFanin0(pNode), vNodeReprs );
    }
    Extra_ProgressBarStop( pProgress );
    Vec_PtrFree( vNodeReprs );

    // finalize the network
    Abc_NtkFinalize( pNtk, pNtkNew );
    return pNtkNew;
}


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

  Synopsis    [Transforms into AIG one node.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_NtkFromFraig2_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, Vec_Ptr_t * vNodeReprs )
{
    Abc_Obj_t * pRepr;
    // skip the PIs and constants
    if ( Abc_ObjFaninNum(pNode) < 2 )
        return;
    // if this node is already visited, skip
    if ( Abc_NodeIsTravIdCurrent( pNode ) )
        return;
    // mark the node as visited
    Abc_NodeSetTravIdCurrent( pNode );
    assert( Abc_ObjIsNode( pNode ) );
    // get the node's representative
461
    if ( (pRepr = (Abc_Obj_t *)Vec_PtrEntry(vNodeReprs, pNode->Id)) )
Alan Mishchenko committed
462 463 464 465 466 467 468
    {
        Abc_NtkFromFraig2_rec( pNtkNew, pRepr, vNodeReprs );
        pNode->pCopy = Abc_ObjNotCond( pRepr->pCopy, pRepr->fPhase ^ pNode->fPhase );
        return;
    }
    Abc_NtkFromFraig2_rec( pNtkNew, Abc_ObjFanin0(pNode), vNodeReprs );
    Abc_NtkFromFraig2_rec( pNtkNew, Abc_ObjFanin1(pNode), vNodeReprs );
469
    pNode->pCopy = Abc_AigAnd( (Abc_Aig_t *)pNtkNew->pManFunc, Abc_ObjChild0Copy(pNode), Abc_ObjChild1Copy(pNode) );
Alan Mishchenko committed
470
}
Alan Mishchenko committed
471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488



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

  Synopsis    [Interfaces the network with the FRAIG package.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Abc_Ntk_t * Abc_NtkFraigTrust( Abc_Ntk_t * pNtk )
{
    Abc_Ntk_t * pNtkNew;

Alan Mishchenko committed
489
    if ( !Abc_NtkIsSopLogic(pNtk) )
Alan Mishchenko committed
490 491 492 493 494 495 496 497 498 499 500 501
    {
        printf( "Abc_NtkFraigTrust: Trust mode works for netlists and logic SOP networks.\n" );
        return NULL;
    }

    if ( !Abc_NtkFraigTrustCheck(pNtk) )
    {
        printf( "Abc_NtkFraigTrust: The network does not look like an AIG with choice nodes.\n" );
        return NULL;
    }
    
    // perform strashing
Alan Mishchenko committed
502
    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
Alan Mishchenko committed
503 504
    Abc_NtkFraigTrustOne( pNtk, pNtkNew );
    Abc_NtkFinalize( pNtk, pNtkNew );
Alan Mishchenko committed
505
    Abc_NtkReassignIds( pNtkNew );
Alan Mishchenko committed
506 507

    // print a warning about choice nodes
Alan Mishchenko committed
508
    printf( "Warning: The resulting AIG contains %d choice nodes.\n", Abc_NtkGetChoiceNum( pNtkNew ) );
Alan Mishchenko committed
509 510

    // make sure that everything is okay
Alan Mishchenko committed
511
    if ( !Abc_NtkCheck( pNtkNew ) )
Alan Mishchenko committed
512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539
    {
        printf( "Abc_NtkFraigTrust: The network check has failed.\n" );
        Abc_NtkDelete( pNtkNew );
        return NULL;
    }
    return pNtkNew;
}

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

  Synopsis    [Checks whether the node can be processed in the trust mode.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_NtkFraigTrustCheck( Abc_Ntk_t * pNtk )
{
    Abc_Obj_t * pNode;
    int i, nFanins;
    Abc_NtkForEachNode( pNtk, pNode, i )
    {
        nFanins = Abc_ObjFaninNum(pNode);
        if ( nFanins < 2 )
            continue;
540
        if ( nFanins == 2 && Abc_SopIsAndType((char *)pNode->pData) )
Alan Mishchenko committed
541
            continue;
542
        if ( !Abc_SopIsOrType((char *)pNode->pData) )
Alan Mishchenko committed
543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566
            return 0;
    }
    return 1;
}

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

  Synopsis    [Interfaces the network with the FRAIG package.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_NtkFraigTrustOne( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
{
    ProgressBar * pProgress;
    Vec_Ptr_t * vNodes;
    Abc_Obj_t * pNode, * pNodeNew, * pObj;
    int i;

    // perform strashing
Alan Mishchenko committed
567
    vNodes = Abc_NtkDfs( pNtk, 0 );
Alan Mishchenko committed
568
    pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize );
569
    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
Alan Mishchenko committed
570 571 572 573 574
    {
        Extra_ProgressBarUpdate( pProgress, i, NULL );
        // get the node
        assert( Abc_ObjIsNode(pNode) );
         // strash the node
Alan Mishchenko committed
575
        pNodeNew = Abc_NodeFraigTrust( pNtkNew, pNode );
Alan Mishchenko committed
576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600
        // get the old object
        if ( Abc_NtkIsNetlist(pNtk) )
            pObj = Abc_ObjFanout0( pNode ); // the fanout net 
        else 
            pObj = pNode; // the node itself
        // make sure the node is not yet strashed
        assert( pObj->pCopy == NULL );
        // mark the old object with the new AIG node
        pObj->pCopy = pNodeNew;
    }
    Vec_PtrFree( vNodes );
    Extra_ProgressBarStop( pProgress );
}

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

  Synopsis    [Transforms one node into a FRAIG in the trust mode.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
601
Abc_Obj_t * Abc_NodeFraigTrust( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode )
Alan Mishchenko committed
602 603 604 605 606 607 608 609
{
    Abc_Obj_t * pSum, * pFanin;
    void ** ppTail;
    int i, nFanins, fCompl;

    assert( Abc_ObjIsNode(pNode) );
    // get the number of node's fanins
    nFanins = Abc_ObjFaninNum( pNode );
610
    assert( nFanins == Abc_SopGetVarNum((char *)pNode->pData) );
Alan Mishchenko committed
611 612
    // check if it is a constant
    if ( nFanins == 0 )
613
        return Abc_ObjNotCond( Abc_AigConst1(pNtkNew), Abc_SopIsConst0((char *)pNode->pData) );
Alan Mishchenko committed
614
    if ( nFanins == 1 )
615 616 617 618 619 620 621
        return Abc_ObjNotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_SopIsInv((char *)pNode->pData) );
    if ( nFanins == 2 && Abc_SopIsAndType((char *)pNode->pData) )
        return Abc_AigAnd( (Abc_Aig_t *)pNtkNew->pManFunc, 
            Abc_ObjNotCond( Abc_ObjFanin0(pNode)->pCopy, !Abc_SopGetIthCareLit((char *)pNode->pData,0) ),
            Abc_ObjNotCond( Abc_ObjFanin1(pNode)->pCopy, !Abc_SopGetIthCareLit((char *)pNode->pData,1) )  );
    assert( Abc_SopIsOrType((char *)pNode->pData) );
    fCompl = Abc_SopGetIthCareLit((char *)pNode->pData,0);
Alan Mishchenko committed
622 623 624 625 626 627 628 629 630 631 632
    // get the root of the choice node (the first fanin)
    pSum = Abc_ObjFanin0(pNode)->pCopy;
    // connect other fanins
    ppTail = &pSum->pData;
    Abc_ObjForEachFanin( pNode, pFanin, i )
    {
        if ( i == 0 )
            continue;
        *ppTail = pFanin->pCopy;
        ppTail = &pFanin->pCopy->pData;
        // set the complemented bit of this cut
633
        if ( fCompl ^ Abc_SopGetIthCareLit((char *)pNode->pData, i) )
Alan Mishchenko committed
634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653
            pFanin->pCopy->fPhase = 1;
    }
    assert( *ppTail == NULL );
    return pSum;
}




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

  Synopsis    [Interfaces the network with the FRAIG package.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
654
int Abc_NtkFraigStore( Abc_Ntk_t * pNtkAdd )
Alan Mishchenko committed
655
{
Alan Mishchenko committed
656 657 658 659 660
    Vec_Ptr_t * vStore;
    Abc_Ntk_t * pNtk;
    // create the network to be stored
    pNtk = Abc_NtkStrash( pNtkAdd, 0, 0, 0 );
    if ( pNtk == NULL )
Alan Mishchenko committed
661
    {
Alan Mishchenko committed
662
        printf( "Abc_NtkFraigStore: Initial strashing has failed.\n" );
Alan Mishchenko committed
663 664 665
        return 0;
    }
    // get the network currently stored
Alan Mishchenko committed
666 667
    vStore = Abc_FrameReadStore();
    if ( Vec_PtrSize(vStore) > 0 )
Alan Mishchenko committed
668
    {
Alan Mishchenko committed
669 670
        // check that the networks have the same PIs
        // reorder PIs of pNtk2 according to pNtk1
671
        if ( !Abc_NtkCompareSignals( pNtk, (Abc_Ntk_t *)Vec_PtrEntry(vStore, 0), 1, 1 ) )
Alan Mishchenko committed
672
        {
Alan Mishchenko committed
673 674 675
            printf( "Trying to store the network with different primary inputs.\n" );
            printf( "The previously stored networks are deleted and this one is added.\n" );
            Abc_NtkFraigStoreClean();
Alan Mishchenko committed
676 677
        }
    }
Alan Mishchenko committed
678 679
    Vec_PtrPush( vStore, pNtk );
//    printf( "The number of AIG nodes added to storage = %5d.\n", Abc_NtkNodeNum(pNtk) );
Alan Mishchenko committed
680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695
    return 1;
}

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

  Synopsis    [Interfaces the network with the FRAIG package.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Abc_Ntk_t * Abc_NtkFraigRestore()
{
Alan Mishchenko committed
696
    extern Abc_Ntk_t * Abc_NtkFraigPartitioned( Vec_Ptr_t * vStore, void * pParams );
Alan Mishchenko committed
697
    Fraig_Params_t Params;
Alan Mishchenko committed
698 699
    Vec_Ptr_t * vStore;
    Abc_Ntk_t * pNtk, * pFraig;
Alan Mishchenko committed
700
    int nWords1, nWords2, nWordsMin;
701
//    abctime clk = Abc_Clock();
Alan Mishchenko committed
702 703

    // get the stored network
Alan Mishchenko committed
704 705
    vStore = Abc_FrameReadStore();
    if ( Vec_PtrSize(vStore) == 0 )
Alan Mishchenko committed
706 707 708 709
    {
        printf( "There are no network currently in storage.\n" );
        return NULL;
    }
Alan Mishchenko committed
710
//    printf( "Currently stored %d networks will be fraiged.\n", Vec_PtrSize(vStore) );
711
    pNtk = (Abc_Ntk_t *)Vec_PtrEntry( vStore, 0 );
Alan Mishchenko committed
712 713 714

    // swap the first and last network
    // this should lead to the primary choice being "better" because of synthesis
715 716 717 718 719 720
    if ( Vec_PtrSize(vStore) > 1 )
    {
        pNtk = (Abc_Ntk_t *)Vec_PtrPop( vStore );
        Vec_PtrPush( vStore, Vec_PtrEntry(vStore,0) );
        Vec_PtrWriteEntry( vStore, 0, pNtk );
    }
Alan Mishchenko committed
721

Alan Mishchenko committed
722 723 724 725 726
    // to determine the number of simulation patterns
    // use the following strategy
    // at least 64 words (32 words random and 32 words dynamic)
    // no more than 256M for one circuit (128M + 128M)
    nWords1 = 32;
Alan Mishchenko committed
727
    nWords2 = (1<<27) / (Abc_NtkNodeNum(pNtk) + Abc_NtkCiNum(pNtk));
728
    nWordsMin = Abc_MinInt( nWords1, nWords2 );
Alan Mishchenko committed
729 730 731

    // set parameters for fraiging
    Fraig_ParamsSetDefault( &Params );
Alan Mishchenko committed
732 733 734 735 736 737 738 739 740
    Params.nPatsRand  = nWordsMin * 32;    // the number of words of random simulation info
    Params.nPatsDyna  = nWordsMin * 32;    // the number of words of dynamic simulation info
    Params.nBTLimit   = 1000;              // the max number of backtracks to perform
    Params.fFuncRed   =    1;              // performs only one level hashing
    Params.fFeedBack  =    1;              // enables solver feedback
    Params.fDist1Pats =    1;              // enables distance-1 patterns
    Params.fDoSparse  =    1;              // performs equiv tests for sparse functions 
    Params.fChoicing  =    1;              // enables recording structural choices
    Params.fTryProve  =    0;              // tries to solve the final miter
Alan Mishchenko committed
741
    Params.fInternal  =    1;              // does not show progress bar
Alan Mishchenko committed
742 743 744 745 746
    Params.fVerbose   =    0;              // the verbosiness flag

    // perform partitioned computation of structural choices
    pFraig = Abc_NtkFraigPartitioned( vStore, &Params );
    Abc_NtkFraigStoreClean();
747
//ABC_PRT( "Total choicing time", Abc_Clock() - clk );
Alan Mishchenko committed
748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763
    return pFraig;
}

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

  Synopsis    [Interfaces the network with the FRAIG package.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_NtkFraigStoreClean()
{
Alan Mishchenko committed
764 765 766 767
    Vec_Ptr_t * vStore;
    Abc_Ntk_t * pNtk;
    int i;
    vStore = Abc_FrameReadStore();
768
    Vec_PtrForEachEntry( Abc_Ntk_t *, vStore, pNtk, i )
Alan Mishchenko committed
769 770
        Abc_NtkDelete( pNtk );
    Vec_PtrClear( vStore );
Alan Mishchenko committed
771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790
}

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

  Synopsis    [Checks the correctness of stored networks.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_NtkFraigStoreCheck( Abc_Ntk_t * pFraig )
{
    Abc_Obj_t * pNode0, * pNode1;
    int nPoOrig, nPoFinal, nStored; 
    int i, k;
    // check that the PO functions are correct
    nPoFinal = Abc_NtkPoNum(pFraig);
Alan Mishchenko committed
791
    nStored  = Abc_FrameReadStoreSize();
Alan Mishchenko committed
792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810
    assert( nPoFinal % nStored == 0 );
    nPoOrig  = nPoFinal / nStored;
    for ( i = 0; i < nPoOrig; i++ )
    {
        pNode0 = Abc_ObjFanin0( Abc_NtkPo(pFraig, i) ); 
        for ( k = 1; k < nStored; k++ )
        {
            pNode1 = Abc_ObjFanin0( Abc_NtkPo(pFraig, k*nPoOrig+i) ); 
            if ( pNode0 != pNode1 )
                printf( "Verification for PO #%d of network #%d has failed. The PO function is not used.\n", i+1, k+1 );
        }
    }
}

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


811 812
ABC_NAMESPACE_IMPL_END