abcDar.c 145 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    [abcDar.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Network and node package.]

  Synopsis    [DAG-aware rewriting.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

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

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

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

21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36
#include "base/abc/abc.h"
#include "base/main/main.h"
#include "aig/gia/giaAig.h"
#include "opt/dar/dar.h"
#include "sat/cnf/cnf.h"
#include "proof/fra/fra.h"
#include "proof/fraig/fraig.h"
#include "proof/int/int.h"
#include "proof/dch/dch.h"
#include "proof/ssw/ssw.h"
#include "opt/cgt/cgt.h"
#include "proof/bbr/bbr.h"
#include "aig/gia/gia.h"
#include "proof/cec/cec.h"
#include "opt/csw/csw.h"
#include "proof/pdr/pdr.h"
37
#include "sat/bmc/bmc.h"
Alan Mishchenko committed
38

39 40
ABC_NAMESPACE_IMPL_START

Alan Mishchenko committed
41 42 43 44 45 46 47 48 49 50
////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

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

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

51 52 53 54 55 56 57 58 59 60 61 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 90 91 92 93 94 95 96 97 98 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
  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_ObjCompareById( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 )
{
    return Abc_ObjId(Abc_ObjRegular(*pp1)) - Abc_ObjId(Abc_ObjRegular(*pp2));
}

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

  Synopsis    [Collects the supergate.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_CollectTopOr_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vSuper )
{
    if ( Abc_ObjIsComplement(pObj) || !Abc_ObjIsNode(pObj) )
    {
        Vec_PtrPush( vSuper, pObj );
        return;
    }
    // go through the branches
    Abc_CollectTopOr_rec( Abc_ObjChild0(pObj), vSuper );
    Abc_CollectTopOr_rec( Abc_ObjChild1(pObj), vSuper );
}
void Abc_CollectTopOr( Abc_Obj_t * pObj, Vec_Ptr_t * vSuper )
{
    Vec_PtrClear( vSuper );
    if ( Abc_ObjIsComplement(pObj) )
    {
        Abc_CollectTopOr_rec( Abc_ObjNot(pObj), vSuper );
        Vec_PtrUniqify( vSuper, (int (*)())Abc_ObjCompareById );
    }
    else
        Vec_PtrPush( vSuper, Abc_ObjNot(pObj) );
}

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

  Synopsis    [Converts the network from the AIG manager into ABC.]

  Description [The returned map maps new PO IDs into old ones.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Aig_Man_t * Abc_NtkToDarBmc( Abc_Ntk_t * pNtk, Vec_Int_t ** pvMap )
{
    Aig_Man_t * pMan;
    Abc_Obj_t * pObj, * pTemp;
    Vec_Ptr_t * vDrivers;
    Vec_Ptr_t * vSuper;
    int i, k, nDontCares;

    // print warning about initial values
    nDontCares = 0;
    Abc_NtkForEachLatch( pNtk, pObj, i )
        if ( Abc_LatchIsInitDc(pObj) )
        {
            Abc_LatchSetInit0(pObj);
            nDontCares++;
        }
    if ( nDontCares )
    {
128 129 130 131
        Abc_Print( 1, "Warning: %d registers in this network have don't-care init values.\n", nDontCares );
        Abc_Print( 1, "The don't-care are assumed to be 0. The result may not verify.\n" );
        Abc_Print( 1, "Use command \"print_latch\" to see the init values of registers.\n" );
        Abc_Print( 1, "Use command \"zero\" to convert or \"init\" to change the values.\n" );
132 133 134 135 136
    }

    // collect the drivers
    vSuper   = Vec_PtrAlloc( 100 );
    vDrivers = Vec_PtrAlloc( 100 );
137
    if ( pvMap ) 
138 139 140
    *pvMap   = Vec_IntAlloc( 100 );
    Abc_NtkForEachPo( pNtk, pObj, i )
    {
141 142 143 144 145 146 147
        if ( pNtk->nConstrs && i >= pNtk->nConstrs )
        {
            Vec_PtrPush( vDrivers, Abc_ObjNot(Abc_ObjChild0(pObj)) );
            if ( pvMap )
            Vec_IntPush( *pvMap, i );
            continue;
        }
148 149 150 151 152 153 154 155 156 157 158 159 160
        Abc_CollectTopOr( Abc_ObjChild0(pObj), vSuper );
        Vec_PtrForEachEntry( Abc_Obj_t *, vSuper, pTemp, k )
        {
            Vec_PtrPush( vDrivers, pTemp );
            if ( pvMap )
            Vec_IntPush( *pvMap, i );
        }       
    }
    Vec_PtrFree( vSuper );

    // create network
    pMan = Aig_ManStart( Abc_NtkNodeNum(pNtk) + 100 );
    pMan->nConstrs = pNtk->nConstrs;
161
    pMan->nBarBufs = pNtk->nBarBufs;
162
    pMan->pName = Extra_UtilStrsav( pNtk->pName );
163
    pMan->pSpec = Extra_UtilStrsav( pNtk->pSpec );
164 165 166
    // transfer the pointers to the basic nodes
    Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Aig_ManConst1(pMan);
    Abc_NtkForEachCi( pNtk, pObj, i )
167
        pObj->pCopy = (Abc_Obj_t *)Aig_ObjCreateCi(pMan);
168 169 170 171 172 173 174 175
    // create flops
    Abc_NtkForEachLatch( pNtk, pObj, i )
        Abc_ObjFanout0(pObj)->pCopy = Abc_ObjNotCond( Abc_ObjFanout0(pObj)->pCopy, Abc_LatchIsInit1(pObj) );
    // copy internal nodes
    Abc_NtkForEachNode( pNtk, pObj, i )
        pObj->pCopy = (Abc_Obj_t *)Aig_And( pMan, (Aig_Obj_t *)Abc_ObjChild0Copy(pObj), (Aig_Obj_t *)Abc_ObjChild1Copy(pObj) );
    // create the POs
    Vec_PtrForEachEntry( Abc_Obj_t *, vDrivers, pTemp, k )
176
        Aig_ObjCreateCo( pMan, (Aig_Obj_t *)Abc_ObjNotCond(Abc_ObjRegular(pTemp)->pCopy, !Abc_ObjIsComplement(pTemp)) );
177 178 179
    Vec_PtrFree( vDrivers );
    // create flops
    Abc_NtkForEachLatchInput( pNtk, pObj, i )
180
        Aig_ObjCreateCo( pMan, (Aig_Obj_t *)Abc_ObjNotCond(Abc_ObjChild0Copy(pObj), Abc_LatchIsInit1(Abc_ObjFanout0(pObj))) );
181 182 183 184 185 186

    // remove dangling nodes
    Aig_ManSetRegNum( pMan, Abc_NtkLatchNum(pNtk) );
    Aig_ManCleanup( pMan );
    if ( !Aig_ManCheck( pMan ) )
    {
187
        Abc_Print( 1, "Abc_NtkToDarBmc: AIG check has failed.\n" );
188 189 190 191 192 193 194 195 196
        Aig_ManStop( pMan );
        return NULL;
    }
    return pMan;
}


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

197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213
  Synopsis    [Collects information about what flops have unknown values.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t * Abc_NtkFindDcLatches( Abc_Ntk_t * pNtk )
{
    Vec_Int_t * vUnknown;
    Abc_Obj_t * pObj;
    int i;
    vUnknown = Vec_IntStart( Abc_NtkLatchNum(pNtk) );
    Abc_NtkForEachLatch( pNtk, pObj, i )
        if ( Abc_LatchIsInitDc(pObj) )
214
        {
215
            Vec_IntWriteEntry( vUnknown, i, 1 );
216 217
            Abc_LatchSetInit0(pObj);
        }
218 219 220 221 222
    return vUnknown;
}

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

Alan Mishchenko committed
223 224
  Synopsis    [Converts the network from the AIG manager into ABC.]

Alan Mishchenko committed
225
  Description [Assumes that registers are ordered after PIs/POs.]
Alan Mishchenko committed
226 227 228 229 230 231
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
232
Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters )
Alan Mishchenko committed
233
{
234
    Vec_Ptr_t * vNodes;
Alan Mishchenko committed
235
    Aig_Man_t * pMan;
Alan Mishchenko committed
236
    Aig_Obj_t * pObjNew;
Alan Mishchenko committed
237
    Abc_Obj_t * pObj;
Alan Mishchenko committed
238
    int i, nNodes, nDontCares;
Alan Mishchenko committed
239
    // make sure the latches follow PIs/POs
Alan Mishchenko committed
240 241
    if ( fRegisters ) 
    { 
Alan Mishchenko committed
242 243 244 245 246 247
        assert( Abc_NtkBoxNum(pNtk) == Abc_NtkLatchNum(pNtk) );
        Abc_NtkForEachCi( pNtk, pObj, i )
            if ( i < Abc_NtkPiNum(pNtk) )
            {
                assert( Abc_ObjIsPi(pObj) );
                if ( !Abc_ObjIsPi(pObj) )
248
                    Abc_Print( 1, "Abc_NtkToDar(): Temporary bug: The PI ordering is wrong!\n" );
Alan Mishchenko committed
249 250 251 252 253 254 255 256
            }
            else
                assert( Abc_ObjIsBo(pObj) );
        Abc_NtkForEachCo( pNtk, pObj, i )
            if ( i < Abc_NtkPoNum(pNtk) )
            {
                assert( Abc_ObjIsPo(pObj) );
                if ( !Abc_ObjIsPo(pObj) )
257
                    Abc_Print( 1, "Abc_NtkToDar(): Temporary bug: The PO ordering is wrong!\n" );
Alan Mishchenko committed
258 259 260
            }
            else
                assert( Abc_ObjIsBi(pObj) );
Alan Mishchenko committed
261 262 263 264 265 266 267 268 269 270
        // print warning about initial values
        nDontCares = 0;
        Abc_NtkForEachLatch( pNtk, pObj, i )
            if ( Abc_LatchIsInitDc(pObj) )
            {
                Abc_LatchSetInit0(pObj);
                nDontCares++;
            }
        if ( nDontCares )
        {
271 272 273 274
            Abc_Print( 1, "Warning: %d registers in this network have don't-care init values.\n", nDontCares );
            Abc_Print( 1, "The don't-care are assumed to be 0. The result may not verify.\n" );
            Abc_Print( 1, "Use command \"print_latch\" to see the init values of registers.\n" );
            Abc_Print( 1, "Use command \"zero\" to convert or \"init\" to change the values.\n" );
Alan Mishchenko committed
275
        }
Alan Mishchenko committed
276
    }
Alan Mishchenko committed
277
    // create the manager
Alan Mishchenko committed
278
    pMan = Aig_ManStart( Abc_NtkNodeNum(pNtk) + 100 );
Alan Mishchenko committed
279
    pMan->fCatchExor = fExors;
280
    pMan->nConstrs = pNtk->nConstrs;
281
    pMan->nBarBufs = pNtk->nBarBufs;
Alan Mishchenko committed
282
    pMan->pName = Extra_UtilStrsav( pNtk->pName );
283
    pMan->pSpec = Extra_UtilStrsav( pNtk->pSpec );
Alan Mishchenko committed
284
    // transfer the pointers to the basic nodes
Alan Mishchenko committed
285
    Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Aig_ManConst1(pMan);
Alan Mishchenko committed
286
    Abc_NtkForEachCi( pNtk, pObj, i )
287
    {
288
        pObj->pCopy = (Abc_Obj_t *)Aig_ObjCreateCi(pMan);
289 290 291
        // initialize logic level of the CIs
        ((Aig_Obj_t *)pObj->pCopy)->Level = pObj->Level;
    }
Alan Mishchenko committed
292
    // complement the 1-values registers
Alan Mishchenko committed
293
    if ( fRegisters ) {
Alan Mishchenko committed
294 295 296
        Abc_NtkForEachLatch( pNtk, pObj, i )
            if ( Abc_LatchIsInit1(pObj) )
                Abc_ObjFanout0(pObj)->pCopy = Abc_ObjNot(Abc_ObjFanout0(pObj)->pCopy);
Alan Mishchenko committed
297
    }
Alan Mishchenko committed
298
    // perform the conversion of the internal nodes (assumes DFS ordering)
Alan Mishchenko committed
299
//    pMan->fAddStrash = 1;
300 301 302
    vNodes = Abc_NtkDfs( pNtk, 0 );
    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
//    Abc_NtkForEachNode( pNtk, pObj, i )
Alan Mishchenko committed
303
    {
Alan Mishchenko committed
304
        pObj->pCopy = (Abc_Obj_t *)Aig_And( pMan, (Aig_Obj_t *)Abc_ObjChild0Copy(pObj), (Aig_Obj_t *)Abc_ObjChild1Copy(pObj) );
305
//        Abc_Print( 1, "%d->%d ", pObj->Id, ((Aig_Obj_t *)pObj->pCopy)->Id );
Alan Mishchenko committed
306
    }
307
    Vec_PtrFree( vNodes );
Alan Mishchenko committed
308
    pMan->fAddStrash = 0;
Alan Mishchenko committed
309 310
    // create the POs
    Abc_NtkForEachCo( pNtk, pObj, i )
311
        Aig_ObjCreateCo( pMan, (Aig_Obj_t *)Abc_ObjChild0Copy(pObj) );
Alan Mishchenko committed
312
    // complement the 1-valued registers
Alan Mishchenko committed
313
    Aig_ManSetRegNum( pMan, Abc_NtkLatchNum(pNtk) );
Alan Mishchenko committed
314 315
    if ( fRegisters )
        Aig_ManForEachLiSeq( pMan, pObjNew, i )
Alan Mishchenko committed
316
            if ( Abc_LatchIsInit1(Abc_ObjFanout0(Abc_NtkCo(pNtk,i))) )
Alan Mishchenko committed
317 318
                pObjNew->pFanin0 = Aig_Not(pObjNew->pFanin0);
    // remove dangling nodes
Alan Mishchenko committed
319
    nNodes = (Abc_NtkGetChoiceNum(pNtk) == 0)? Aig_ManCleanup( pMan ) : 0;
Alan Mishchenko committed
320
    if ( !fExors && nNodes )
321
        Abc_Print( 1, "Abc_NtkToDar(): Unexpected %d dangling nodes when converting to AIG!\n", nNodes );
Alan Mishchenko committed
322
//Aig_ManDumpVerilog( pMan, "test.v" );
Alan Mishchenko committed
323 324 325 326 327 328 329 330 331 332
    // save the number of registers
    if ( fRegisters )
    {
        Aig_ManSetRegNum( pMan, Abc_NtkLatchNum(pNtk) );
        pMan->vFlopNums = Vec_IntStartNatural( pMan->nRegs );
//        pMan->vFlopNums = NULL;
//        pMan->vOnehots = Abc_NtkConverLatchNamesIntoNumbers( pNtk );
        if ( pNtk->vOnehots )
            pMan->vOnehots = (Vec_Ptr_t *)Vec_VecDupInt( (Vec_Vec_t *)pNtk->vOnehots );
    }
Alan Mishchenko committed
333 334
    if ( !Aig_ManCheck( pMan ) )
    {
335
        Abc_Print( 1, "Abc_NtkToDar: AIG check has failed.\n" );
Alan Mishchenko committed
336 337 338
        Aig_ManStop( pMan );
        return NULL;
    }
Alan Mishchenko committed
339 340 341 342 343 344 345
    return pMan;
}

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

  Synopsis    [Converts the network from the AIG manager into ABC.]

Alan Mishchenko committed
346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361
  Description [Assumes that registers are ordered after PIs/POs.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Aig_Man_t * Abc_NtkToDarChoices( Abc_Ntk_t * pNtk )
{
    Aig_Man_t * pMan;
    Abc_Obj_t * pObj, * pPrev, * pFanin;
    Vec_Ptr_t * vNodes;
    int i;
    vNodes = Abc_AigDfs( pNtk, 0, 0 );
    // create the manager
    pMan = Aig_ManStart( Abc_NtkNodeNum(pNtk) + 100 );
362
    pMan->nConstrs = pNtk->nConstrs;
363
    pMan->nBarBufs = pNtk->nBarBufs;
364 365
    pMan->pName = Extra_UtilStrsav( pNtk->pName );
    pMan->pSpec = Extra_UtilStrsav( pNtk->pSpec );
Alan Mishchenko committed
366 367
    if ( Abc_NtkGetChoiceNum(pNtk) )
    {
Alan Mishchenko committed
368
        pMan->pEquivs = ABC_ALLOC( Aig_Obj_t *, Abc_NtkObjNum(pNtk) );
Alan Mishchenko committed
369 370 371 372 373
        memset( pMan->pEquivs, 0, sizeof(Aig_Obj_t *) * Abc_NtkObjNum(pNtk) );
    }
    // transfer the pointers to the basic nodes
    Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Aig_ManConst1(pMan);
    Abc_NtkForEachCi( pNtk, pObj, i )
374
        pObj->pCopy = (Abc_Obj_t *)Aig_ObjCreateCi(pMan);
Alan Mishchenko committed
375
    // perform the conversion of the internal nodes (assumes DFS ordering)
376
    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
Alan Mishchenko committed
377 378
    {
        pObj->pCopy = (Abc_Obj_t *)Aig_And( pMan, (Aig_Obj_t *)Abc_ObjChild0Copy(pObj), (Aig_Obj_t *)Abc_ObjChild1Copy(pObj) );
379
//        Abc_Print( 1, "%d->%d ", pObj->Id, ((Aig_Obj_t *)pObj->pCopy)->Id );
Alan Mishchenko committed
380 381
        if ( Abc_AigNodeIsChoice( pObj ) )
        {
382
            for ( pPrev = pObj, pFanin = (Abc_Obj_t *)pObj->pData; pFanin; pPrev = pFanin, pFanin = (Abc_Obj_t *)pFanin->pData )
Alan Mishchenko committed
383 384 385 386 387 388 389
                Aig_ObjSetEquiv( pMan, (Aig_Obj_t *)pPrev->pCopy, (Aig_Obj_t *)pFanin->pCopy );
//            Aig_ManCreateChoice( pIfMan, (Aig_Obj_t *)pNode->pCopy );
        }
    }
    Vec_PtrFree( vNodes );
    // create the POs
    Abc_NtkForEachCo( pNtk, pObj, i )
390
        Aig_ObjCreateCo( pMan, (Aig_Obj_t *)Abc_ObjChild0Copy(pObj) );
Alan Mishchenko committed
391 392 393 394
    // complement the 1-valued registers
    Aig_ManSetRegNum( pMan, 0 );
    if ( !Aig_ManCheck( pMan ) )
    {
395
        Abc_Print( 1, "Abc_NtkToDar: AIG check has failed.\n" );
Alan Mishchenko committed
396 397 398 399 400 401 402 403 404 405
        Aig_ManStop( pMan );
        return NULL;
    }
    return pMan;
}

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

  Synopsis    [Converts the network from the AIG manager into ABC.]

Alan Mishchenko committed
406 407 408 409 410 411 412
  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
413
Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
Alan Mishchenko committed
414 415 416
{
    Vec_Ptr_t * vNodes;
    Abc_Ntk_t * pNtkNew;
Alan Mishchenko committed
417
    Aig_Obj_t * pObj;
Alan Mishchenko committed
418
    int i;
Alan Mishchenko committed
419
    assert( pMan->nAsserts == 0 );
Alan Mishchenko committed
420
//    assert( Aig_ManRegNum(pMan) == Abc_NtkLatchNum(pNtkOld) );
Alan Mishchenko committed
421
    // perform strashing
Alan Mishchenko committed
422
    pNtkNew = Abc_NtkStartFrom( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
423
    pNtkNew->nConstrs = pMan->nConstrs;
424
    pNtkNew->nBarBufs = pNtkOld->nBarBufs;
Alan Mishchenko committed
425
    // transfer the pointers to the basic nodes
Alan Mishchenko committed
426
    Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
427
    Aig_ManForEachCi( pMan, pObj, i )
428
    {
Alan Mishchenko committed
429
        pObj->pData = Abc_NtkCi(pNtkNew, i);
430 431 432
        // initialize logic level of the CIs
        ((Abc_Obj_t *)pObj->pData)->Level = pObj->Level;
    }
Alan Mishchenko committed
433
    // rebuild the AIG
Alan Mishchenko committed
434
    vNodes = Aig_ManDfs( pMan, 1 );
435
    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
Alan Mishchenko committed
436 437
        if ( Aig_ObjIsBuf(pObj) )
            pObj->pData = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
Alan Mishchenko committed
438
        else
439
            pObj->pData = Abc_AigAnd( (Abc_Aig_t *)pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
Alan Mishchenko committed
440 441
    Vec_PtrFree( vNodes );
    // connect the PO nodes
442
    Aig_ManForEachCo( pMan, pObj, i )
Alan Mishchenko committed
443
    {
444
        if ( pMan->nAsserts && i == Aig_ManCoNum(pMan) - pMan->nAsserts )
Alan Mishchenko committed
445
            break;
Alan Mishchenko committed
446
        Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) );
Alan Mishchenko committed
447 448
    }
    // if there are assertions, add them
Alan Mishchenko committed
449
    if ( !Abc_NtkCheck( pNtkNew ) )
450
        Abc_Print( 1, "Abc_NtkFromDar(): Network check has failed.\n" );
451
//Abc_NtkPrintCiLevels( pNtkNew );
Alan Mishchenko committed
452 453 454
    return pNtkNew;
}

Alan Mishchenko committed
455 456 457 458
/**Function*************************************************************

  Synopsis    [Converts the network from the AIG manager into ABC.]

Alan Mishchenko committed
459 460 461 462 463 464 465 466 467 468
  Description [This procedure should be called after seq sweeping, 
  which changes the number of registers.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
{
Alan Mishchenko committed
469
    Vec_Ptr_t * vNodes; 
Alan Mishchenko committed
470 471
    Abc_Ntk_t * pNtkNew;
    Abc_Obj_t * pObjNew, * pLatch;
Alan Mishchenko committed
472
    Aig_Obj_t * pObj, * pObjLo, * pObjLi;
Alan Mishchenko committed
473 474
    int i, iNodeId, nDigits; 
    assert( pMan->nAsserts == 0 );
475
    assert( pNtkOld->nBarBufs == 0 );
Alan Mishchenko committed
476 477 478
//    assert( Aig_ManRegNum(pMan) != Abc_NtkLatchNum(pNtkOld) );
    // perform strashing
    pNtkNew = Abc_NtkStartFromNoLatches( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
479
    pNtkNew->nConstrs = pMan->nConstrs;
480
    pNtkNew->nBarBufs = pMan->nBarBufs;
Alan Mishchenko committed
481
    // consider the case of target enlargement
482
    if ( Abc_NtkCiNum(pNtkNew) < Aig_ManCiNum(pMan) - Aig_ManRegNum(pMan) )
Alan Mishchenko committed
483
    {
484
        for ( i = Aig_ManCiNum(pMan) - Aig_ManRegNum(pMan) - Abc_NtkCiNum(pNtkNew); i > 0; i-- )
Alan Mishchenko committed
485 486 487 488 489
        {
            pObjNew = Abc_NtkCreatePi( pNtkNew );
            Abc_ObjAssignName( pObjNew, Abc_ObjName(pObjNew), NULL );
        }
        Abc_NtkOrderCisCos( pNtkNew );
Alan Mishchenko committed
490
    }
491 492
    assert( Abc_NtkCiNum(pNtkNew) == Aig_ManCiNum(pMan) - Aig_ManRegNum(pMan) );
    assert( Abc_NtkCoNum(pNtkNew) == Aig_ManCoNum(pMan) - Aig_ManRegNum(pMan) );
Alan Mishchenko committed
493 494 495 496 497
    // transfer the pointers to the basic nodes
    Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
    Aig_ManForEachPiSeq( pMan, pObj, i )
        pObj->pData = Abc_NtkCi(pNtkNew, i);
    // create as many latches as there are registers in the manager
Alan Mishchenko committed
498 499 500
    Aig_ManForEachLiLoSeq( pMan, pObjLi, pObjLo, i )
    {
        pObjNew = Abc_NtkCreateLatch( pNtkNew );
Alan Mishchenko committed
501 502
        pObjLi->pData = Abc_NtkCreateBi( pNtkNew );
        pObjLo->pData = Abc_NtkCreateBo( pNtkNew );
503 504
        Abc_ObjAddFanin( pObjNew, (Abc_Obj_t *)pObjLi->pData );
        Abc_ObjAddFanin( (Abc_Obj_t *)pObjLo->pData, pObjNew );
Alan Mishchenko committed
505 506 507
        Abc_LatchSetInit0( pObjNew );
    }
    // rebuild the AIG
Alan Mishchenko committed
508
    vNodes = Aig_ManDfs( pMan, 1 );
509
    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
Alan Mishchenko committed
510 511 512
        if ( Aig_ObjIsBuf(pObj) )
            pObj->pData = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
        else
513
            pObj->pData = Abc_AigAnd( (Abc_Aig_t *)pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
Alan Mishchenko committed
514 515
    Vec_PtrFree( vNodes );
    // connect the PO nodes
516
    Aig_ManForEachCo( pMan, pObj, i )
Alan Mishchenko committed
517
    {
518
//        if ( pMan->nAsserts && i == Aig_ManCoNum(pMan) - pMan->nAsserts )
Alan Mishchenko committed
519
//            break;
Alan Mishchenko committed
520 521 522 523 524
        iNodeId = Nm_ManFindIdByNameTwoTypes( pNtkNew->pManName, Abc_ObjName(Abc_NtkCo(pNtkNew, i)), ABC_OBJ_PI, ABC_OBJ_BO );
        if ( iNodeId >= 0 )
            pObjNew = Abc_NtkObj( pNtkNew, iNodeId );
        else
            pObjNew = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
Alan Mishchenko committed
525
        Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), pObjNew );
Alan Mishchenko committed
526
    }
Alan Mishchenko committed
527 528 529 530
    if ( pMan->vFlopNums == NULL )
        Abc_NtkAddDummyBoxNames( pNtkNew );
    else
    {
Alan Mishchenko committed
531
/*
Alan Mishchenko committed
532 533 534 535
        {
            int i, k, iFlop, Counter = 0;
            FILE * pFile;
            pFile = fopen( "out.txt", "w" );
536
            fAbc_Print( 1, pFile, "The total of %d registers were removed (out of %d):\n", 
Alan Mishchenko committed
537 538 539 540 541 542 543 544 545
                Abc_NtkLatchNum(pNtkOld)-Vec_IntSize(pMan->vFlopNums), Abc_NtkLatchNum(pNtkOld) );
            for ( i = 0; i < Abc_NtkLatchNum(pNtkOld); i++ )
            {
                Vec_IntForEachEntry( pMan->vFlopNums, iFlop, k )
                {
                    if ( i == iFlop )
                        break;
                }
                if ( k == Vec_IntSize(pMan->vFlopNums) )
546
                    fAbc_Print( 1, pFile, "%6d (%6d)  :  %s\n", ++Counter, i, Abc_ObjName( Abc_ObjFanout0(Abc_NtkBox(pNtkOld, i)) ) );
Alan Mishchenko committed
547 548
            }
            fclose( pFile );
549
            //Abc_Print( 1, "\n" );
Alan Mishchenko committed
550
        }
Alan Mishchenko committed
551
*/
Alan Mishchenko committed
552
        assert( Abc_NtkBoxNum(pNtkOld) == Abc_NtkLatchNum(pNtkOld) );
553
        nDigits = Abc_Base10Log( Abc_NtkLatchNum(pNtkNew) );
Alan Mishchenko committed
554 555 556 557 558 559 560 561 562
        Abc_NtkForEachLatch( pNtkNew, pObjNew, i )
        {
            pLatch = Abc_NtkBox( pNtkOld, Vec_IntEntry( pMan->vFlopNums, i ) );
            iNodeId = Nm_ManFindIdByName( pNtkNew->pManName, Abc_ObjName(Abc_ObjFanout0(pLatch)), ABC_OBJ_PO );
            if ( iNodeId >= 0 )
            {
                Abc_ObjAssignName( pObjNew, Abc_ObjNameDummy("l", i, nDigits), NULL );
                Abc_ObjAssignName( Abc_ObjFanin0(pObjNew), Abc_ObjNameDummy("li", i, nDigits), NULL );
                Abc_ObjAssignName( Abc_ObjFanout0(pObjNew), Abc_ObjNameDummy("lo", i, nDigits), NULL );
563
//Abc_Print( 1, "happening   %s -> %s\n", Abc_ObjName(Abc_ObjFanin0(pObjNew)), Abc_ObjName(Abc_ObjFanout0(pObjNew)) );
Alan Mishchenko committed
564 565 566 567 568 569 570
                continue;
            }
            Abc_ObjAssignName( pObjNew, Abc_ObjName(pLatch), NULL );
            Abc_ObjAssignName( Abc_ObjFanin0(pObjNew),  Abc_ObjName(Abc_ObjFanin0(pLatch)), NULL );
            Abc_ObjAssignName( Abc_ObjFanout0(pObjNew), Abc_ObjName(Abc_ObjFanout0(pLatch)), NULL );
        }
    }
Alan Mishchenko committed
571
    // if there are assertions, add them
Alan Mishchenko committed
572
    if ( !Abc_NtkCheck( pNtkNew ) )
573
        Abc_Print( 1, "Abc_NtkFromDar(): Network check has failed.\n" );
Alan Mishchenko committed
574 575 576 577 578 579 580
    return pNtkNew;
}

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

  Synopsis    [Converts the network from the AIG manager into ABC.]

Alan Mishchenko committed
581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598
  Description [This procedure should be called after seq sweeping, 
  which changes the number of registers.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan )
{
    Vec_Ptr_t * vNodes; 
    Abc_Ntk_t * pNtkNew;
    Abc_Obj_t * pObjNew;
    Aig_Obj_t * pObj, * pObjLo, * pObjLi;
    int i; 
    assert( pMan->nAsserts == 0 );
    // perform strashing
    pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
599
    pNtkNew->nConstrs = pMan->nConstrs;
600
    pNtkNew->nBarBufs = pMan->nBarBufs;
Alan Mishchenko committed
601 602 603
    // duplicate the name and the spec
//    pNtkNew->pName = Extra_UtilStrsav(pMan->pName);
//    pNtkNew->pSpec = Extra_UtilStrsav(pMan->pSpec);
Alan Mishchenko committed
604 605 606 607 608
    Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
    // create PIs
    Aig_ManForEachPiSeq( pMan, pObj, i )
    {
        pObjNew = Abc_NtkCreatePi( pNtkNew );
609
//        Abc_ObjAssignName( pObjNew, Abc_ObjName(pObjNew), NULL );
Alan Mishchenko committed
610 611 612 613 614 615
        pObj->pData = pObjNew;
    }
    // create POs
    Aig_ManForEachPoSeq( pMan, pObj, i )
    {
        pObjNew = Abc_NtkCreatePo( pNtkNew );
616
//        Abc_ObjAssignName( pObjNew, Abc_ObjName(pObjNew), NULL );
Alan Mishchenko committed
617 618
        pObj->pData = pObjNew;
    }
619 620
    assert( Abc_NtkCiNum(pNtkNew) == Aig_ManCiNum(pMan) - Aig_ManRegNum(pMan) );
    assert( Abc_NtkCoNum(pNtkNew) == Aig_ManCoNum(pMan) - Aig_ManRegNum(pMan) );
Alan Mishchenko committed
621 622 623 624 625 626
    // create as many latches as there are registers in the manager
    Aig_ManForEachLiLoSeq( pMan, pObjLi, pObjLo, i )
    {
        pObjNew = Abc_NtkCreateLatch( pNtkNew );
        pObjLi->pData = Abc_NtkCreateBi( pNtkNew );
        pObjLo->pData = Abc_NtkCreateBo( pNtkNew );
627 628
        Abc_ObjAddFanin( pObjNew, (Abc_Obj_t *)pObjLi->pData );
        Abc_ObjAddFanin( (Abc_Obj_t *)pObjLo->pData, pObjNew );
Alan Mishchenko committed
629
        Abc_LatchSetInit0( pObjNew );
630 631
//        Abc_ObjAssignName( (Abc_Obj_t *)pObjLi->pData, Abc_ObjName((Abc_Obj_t *)pObjLi->pData), NULL );
//        Abc_ObjAssignName( (Abc_Obj_t *)pObjLo->pData, Abc_ObjName((Abc_Obj_t *)pObjLo->pData), NULL );
Alan Mishchenko committed
632 633 634
    }
    // rebuild the AIG
    vNodes = Aig_ManDfs( pMan, 1 );
635
    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
Alan Mishchenko committed
636 637 638
        if ( Aig_ObjIsBuf(pObj) )
            pObj->pData = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
        else
639
            pObj->pData = Abc_AigAnd( (Abc_Aig_t *)pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
Alan Mishchenko committed
640 641
    Vec_PtrFree( vNodes );
    // connect the PO nodes
642
    Aig_ManForEachCo( pMan, pObj, i )
Alan Mishchenko committed
643 644 645 646
    {
        pObjNew = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
        Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), pObjNew );
    }
647 648 649 650 651

    Abc_NtkAddDummyPiNames( pNtkNew );
    Abc_NtkAddDummyPoNames( pNtkNew );
    Abc_NtkAddDummyBoxNames( pNtkNew );

Alan Mishchenko committed
652 653
    // check the resulting AIG
    if ( !Abc_NtkCheck( pNtkNew ) )
654
        Abc_Print( 1, "Abc_NtkFromAigPhase(): Network check has failed.\n" );
Alan Mishchenko committed
655 656 657
    return pNtkNew;
}

658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721


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

  Synopsis    [Creates local function of the node.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Hop_Obj_t * Abc_ObjHopFromGia_rec( Hop_Man_t * pHopMan, Gia_Man_t * p, int Id, Vec_Ptr_t * vCopies )
{
    Gia_Obj_t * pObj;
    Hop_Obj_t * gFunc, * gFunc0, * gFunc1;
    if ( Gia_ObjIsTravIdCurrentId(p, Id) )
        return (Hop_Obj_t *)Vec_PtrEntry( vCopies, Id );
    Gia_ObjSetTravIdCurrentId(p, Id);
    pObj = Gia_ManObj(p, Id);
    assert( Gia_ObjIsAnd(pObj) );
    // compute the functions of the children
    gFunc0 = Abc_ObjHopFromGia_rec( pHopMan, p, Gia_ObjFaninId0(pObj, Id), vCopies );
    gFunc1 = Abc_ObjHopFromGia_rec( pHopMan, p, Gia_ObjFaninId1(pObj, Id), vCopies );
    // get the function of the cut
    gFunc  = Hop_And( pHopMan, Hop_NotCond(gFunc0, Gia_ObjFaninC0(pObj)), Hop_NotCond(gFunc1, Gia_ObjFaninC1(pObj)) );  
    Vec_PtrWriteEntry( vCopies, Id, gFunc );
    return gFunc;
}
Hop_Obj_t * Abc_ObjHopFromGia( Hop_Man_t * pHopMan, Gia_Man_t * p, int GiaId, Vec_Ptr_t * vCopies )
{
    int k, iFan;
    assert( Gia_ObjIsLut(p, GiaId) );
    assert( Gia_ObjLutSize(p, GiaId) > 0 );
    Gia_ManIncrementTravId( p );
    Gia_LutForEachFanin( p, GiaId, iFan, k )
    {
        Gia_ObjSetTravIdCurrentId(p, iFan);
        Vec_PtrWriteEntry( vCopies, iFan, Hop_IthVar(pHopMan, k) );
    }
    return Abc_ObjHopFromGia_rec( pHopMan, p, GiaId, vCopies );
}

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

  Synopsis    [Converts the network from the mapped GIA manager.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Abc_Ntk_t * Abc_NtkFromMappedGia( Gia_Man_t * p )
{
    int fVerbose = 0;
    int fDuplicate = 0;
    Abc_Ntk_t * pNtkNew;
    Abc_Obj_t * pObjNew, * pObjNewLi, * pObjNewLo, * pConst0 = NULL;
    Gia_Obj_t * pObj, * pObjLi, * pObjLo;
    Vec_Ptr_t * vReflect;
    int i, k, iFan, nDupGates; 
722
    assert( Gia_ManHasMapping(p) );
723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762
    pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_AIG, 1 );
    // duplicate the name and the spec
    pNtkNew->pName = Extra_UtilStrsav(p->pName);
    pNtkNew->pSpec = Extra_UtilStrsav(p->pSpec);
    Gia_ManFillValue( p );
    // create constant
    pConst0 = Abc_NtkCreateNodeConst0( pNtkNew );
    Gia_ManConst0(p)->Value = Abc_ObjId(pConst0);
    // create PIs
    Gia_ManForEachPi( p, pObj, i )
        pObj->Value = Abc_ObjId( Abc_NtkCreatePi( pNtkNew ) );
    // create POs
    Gia_ManForEachPo( p, pObj, i )
        pObj->Value = Abc_ObjId( Abc_NtkCreatePo( pNtkNew ) );
    // create as many latches as there are registers in the manager
    Gia_ManForEachRiRo( p, pObjLi, pObjLo, i )
    {
        pObjNew = Abc_NtkCreateLatch( pNtkNew );
        pObjNewLi = Abc_NtkCreateBi( pNtkNew );
        pObjNewLo = Abc_NtkCreateBo( pNtkNew );
        Abc_ObjAddFanin( pObjNew, pObjNewLi );
        Abc_ObjAddFanin( pObjNewLo, pObjNew );
        pObjLi->Value = Abc_ObjId( pObjNewLi );
        pObjLo->Value = Abc_ObjId( pObjNewLo );
        Abc_LatchSetInit0( pObjNew );
    }
    // rebuild the AIG
    vReflect = Vec_PtrStart( Gia_ManObjNum(p) );
    Gia_ManForEachLut( p, i )
    {
        pObj = Gia_ManObj(p, i);
        assert( pObj->Value == ~0 );
        if ( Gia_ObjLutSize(p, i) == 0 )
        {
            pObj->Value = Abc_ObjId(pConst0);
            continue;
        }
        pObjNew = Abc_NtkCreateNode( pNtkNew );
        Gia_LutForEachFanin( p, i, iFan, k )
            Abc_ObjAddFanin( pObjNew, Abc_NtkObj(pNtkNew, Gia_ObjValue(Gia_ManObj(p, iFan))) );
763
        pObjNew->pData = Abc_ObjHopFromGia( (Hop_Man_t *)pNtkNew->pManFunc, p, i, vReflect );
764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787
        pObj->Value = Abc_ObjId( pObjNew );
    }
    Vec_PtrFree( vReflect );
    // connect the PO nodes
    Gia_ManForEachCo( p, pObj, i )
    {
        pObjNew = Abc_NtkObj( pNtkNew, Gia_ObjValue(Gia_ObjFanin0(pObj)) );
        Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), Abc_ObjNotCond( pObjNew, Gia_ObjFaninC0(pObj) ) );
    }
    // create names
    Abc_NtkAddDummyPiNames( pNtkNew );
    Abc_NtkAddDummyPoNames( pNtkNew );
    Abc_NtkAddDummyBoxNames( pNtkNew );

    // decouple the PO driver nodes to reduce the number of levels
    nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, fDuplicate );
    if ( fVerbose && nDupGates && !Abc_FrameReadFlag("silentmode") )
    {
        if ( !fDuplicate )
            printf( "Added %d buffers/inverters to decouple the CO drivers.\n", nDupGates );
        else
            printf( "Duplicated %d gates to decouple the CO drivers.\n", nDupGates );
    }
    // remove const node if it is not used
788
    if ( !Abc_ObjIsNone(pConst0) && Abc_ObjFanoutNum(pConst0) == 0 )
789 790 791 792 793 794 795 796 797 798 799 800 801
        Abc_NtkDeleteObj( pConst0 );

    assert( Gia_ManPiNum(p) == Abc_NtkPiNum(pNtkNew) );
    assert( Gia_ManPoNum(p) == Abc_NtkPoNum(pNtkNew) );
    assert( Gia_ManRegNum(p) == Abc_NtkLatchNum(pNtkNew) );

    // check the resulting AIG
    if ( !Abc_NtkCheck( pNtkNew ) )
        Abc_Print( 1, "Abc_NtkFromMappedGia(): Network check has failed.\n" );
    return pNtkNew;
}


Alan Mishchenko committed
802 803 804 805
/**Function*************************************************************

  Synopsis    [Converts the network from the AIG manager into ABC.]

Alan Mishchenko committed
806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821
  Description [This procedure should be called after seq sweeping, 
  which changes the number of registers.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Abc_Ntk_t * Abc_NtkAfterTrim( Aig_Man_t * pMan, Abc_Ntk_t * pNtkOld )
{
    Vec_Ptr_t * vNodes; 
    Abc_Ntk_t * pNtkNew;
    Abc_Obj_t * pObjNew, * pObjOld;
    Aig_Obj_t * pObj, * pObjLo, * pObjLi;
    int i; 
    assert( pMan->nAsserts == 0 );
822
    assert( pNtkOld->nBarBufs == 0 );
Alan Mishchenko committed
823 824 825 826 827 828
    assert( Aig_ManRegNum(pMan) <= Abc_NtkLatchNum(pNtkOld) );
    assert( Saig_ManPiNum(pMan) <= Abc_NtkCiNum(pNtkOld) );
    assert( Saig_ManPoNum(pMan) == Abc_NtkPoNum(pNtkOld) );
    assert( pMan->vCiNumsOrig != NULL );
    // perform strashing
    pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
829
    pNtkNew->nConstrs = pMan->nConstrs;
830
    pNtkNew->nBarBufs = pMan->nBarBufs;
Alan Mishchenko committed
831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852
    // duplicate the name and the spec
//    pNtkNew->pName = Extra_UtilStrsav(pMan->pName);
//    pNtkNew->pSpec = Extra_UtilStrsav(pMan->pSpec);
    Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
    // create PIs
    Aig_ManForEachPiSeq( pMan, pObj, i )
    {
        pObjNew = Abc_NtkCreatePi( pNtkNew );
        pObj->pData = pObjNew;
        // find the name
        pObjOld = Abc_NtkCi( pNtkOld, Vec_IntEntry(pMan->vCiNumsOrig, i) );
        Abc_ObjAssignName( pObjNew, Abc_ObjName(pObjOld), NULL );
    }
    // create POs
    Aig_ManForEachPoSeq( pMan, pObj, i )
    {
        pObjNew = Abc_NtkCreatePo( pNtkNew );
        pObj->pData = pObjNew;
        // find the name
        pObjOld = Abc_NtkCo( pNtkOld, i );
        Abc_ObjAssignName( pObjNew, Abc_ObjName(pObjOld), NULL );
    }
853 854
    assert( Abc_NtkCiNum(pNtkNew) == Aig_ManCiNum(pMan) - Aig_ManRegNum(pMan) );
    assert( Abc_NtkCoNum(pNtkNew) == Aig_ManCoNum(pMan) - Aig_ManRegNum(pMan) );
Alan Mishchenko committed
855 856 857 858 859 860
    // create as many latches as there are registers in the manager
    Aig_ManForEachLiLoSeq( pMan, pObjLi, pObjLo, i )
    {
        pObjNew = Abc_NtkCreateLatch( pNtkNew );
        pObjLi->pData = Abc_NtkCreateBi( pNtkNew );
        pObjLo->pData = Abc_NtkCreateBo( pNtkNew );
861 862
        Abc_ObjAddFanin( pObjNew, (Abc_Obj_t *)pObjLi->pData );
        Abc_ObjAddFanin( (Abc_Obj_t *)pObjLo->pData, pObjNew );
Alan Mishchenko committed
863 864 865
        Abc_LatchSetInit0( pObjNew );
        // find the name
        pObjOld = Abc_NtkCi( pNtkOld, Vec_IntEntry(pMan->vCiNumsOrig, Saig_ManPiNum(pMan)+i) );
866
        Abc_ObjAssignName( (Abc_Obj_t *)pObjLo->pData, Abc_ObjName(pObjOld), NULL );
Alan Mishchenko committed
867 868
        // find the name
        pObjOld = Abc_NtkCo( pNtkOld, Saig_ManPoNum(pMan)+i );
869
        Abc_ObjAssignName( (Abc_Obj_t *)pObjLi->pData, Abc_ObjName(pObjOld), NULL );
Alan Mishchenko committed
870 871 872
    }
    // rebuild the AIG
    vNodes = Aig_ManDfs( pMan, 1 );
873
    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
Alan Mishchenko committed
874 875 876
        if ( Aig_ObjIsBuf(pObj) )
            pObj->pData = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
        else
877
            pObj->pData = Abc_AigAnd( (Abc_Aig_t *)pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
Alan Mishchenko committed
878 879
    Vec_PtrFree( vNodes );
    // connect the PO nodes
880
    Aig_ManForEachCo( pMan, pObj, i )
Alan Mishchenko committed
881 882 883 884 885 886
    {
        pObjNew = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
        Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), pObjNew );
    }
    // check the resulting AIG
    if ( !Abc_NtkCheck( pNtkNew ) )
887
        Abc_Print( 1, "Abc_NtkAfterTrim(): Network check has failed.\n" );
Alan Mishchenko committed
888 889 890 891 892 893 894
    return pNtkNew;
}

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

  Synopsis    [Converts the network from the AIG manager into ABC.]

Alan Mishchenko committed
895 896 897 898 899 900 901
  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
902 903 904 905 906
Abc_Ntk_t * Abc_NtkFromDarChoices( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
{
    Abc_Ntk_t * pNtkNew;
    Aig_Obj_t * pObj, * pTemp;
    int i;
Alan Mishchenko committed
907
    assert( pMan->pEquivs != NULL );
Alan Mishchenko committed
908 909
    assert( Aig_ManBufNum(pMan) == 0 );
    // perform strashing
Alan Mishchenko committed
910
    pNtkNew = Abc_NtkStartFrom( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
911
    pNtkNew->nConstrs = pMan->nConstrs;
912
    pNtkNew->nBarBufs = pNtkOld->nBarBufs;
Alan Mishchenko committed
913
    // transfer the pointers to the basic nodes
914
    Aig_ManCleanData( pMan );
Alan Mishchenko committed
915
    Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
916
    Aig_ManForEachCi( pMan, pObj, i )
Alan Mishchenko committed
917 918
        pObj->pData = Abc_NtkCi(pNtkNew, i);
    // rebuild the AIG
919
    Aig_ManForEachNode( pMan, pObj, i )
Alan Mishchenko committed
920
    {
921
        pObj->pData = Abc_AigAnd( (Abc_Aig_t *)pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
Alan Mishchenko committed
922
        if ( (pTemp = Aig_ObjEquiv(pMan, pObj)) )
Alan Mishchenko committed
923 924
        {
            assert( pTemp->pData != NULL );
925
            ((Abc_Obj_t *)pObj->pData)->pData = ((Abc_Obj_t *)pTemp->pData);
Alan Mishchenko committed
926 927 928
        }
    }
    // connect the PO nodes
929
    Aig_ManForEachCo( pMan, pObj, i )
Alan Mishchenko committed
930 931
        Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) );
    if ( !Abc_NtkCheck( pNtkNew ) )
932
        Abc_Print( 1, "Abc_NtkFromDar(): Network check has failed.\n" );
933 934 935 936 937 938 939 940 941 942 943 944 945 946 947

    // verify topological order
    if ( 0 )
    {
        Abc_Obj_t * pNode;
        Abc_NtkForEachNode( pNtkNew, pNode, i )
            if ( Abc_AigNodeIsChoice( pNode ) )
            {
                int Counter = 0;
                for ( pNode = Abc_ObjEquiv(pNode); pNode; pNode = Abc_ObjEquiv(pNode) )
                    Counter++;
                printf( "%d ", Counter );
            }
        printf( "\n" );
    }
Alan Mishchenko committed
948 949 950 951 952
    return pNtkNew;
}

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

Alan Mishchenko committed
953 954 955 956 957 958 959 960 961 962 963 964 965 966 967 968 969
  Synopsis    [Converts the network from the AIG manager into ABC.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Abc_Ntk_t * Abc_NtkFromDarSeq( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
{
    Vec_Ptr_t * vNodes;
    Abc_Ntk_t * pNtkNew;
    Abc_Obj_t * pObjNew, * pFaninNew, * pFaninNew0, * pFaninNew1;
    Aig_Obj_t * pObj;
    int i;
//    assert( Aig_ManLatchNum(pMan) > 0 );
970
    assert( pNtkOld->nBarBufs == 0 );
Alan Mishchenko committed
971 972
    // perform strashing
    pNtkNew = Abc_NtkStartFromNoLatches( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
973
    pNtkNew->nConstrs = pMan->nConstrs;
974
    pNtkNew->nBarBufs = pMan->nBarBufs;
Alan Mishchenko committed
975 976
    // transfer the pointers to the basic nodes
    Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
977
    Aig_ManForEachCi( pMan, pObj, i )
Alan Mishchenko committed
978 979 980 981 982 983 984 985 986 987 988 989 990 991
        pObj->pData = Abc_NtkPi(pNtkNew, i);
    // create latches of the new network
    Aig_ManForEachObj( pMan, pObj, i )
    {
        pObjNew = Abc_NtkCreateLatch( pNtkNew );
        pFaninNew0 = Abc_NtkCreateBi( pNtkNew );
        pFaninNew1 = Abc_NtkCreateBo( pNtkNew );
        Abc_ObjAddFanin( pObjNew, pFaninNew0 );
        Abc_ObjAddFanin( pFaninNew1, pObjNew );
        Abc_LatchSetInit0( pObjNew );
        pObj->pData = Abc_ObjFanout0( pObjNew );
    }
    Abc_NtkAddDummyBoxNames( pNtkNew );
    // rebuild the AIG
Alan Mishchenko committed
992
    vNodes = Aig_ManDfs( pMan, 1 );
993
    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
Alan Mishchenko committed
994 995 996 997 998 999 1000 1001 1002
    {
        // add the first fanin
        pObj->pData = pFaninNew0 = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
        if ( Aig_ObjIsBuf(pObj) )
            continue;
        // add the second fanin
        pFaninNew1 = (Abc_Obj_t *)Aig_ObjChild1Copy(pObj);
        // create the new node
        if ( Aig_ObjIsExor(pObj) )
1003
            pObj->pData = pObjNew = Abc_AigXor( (Abc_Aig_t *)pNtkNew->pManFunc, pFaninNew0, pFaninNew1 );
Alan Mishchenko committed
1004
        else
1005
            pObj->pData = pObjNew = Abc_AigAnd( (Abc_Aig_t *)pNtkNew->pManFunc, pFaninNew0, pFaninNew1 );
Alan Mishchenko committed
1006 1007 1008
    }
    Vec_PtrFree( vNodes );
    // connect the PO nodes
1009
    Aig_ManForEachCo( pMan, pObj, i )
Alan Mishchenko committed
1010 1011 1012 1013 1014 1015 1016 1017
    {
        pFaninNew = (Abc_Obj_t *)Aig_ObjChild0Copy( pObj );
        Abc_ObjAddFanin( Abc_NtkPo(pNtkNew, i), pFaninNew );
    }
    // connect the latches
    Aig_ManForEachObj( pMan, pObj, i )
    {
        pFaninNew = (Abc_Obj_t *)Aig_ObjChild0Copy( pObj );
1018
        Abc_ObjAddFanin( Abc_ObjFanin0(Abc_ObjFanin0((Abc_Obj_t *)pObj->pData)), pFaninNew );
Alan Mishchenko committed
1019 1020
    }
    if ( !Abc_NtkCheck( pNtkNew ) )
1021
        Abc_Print( 1, "Abc_NtkFromIvySeq(): Network check has failed.\n" );
Alan Mishchenko committed
1022 1023 1024 1025 1026
    return pNtkNew;
}

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

Alan Mishchenko committed
1027 1028 1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 1046 1047 1048 1049 1050 1051 1052 1053 1054 1055 1056 1057 1058 1059 1060 1061 1062 1063 1064 1065 1066 1067 1068 1069 1070
  Synopsis    [Collects CI of the network.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Ptr_t * Abc_NtkCollectCiNames( Abc_Ntk_t * pNtk )
{
    Abc_Obj_t * pObj;
    int i;
    Vec_Ptr_t * vNames;
    vNames = Vec_PtrAlloc( 100 );
    Abc_NtkForEachCi( pNtk, pObj, i )
        Vec_PtrPush( vNames, Extra_UtilStrsav(Abc_ObjName(pObj)) );
    return vNames;
}

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

  Synopsis    [Collects CO of the network.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Ptr_t * Abc_NtkCollectCoNames( Abc_Ntk_t * pNtk )
{
    Abc_Obj_t * pObj;
    int i;
    Vec_Ptr_t * vNames;
    vNames = Vec_PtrAlloc( 100 );
    Abc_NtkForEachCo( pNtk, pObj, i )
        Vec_PtrPush( vNames, Extra_UtilStrsav(Abc_ObjName(pObj)) );
    return vNames;
}

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

Alan Mishchenko committed
1071 1072 1073 1074 1075 1076 1077 1078 1079 1080 1081 1082 1083 1084 1085 1086 1087
  Synopsis    [Collect latch values.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t * Abc_NtkGetLatchValues( Abc_Ntk_t * pNtk )
{
    Vec_Int_t * vInits;
    Abc_Obj_t * pLatch;
    int i;
    vInits = Vec_IntAlloc( Abc_NtkLatchNum(pNtk) );
    Abc_NtkForEachLatch( pNtk, pLatch, i )
    {
Alan Mishchenko committed
1088 1089 1090 1091 1092 1093 1094 1095
        if ( Abc_LatchIsInit0(pLatch) )
            Vec_IntPush( vInits, 0 );
        else if ( Abc_LatchIsInit1(pLatch) )
            Vec_IntPush( vInits, 1 );
        else if ( Abc_LatchIsInitDc(pLatch) )
            Vec_IntPush( vInits, 2 );
        else
            assert( 0 );
Alan Mishchenko committed
1096 1097 1098 1099 1100 1101
    }
    return vInits;
}

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

Alan Mishchenko committed
1102 1103 1104 1105 1106 1107 1108 1109 1110 1111 1112
  Synopsis    [Gives the current ABC network to AIG manager for processing.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk )
{
Alan Mishchenko committed
1113 1114 1115
    Abc_Ntk_t * pNtkAig = NULL;
    Aig_Man_t * pMan;
    extern void Fra_ManPartitionTest( Aig_Man_t * p, int nComLim );
Alan Mishchenko committed
1116 1117 1118

    assert( Abc_NtkIsStrash(pNtk) );
    // convert to the AIG manager
Alan Mishchenko committed
1119
    pMan = Abc_NtkToDar( pNtk, 0, 0 );
Alan Mishchenko committed
1120 1121 1122
    if ( pMan == NULL )
        return NULL;

Alan Mishchenko committed
1123 1124 1125
    // perform computation
//    Fra_ManPartitionTest( pMan, 4 );
    pNtkAig = Abc_NtkFromDar( pNtk, pMan );
Alan Mishchenko committed
1126
    Aig_ManStop( pMan );
Alan Mishchenko committed
1127

Alan Mishchenko committed
1128
    // make sure everything is okay
Alan Mishchenko committed
1129
    if ( pNtkAig && !Abc_NtkCheck( pNtkAig ) )
Alan Mishchenko committed
1130
    {
1131
        Abc_Print( 1, "Abc_NtkDar: The network check has failed.\n" );
Alan Mishchenko committed
1132 1133 1134 1135 1136 1137
        Abc_NtkDelete( pNtkAig );
        return NULL;
    }
    return pNtkAig;
}

Alan Mishchenko committed
1138

Alan Mishchenko committed
1139 1140 1141 1142 1143 1144 1145 1146 1147 1148 1149
/**Function*************************************************************

  Synopsis    [Gives the current ABC network to AIG manager for processing.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
1150
Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, int fProve, int fTransfer, int fSpeculate, int fChoicing, int fVerbose )
Alan Mishchenko committed
1151
{
Alan Mishchenko committed
1152
    Fra_Par_t Pars, * pPars = &Pars; 
Alan Mishchenko committed
1153
    Abc_Ntk_t * pNtkAig;
Alan Mishchenko committed
1154
    Aig_Man_t * pMan, * pTemp;
Alan Mishchenko committed
1155
    pMan = Abc_NtkToDar( pNtk, 0, 0 );
Alan Mishchenko committed
1156 1157
    if ( pMan == NULL )
        return NULL;
Alan Mishchenko committed
1158 1159 1160 1161 1162 1163 1164 1165 1166 1167 1168 1169 1170
    Fra_ParamsDefault( pPars );
    pPars->nBTLimitNode = nConfLimit;
    pPars->fChoicing    = fChoicing;
    pPars->fDoSparse    = fDoSparse;
    pPars->fSpeculate   = fSpeculate;
    pPars->fProve       = fProve;
    pPars->fVerbose     = fVerbose;
    pMan = Fra_FraigPerform( pTemp = pMan, pPars );
    if ( fChoicing )
        pNtkAig = Abc_NtkFromDarChoices( pNtk, pMan );
    else
        pNtkAig = Abc_NtkFromDar( pNtk, pMan );
    Aig_ManStop( pTemp );
Alan Mishchenko committed
1171
    Aig_ManStop( pMan );
Alan Mishchenko committed
1172 1173 1174
    return pNtkAig;
}

Alan Mishchenko committed
1175 1176
/**Function*************************************************************

Alan Mishchenko committed
1177
  Synopsis    [Gives the current ABC network to AIG manager for processing.]
Alan Mishchenko committed
1178 1179 1180 1181 1182 1183

  Description []
               
  SideEffects []

  SeeAlso     []
Alan Mishchenko committed
1184

Alan Mishchenko committed
1185
***********************************************************************/
Alan Mishchenko committed
1186 1187 1188 1189
Abc_Ntk_t * Abc_NtkDarFraigPart( Abc_Ntk_t * pNtk, int nPartSize, int nConfLimit, int nLevelMax, int fVerbose )
{
    Abc_Ntk_t * pNtkAig;
    Aig_Man_t * pMan, * pTemp;
Alan Mishchenko committed
1190
    pMan = Abc_NtkToDar( pNtk, 0, 0 );
Alan Mishchenko committed
1191 1192 1193 1194 1195 1196 1197 1198 1199 1200 1201 1202 1203 1204 1205 1206 1207 1208 1209 1210
    if ( pMan == NULL )
        return NULL;
    pMan = Aig_ManFraigPartitioned( pTemp = pMan, nPartSize, nConfLimit, nLevelMax, fVerbose );
    Aig_ManStop( pTemp );
    pNtkAig = Abc_NtkFromDar( pNtk, pMan );
    Aig_ManStop( pMan );
    return pNtkAig;
}

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

  Synopsis    [Gives the current ABC network to AIG manager for processing.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
1211
Abc_Ntk_t * Abc_NtkCSweep( Abc_Ntk_t * pNtk, int nCutsMax, int nLeafMax, int fVerbose )
Alan Mishchenko committed
1212
{
1213
//    extern Aig_Man_t * Csw_Sweep( Aig_Man_t * pAig, int nCutsMax, int nLeafMax, int fVerbose );
Alan Mishchenko committed
1214
    Abc_Ntk_t * pNtkAig;
Alan Mishchenko committed
1215
    Aig_Man_t * pMan, * pTemp;
Alan Mishchenko committed
1216
    pMan = Abc_NtkToDar( pNtk, 0, 0 );
Alan Mishchenko committed
1217 1218
    if ( pMan == NULL )
        return NULL;
Alan Mishchenko committed
1219 1220
    pMan = Csw_Sweep( pTemp = pMan, nCutsMax, nLeafMax, fVerbose );
    pNtkAig = Abc_NtkFromDar( pNtk, pMan );
Alan Mishchenko committed
1221
    Aig_ManStop( pTemp );
Alan Mishchenko committed
1222 1223 1224 1225 1226 1227 1228 1229 1230 1231 1232 1233 1234 1235 1236 1237 1238 1239 1240
    Aig_ManStop( pMan );
    return pNtkAig;
}

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

  Synopsis    [Gives the current ABC network to AIG manager for processing.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Abc_Ntk_t * Abc_NtkDRewrite( Abc_Ntk_t * pNtk, Dar_RwrPar_t * pPars )
{
    Aig_Man_t * pMan, * pTemp;
    Abc_Ntk_t * pNtkAig;
1241
    abctime clk;
Alan Mishchenko committed
1242
    assert( Abc_NtkIsStrash(pNtk) );
Alan Mishchenko committed
1243
    pMan = Abc_NtkToDar( pNtk, 0, 0 );
Alan Mishchenko committed
1244 1245 1246 1247 1248
    if ( pMan == NULL )
        return NULL;
//    Aig_ManPrintStats( pMan );
/*
//    Aig_ManSupports( pMan );
Alan Mishchenko committed
1249
    {
Alan Mishchenko committed
1250 1251 1252
        Vec_Vec_t * vParts;
        vParts = Aig_ManPartitionSmart( pMan, 50, 1, NULL );
        Vec_VecFree( vParts );
Alan Mishchenko committed
1253
    }
Alan Mishchenko committed
1254 1255 1256 1257 1258
*/
    Dar_ManRewrite( pMan, pPars );
//    pMan = Dar_ManBalance( pTemp = pMan, pPars->fUpdateLevel );
//    Aig_ManStop( pTemp );

1259
clk = Abc_Clock();
Alan Mishchenko committed
1260
    pMan = Aig_ManDupDfs( pTemp = pMan ); 
Alan Mishchenko committed
1261
    Aig_ManStop( pTemp );
1262
//ABC_PRT( "time", Abc_Clock() - clk );
Alan Mishchenko committed
1263 1264 1265

//    Aig_ManPrintStats( pMan );
    pNtkAig = Abc_NtkFromDar( pNtk, pMan );
Alan Mishchenko committed
1266 1267 1268 1269 1270 1271 1272 1273 1274 1275 1276 1277 1278 1279 1280
    Aig_ManStop( pMan );
    return pNtkAig;
}

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

  Synopsis    [Gives the current ABC network to AIG manager for processing.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
1281
Abc_Ntk_t * Abc_NtkDRefactor( Abc_Ntk_t * pNtk, Dar_RefPar_t * pPars )
Alan Mishchenko committed
1282
{
Alan Mishchenko committed
1283
    Aig_Man_t * pMan, * pTemp;
Alan Mishchenko committed
1284
    Abc_Ntk_t * pNtkAig;
1285
    abctime clk;
Alan Mishchenko committed
1286
    assert( Abc_NtkIsStrash(pNtk) );
Alan Mishchenko committed
1287
    pMan = Abc_NtkToDar( pNtk, 0, 0 );
Alan Mishchenko committed
1288 1289 1290
    if ( pMan == NULL )
        return NULL;
//    Aig_ManPrintStats( pMan );
Alan Mishchenko committed
1291

Alan Mishchenko committed
1292 1293 1294 1295
    Dar_ManRefactor( pMan, pPars );
//    pMan = Dar_ManBalance( pTemp = pMan, pPars->fUpdateLevel );
//    Aig_ManStop( pTemp );

1296
clk = Abc_Clock();
Alan Mishchenko committed
1297
    pMan = Aig_ManDupDfs( pTemp = pMan ); 
Alan Mishchenko committed
1298
    Aig_ManStop( pTemp );
1299
//ABC_PRT( "time", Abc_Clock() - clk );
Alan Mishchenko committed
1300 1301 1302 1303 1304

//    Aig_ManPrintStats( pMan );
    pNtkAig = Abc_NtkFromDar( pNtk, pMan );
    Aig_ManStop( pMan );
    return pNtkAig;
Alan Mishchenko committed
1305 1306
}

Alan Mishchenko committed
1307 1308 1309 1310 1311 1312 1313 1314 1315 1316 1317
/**Function*************************************************************

  Synopsis    [Gives the current ABC network to AIG manager for processing.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
1318
Abc_Ntk_t * Abc_NtkDC2( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fFanout, int fPower, int fVerbose )
Alan Mishchenko committed
1319 1320 1321
{
    Aig_Man_t * pMan, * pTemp;
    Abc_Ntk_t * pNtkAig;
1322
    abctime clk;
Alan Mishchenko committed
1323
    assert( Abc_NtkIsStrash(pNtk) );
Alan Mishchenko committed
1324
    pMan = Abc_NtkToDar( pNtk, 0, 0 );
Alan Mishchenko committed
1325 1326
    if ( pMan == NULL )
        return NULL;
Alan Mishchenko committed
1327
//    Aig_ManPrintStats( pMan );
Alan Mishchenko committed
1328

1329
clk = Abc_Clock();
Alan Mishchenko committed
1330
    pMan = Dar_ManCompress2( pTemp = pMan, fBalance, fUpdateLevel, fFanout, fPower, fVerbose ); 
Alan Mishchenko committed
1331
    Aig_ManStop( pTemp );
1332
//ABC_PRT( "time", Abc_Clock() - clk );
Alan Mishchenko committed
1333

Alan Mishchenko committed
1334 1335
//    Aig_ManPrintStats( pMan );
    pNtkAig = Abc_NtkFromDar( pNtk, pMan );
Alan Mishchenko committed
1336 1337 1338 1339 1340 1341 1342 1343 1344 1345 1346 1347 1348 1349 1350
    Aig_ManStop( pMan );
    return pNtkAig;
}

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

  Synopsis    [Gives the current ABC network to AIG manager for processing.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
1351
Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fConstruct, int nConfMax, int nLevelMax, int fVerbose )
Alan Mishchenko committed
1352
{
Alan Mishchenko committed
1353 1354 1355
    Aig_Man_t * pMan, * pTemp;
    Abc_Ntk_t * pNtkAig;
    assert( Abc_NtkIsStrash(pNtk) );
Alan Mishchenko committed
1356
    pMan = Abc_NtkToDar( pNtk, 0, 0 );
Alan Mishchenko committed
1357 1358
    if ( pMan == NULL )
        return NULL;
Alan Mishchenko committed
1359
    pMan = Dar_ManChoice( pTemp = pMan, fBalance, fUpdateLevel, fConstruct, nConfMax, nLevelMax, fVerbose );
Alan Mishchenko committed
1360 1361 1362 1363 1364 1365 1366
    Aig_ManStop( pTemp );
    pNtkAig = Abc_NtkFromDarChoices( pNtk, pMan );
    Aig_ManStop( pMan );
    return pNtkAig;
}

/**Function*************************************************************
Alan Mishchenko committed
1367 1368 1369 1370 1371 1372 1373 1374 1375 1376 1377 1378

  Synopsis    [Gives the current ABC network to AIG manager for processing.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Abc_Ntk_t * Abc_NtkDch( Abc_Ntk_t * pNtk, Dch_Pars_t * pPars )
{
1379
    extern Gia_Man_t * Dar_NewChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fPower, int fLightSynth, int fVerbose );
Alan Mishchenko committed
1380
    extern Aig_Man_t * Cec_ComputeChoices( Gia_Man_t * pGia, Dch_Pars_t * pPars );
Alan Mishchenko committed
1381 1382 1383

    Aig_Man_t * pMan, * pTemp;
    Abc_Ntk_t * pNtkAig;
Alan Mishchenko committed
1384
    Gia_Man_t * pGia;
1385
    abctime clk;
Alan Mishchenko committed
1386 1387 1388 1389
    assert( Abc_NtkIsStrash(pNtk) );
    pMan = Abc_NtkToDar( pNtk, 0, 0 );
    if ( pMan == NULL )
        return NULL;
1390
clk = Abc_Clock();
Alan Mishchenko committed
1391
    if ( pPars->fSynthesis )
1392
        pGia = Dar_NewChoiceSynthesis( pMan, 1, 1, pPars->fPower, pPars->fLightSynth, pPars->fVerbose );
Alan Mishchenko committed
1393 1394
    else
    {
Alan Mishchenko committed
1395 1396
        pGia = Gia_ManFromAig( pMan );
        Aig_ManStop( pMan );
Alan Mishchenko committed
1397
    }
1398
pPars->timeSynth = Abc_Clock() - clk;
Alan Mishchenko committed
1399
    if ( pPars->fUseGia )
Alan Mishchenko committed
1400
        pMan = Cec_ComputeChoices( pGia, pPars );
Alan Mishchenko committed
1401
    else
Alan Mishchenko committed
1402 1403 1404 1405 1406 1407
    {
        pMan = Gia_ManToAigSkip( pGia, 3 );
        Gia_ManStop( pGia );
        pMan = Dch_ComputeChoices( pTemp = pMan, pPars );
        Aig_ManStop( pTemp );
    }
Alan Mishchenko committed
1408
    pNtkAig = Abc_NtkFromDarChoices( pNtk, pMan );
Alan Mishchenko committed
1409 1410 1411 1412 1413
    Aig_ManStop( pMan );
    return pNtkAig;
}

/**Function*************************************************************
Alan Mishchenko committed
1414 1415 1416 1417 1418 1419 1420 1421 1422 1423 1424 1425 1426 1427

  Synopsis    [Gives the current ABC network to AIG manager for processing.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Abc_Ntk_t * Abc_NtkDrwsat( Abc_Ntk_t * pNtk, int fBalance, int fVerbose )
{
    Aig_Man_t * pMan, * pTemp;
    Abc_Ntk_t * pNtkAig;
1428
    abctime clk;
Alan Mishchenko committed
1429
    assert( Abc_NtkIsStrash(pNtk) );
Alan Mishchenko committed
1430
    pMan = Abc_NtkToDar( pNtk, 0, 0 );
Alan Mishchenko committed
1431 1432 1433 1434
    if ( pMan == NULL )
        return NULL;
//    Aig_ManPrintStats( pMan );

1435
clk = Abc_Clock();
Alan Mishchenko committed
1436 1437
    pMan = Dar_ManRwsat( pTemp = pMan, fBalance, fVerbose ); 
    Aig_ManStop( pTemp );
1438
//ABC_PRT( "time", Abc_Clock() - clk );
Alan Mishchenko committed
1439 1440 1441 1442 1443 1444 1445 1446 1447 1448 1449 1450 1451 1452 1453 1454 1455 1456 1457 1458 1459 1460 1461 1462 1463 1464 1465 1466 1467 1468 1469 1470

//    Aig_ManPrintStats( pMan );
    pNtkAig = Abc_NtkFromDar( pNtk, pMan );
    Aig_ManStop( pMan );
    return pNtkAig;
}

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

  Synopsis    [Gives the current ABC network to AIG manager for processing.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Abc_Ntk_t * Abc_NtkConstructFromCnf( Abc_Ntk_t * pNtk, Cnf_Man_t * p, Vec_Ptr_t * vMapped )
{
    Abc_Ntk_t * pNtkNew;
    Abc_Obj_t * pNode, * pNodeNew;
    Aig_Obj_t * pObj, * pLeaf;
    Cnf_Cut_t * pCut;
    Vec_Int_t * vCover;
    unsigned uTruth;
    int i, k, nDupGates;
    // create the new network
    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP );
    // make the mapper point to the new network
    Aig_ManConst1(p->pManAig)->pData = Abc_NtkCreateNodeConst1(pNtkNew);
    Abc_NtkForEachCi( pNtk, pNode, i )
1471
        Aig_ManCi(p->pManAig, i)->pData = pNode->pCopy;
Alan Mishchenko committed
1472 1473
    // process the nodes in topological order
    vCover = Vec_IntAlloc( 1 << 16 );
1474
    Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i )
Alan Mishchenko committed
1475 1476 1477 1478
    {
        // create new node
        pNodeNew = Abc_NtkCreateNode( pNtkNew );
        // add fanins according to the cut
1479
        pCut = (Cnf_Cut_t *)pObj->pData;
Alan Mishchenko committed
1480
        Cnf_CutForEachLeaf( p->pManAig, pCut, pLeaf, k )
1481
            Abc_ObjAddFanin( pNodeNew, (Abc_Obj_t *)pLeaf->pData );
Alan Mishchenko committed
1482 1483 1484 1485 1486
        // add logic function
        if ( pCut->nFanins < 5 )
        {
            uTruth = 0xFFFF & *Cnf_CutTruth(pCut);
            Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vCover );
1487
            pNodeNew->pData = Abc_SopCreateFromIsop( (Mem_Flex_t *)pNtkNew->pManFunc, pCut->nFanins, vCover );
Alan Mishchenko committed
1488 1489
        }
        else
1490
            pNodeNew->pData = Abc_SopCreateFromIsop( (Mem_Flex_t *)pNtkNew->pManFunc, pCut->nFanins, pCut->vIsop[1] );
Alan Mishchenko committed
1491 1492 1493 1494 1495 1496 1497
        // save the node
        pObj->pData = pNodeNew;
    }
    Vec_IntFree( vCover );
    // add the CO drivers
    Abc_NtkForEachCo( pNtk, pNode, i )
    {
1498
        pObj = Aig_ManCo(p->pManAig, i);
1499
        pNodeNew = Abc_ObjNotCond( (Abc_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
Alan Mishchenko committed
1500 1501 1502 1503 1504 1505 1506 1507 1508 1509 1510 1511
        Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
    }

    // remove the constant node if not used
    pNodeNew = (Abc_Obj_t *)Aig_ManConst1(p->pManAig)->pData;
    if ( Abc_ObjFanoutNum(pNodeNew) == 0 )
        Abc_NtkDeleteObj( pNodeNew );
    // minimize the node
//    Abc_NtkSweep( pNtkNew, 0 );
    // decouple the PO driver nodes to reduce the number of levels
    nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
//    if ( nDupGates && If_ManReadVerbose(pIfMan) )
1512
//        Abc_Print( 1, "Duplicated %d gates to decouple the CO drivers.\n", nDupGates );
Alan Mishchenko committed
1513
    if ( !Abc_NtkCheck( pNtkNew ) )
1514
        Abc_Print( 1, "Abc_NtkConstructFromCnf(): Network check has failed.\n" );
Alan Mishchenko committed
1515 1516
    return pNtkNew;
}
Alan Mishchenko committed
1517
 
Alan Mishchenko committed
1518 1519 1520 1521 1522 1523 1524 1525 1526 1527 1528
/**Function*************************************************************

  Synopsis    [Gives the current ABC network to AIG manager for processing.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
1529
Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName, int fFastAlgo, int fChangePol, int fVerbose )
Alan Mishchenko committed
1530
{
1531
//    Vec_Ptr_t * vMapped = NULL;
Alan Mishchenko committed
1532
    Aig_Man_t * pMan;
1533
//    Cnf_Man_t * pManCnf = NULL;
Alan Mishchenko committed
1534 1535
    Cnf_Dat_t * pCnf;
    Abc_Ntk_t * pNtkNew = NULL;
1536
    abctime clk = Abc_Clock();
Alan Mishchenko committed
1537 1538 1539
    assert( Abc_NtkIsStrash(pNtk) );

    // convert to the AIG manager
Alan Mishchenko committed
1540
    pMan = Abc_NtkToDar( pNtk, 0, 0 );
Alan Mishchenko committed
1541 1542 1543 1544
    if ( pMan == NULL )
        return NULL;
    if ( !Aig_ManCheck( pMan ) )
    {
1545
        Abc_Print( 1, "Abc_NtkDarToCnf: AIG check has failed.\n" );
Alan Mishchenko committed
1546 1547 1548 1549
        Aig_ManStop( pMan );
        return NULL;
    }
    // perform balance
1550
    if ( fVerbose )
Alan Mishchenko committed
1551 1552 1553
    Aig_ManPrintStats( pMan );

    // derive CNF
1554 1555 1556 1557 1558 1559 1560 1561 1562 1563
    if ( fFastAlgo )
        pCnf = Cnf_DeriveFast( pMan, 0 );
    else
        pCnf = Cnf_Derive( pMan, 0 );

    // adjust polarity
    if ( fChangePol )
        Cnf_DataTranformPolarity( pCnf, 0 );

    // print stats
1564
//    if ( fVerbose )
1565
    {
1566
        Abc_Print( 1, "CNF stats: Vars = %6d. Clauses = %7d. Literals = %8d.   ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
1567
        Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1568
    }
Alan Mishchenko committed
1569

Alan Mishchenko committed
1570
/*
Alan Mishchenko committed
1571
    // write the network for verification
Alan Mishchenko committed
1572
    pManCnf = Cnf_ManRead();
Alan Mishchenko committed
1573 1574 1575
    vMapped = Cnf_ManScanMapping( pManCnf, 1, 0 );
    pNtkNew = Abc_NtkConstructFromCnf( pNtk, pManCnf, vMapped );
    Vec_PtrFree( vMapped );
Alan Mishchenko committed
1576
*/
Alan Mishchenko committed
1577
    // write CNF into a file
1578
    Cnf_DataWriteIntoFile( pCnf, pFileName, 0, NULL, NULL );
Alan Mishchenko committed
1579
    Cnf_DataFree( pCnf );
1580
    Cnf_ManFree();
Alan Mishchenko committed
1581 1582 1583 1584 1585 1586 1587 1588 1589 1590 1591 1592 1593 1594 1595 1596
    Aig_ManStop( pMan );
    return pNtkNew;
}


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

  Synopsis    [Solves combinational miter using a SAT solver.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
1597
int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose )
Alan Mishchenko committed
1598 1599
{
    Aig_Man_t * pMan;
1600
    int RetValue;//, clk = Abc_Clock();
Alan Mishchenko committed
1601 1602
    assert( Abc_NtkIsStrash(pNtk) );
    assert( Abc_NtkLatchNum(pNtk) == 0 );
1603
//    assert( Abc_NtkPoNum(pNtk) == 1 );
Alan Mishchenko committed
1604
    pMan = Abc_NtkToDar( pNtk, 0, 0 );
1605
    RetValue = Fra_FraigSat( pMan, nConfLimit, nInsLimit, nLearnedStart, nLearnedDelta, nLearnedPerce, fAlignPol, fAndOuts, fNewSolver, fVerbose ); 
1606
    pNtk->pModel = (int *)pMan->pData, pMan->pData = NULL;
Alan Mishchenko committed
1607 1608 1609 1610 1611 1612 1613 1614 1615 1616 1617 1618 1619 1620 1621 1622 1623 1624 1625
    Aig_ManStop( pMan );
    return RetValue;
}

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

  Synopsis    [Solves combinational miter using a SAT solver.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_NtkPartitionedSat( Abc_Ntk_t * pNtk, int nAlgo, int nPartSize, int nConfPart, int nConfTotal, int fAlignPol, int fSynthesize, int fVerbose )
{
    extern int Aig_ManPartitionedSat( Aig_Man_t * pNtk, int nAlgo, int nPartSize, int nConfPart, int nConfTotal, int fAlignPol, int fSynthesize, int fVerbose );
    Aig_Man_t * pMan;
1626
    int RetValue;//, clk = Abc_Clock();
Alan Mishchenko committed
1627 1628 1629 1630
    assert( Abc_NtkIsStrash(pNtk) );
    assert( Abc_NtkLatchNum(pNtk) == 0 );
    pMan = Abc_NtkToDar( pNtk, 0, 0 );
    RetValue = Aig_ManPartitionedSat( pMan, nAlgo, nPartSize, nConfPart, nConfTotal, fAlignPol, fSynthesize, fVerbose ); 
1631
    pNtk->pModel = (int *)pMan->pData, pMan->pData = NULL;
Alan Mishchenko committed
1632 1633 1634 1635 1636 1637 1638 1639 1640 1641 1642 1643 1644 1645 1646
    Aig_ManStop( pMan );
    return RetValue;
}

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

  Synopsis    [Gives the current ABC network to AIG manager for processing.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
1647
int Abc_NtkDarCec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int fPartition, int fVerbose )
Alan Mishchenko committed
1648 1649 1650
{
    Aig_Man_t * pMan, * pMan1, * pMan2;
    Abc_Ntk_t * pMiter;
1651
    int RetValue;
1652
    abctime clkTotal = Abc_Clock();
Alan Mishchenko committed
1653 1654 1655 1656 1657 1658 1659 1660 1661 1662 1663
/*
    {
    extern void Cec_ManVerifyTwoAigs( Aig_Man_t * pAig0, Aig_Man_t * pAig1, int fVerbose );
    Aig_Man_t * pAig0 = Abc_NtkToDar( pNtk1, 0, 0 );
    Aig_Man_t * pAig1 = Abc_NtkToDar( pNtk2, 0, 0 );
    Cec_ManVerifyTwoAigs( pAig0, pAig1, 1 );
    Aig_ManStop( pAig0 );
    Aig_ManStop( pAig1 );
    return 1;
    }
*/
Alan Mishchenko committed
1664 1665 1666
    // cannot partition if it is already a miter
    if ( pNtk2 == NULL && fPartition == 1 )
    {
1667
        Abc_Print( 1, "Abc_NtkDarCec(): Switching to non-partitioned CEC for the miter.\n" );
Alan Mishchenko committed
1668 1669 1670 1671 1672 1673
        fPartition = 0;
    }

    // if partitioning is selected, call partitioned CEC
    if ( fPartition )
    {
Alan Mishchenko committed
1674 1675
        pMan1 = Abc_NtkToDar( pNtk1, 0, 0 );
        pMan2 = Abc_NtkToDar( pNtk2, 0, 0 );
Alan Mishchenko committed
1676
        RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, nConfLimit, 100, 1, fVerbose );
Alan Mishchenko committed
1677 1678 1679 1680 1681 1682 1683 1684
        Aig_ManStop( pMan1 );
        Aig_ManStop( pMan2 );
        goto finish;
    }

    if ( pNtk2 != NULL )
    {
        // get the miter of the two networks
Alan Mishchenko committed
1685
        pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0, 0, 0 );
Alan Mishchenko committed
1686 1687
        if ( pMiter == NULL )
        {
1688
            Abc_Print( 1, "Miter computation has failed.\n" );
Alan Mishchenko committed
1689 1690 1691 1692 1693 1694 1695 1696 1697 1698 1699
            return 0;
        }
    }
    else
    {
        pMiter = Abc_NtkDup( pNtk1 );
    }
    RetValue = Abc_NtkMiterIsConstant( pMiter );
    if ( RetValue == 0 )
    {
//        extern void Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel, int nFrames );
1700
        Abc_Print( 1, "Networks are NOT EQUIVALENT after structural hashing.\n" );
Alan Mishchenko committed
1701 1702 1703 1704 1705
        // report the error
        if ( pNtk2 == NULL )
            pNtk1->pModel = Abc_NtkVerifyGetCleanModel( pNtk1, 1 );
//        pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, nFrames );
//        Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pMiter->pModel, nFrames );
Alan Mishchenko committed
1706
//        ABC_FREE( pMiter->pModel );
Alan Mishchenko committed
1707 1708 1709 1710 1711 1712
        Abc_NtkDelete( pMiter );
        return 0;
    }
    if ( RetValue == 1 )
    {
        Abc_NtkDelete( pMiter );
1713
        Abc_Print( 1, "Networks are equivalent after structural hashing.\n" );
Alan Mishchenko committed
1714 1715 1716 1717
        return 1;
    }

    // derive the AIG manager
Alan Mishchenko committed
1718
    pMan = Abc_NtkToDar( pMiter, 0, 0 );
Alan Mishchenko committed
1719 1720 1721
    Abc_NtkDelete( pMiter );
    if ( pMan == NULL )
    {
1722
        Abc_Print( 1, "Converting miter into AIG has failed.\n" );
Alan Mishchenko committed
1723 1724 1725
        return -1;
    }
    // perform verification
Alan Mishchenko committed
1726
    RetValue = Fra_FraigCec( &pMan, 100000, fVerbose );
Alan Mishchenko committed
1727 1728
    // transfer model if given
    if ( pNtk2 == NULL )
1729
        pNtk1->pModel = (int *)pMan->pData, pMan->pData = NULL;
Alan Mishchenko committed
1730 1731 1732 1733 1734 1735
    Aig_ManStop( pMan );

finish:
    // report the miter
    if ( RetValue == 1 )
    {
1736
        Abc_Print( 1, "Networks are equivalent.   " );
1737
ABC_PRT( "Time", Abc_Clock() - clkTotal );
Alan Mishchenko committed
1738 1739 1740
    }
    else if ( RetValue == 0 )
    {
1741
        Abc_Print( 1, "Networks are NOT EQUIVALENT.   " );
1742
ABC_PRT( "Time", Abc_Clock() - clkTotal );
Alan Mishchenko committed
1743 1744 1745
    }
    else
    {
1746
        Abc_Print( 1, "Networks are UNDECIDED.   " );
1747
ABC_PRT( "Time", Abc_Clock() - clkTotal );
Alan Mishchenko committed
1748 1749 1750 1751 1752 1753 1754 1755 1756 1757 1758 1759 1760 1761 1762 1763
    }
    fflush( stdout );
    return RetValue;
}

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

  Synopsis    [Gives the current ABC network to AIG manager for processing.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
1764
Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, Fra_Ssw_t * pPars )
Alan Mishchenko committed
1765 1766
{
    Fraig_Params_t Params;
Alan Mishchenko committed
1767
    Abc_Ntk_t * pNtkAig = NULL, * pNtkFraig;
Alan Mishchenko committed
1768
    Aig_Man_t * pMan, * pTemp;
1769
    abctime clk = Abc_Clock();
Alan Mishchenko committed
1770 1771 1772 1773 1774 1775

    // preprocess the miter by fraiging it
    // (note that for each functional class, fraiging leaves one representative;
    // so fraiging does not reduce the number of functions represented by nodes
    Fraig_ParamsSetDefault( &Params );
    Params.nBTLimit = 100000;
Alan Mishchenko committed
1776 1777
    if ( pPars->fFraiging && pPars->nPartSize == 0 )
    {
Alan Mishchenko committed
1778
        pNtkFraig = Abc_NtkFraig( pNtk, &Params, 0, 0 );
Alan Mishchenko committed
1779
if ( pPars->fVerbose ) 
Alan Mishchenko committed
1780
{
1781
ABC_PRT( "Initial fraiging time", Abc_Clock() - clk );
Alan Mishchenko committed
1782
}
Alan Mishchenko committed
1783 1784 1785
    }
    else
        pNtkFraig = Abc_NtkDup( pNtk );
Alan Mishchenko committed
1786

Alan Mishchenko committed
1787
    pMan = Abc_NtkToDar( pNtkFraig, 0, 1 );
Alan Mishchenko committed
1788 1789 1790 1791
    Abc_NtkDelete( pNtkFraig );
    if ( pMan == NULL )
        return NULL;

Alan Mishchenko committed
1792
//    pPars->TimeLimit = 5.0;
Alan Mishchenko committed
1793
    pMan = Fra_FraigInduction( pTemp = pMan, pPars );
Alan Mishchenko committed
1794
    Aig_ManStop( pTemp );
Alan Mishchenko committed
1795
    if ( pMan )
Alan Mishchenko committed
1796
    {
Alan Mishchenko committed
1797 1798 1799 1800 1801 1802 1803 1804 1805 1806 1807
        if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) )
            pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
        else
        {
            Abc_Obj_t * pObj;
            int i;
            pNtkAig = Abc_NtkFromDar( pNtk, pMan );
            Abc_NtkForEachLatch( pNtkAig, pObj, i )
                Abc_LatchSetInit0( pObj );
        }
        Aig_ManStop( pMan );
Alan Mishchenko committed
1808 1809 1810 1811 1812 1813
    }
    return pNtkAig;
}

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

Alan Mishchenko committed
1814 1815 1816 1817 1818 1819 1820 1821 1822 1823 1824
  Synopsis    [Print Latch Equivalence Classes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_NtkPrintLatchEquivClasses( Abc_Ntk_t * pNtk, Aig_Man_t * pAig )
{
1825
    int header_dumped = 0;
Alan Mishchenko committed
1826
    int num_orig_latches = Abc_NtkLatchNum(pNtk);
Alan Mishchenko committed
1827
    char **pNames = ABC_ALLOC( char *, num_orig_latches );
1828
    int *p_irrelevant = ABC_ALLOC( int, num_orig_latches );
Alan Mishchenko committed
1829 1830 1831 1832 1833 1834 1835 1836 1837
    char * pFlopName, * pReprName;
    Aig_Obj_t * pFlop, * pRepr;
    Abc_Obj_t * pNtkFlop; 
    int repr_idx;
    int i;

    Abc_NtkForEachLatch( pNtk, pNtkFlop, i )
    {
        char *temp_name = Abc_ObjName( Abc_ObjFanout0(pNtkFlop) );
Alan Mishchenko committed
1838
        pNames[i] = ABC_ALLOC( char , strlen(temp_name)+1);
Alan Mishchenko committed
1839 1840 1841 1842
        strcpy(pNames[i], temp_name);
    }
    i = 0;
    
1843
    Aig_ManSetCioIds( pAig );
Alan Mishchenko committed
1844 1845 1846 1847 1848 1849 1850 1851 1852 1853
    Saig_ManForEachLo( pAig, pFlop, i )
    {
        p_irrelevant[i] = false;
        
        pFlopName = pNames[i];

        pRepr = Aig_ObjRepr(pAig, pFlop);

        if ( pRepr == NULL )
        {
1854
            // Abc_Print( 1, "Nothing equivalent to flop %s\n", pFlopName);
Alan Mishchenko committed
1855
//            p_irrelevant[i] = true;
Alan Mishchenko committed
1856 1857 1858 1859 1860
            continue;
        }

        if (!header_dumped)
        {
1861
            Abc_Print( 1, "Here are the flop equivalences:\n");
Alan Mishchenko committed
1862 1863 1864 1865 1866 1867
            header_dumped = true;
        }

        // pRepr is representative of the equivalence class, to which pFlop belongs
        if ( Aig_ObjIsConst1(pRepr) )
        {
1868 1869
            Abc_Print( 1, "Original flop %s is proved equivalent to constant.\n", pFlopName );
            // Abc_Print( 1, "Original flop # %d is proved equivalent to constant.\n", i );
Alan Mishchenko committed
1870 1871 1872 1873
            continue;
        }

        assert( Saig_ObjIsLo( pAig, pRepr ) );
1874
        repr_idx = Aig_ObjCioId(pRepr) - Saig_ManPiNum(pAig);
Alan Mishchenko committed
1875
        pReprName = pNames[repr_idx];
1876 1877
        Abc_Print( 1, "Original flop %s is proved equivalent to flop %s.\n",  pFlopName, pReprName );
        // Abc_Print( 1, "Original flop # %d is proved equivalent to flop # %d.\n",  i, repr_idx );
Alan Mishchenko committed
1878 1879 1880 1881 1882 1883 1884 1885 1886
    }

    header_dumped = false;
    for (i=0; i<num_orig_latches; ++i)
    {
        if (p_irrelevant[i])
        {
            if (!header_dumped)
            {
1887
                Abc_Print( 1, "The following flops have been deemed irrelevant:\n");
Alan Mishchenko committed
1888 1889
                header_dumped = true;
            }
1890
            Abc_Print( 1, "%s ", pNames[i]);
Alan Mishchenko committed
1891 1892
        }
        
Alan Mishchenko committed
1893
        ABC_FREE(pNames[i]);
Alan Mishchenko committed
1894 1895
    }
    if (header_dumped)
1896
        Abc_Print( 1, "\n");
Alan Mishchenko committed
1897
    
Alan Mishchenko committed
1898 1899
    ABC_FREE(pNames);
    ABC_FREE(p_irrelevant);
Alan Mishchenko committed
1900 1901 1902 1903
}

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

Alan Mishchenko committed
1904 1905 1906 1907 1908 1909 1910 1911 1912 1913 1914 1915 1916 1917 1918 1919 1920 1921 1922
  Synopsis    [Gives the current ABC network to AIG manager for processing.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Abc_Ntk_t * Abc_NtkDarSeqSweep2( Abc_Ntk_t * pNtk, Ssw_Pars_t * pPars )
{
    Abc_Ntk_t * pNtkAig;
    Aig_Man_t * pMan, * pTemp;

    pMan = Abc_NtkToDar( pNtk, 0, 1 );
    if ( pMan == NULL )
        return NULL;

    pMan = Ssw_SignalCorrespondence( pTemp = pMan, pPars );
Alan Mishchenko committed
1923 1924 1925 1926

    if ( pPars->fFlopVerbose )
        Abc_NtkPrintLatchEquivClasses(pNtk, pTemp);

1927
    Aig_ManStop( pTemp );
Alan Mishchenko committed
1928 1929 1930 1931 1932 1933 1934 1935 1936 1937 1938 1939 1940 1941 1942 1943 1944 1945 1946
    if ( pMan == NULL )
        return NULL;

    if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) )
        pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
    else
    {
        Abc_Obj_t * pObj;
        int i;
        pNtkAig = Abc_NtkFromDar( pNtk, pMan );
        Abc_NtkForEachLatch( pNtkAig, pObj, i )
            Abc_LatchSetInit0( pObj );
    }
    Aig_ManStop( pMan );
    return pNtkAig;
}

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

Alan Mishchenko committed
1947 1948
  Synopsis    [Computes latch correspondence.]

Alan Mishchenko committed
1949
  Description [] 
Alan Mishchenko committed
1950 1951 1952 1953 1954 1955 1956 1957 1958
               
  SideEffects []

  SeeAlso     []
 
***********************************************************************/
Abc_Ntk_t * Abc_NtkDarLcorr( Abc_Ntk_t * pNtk, int nFramesP, int nConfMax, int fVerbose )
{
    Aig_Man_t * pMan, * pTemp;
Alan Mishchenko committed
1959
    Abc_Ntk_t * pNtkAig = NULL;
Alan Mishchenko committed
1960
    pMan = Abc_NtkToDar( pNtk, 0, 1 );
Alan Mishchenko committed
1961 1962
    if ( pMan == NULL )
        return NULL;
Alan Mishchenko committed
1963
    pMan = Fra_FraigLatchCorrespondence( pTemp = pMan, nFramesP, nConfMax, 0, fVerbose, NULL, 0.0 );
Alan Mishchenko committed
1964
    Aig_ManStop( pTemp );
Alan Mishchenko committed
1965
    if ( pMan )
Alan Mishchenko committed
1966
    {
Alan Mishchenko committed
1967 1968 1969 1970 1971 1972 1973 1974 1975 1976 1977
        if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) )
            pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
        else
        {
            Abc_Obj_t * pObj;
            int i;
            pNtkAig = Abc_NtkFromDar( pNtk, pMan );
            Abc_NtkForEachLatch( pNtkAig, pObj, i )
                Abc_LatchSetInit0( pObj );
        }
        Aig_ManStop( pMan );
Alan Mishchenko committed
1978 1979 1980 1981 1982 1983
    }
    return pNtkAig;
}

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

Alan Mishchenko committed
1984 1985 1986 1987 1988 1989 1990 1991 1992 1993 1994 1995 1996 1997 1998 1999 2000 2001 2002 2003 2004 2005 2006 2007 2008 2009 2010 2011 2012 2013 2014 2015 2016 2017 2018 2019 2020 2021 2022 2023 2024
  Synopsis    [Computes latch correspondence.]

  Description [] 
               
  SideEffects []

  SeeAlso     []
 
***********************************************************************/
Abc_Ntk_t * Abc_NtkDarLcorrNew( Abc_Ntk_t * pNtk, int nVarsMax, int nConfMax, int fVerbose )
{
    Ssw_Pars_t Pars, * pPars = &Pars;
    Aig_Man_t * pMan, * pTemp;
    Abc_Ntk_t * pNtkAig = NULL;
    pMan = Abc_NtkToDar( pNtk, 0, 1 );
    if ( pMan == NULL )
        return NULL;
    Ssw_ManSetDefaultParams( pPars );
    pPars->fLatchCorrOpt = 1;
    pPars->nBTLimit      = nConfMax;
    pPars->nSatVarMax    = nVarsMax;
    pPars->fVerbose      = fVerbose;
    pMan = Ssw_SignalCorrespondence( pTemp = pMan, pPars );
    Aig_ManStop( pTemp );
    if ( pMan )
    {
        if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) )
            pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
        else
        {
            Abc_Obj_t * pObj;
            int i;
            pNtkAig = Abc_NtkFromDar( pNtk, pMan );
            Abc_NtkForEachLatch( pNtkAig, pObj, i )
                Abc_LatchSetInit0( pObj );
        }
        Aig_ManStop( pMan );
    }
    return pNtkAig;
}

Alan Mishchenko committed
2025 2026
/*
#include <signal.h>
2027
#include "misc/util/utilMem.h"
Alan Mishchenko committed
2028 2029 2030
static void sigfunc( int signo ) 
{
    if (signo == SIGINT) {
2031
        Abc_Print( 1, "SIGINT received!\n");
Alan Mishchenko committed
2032 2033 2034 2035 2036
        s_fInterrupt = 1;
    }
}
*/

Alan Mishchenko committed
2037 2038
/**Function*************************************************************

Alan Mishchenko committed
2039 2040 2041 2042 2043 2044 2045 2046 2047
  Synopsis    [Gives the current ABC network to AIG manager for processing.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
2048
int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nStart, int nFrames, int nSizeMax, int nNodeDelta, int nTimeOut, int nBTLimit, int nBTLimitAll, int fRewrite, int fNewAlgo, int fOrDecomp, int nCofFanLit, int fVerbose, int * piFrames )
Alan Mishchenko committed
2049 2050
{
    Aig_Man_t * pMan;
2051
    Vec_Int_t * vMap = NULL;
2052
    int status, RetValue = -1;
2053 2054
    abctime clk = Abc_Clock();
    abctime nTimeLimit = nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
Alan Mishchenko committed
2055
    // derive the AIG manager
2056 2057 2058 2059
    if ( fOrDecomp )
        pMan = Abc_NtkToDarBmc( pNtk, &vMap );
    else
        pMan = Abc_NtkToDar( pNtk, 0, 1 );
Alan Mishchenko committed
2060 2061
    if ( pMan == NULL )
    {
2062
        Abc_Print( 1, "Converting miter into AIG has failed.\n" );
Alan Mishchenko committed
2063
        return RetValue;
Alan Mishchenko committed
2064 2065
    }
    assert( pMan->nRegs > 0 );
2066
    assert( vMap == NULL || Vec_IntSize(vMap) == Saig_ManPoNum(pMan) );
2067
    if ( fVerbose && vMap && Abc_NtkPoNum(pNtk) != Saig_ManPoNum(pMan) ) 
2068
        Abc_Print( 1, "Expanded %d outputs into %d outputs using OR decomposition.\n", Abc_NtkPoNum(pNtk), Saig_ManPoNum(pMan) );
2069

Alan Mishchenko committed
2070
    // perform verification
2071
    if ( fNewAlgo ) // command 'bmc'
Alan Mishchenko committed
2072
    {
Alan Mishchenko committed
2073
        int iFrame;
Alan Mishchenko committed
2074
        RetValue = Saig_ManBmcSimple( pMan, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, &iFrame, nCofFanLit );
2075 2076
        if ( piFrames )
            *piFrames = iFrame;
Alan Mishchenko committed
2077 2078
        ABC_FREE( pNtk->pModel );
        ABC_FREE( pNtk->pSeqModel );
Alan Mishchenko committed
2079
        pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
Alan Mishchenko committed
2080
        if ( RetValue == 1 )
2081
            Abc_Print( 1, "Incorrect return value.  " );
Alan Mishchenko committed
2082
        else if ( RetValue == -1 )
2083
        {
2084
            Abc_Print( 1, "No output asserted in %d frames. Resource limit reached ", Abc_MaxInt(iFrame+1,0) );
2085
            if ( nTimeLimit && Abc_Clock() > nTimeLimit )
2086
                Abc_Print( 1, "(timeout %d sec). ", nTimeLimit );
2087
            else
2088
                Abc_Print( 1, "(conf limit %d). ", nBTLimit );
2089
        }
Alan Mishchenko committed
2090 2091
        else // if ( RetValue == 0 )
        {
2092
            Abc_Cex_t * pCex = pNtk->pSeqModel;
2093
            Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pCex->iPo, pNtk->pName, pCex->iFrame );
Alan Mishchenko committed
2094
        }
2095
ABC_PRT( "Time", Abc_Clock() - clk );
Alan Mishchenko committed
2096 2097
    }
    else
2098
    { 
2099
        RetValue = Saig_BmcPerform( pMan, nStart, nFrames, nNodeDelta, nTimeOut, nBTLimit, nBTLimitAll, fVerbose, 0, piFrames, 0 );
Alan Mishchenko committed
2100 2101
        ABC_FREE( pNtk->pModel );
        ABC_FREE( pNtk->pSeqModel );
Alan Mishchenko committed
2102
        pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
Alan Mishchenko committed
2103
    }
Alan Mishchenko committed
2104 2105 2106
    // verify counter-example
    if ( pNtk->pSeqModel ) 
    {
2107
        status = Saig_ManVerifyCex( pMan, pNtk->pSeqModel );
Alan Mishchenko committed
2108
        if ( status == 0 )
2109
            Abc_Print( 1, "Abc_NtkDarBmc(): Counter-example verification has FAILED.\n" );
Alan Mishchenko committed
2110
    }
Alan Mishchenko committed
2111
    Aig_ManStop( pMan );
2112 2113 2114
    // update the counter-example
    if ( pNtk->pSeqModel && vMap )
        pNtk->pSeqModel->iPo = Vec_IntEntry( vMap, pNtk->pSeqModel->iPo );
2115
    Vec_IntFreeP( &vMap );
Alan Mishchenko committed
2116
    return RetValue;
Alan Mishchenko committed
2117 2118 2119 2120
}

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

2121 2122 2123 2124 2125 2126 2127 2128 2129
  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
2130
int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars, int fOrDecomp )
2131 2132
{
    Aig_Man_t * pMan;
2133
    Vec_Int_t * vMap = NULL;
2134
    int status, RetValue = -1;
2135 2136
    abctime clk = Abc_Clock();
    abctime nTimeOut = pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
2137
    if ( fOrDecomp && !pPars->fSolveAll )
2138
        pMan = Abc_NtkToDarBmc( pNtk, &vMap );
2139 2140
    else
        pMan = Abc_NtkToDar( pNtk, 0, 1 );
2141 2142
    if ( pMan == NULL )
    {
2143
        Abc_Print( 1, "Converting miter into AIG has failed.\n" );
2144 2145 2146
        return RetValue;
    }
    assert( pMan->nRegs > 0 );
2147
    if ( pPars->fVerbose && vMap && Abc_NtkPoNum(pNtk) != Saig_ManPoNum(pMan) ) 
2148
        Abc_Print( 1, "Expanded %d outputs into %d outputs using OR decomposition.\n", Abc_NtkPoNum(pNtk), Saig_ManPoNum(pMan) );
2149

2150 2151 2152 2153
    RetValue = Saig_ManBmcScalable( pMan, pPars );
    ABC_FREE( pNtk->pModel );
    ABC_FREE( pNtk->pSeqModel );
    pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
2154
    if ( !pPars->fSilent )
2155
    {
2156
        if ( RetValue == 1 )
2157
        {
2158
            Abc_Print( 1, "Explored all reachable states after completing %d frames.  ", 1<<Aig_ManRegNum(pMan) );
2159
        }
2160
        else if ( RetValue == -1 )
2161
        {
2162 2163
            if ( pPars->nFailOuts == 0 )
            {
2164
                Abc_Print( 1, "No output asserted in %d frames. Resource limit reached ", Abc_MaxInt(pPars->iFrame+1,0) );
2165 2166 2167 2168 2169
                if ( nTimeOut && Abc_Clock() > nTimeOut )
                    Abc_Print( 1, "(timeout %d sec). ", pPars->nTimeOut );
                else
                    Abc_Print( 1, "(conf limit %d). ", pPars->nConfLimit );
            }
2170
            else
2171 2172 2173 2174 2175 2176 2177
            {
                Abc_Print( 1, "The total of %d outputs asserted in %d frames. Resource limit reached ", pPars->nFailOuts, pPars->iFrame );
                if ( Abc_Clock() > nTimeOut )
                    Abc_Print( 1, "(timeout %d sec). ", pPars->nTimeOut );
                else
                    Abc_Print( 1, "(conf limit %d). ", pPars->nConfLimit );
            }
2178
        }
2179
        else // if ( RetValue == 0 )
2180
        {
2181 2182 2183 2184 2185
            if ( !pPars->fSolveAll )
            {
                Abc_Cex_t * pCex = pNtk->pSeqModel;
                Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pCex->iPo, pNtk->pName, pCex->iFrame );
            }
Alan Mishchenko committed
2186
            else
2187
            {
2188 2189
                int nOutputs = Saig_ManPoNum(pMan) - Saig_ManConstrNum(pMan);
                if ( pMan->vSeqModelVec == NULL || Vec_PtrCountZero(pMan->vSeqModelVec) == nOutputs )
2190
                    Abc_Print( 1, "None of the %d outputs is found to be SAT", nOutputs );
2191
                else if ( Vec_PtrCountZero(pMan->vSeqModelVec) == 0 )
2192
                    Abc_Print( 1, "All %d outputs are found to be SAT", nOutputs );
2193 2194 2195 2196 2197 2198
                else
                {
                    Abc_Print( 1, "Some outputs are SAT (%d out of %d)", nOutputs - Vec_PtrCountZero(pMan->vSeqModelVec), nOutputs );
                    if ( pPars->nDropOuts )
                        Abc_Print( 1, " while others timed out (%d out of %d)", pPars->nDropOuts, nOutputs );
                }
2199 2200
                Abc_Print( 1, " after %d frames", pPars->iFrame );
                Abc_Print( 1, ".   " );
2201
            }
2202
        }
2203 2204 2205 2206 2207 2208 2209
        ABC_PRT( "Time", Abc_Clock() - clk );
    }
    if ( RetValue == 0 && pPars->fSolveAll )
    {
        if ( pNtk->vSeqModelVec )
            Vec_PtrFreeFree( pNtk->vSeqModelVec );
        pNtk->vSeqModelVec = pMan->vSeqModelVec;  pMan->vSeqModelVec = NULL;
2210 2211 2212
    }
    if ( pNtk->pSeqModel ) 
    {
2213
        status = Saig_ManVerifyCex( pMan, pNtk->pSeqModel );
2214
        if ( status == 0 )
2215
            Abc_Print( 1, "Abc_NtkDarBmc3(): Counter-example verification has FAILED.\n" );
2216 2217
    }
    Aig_ManStop( pMan );
2218 2219 2220
    // update the counter-example
    if ( pNtk->pSeqModel && vMap )
        pNtk->pSeqModel->iPo = Vec_IntEntry( vMap, pNtk->pSeqModel->iPo );
2221
    Vec_IntFreeP( &vMap );
2222 2223 2224 2225 2226
    return RetValue;
}

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

Alan Mishchenko committed
2227 2228 2229 2230 2231 2232 2233 2234 2235
  Synopsis    [Gives the current ABC network to AIG manager for processing.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
2236
int Abc_NtkDarBmcInter_int( Aig_Man_t * pMan, Inter_ManParams_t * pPars, Aig_Man_t ** ppNtkRes )
Alan Mishchenko committed
2237
{
2238
    int RetValue = -1, iFrame;
2239
    abctime clk = Abc_Clock();
2240
    int nTotalProvedSat = 0;
Alan Mishchenko committed
2241
    assert( pMan->nRegs > 0 );
2242 2243
    if ( ppNtkRes )
        *ppNtkRes = NULL;
Alan Mishchenko committed
2244
    if ( pPars->fUseSeparate )
Alan Mishchenko committed
2245
    {
Alan Mishchenko committed
2246 2247 2248 2249 2250 2251 2252
        Aig_Man_t * pTemp, * pAux;
        Aig_Obj_t * pObjPo;
        int i, Counter = 0;
        Saig_ManForEachPo( pMan, pObjPo, i )
        {
            if ( Aig_ObjFanin0(pObjPo) == Aig_ManConst1(pMan) )
                continue;
2253
            if ( pPars->fVerbose )
2254
                Abc_Print( 1, "Solving output %2d (out of %2d):\n", i, Saig_ManPoNum(pMan) );
Alan Mishchenko committed
2255
            pTemp = Aig_ManDupOneOutput( pMan, i, 1 );
2256
            pTemp = Aig_ManScl( pAux = pTemp, 1, 1, 0, -1, -1, 0, 0 );
Alan Mishchenko committed
2257
            Aig_ManStop( pAux );
2258 2259 2260
            if ( Aig_ManRegNum(pTemp) == 0 )
            {
                pTemp->pSeqModel = NULL;
2261
                RetValue = Fra_FraigSat( pTemp, pPars->nBTLimit, 0, 0, 0, 0, 0, 0, 0, 0 ); 
2262
                if ( pTemp->pData )
2263
                    pTemp->pSeqModel = Abc_CexCreate( Aig_ManRegNum(pMan), Saig_ManPiNum(pMan), (int *)pTemp->pData, 0, i, 1 );
2264 2265 2266 2267
//                pNtk->pModel = pTemp->pData, pTemp->pData = NULL;
            }
            else
                RetValue = Inter_ManPerformInterpolation( pTemp, pPars, &iFrame );
Alan Mishchenko committed
2268 2269
            if ( pTemp->pSeqModel )
            {
2270 2271
                if ( pPars->fDropSatOuts )
                {
2272
                    Abc_Print( 1, "Output %d proved SAT in frame %d (replacing by const 0 and continuing...)\n", i, pTemp->pSeqModel->iFrame );
2273 2274 2275 2276 2277 2278 2279 2280 2281 2282 2283 2284 2285
                    Aig_ObjPatchFanin0( pMan, pObjPo, Aig_ManConst0(pMan) );
                    Aig_ManStop( pTemp );
                    nTotalProvedSat++;
                    continue;
                }
                else
                {
                    Abc_Cex_t * pCex;
                    pCex = pMan->pSeqModel = pTemp->pSeqModel; pTemp->pSeqModel = NULL;
                    pCex->iPo = i;
                    Aig_ManStop( pTemp );
                    break;
                }
Alan Mishchenko committed
2286 2287 2288 2289 2290
            }
            // if solved, remove the output
            if ( RetValue == 1 )
            {
                Aig_ObjPatchFanin0( pMan, pObjPo, Aig_ManConst0(pMan) );
2291
//                    Abc_Print( 1, "Output %3d : Solved ", i );
Alan Mishchenko committed
2292 2293 2294 2295
            }
            else
            {
                Counter++;
2296
//                    Abc_Print( 1, "Output %3d : Undec  ", i );
Alan Mishchenko committed
2297 2298 2299
            }
//                Aig_ManPrintStats( pTemp );
            Aig_ManStop( pTemp );
2300
            Abc_Print( 1, "Solving output %3d (out of %3d) using interpolation.\r", i, Saig_ManPoNum(pMan) );
Alan Mishchenko committed
2301 2302 2303 2304
        }
        Aig_ManCleanup( pMan );
        if ( pMan->pSeqModel == NULL )
        {
2305
            Abc_Print( 1, "Interpolation left %d (out of %d) outputs unsolved              \n", Counter, Saig_ManPoNum(pMan) );
Alan Mishchenko committed
2306 2307 2308
            if ( Counter )
                RetValue = -1;
        }
2309 2310 2311
        if ( ppNtkRes )
        {
            pTemp = Aig_ManDupUnsolvedOutputs( pMan, 1 );
2312
            *ppNtkRes = Aig_ManScl( pTemp, 1, 1, 0, -1, -1, 0, 0 );
2313 2314
            Aig_ManStop( pTemp );
        }
Alan Mishchenko committed
2315 2316 2317 2318
    }
    else
    {    
        RetValue = Inter_ManPerformInterpolation( pMan, pPars, &iFrame );
Alan Mishchenko committed
2319
    }
2320
    if ( nTotalProvedSat )
2321
        Abc_Print( 1, "The total of %d outputs proved SAT and replaced by const 0 in this run.\n", nTotalProvedSat );
Alan Mishchenko committed
2322
    if ( RetValue == 1 )
2323
        Abc_Print( 1, "Property proved.  " );
Alan Mishchenko committed
2324
    else if ( RetValue == 0 )
2325
        Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d.  ", pMan->pSeqModel ? pMan->pSeqModel->iPo : -1, pMan->pName, iFrame );
Alan Mishchenko committed
2326
    else if ( RetValue == -1 )
2327
        Abc_Print( 1, "Property UNDECIDED.  " );
Alan Mishchenko committed
2328 2329
    else
        assert( 0 );
2330
ABC_PRT( "Time", Abc_Clock() - clk );
Alan Mishchenko committed
2331 2332 2333 2334 2335 2336 2337 2338 2339 2340 2341 2342 2343 2344
    return RetValue;
}

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

  Synopsis    [Gives the current ABC network to AIG manager for processing.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
2345
int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, Inter_ManParams_t * pPars, Abc_Ntk_t ** ppNtkRes )
Alan Mishchenko committed
2346 2347
{
    Aig_Man_t * pMan;
2348 2349 2350
    int RetValue;
    if ( ppNtkRes )
        *ppNtkRes = NULL;
Alan Mishchenko committed
2351 2352 2353
    pMan = Abc_NtkToDar( pNtk, 0, 1 );
    if ( pMan == NULL )
    {
2354
        Abc_Print( 1, "Converting miter into AIG has failed.\n" );
Alan Mishchenko committed
2355 2356
        return -1;
    }
2357 2358 2359 2360 2361 2362 2363 2364 2365 2366 2367
    if ( pPars->fUseSeparate && ppNtkRes )
    {
        Aig_Man_t * pManNew;
        RetValue = Abc_NtkDarBmcInter_int( pMan, pPars, &pManNew );
        *ppNtkRes = Abc_NtkFromAigPhase( pManNew );
        Aig_ManStop( pManNew );
    }
    else
    {
        RetValue = Abc_NtkDarBmcInter_int( pMan, pPars, NULL );
    }
Alan Mishchenko committed
2368 2369 2370
    ABC_FREE( pNtk->pModel );
    ABC_FREE( pNtk->pSeqModel );
    pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
Alan Mishchenko committed
2371
    Aig_ManStop( pMan );
2372
    return RetValue;
Alan Mishchenko committed
2373 2374 2375 2376 2377 2378 2379 2380 2381 2382 2383 2384 2385
}

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

  Synopsis    [Gives the current ABC network to AIG manager for processing.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
2386 2387
int Abc_NtkDarDemiter( Abc_Ntk_t * pNtk )
{ 
2388
    char * pFileNameGeneric, pFileName0[1000], pFileName1[1000];
Alan Mishchenko committed
2389
    Aig_Man_t * pMan, * pPart0, * pPart1;//, * pMiter;
Alan Mishchenko committed
2390 2391 2392 2393
    // derive the AIG manager
    pMan = Abc_NtkToDar( pNtk, 0, 1 );
    if ( pMan == NULL )
    {
2394
        Abc_Print( 1, "Converting network into AIG has failed.\n" );
Alan Mishchenko committed
2395 2396
        return 0;
    }
Alan Mishchenko committed
2397 2398
//    if ( !Saig_ManDemiterSimple( pMan, &pPart0, &pPart1 ) )
    if ( !Saig_ManDemiterSimpleDiff( pMan, &pPart0, &pPart1 ) )
Alan Mishchenko committed
2399
    {
2400
        Aig_ManStop( pMan );
2401
        Abc_Print( 1, "Demitering has failed.\n" );
Alan Mishchenko committed
2402 2403
        return 0;
    }
2404
    // create file names
2405
    pFileNameGeneric = Extra_FileNameGeneric( pNtk->pSpec ? pNtk->pSpec : pNtk->pName );
2406 2407 2408 2409
//    sprintf( pFileName0,  "%s%s",  pFileNameGeneric, "_part0.aig" ); 
//    sprintf( pFileName1,  "%s%s",  pFileNameGeneric, "_part1.aig" ); 
    sprintf( pFileName0,  "%s",  "part0.aig" ); 
    sprintf( pFileName1,  "%s",  "part1.aig" ); 
2410 2411 2412 2413
    ABC_FREE( pFileNameGeneric );
    // dump files
    Ioa_WriteAiger( pPart0, pFileName0, 0, 0 );
    Ioa_WriteAiger( pPart1, pFileName1, 0, 0 );
2414
    Abc_Print( 1, "Demitering produced two files \"%s\" and \"%s\".\n", pFileName0, pFileName1 );
2415 2416 2417 2418
    // create two-level miter
//    pMiter = Saig_ManCreateMiterTwo( pPart0, pPart1, 2 );
//    Aig_ManDumpBlif( pMiter, "miter01.blif", NULL, NULL );
//    Aig_ManStop( pMiter );
2419
//    Abc_Print( 1, "The new miter is written into file \"%s\".\n", "miter01.blif" );
2420 2421 2422 2423 2424 2425 2426 2427 2428 2429 2430 2431 2432 2433 2434 2435 2436 2437 2438 2439 2440 2441 2442 2443 2444
    Aig_ManStop( pPart0 );
    Aig_ManStop( pPart1 );
    Aig_ManStop( pMan );
    return 1;
} 

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

  Synopsis    [Gives the current ABC network to AIG manager for processing.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_NtkDarDemiterNew( Abc_Ntk_t * pNtk )
{ 
    char * pFileNameGeneric, pFileName0[1000], pFileName1[1000];
    Aig_Man_t * pMan, * pPart0, * pPart1;//, * pMiter;
    // derive the AIG manager
    pMan = Abc_NtkToDar( pNtk, 0, 1 );
    if ( pMan == NULL )
    {
2445
        Abc_Print( 1, "Converting network into AIG has failed.\n" );
2446 2447 2448 2449 2450 2451 2452 2453 2454 2455
        return 0;
    }

    Saig_ManDemiterNew( pMan );
    Aig_ManStop( pMan );
    return 1;

//    if ( !Saig_ManDemiterSimple( pMan, &pPart0, &pPart1 ) )
    if ( !Saig_ManDemiterSimpleDiff( pMan, &pPart0, &pPart1 ) )
    {
2456
        Abc_Print( 1, "Demitering has failed.\n" );
2457 2458 2459 2460 2461 2462 2463 2464 2465 2466
        return 0;
    }
    // create file names
    pFileNameGeneric = Extra_FileNameGeneric( pNtk->pSpec );
    sprintf( pFileName0,  "%s%s",  pFileNameGeneric, "_part0.aig" ); 
    sprintf( pFileName1,  "%s%s",  pFileNameGeneric, "_part1.aig" ); 
    ABC_FREE( pFileNameGeneric );
    // dump files
    Ioa_WriteAiger( pPart0, pFileName0, 0, 0 );
    Ioa_WriteAiger( pPart1, pFileName1, 0, 0 );
2467
    Abc_Print( 1, "Demitering produced two files \"%s\" and \"%s\".\n", pFileName0, pFileName1 );
Alan Mishchenko committed
2468
    // create two-level miter
Alan Mishchenko committed
2469 2470 2471
//    pMiter = Saig_ManCreateMiterTwo( pPart0, pPart1, 2 );
//    Aig_ManDumpBlif( pMiter, "miter01.blif", NULL, NULL );
//    Aig_ManStop( pMiter );
2472
//    Abc_Print( 1, "The new miter is written into file \"%s\".\n", "miter01.blif" );
Alan Mishchenko committed
2473 2474 2475 2476
    Aig_ManStop( pPart0 );
    Aig_ManStop( pPart1 );
    Aig_ManStop( pMan );
    return 1;
Alan Mishchenko committed
2477
} 
2478 2479 2480 2481 2482 2483 2484 2485 2486 2487 2488 2489 2490 2491 2492 2493 2494 2495

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

  Synopsis    [Gives the current ABC network to AIG manager for processing.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_NtkDarDemiterDual( Abc_Ntk_t * pNtk, int fVerbose )
{ 
    char * pFileNameGeneric, pFileName0[1000], pFileName1[1000];
    Aig_Man_t * pMan, * pPart0, * pPart1;//, * pMiter;
    if ( (Abc_NtkPoNum(pNtk) & 1) )
    {
2496
        Abc_Print( 1, "The number of POs should be even.\n" );
2497 2498 2499 2500 2501 2502
        return 0;
    }
    // derive the AIG manager
    pMan = Abc_NtkToDar( pNtk, 0, 1 );
    if ( pMan == NULL )
    {
2503
        Abc_Print( 1, "Converting network into AIG has failed.\n" );
2504 2505 2506 2507 2508
        return 0;
    }
//    if ( !Saig_ManDemiterSimple( pMan, &pPart0, &pPart1 ) )
    if ( !Saig_ManDemiterDual( pMan, &pPart0, &pPart1 ) )
    {
2509
        Abc_Print( 1, "Demitering has failed.\n" );
2510 2511 2512 2513
        return 0;
    }
    // create new AIG
    ABC_FREE( pPart0->pName );
2514
    pPart0->pName = Abc_UtilStrsav( "part0" );
2515 2516
    // create new AIGs
    ABC_FREE( pPart1->pName );
2517
    pPart1->pName = Abc_UtilStrsav( "part1" );
2518 2519
    // create file names
    pFileNameGeneric = Extra_FileNameGeneric( pNtk->pSpec );
2520 2521 2522 2523
//    sprintf( pFileName0,  "%s%s",  pFileNameGeneric, "_part0.aig" ); 
//    sprintf( pFileName1,  "%s%s",  pFileNameGeneric, "_part1.aig" ); 
    sprintf( pFileName0,  "%s",  "part0.aig" ); 
    sprintf( pFileName1,  "%s",  "part1.aig" ); 
2524 2525 2526
    ABC_FREE( pFileNameGeneric );
    Ioa_WriteAiger( pPart0, pFileName0, 0, 0 );
    Ioa_WriteAiger( pPart1, pFileName1, 0, 0 );
2527
    Abc_Print( 1, "Demitering produced two files \"%s\" and \"%s\".\n", pFileName0, pFileName1 );
2528 2529 2530
    // dump files
    if ( fVerbose )
    {
2531
//        Abc_Print( 1, "Init:  " );
2532
        Aig_ManPrintStats( pMan );
2533
//        Abc_Print( 1, "Part1: " );
2534
        Aig_ManPrintStats( pPart0 );
2535
//        Abc_Print( 1, "Part2: " );
2536 2537 2538 2539 2540 2541
        Aig_ManPrintStats( pPart1 );
    }
    // create two-level miter
//    pMiter = Saig_ManCreateMiterTwo( pPart0, pPart1, 2 );
//    Aig_ManDumpBlif( pMiter, "miter01.blif", NULL, NULL );
//    Aig_ManStop( pMiter );
2542
//    Abc_Print( 1, "The new miter is written into file \"%s\".\n", "miter01.blif" );
2543 2544 2545 2546 2547
    Aig_ManStop( pPart0 );
    Aig_ManStop( pPart1 );
    Aig_ManStop( pMan );
    return 1;
} 
Alan Mishchenko committed
2548
 
Alan Mishchenko committed
2549 2550 2551 2552 2553 2554 2555 2556 2557 2558 2559
/**Function*************************************************************

  Synopsis    [Gives the current ABC network to AIG manager for processing.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
2560
int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar, int nBmcFramesMax, int nBmcConfMax )
Alan Mishchenko committed
2561 2562
{
    Aig_Man_t * pMan;
2563
    int iFrame = -1, RetValue = -1;
2564
    abctime clkTotal = Abc_Clock();
Alan Mishchenko committed
2565
    if ( pSecPar->fTryComb || Abc_NtkLatchNum(pNtk) == 0 )
Alan Mishchenko committed
2566 2567 2568
    {
        Prove_Params_t Params, * pParams = &Params;
        Abc_Ntk_t * pNtkComb;
2569
        int RetValue;
2570
        abctime clk = Abc_Clock();
Alan Mishchenko committed
2571
        if ( Abc_NtkLatchNum(pNtk) == 0 )
2572
            Abc_Print( 1, "The network has no latches. Running CEC.\n" );
Alan Mishchenko committed
2573 2574 2575 2576 2577
        // create combinational network
        pNtkComb = Abc_NtkDup( pNtk );
        Abc_NtkMakeComb( pNtkComb, 1 );
        // solve it using combinational equivalence checking
        Prove_ParamsSetDefault( pParams );
Alan Mishchenko committed
2578
        pParams->fVerbose = 1;
Alan Mishchenko committed
2579 2580
        RetValue = Abc_NtkIvyProve( &pNtkComb, pParams );
        // transfer model if given
Alan Mishchenko committed
2581
//        pNtk->pModel = pNtkComb->pModel; pNtkComb->pModel = NULL;
Alan Mishchenko committed
2582 2583 2584
        if ( RetValue == 0  && (Abc_NtkLatchNum(pNtk) == 0) )
        {
            pNtk->pModel = pNtkComb->pModel; pNtkComb->pModel = NULL;
2585
            Abc_Print( 1, "Networks are not equivalent.\n" );
2586
            ABC_PRT( "Time", Abc_Clock() - clk );
Alan Mishchenko committed
2587 2588
            if ( pSecPar->fReportSolution )
            {
2589
                Abc_Print( 1, "SOLUTION: FAIL       " );
2590
                ABC_PRT( "Time", Abc_Clock() - clkTotal );
Alan Mishchenko committed
2591 2592 2593
            }
            return RetValue;
        }
Alan Mishchenko committed
2594 2595 2596 2597
        Abc_NtkDelete( pNtkComb );
        // return the result, if solved
        if ( RetValue == 1 )
        {
2598
            Abc_Print( 1, "Networks are equivalent after CEC.   " );
2599
            ABC_PRT( "Time", Abc_Clock() - clk );
Alan Mishchenko committed
2600 2601
            if ( pSecPar->fReportSolution )
            {
2602
            Abc_Print( 1, "SOLUTION: PASS       " );
2603
            ABC_PRT( "Time", Abc_Clock() - clkTotal );
Alan Mishchenko committed
2604
            }
Alan Mishchenko committed
2605 2606 2607
            return RetValue;
        }
    }
2608 2609 2610 2611
    // derive the AIG manager
    pMan = Abc_NtkToDar( pNtk, 0, 1 );
    if ( pMan == NULL )
    {
2612
        Abc_Print( 1, "Converting miter into AIG has failed.\n" );
2613 2614 2615 2616
        return -1;
    }
    assert( pMan->nRegs > 0 );

Alan Mishchenko committed
2617
    if ( pSecPar->fTryBmc )
Alan Mishchenko committed
2618
    {
2619
        RetValue = Saig_BmcPerform( pMan, 0, nBmcFramesMax, 2000, 0, nBmcConfMax, 0, pSecPar->fVerbose, 0, &iFrame, 0 );
Alan Mishchenko committed
2620
        if ( RetValue == 0 )
Alan Mishchenko committed
2621
        {
2622
            Abc_Print( 1, "Networks are not equivalent.\n" );
Alan Mishchenko committed
2623 2624
            if ( pSecPar->fReportSolution )
            {
2625
                Abc_Print( 1, "SOLUTION: FAIL       " );
2626
                ABC_PRT( "Time", Abc_Clock() - clkTotal );
Alan Mishchenko committed
2627
            }
2628 2629 2630 2631
            // return the counter-example generated
            ABC_FREE( pNtk->pModel );
            ABC_FREE( pNtk->pSeqModel );
            pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
2632
            Aig_ManStop( pMan );
Alan Mishchenko committed
2633
            return RetValue;
Alan Mishchenko committed
2634
        }
Alan Mishchenko committed
2635
    } 
Alan Mishchenko committed
2636
    // perform verification
Alan Mishchenko committed
2637
    if ( pSecPar->fUseNewProver )
Alan Mishchenko committed
2638
    {
Alan Mishchenko committed
2639 2640 2641 2642
        RetValue = Ssw_SecGeneralMiter( pMan, NULL );
    }
    else
    {
Alan Mishchenko committed
2643
        RetValue = Fra_FraigSec( pMan, pSecPar, NULL );
Alan Mishchenko committed
2644 2645
        ABC_FREE( pNtk->pModel );
        ABC_FREE( pNtk->pSeqModel );
Alan Mishchenko committed
2646 2647 2648
        pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
        if ( pNtk->pSeqModel )
        {
2649
            Abc_Cex_t * pCex = pNtk->pSeqModel;
2650
            Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d.\n", pCex->iPo, pNtk->pName, pCex->iFrame );
2651
            if ( !Saig_ManVerifyCex( pMan, pNtk->pSeqModel ) )
2652
                Abc_Print( 1, "Abc_NtkDarProve(): Counter-example verification has FAILED.\n" );
Alan Mishchenko committed
2653
        }
Alan Mishchenko committed
2654 2655 2656 2657 2658 2659 2660 2661 2662 2663 2664 2665 2666 2667 2668 2669
    }
    Aig_ManStop( pMan );
    return RetValue;
}

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

  Synopsis    [Gives the current ABC network to AIG manager for processing.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
2670
int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Fra_Sec_t * pSecPar )
Alan Mishchenko committed
2671 2672 2673
{
//    Fraig_Params_t Params;
    Aig_Man_t * pMan;
Alan Mishchenko committed
2674
    Abc_Ntk_t * pMiter;//, * pTemp;
Alan Mishchenko committed
2675
    int RetValue;
Alan Mishchenko committed
2676
 
Alan Mishchenko committed
2677
    // get the miter of the two networks
Alan Mishchenko committed
2678
    pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0, 0, 0 );
Alan Mishchenko committed
2679 2680
    if ( pMiter == NULL )
    {
2681
        Abc_Print( 1, "Miter computation has failed.\n" );
Alan Mishchenko committed
2682 2683 2684 2685 2686 2687
        return 0;
    }
    RetValue = Abc_NtkMiterIsConstant( pMiter );
    if ( RetValue == 0 )
    {
        extern void Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel, int nFrames );
2688
        Abc_Print( 1, "Networks are NOT EQUIVALENT after structural hashing.\n" );
Alan Mishchenko committed
2689
        // report the error
Alan Mishchenko committed
2690
        pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, pSecPar->nFramesMax );
2691
//        Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pMiter->pModel, pSecPar->nFramesMax );
Alan Mishchenko committed
2692
        ABC_FREE( pMiter->pModel );
Alan Mishchenko committed
2693 2694 2695 2696 2697 2698
        Abc_NtkDelete( pMiter );
        return 0;
    }
    if ( RetValue == 1 )
    {
        Abc_NtkDelete( pMiter );
2699
        Abc_Print( 1, "Networks are equivalent after structural hashing.\n" );
Alan Mishchenko committed
2700 2701 2702
        return 1;
    }

Alan Mishchenko committed
2703
    // commented out because sometimes the problem became non-inductive
Alan Mishchenko committed
2704
/*
Alan Mishchenko committed
2705 2706 2707 2708
    // preprocess the miter by fraiging it
    // (note that for each functional class, fraiging leaves one representative;
    // so fraiging does not reduce the number of functions represented by nodes
    Fraig_ParamsSetDefault( &Params );
Alan Mishchenko committed
2709
    Params.nBTLimit = 100000;
Alan Mishchenko committed
2710 2711
    pMiter = Abc_NtkFraig( pTemp = pMiter, &Params, 0, 0 );
    Abc_NtkDelete( pTemp );
Alan Mishchenko committed
2712 2713 2714 2715
    RetValue = Abc_NtkMiterIsConstant( pMiter );
    if ( RetValue == 0 )
    {
        extern void Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel, int nFrames );
2716
        Abc_Print( 1, "Networks are NOT EQUIVALENT after structural hashing.\n" );
Alan Mishchenko committed
2717 2718 2719
        // report the error
        pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, nFrames );
        Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pMiter->pModel, nFrames );
Alan Mishchenko committed
2720
        ABC_FREE( pMiter->pModel );
Alan Mishchenko committed
2721 2722 2723 2724 2725 2726
        Abc_NtkDelete( pMiter );
        return 0;
    }
    if ( RetValue == 1 )
    {
        Abc_NtkDelete( pMiter );
2727
        Abc_Print( 1, "Networks are equivalent after structural hashing.\n" );
Alan Mishchenko committed
2728 2729 2730
        return 1;
    }
*/
Alan Mishchenko committed
2731
    // derive the AIG manager
Alan Mishchenko committed
2732
    pMan = Abc_NtkToDar( pMiter, 0, 1 );
Alan Mishchenko committed
2733 2734 2735
    Abc_NtkDelete( pMiter );
    if ( pMan == NULL )
    {
2736
        Abc_Print( 1, "Converting miter into AIG has failed.\n" );
Alan Mishchenko committed
2737 2738 2739 2740 2741
        return -1;
    }
    assert( pMan->nRegs > 0 );

    // perform verification
Alan Mishchenko committed
2742
    RetValue = Fra_FraigSec( pMan, pSecPar, NULL );
Alan Mishchenko committed
2743 2744 2745 2746
    Aig_ManStop( pMan );
    return RetValue;
}

2747 2748 2749 2750 2751 2752 2753 2754 2755 2756 2757
/**Function*************************************************************

  Synopsis    [Gives the current ABC network to AIG manager for processing.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
2758
int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars )
2759
{
2760
    int RetValue = -1;
2761
    abctime clk = Abc_Clock();
2762 2763 2764 2765
    Aig_Man_t * pMan;
    pMan = Abc_NtkToDar( pNtk, 0, 1 );
    if ( pMan == NULL )
    {
2766
        Abc_Print( 1, "Converting network into AIG has failed.\n" );
2767 2768
        return -1;
    }
2769
    RetValue = Pdr_ManSolve( pMan, pPars );
2770
    pPars->nDropOuts = Saig_ManPoNum(pMan) - pPars->nProveOuts - pPars->nFailOuts;
2771 2772
    if ( !pPars->fSilent )
    {
2773 2774 2775 2776
        if ( pPars->fSolveAll )
            Abc_Print( 1, "Properties:  All = %d. Proved = %d. Disproved = %d. Undecided = %d.   ", 
                Saig_ManPoNum(pMan), pPars->nProveOuts, pPars->nFailOuts, pPars->nDropOuts );
        else if ( RetValue == 1 )
2777
            Abc_Print( 1, "Property proved.  " );
2778
        else 
2779
        {
2780
            if ( RetValue == 0 )
2781
            {
2782 2783 2784 2785 2786 2787 2788 2789
                if ( pMan->pSeqModel == NULL )
                    Abc_Print( 1, "Abc_NtkDarPdr(): Counter-example is not available.\n" );
                else
                {
                    Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d.  ", pMan->pSeqModel->iPo, pNtk->pName, pMan->pSeqModel->iFrame );
                    if ( !Saig_ManVerifyCex( pMan, pMan->pSeqModel ) )
                        Abc_Print( 1, "Abc_NtkDarPdr(): Counter-example verification has FAILED.\n" );
                }
2790
            }
2791 2792 2793 2794
            else if ( RetValue == -1 )
                Abc_Print( 1, "Property UNDECIDED.  " );
            else
                assert( 0 );
2795
        }
2796
        ABC_PRT( "Time", Abc_Clock() - clk );
2797 2798 2799 2800 2801 2802 2803 2804 2805 2806 2807 2808 2809 2810 2811 2812
/*
        Abc_Print( 1, "Status: " );
        if ( pPars->pOutMap )
        {
            int i;
            for ( i = 0; i < Saig_ManPoNum(pMan); i++ )
                if ( pPars->pOutMap[i] == 1 )
                    Abc_Print( 1, "%d=%s ", i, "unsat" );
                else if ( pPars->pOutMap[i] == 0 )
                    Abc_Print( 1, "%d=%s ", i, "sat" );
                else if ( pPars->pOutMap[i] < 0 )
                    Abc_Print( 1, "%d=%s ", i, "undec" );
                else assert( 0 );
        }
        Abc_Print( 1, "\n" );
*/
2813
    }
2814 2815
    ABC_FREE( pNtk->pSeqModel );
    pNtk->pSeqModel = pMan->pSeqModel;
2816
    pMan->pSeqModel = NULL;
2817 2818 2819 2820
    if ( pNtk->vSeqModelVec )
        Vec_PtrFreeFree( pNtk->vSeqModelVec );
    pNtk->vSeqModelVec = pMan->vSeqModelVec;
    pMan->vSeqModelVec = NULL;
2821 2822 2823
    Aig_ManStop( pMan );
    return RetValue;
}
Alan Mishchenko committed
2824 2825 2826 2827 2828 2829 2830 2831 2832 2833 2834 2835 2836 2837 2838 2839 2840 2841 2842 2843

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

  Synopsis    [Performs BDD-based reachability analysis.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_NtkDarAbSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fVerbose )
{
    Aig_Man_t * pMan1, * pMan2 = NULL;
    int RetValue;
    // derive AIG manager
    pMan1 = Abc_NtkToDar( pNtk1, 0, 1 );
    if ( pMan1 == NULL )
    {
2844
        Abc_Print( 1, "Converting miter into AIG has failed.\n" );
Alan Mishchenko committed
2845 2846 2847 2848 2849 2850 2851 2852 2853
        return -1;
    }
    assert( Aig_ManRegNum(pMan1) > 0 );
    // derive AIG manager
    if ( pNtk2 )
    {
        pMan2 = Abc_NtkToDar( pNtk2, 0, 1 );
        if ( pMan2 == NULL )
        {
2854
            Aig_ManStop( pMan1 );
2855
            Abc_Print( 1, "Converting miter into AIG has failed.\n" );
Alan Mishchenko committed
2856 2857 2858
            return -1;
        }
        assert( Aig_ManRegNum(pMan2) > 0 );
2859 2860 2861 2862
        if ( Saig_ManPiNum(pMan1) != Saig_ManPiNum(pMan2) )
        {
            Aig_ManStop( pMan1 );
            Aig_ManStop( pMan2 );
2863
            Abc_Print( 1, "The networks have different number of PIs.\n" );
2864 2865 2866 2867 2868 2869
            return -1;
        }
        if ( Saig_ManPoNum(pMan1) != Saig_ManPoNum(pMan2) )
        {
            Aig_ManStop( pMan1 );
            Aig_ManStop( pMan2 );
2870
            Abc_Print( 1, "The networks have different number of POs.\n" );
2871 2872 2873 2874 2875 2876
            return -1;
        }
        if ( Aig_ManRegNum(pMan1) != Aig_ManRegNum(pMan2) )
        {
            Aig_ManStop( pMan1 );
            Aig_ManStop( pMan2 );
2877
            Abc_Print( 1, "The networks have different number of flops.\n" );
2878 2879
            return -1;
        }
Alan Mishchenko committed
2880 2881 2882 2883 2884 2885 2886 2887 2888 2889 2890 2891 2892 2893 2894 2895 2896 2897 2898 2899 2900 2901 2902 2903 2904 2905 2906 2907 2908
    }
    // perform verification
    RetValue = Ssw_SecSpecialMiter( pMan1, pMan2, nFrames, fVerbose );
    Aig_ManStop( pMan1 );
    if ( pMan2 )
        Aig_ManStop( pMan2 );
    return RetValue;
}


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

  Synopsis    [Gives the current ABC network to AIG manager for processing.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_NtkDarSimSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Ssw_Pars_t * pPars )
{
    Aig_Man_t * pMan1, * pMan2 = NULL;
    int RetValue;
    // derive AIG manager
    pMan1 = Abc_NtkToDar( pNtk1, 0, 1 );
    if ( pMan1 == NULL )
    {
2909
        Abc_Print( 1, "Converting miter into AIG has failed.\n" );
Alan Mishchenko committed
2910 2911 2912 2913 2914 2915 2916 2917 2918
        return -1;
    }
    assert( Aig_ManRegNum(pMan1) > 0 );
    // derive AIG manager
    if ( pNtk2 )
    {
        pMan2 = Abc_NtkToDar( pNtk2, 0, 1 );
        if ( pMan2 == NULL )
        {
2919
            Abc_Print( 1, "Converting miter into AIG has failed.\n" );
Alan Mishchenko committed
2920 2921 2922 2923 2924 2925 2926 2927 2928 2929 2930 2931 2932 2933 2934 2935 2936 2937 2938 2939 2940 2941 2942 2943 2944 2945 2946 2947 2948 2949 2950 2951 2952 2953 2954
            return -1;
        }
        assert( Aig_ManRegNum(pMan2) > 0 );
    }

    // perform verification
    RetValue = Ssw_SecWithSimilarity( pMan1, pMan2, pPars );
    Aig_ManStop( pMan1 );
    if ( pMan2 )
        Aig_ManStop( pMan2 );
    return RetValue;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Abc_Ntk_t * Abc_NtkDarMatch( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nDist, int fVerbose )
{
    extern Vec_Int_t * Saig_StrSimPerformMatching( Aig_Man_t * p0, Aig_Man_t * p1, int nDist, int fVerbose, Aig_Man_t ** ppMiter );
    Abc_Ntk_t * pNtkAig;
    Aig_Man_t * pMan1, * pMan2 = NULL, * pManRes;
    Vec_Int_t * vPairs;
    assert( Abc_NtkIsStrash(pNtk1) );
    // derive AIG manager
    pMan1 = Abc_NtkToDar( pNtk1, 0, 1 );
    if ( pMan1 == NULL )
    {
2955
        Abc_Print( 1, "Converting miter into AIG has failed.\n" );
Alan Mishchenko committed
2956 2957 2958 2959 2960 2961 2962 2963 2964
        return NULL;
    }
    assert( Aig_ManRegNum(pMan1) > 0 );
    // derive AIG manager
    if ( pNtk2 )
    {
        pMan2 = Abc_NtkToDar( pNtk2, 0, 1 );
        if ( pMan2 == NULL )
        {
2965
            Abc_Print( 1, "Converting miter into AIG has failed.\n" );
Alan Mishchenko committed
2966 2967 2968 2969 2970 2971 2972 2973 2974 2975 2976 2977 2978 2979 2980 2981 2982 2983 2984
            return NULL;
        }
        assert( Aig_ManRegNum(pMan2) > 0 );
    }

    // perform verification
    vPairs = Saig_StrSimPerformMatching( pMan1, pMan2, nDist, 1, &pManRes );
    pNtkAig = Abc_NtkFromAigPhase( pManRes );
    if ( vPairs )
        Vec_IntFree( vPairs );
    if ( pManRes )
        Aig_ManStop( pManRes );
    Aig_ManStop( pMan1 );
    if ( pMan2 )
        Aig_ManStop( pMan2 );
    return pNtkAig;
}


Alan Mishchenko committed
2985 2986 2987 2988 2989 2990 2991 2992 2993 2994 2995
/**Function*************************************************************

  Synopsis    [Gives the current ABC network to AIG manager for processing.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
2996
Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchConst, int fLatchEqual, int fSaveNames, int fUseMvSweep, int nFramesSymb, int nFramesSatur, int fVerbose, int fVeryVerbose )
Alan Mishchenko committed
2997
{
Alan Mishchenko committed
2998
    extern void Aig_ManPrintControlFanouts( Aig_Man_t * p );
Alan Mishchenko committed
2999
    Abc_Ntk_t * pNtkAig;
Alan Mishchenko committed
3000
    Aig_Man_t * pMan, * pTemp;
Alan Mishchenko committed
3001
    pMan = Abc_NtkToDar( pNtk, 0, 1 );
Alan Mishchenko committed
3002 3003
    if ( pMan == NULL )
        return NULL;
3004 3005 3006 3007
    if ( fSaveNames )
    {
        Aig_ManSeqCleanup( pMan );
        if ( fLatchConst && pMan->nRegs )
3008
            pMan = Aig_ManConstReduce( pMan, fUseMvSweep, nFramesSymb, nFramesSatur, fVerbose, fVeryVerbose );
3009 3010 3011 3012 3013 3014 3015 3016
        if ( fLatchEqual && pMan->nRegs )
            pMan = Aig_ManReduceLaches( pMan, fVerbose );
    }
    else
    {
        if ( pMan->vFlopNums )
            Vec_IntFree( pMan->vFlopNums );
        pMan->vFlopNums = NULL;
3017
        pMan = Aig_ManScl( pTemp = pMan, fLatchConst, fLatchEqual, fUseMvSweep, nFramesSymb, nFramesSatur, fVerbose, fVeryVerbose );
3018 3019
        Aig_ManStop( pTemp );
    }
Alan Mishchenko committed
3020

Alan Mishchenko committed
3021
    pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
Alan Mishchenko committed
3022
//Aig_ManPrintControlFanouts( pMan );
Alan Mishchenko committed
3023 3024 3025 3026 3027 3028 3029 3030 3031 3032 3033 3034 3035 3036 3037 3038 3039 3040 3041
    Aig_ManStop( pMan );
    return pNtkAig;
}

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

  Synopsis    [Gives the current ABC network to AIG manager for processing.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
{
    Abc_Ntk_t * pNtkAig;
    Aig_Man_t * pMan, * pTemp;
Alan Mishchenko committed
3042
    pMan = Abc_NtkToDar( pNtk, 0, 1 );
Alan Mishchenko committed
3043 3044 3045 3046 3047 3048 3049
    if ( pMan == NULL )
        return NULL;
//    Aig_ManReduceLachesCount( pMan );
    if ( pMan->vFlopNums )
        Vec_IntFree( pMan->vFlopNums ); 
    pMan->vFlopNums = NULL;

Alan Mishchenko committed
3050
    pMan = Rtm_ManRetime( pTemp = pMan, 1, nStepsMax, fVerbose );
Alan Mishchenko committed
3051 3052 3053
    Aig_ManStop( pTemp );

//    pMan = Aig_ManReduceLaches( pMan, 1 );
3054
//    pMan = Aig_ManConstReduce( pMan, 1, 0 );
Alan Mishchenko committed
3055 3056 3057 3058 3059 3060 3061 3062 3063 3064 3065 3066 3067 3068 3069 3070 3071

    pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
    Aig_ManStop( pMan );
    return pNtkAig;
}

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

  Synopsis    [Gives the current ABC network to AIG manager for processing.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
3072
Abc_Ntk_t * Abc_NtkDarRetimeF( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
Alan Mishchenko committed
3073 3074 3075 3076 3077 3078
{
    Abc_Ntk_t * pNtkAig;
    Aig_Man_t * pMan, * pTemp;
    pMan = Abc_NtkToDar( pNtk, 0, 1 );
    if ( pMan == NULL )
        return NULL;
Alan Mishchenko committed
3079
//    Aig_ManReduceLachesCount( pMan );
Alan Mishchenko committed
3080 3081 3082 3083
    if ( pMan->vFlopNums )
        Vec_IntFree( pMan->vFlopNums ); 
    pMan->vFlopNums = NULL;

Alan Mishchenko committed
3084
    pMan = Aig_ManRetimeFrontier( pTemp = pMan, nStepsMax );
Alan Mishchenko committed
3085 3086
    Aig_ManStop( pTemp );

Alan Mishchenko committed
3087
//    pMan = Aig_ManReduceLaches( pMan, 1 );
3088
//    pMan = Aig_ManConstReduce( pMan, 1, 0 );
Alan Mishchenko committed
3089

Alan Mishchenko committed
3090 3091 3092 3093 3094 3095 3096 3097 3098 3099 3100 3101 3102 3103 3104 3105
    pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
    Aig_ManStop( pMan );
    return pNtkAig;
}

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

  Synopsis    [Gives the current ABC network to AIG manager for processing.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
3106
Abc_Ntk_t * Abc_NtkDarRetimeMostFwd( Abc_Ntk_t * pNtk, int nMaxIters, int fVerbose )
Alan Mishchenko committed
3107
{
Alan Mishchenko committed
3108 3109
    extern Aig_Man_t * Saig_ManRetimeForward( Aig_Man_t * p, int nIters, int fVerbose );

Alan Mishchenko committed
3110 3111
    Abc_Ntk_t * pNtkAig;
    Aig_Man_t * pMan, * pTemp;
Alan Mishchenko committed
3112
    pMan = Abc_NtkToDar( pNtk, 0, 1 );
Alan Mishchenko committed
3113 3114 3115 3116 3117 3118 3119
    if ( pMan == NULL )
        return NULL;
//    Aig_ManReduceLachesCount( pMan );
    if ( pMan->vFlopNums )
        Vec_IntFree( pMan->vFlopNums ); 
    pMan->vFlopNums = NULL;

Alan Mishchenko committed
3120
    pMan = Saig_ManRetimeForward( pTemp = pMan, nMaxIters, fVerbose );
Alan Mishchenko committed
3121 3122 3123
    Aig_ManStop( pTemp );

//    pMan = Aig_ManReduceLaches( pMan, 1 );
3124
//    pMan = Aig_ManConstReduce( pMan, 1, 0 );
Alan Mishchenko committed
3125 3126 3127 3128 3129 3130 3131 3132 3133 3134 3135 3136 3137 3138 3139 3140 3141

    pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
    Aig_ManStop( pMan );
    return pNtkAig;
}

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

  Synopsis    [Gives the current ABC network to AIG manager for processing.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
3142 3143 3144 3145 3146 3147 3148 3149 3150 3151 3152 3153 3154 3155 3156 3157 3158 3159 3160 3161 3162 3163 3164 3165 3166 3167 3168 3169 3170 3171 3172
Abc_Ntk_t * Abc_NtkDarRetimeMinArea( Abc_Ntk_t * pNtk, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose )
{
    extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
    Abc_Ntk_t * pNtkAig;
    Aig_Man_t * pMan, * pTemp;
    pMan = Abc_NtkToDar( pNtk, 0, 1 );
    if ( pMan == NULL )
        return NULL;
    if ( pMan->vFlopNums )
        Vec_IntFree( pMan->vFlopNums ); 
    pMan->vFlopNums = NULL;

    pMan = Saig_ManRetimeMinArea( pTemp = pMan, nMaxIters, fForwardOnly, fBackwardOnly, fInitial, fVerbose );
    Aig_ManStop( pTemp );

    pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
    Aig_ManStop( pMan );
    return pNtkAig;
}

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

  Synopsis    [Gives the current ABC network to AIG manager for processing.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
3173 3174 3175 3176 3177 3178 3179 3180 3181 3182 3183 3184 3185
Abc_Ntk_t * Abc_NtkDarRetimeStep( Abc_Ntk_t * pNtk, int fVerbose )
{
    Abc_Ntk_t * pNtkAig;
    Aig_Man_t * pMan;
    assert( Abc_NtkIsStrash(pNtk) );
    pMan = Abc_NtkToDar( pNtk, 0, 1 );
    if ( pMan == NULL )
        return NULL;
    if ( pMan->vFlopNums )
        Vec_IntFree( pMan->vFlopNums ); 
    pMan->vFlopNums = NULL;

    Aig_ManPrintStats(pMan);
Alan Mishchenko committed
3186
    Saig_ManRetimeSteps( pMan, 1000, 1, 0 );
Alan Mishchenko committed
3187 3188 3189 3190 3191 3192 3193 3194 3195 3196 3197 3198 3199 3200 3201 3202 3203 3204
    Aig_ManPrintStats(pMan);

    pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
    Aig_ManStop( pMan );
    return pNtkAig;
}

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

  Synopsis    [Gives the current ABC network to AIG manager for processing.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
3205
/*
Alan Mishchenko committed
3206
Abc_Ntk_t * Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk, int nIters, int nSteps, int fRetimingOnly, int fAddBugs, int fUseCnf, int fVerbose )
Alan Mishchenko committed
3207
{
Alan Mishchenko committed
3208 3209
    Abc_Ntk_t * pNtkAig;
    Aig_Man_t * pMan, * pTemp;
Alan Mishchenko committed
3210
    pMan = Abc_NtkToDar( pNtk, 0, 1 );
Alan Mishchenko committed
3211
    if ( pMan == NULL )
Alan Mishchenko committed
3212
        return NULL;
Alan Mishchenko committed
3213 3214 3215
    if ( pMan->vFlopNums )
        Vec_IntFree( pMan->vFlopNums ); 
    pMan->vFlopNums = NULL;
Alan Mishchenko committed
3216

Alan Mishchenko committed
3217 3218 3219 3220
    pMan = Saig_ManHaigRecord( pTemp = pMan, nIters, nSteps, fRetimingOnly, fAddBugs, fUseCnf, fVerbose );
    Aig_ManStop( pTemp );

    pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
Alan Mishchenko committed
3221
    Aig_ManStop( pMan );
Alan Mishchenko committed
3222
    return pNtkAig;
Alan Mishchenko committed
3223
}
Alan Mishchenko committed
3224
*/
Alan Mishchenko committed
3225 3226 3227 3228 3229 3230 3231 3232 3233 3234 3235 3236

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

  Synopsis    [Performs random simulation.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
3237
int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, int fNew, int fMiter, int fVerbose, char * pFileSim )
Alan Mishchenko committed
3238 3239
{
    Aig_Man_t * pMan;
3240
    Abc_Cex_t * pCex;
3241
    int status, RetValue = -1;
3242
    abctime clk = Abc_Clock();
Alan Mishchenko committed
3243 3244
    if ( Abc_NtkGetChoiceNum(pNtk) )
    {
3245
        Abc_Print( 1, "Removing %d choices from the AIG.\n", Abc_NtkGetChoiceNum(pNtk) );
3246
        Abc_AigCleanup((Abc_Aig_t *)pNtk->pManFunc);
Alan Mishchenko committed
3247
    }
Alan Mishchenko committed
3248
    pMan = Abc_NtkToDar( pNtk, 0, 1 );
3249
    if ( fNew )
Alan Mishchenko committed
3250
    {
Alan Mishchenko committed
3251 3252 3253 3254 3255 3256 3257 3258 3259 3260 3261
        Gia_Man_t * pGia;
        Gia_ParSim_t Pars, * pPars = &Pars;
        Gia_ManSimSetDefaultParams( pPars );
        pPars->nWords = nWords;
        pPars->nIters = nFrames;
        pPars->TimeLimit = TimeOut;
        pPars->fCheckMiter = fMiter;
        pPars->fVerbose = fVerbose;
        pGia = Gia_ManFromAig( pMan );
        if ( Gia_ManSimSimulate( pGia, pPars ) )
        { 
3262
            if ( pGia->pCexSeq )
Alan Mishchenko committed
3263
            {
3264
                Abc_Print( 1, "Simulation of %d frames with %d words asserted output %d in frame %d. ", 
3265
                    nFrames, nWords, pGia->pCexSeq->iPo, pGia->pCexSeq->iFrame );
3266
                status = Saig_ManVerifyCex( pMan, pGia->pCexSeq );
Alan Mishchenko committed
3267
                if ( status == 0 )
3268
                    Abc_Print( 1, "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
Alan Mishchenko committed
3269
            }
Alan Mishchenko committed
3270 3271
            ABC_FREE( pNtk->pModel );
            ABC_FREE( pNtk->pSeqModel );
3272 3273
            pNtk->pSeqModel = pGia->pCexSeq; pGia->pCexSeq = NULL;
            RetValue = 0;
Alan Mishchenko committed
3274 3275 3276
        }
        else
        {
3277
            Abc_Print( 1, "Simulation of %d frames with %d words did not assert the outputs.    ", 
Alan Mishchenko committed
3278 3279
                nFrames, nWords );
        }
Alan Mishchenko committed
3280
        Gia_ManStop( pGia );
Alan Mishchenko committed
3281
    }
3282
    else // comb/seq simulator
Alan Mishchenko committed
3283
    {
Alan Mishchenko committed
3284
        Fra_Sml_t * pSml;
3285 3286 3287 3288 3289 3290 3291 3292 3293
        if ( pFileSim != NULL )
        {
            assert( Abc_NtkLatchNum(pNtk) == 0 );
            pSml = Fra_SmlSimulateCombGiven( pMan, pFileSim, fMiter, fVerbose );
        }
        else if ( Abc_NtkLatchNum(pNtk) == 0 )
            pSml = Fra_SmlSimulateComb( pMan, nWords, fMiter );
        else
            pSml = Fra_SmlSimulateSeq( pMan, 0, nFrames, nWords, fMiter );
Alan Mishchenko committed
3294 3295 3296 3297
        if ( pSml->fNonConstOut )
        {
            pCex = Fra_SmlGetCounterExample( pSml );
            if ( pCex )
Alan Mishchenko committed
3298
            {
3299 3300 3301 3302
                Abc_Print( 1, "Simulation of %d frame%s with %d word%s asserted output %d in frame %d. ", 
                    pSml->nFrames, pSml->nFrames == 1 ? "": "s", 
                    pSml->nWordsFrame, pSml->nWordsFrame == 1 ? "": "s", 
                    pCex->iPo, pCex->iFrame );
3303
                status = Saig_ManVerifyCex( pMan, pCex );
Alan Mishchenko committed
3304
                if ( status == 0 )
3305
                    Abc_Print( 1, "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
Alan Mishchenko committed
3306
            }
Alan Mishchenko committed
3307 3308
            ABC_FREE( pNtk->pModel );
            ABC_FREE( pNtk->pSeqModel );
Alan Mishchenko committed
3309
            pNtk->pSeqModel = pCex;
3310
            RetValue = 0;
Alan Mishchenko committed
3311 3312 3313
        }
        else
        {
3314
            Abc_Print( 1, "Simulation of %d frames with %d words did not assert the outputs.    ", 
Alan Mishchenko committed
3315 3316 3317
                nFrames, nWords );
        }
        Fra_SmlStop( pSml );
Alan Mishchenko committed
3318
    }
3319
    ABC_PRT( "Time", Abc_Clock() - clk );
Alan Mishchenko committed
3320 3321 3322 3323 3324 3325
    Aig_ManStop( pMan );
    return RetValue;
}

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

3326 3327 3328 3329 3330 3331 3332 3333 3334
  Synopsis    [Performs random simulation.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
3335
int Abc_NtkDarSeqSim3( Abc_Ntk_t * pNtk, Ssw_RarPars_t * pPars )
3336 3337
{
    Aig_Man_t * pMan;
3338
    int status, RetValue = -1;
3339
//    abctime clk = Abc_Clock();
3340 3341
    if ( Abc_NtkGetChoiceNum(pNtk) )
    {
3342
        Abc_Print( 1, "Removing %d choices from the AIG.\n", Abc_NtkGetChoiceNum(pNtk) );
3343 3344 3345
        Abc_AigCleanup((Abc_Aig_t *)pNtk->pManFunc);
    }
    pMan = Abc_NtkToDar( pNtk, 0, 1 );
3346
    if ( Ssw_RarSimulate( pMan, pPars ) == 0 )
3347 3348 3349
    { 
        if ( pMan->pSeqModel )
        {
3350 3351
//            Abc_Print( 1, "Simulation of %d frames with %d words asserted output %d in frame %d. ", 
//                nFrames, nWords, pMan->pSeqModel->iPo, pMan->pSeqModel->iFrame );
3352 3353
            status = Saig_ManVerifyCex( pMan, pMan->pSeqModel );
            if ( status == 0 )
3354
                Abc_Print( 1, "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
3355 3356 3357 3358 3359 3360 3361 3362
        }
        ABC_FREE( pNtk->pModel );
        ABC_FREE( pNtk->pSeqModel );
        pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
        RetValue = 0;
    }
    else
    {
3363
//        Abc_Print( 1, "Simulation of %d frames with %d words did not assert the outputs.    ", 
3364
//            nFrames, nWords );
3365
    }
3366 3367 3368
    if ( pNtk->vSeqModelVec )
        Vec_PtrFreeFree( pNtk->vSeqModelVec );
    pNtk->vSeqModelVec = pMan->vSeqModelVec;  pMan->vSeqModelVec = NULL;
3369
//    ABC_PRT( "Time", Abc_Clock() - clk );
3370
    pNtk->pData = pMan->pData; pMan->pData = NULL;
3371 3372 3373 3374 3375 3376
    Aig_ManStop( pMan );
    return RetValue;
}

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

Alan Mishchenko committed
3377 3378 3379 3380 3381 3382 3383 3384 3385 3386 3387 3388 3389 3390 3391 3392
  Synopsis    [Gives the current ABC network to AIG manager for processing.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_NtkDarClau( Abc_Ntk_t * pNtk, int nFrames, int nPref, int nClauses, int nLutSize, int nLevels, int nCutsMax, int nBatches, int fStepUp, int fBmc, int fRefs, int fTarget, int fVerbose, int fVeryVerbose )
{
    extern int Fra_Clau( Aig_Man_t * pMan, int nIters, int fVerbose, int fVeryVerbose );
    extern int Fra_Claus( Aig_Man_t * pAig, int nFrames, int nPref, int nClauses, int nLutSize, int nLevels, int nCutsMax, int nBatches, int fStepUp, int fBmc, int fRefs, int fTarget, int fVerbose, int fVeryVerbose );
    Aig_Man_t * pMan;
    if ( fTarget && Abc_NtkPoNum(pNtk) != 1 )
    {
3393
        Abc_Print( 1, "The number of outputs should be 1.\n" );
Alan Mishchenko committed
3394 3395
        return 1;
    }
Alan Mishchenko committed
3396
    pMan = Abc_NtkToDar( pNtk, 0, 1 );
Alan Mishchenko committed
3397 3398 3399 3400 3401 3402 3403 3404 3405 3406 3407 3408 3409 3410 3411 3412 3413 3414 3415 3416 3417 3418 3419 3420 3421 3422 3423 3424
    if ( pMan == NULL )
        return 1;
//    Aig_ManReduceLachesCount( pMan );
    if ( pMan->vFlopNums )
        Vec_IntFree( pMan->vFlopNums ); 
    pMan->vFlopNums = NULL;

//    Fra_Clau( pMan, nStepsMax, fVerbose, fVeryVerbose );
    Fra_Claus( pMan, nFrames, nPref, nClauses, nLutSize, nLevels, nCutsMax, nBatches, fStepUp, fBmc, fRefs, fTarget, fVerbose, fVeryVerbose );
    Aig_ManStop( pMan );
    return 1;
}

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

  Synopsis    [Performs targe enlargement.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Abc_Ntk_t * Abc_NtkDarEnlarge( Abc_Ntk_t * pNtk, int nFrames, int fVerbose )
{
    Abc_Ntk_t * pNtkAig;
    Aig_Man_t * pMan, * pTemp;
Alan Mishchenko committed
3425
    pMan = Abc_NtkToDar( pNtk, 0, 1 );
Alan Mishchenko committed
3426 3427 3428 3429 3430 3431 3432 3433
    if ( pMan == NULL )
        return NULL;
    pMan = Aig_ManFrames( pTemp = pMan, nFrames, 0, 1, 1, 1, NULL );
    Aig_ManStop( pTemp );
    pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
    Aig_ManStop( pMan );
    return pNtkAig;
}
Alan Mishchenko committed
3434

Alan Mishchenko committed
3435 3436
/**Function*************************************************************

3437 3438 3439 3440 3441 3442 3443 3444 3445
  Synopsis    [Performs targe enlargement.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
3446
Abc_Ntk_t * Abc_NtkDarTempor( Abc_Ntk_t * pNtk, int nFrames, int TimeOut, int nConfLimit, int fUseBmc, int fUseTransSigs, int fVerbose, int fVeryVerbose )
3447
{
3448
    extern Aig_Man_t * Saig_ManTempor( Aig_Man_t * pAig, int nFrames, int TimeOut, int nConfLimit, int fUseBmc, int fUseTransSigs, int fVerbose, int fVeryVerbose );
3449 3450 3451 3452 3453
    Abc_Ntk_t * pNtkAig;
    Aig_Man_t * pMan, * pTemp;
    pMan = Abc_NtkToDar( pNtk, 0, 1 );
    if ( pMan == NULL )
        return NULL;
3454
    pTemp = Saig_ManTempor( pMan, nFrames, TimeOut, nConfLimit, fUseBmc, fUseTransSigs, fVerbose, fVeryVerbose );
3455 3456 3457 3458 3459 3460 3461 3462 3463 3464
    Aig_ManStop( pMan );
    if ( pTemp == NULL )
        return Abc_NtkDup( pNtk );
    pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pTemp );
    Aig_ManStop( pTemp );
    return pNtkAig;
}

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

Alan Mishchenko committed
3465
  Synopsis    [Performs induction for property only.]
Alan Mishchenko committed
3466 3467 3468 3469 3470 3471 3472 3473

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
3474
int Abc_NtkDarInduction( Abc_Ntk_t * pNtk, int nTimeOut, int nFramesMax, int nConfMax, int fUnique, int fUniqueAll, int fGetCex, int fVerbose, int fVeryVerbose )
3475
{ 
3476
    Aig_Man_t * pMan;
3477
    abctime clkTotal = Abc_Clock();
Alan Mishchenko committed
3478 3479 3480
    int RetValue;
    pMan = Abc_NtkToDar( pNtk, 0, 1 );
    if ( pMan == NULL )
3481
        return -1;
3482
    RetValue = Saig_ManInduction( pMan, nTimeOut, nFramesMax, nConfMax, fUnique, fUniqueAll, fGetCex, fVerbose, fVeryVerbose );
Alan Mishchenko committed
3483 3484
    if ( RetValue == 1 )
    {
3485
        Abc_Print( 1, "Networks are equivalent.   " );
3486
ABC_PRT( "Time", Abc_Clock() - clkTotal );
Alan Mishchenko committed
3487 3488 3489
    }
    else if ( RetValue == 0 )
    {
3490
        Abc_Print( 1, "Networks are NOT EQUIVALENT.   " );
3491
ABC_PRT( "Time", Abc_Clock() - clkTotal );
Alan Mishchenko committed
3492 3493 3494
    }
    else
    {
3495
        Abc_Print( 1, "Networks are UNDECIDED.   " );
3496
ABC_PRT( "Time", Abc_Clock() - clkTotal );
Alan Mishchenko committed
3497
    }
3498 3499 3500 3501 3502 3503 3504
    if ( fGetCex )
    {
        ABC_FREE( pNtk->pModel );
        ABC_FREE( pNtk->pSeqModel );
        pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
    }
    Aig_ManStop( pMan );
3505
    return RetValue;
Alan Mishchenko committed
3506 3507
}

Alan Mishchenko committed
3508 3509 3510 3511 3512 3513 3514 3515 3516 3517 3518 3519

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

  Synopsis    [Interplates two networks.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
3520
Abc_Ntk_t * Abc_NtkInterOne( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fRelation, int fVerbose )
Alan Mishchenko committed
3521
{
Alan Mishchenko committed
3522
    extern Aig_Man_t * Aig_ManInter( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fRelation, int fVerbose );
Alan Mishchenko committed
3523 3524 3525 3526
    Abc_Ntk_t * pNtkAig;
    Aig_Man_t * pManOn, * pManOff, * pManAig;
    if ( Abc_NtkCoNum(pNtkOn) != 1 || Abc_NtkCoNum(pNtkOff) != 1 )
    {
3527
        Abc_Print( 1, "Currently works only for single-output networks.\n" );
Alan Mishchenko committed
3528 3529 3530 3531
        return NULL;
    }
    if ( Abc_NtkCiNum(pNtkOn) != Abc_NtkCiNum(pNtkOff) )
    {
3532
        Abc_Print( 1, "The number of PIs should be the same.\n" );
Alan Mishchenko committed
3533 3534 3535
        return NULL;
    }
    // create internal AIGs
Alan Mishchenko committed
3536
    pManOn = Abc_NtkToDar( pNtkOn, 0, 0 );
Alan Mishchenko committed
3537 3538
    if ( pManOn == NULL )
        return NULL;
Alan Mishchenko committed
3539
    pManOff = Abc_NtkToDar( pNtkOff, 0, 0 );
Alan Mishchenko committed
3540 3541 3542
    if ( pManOff == NULL )
        return NULL;
    // derive the interpolant
Alan Mishchenko committed
3543
    pManAig = Aig_ManInter( pManOn, pManOff, fRelation, fVerbose );
Alan Mishchenko committed
3544 3545
    if ( pManAig == NULL )
    {
3546
        Abc_Print( 1, "Interpolant computation failed.\n" );
Alan Mishchenko committed
3547 3548 3549 3550
        return NULL;
    }
    Aig_ManStop( pManOn );
    Aig_ManStop( pManOff );
Alan Mishchenko committed
3551 3552 3553 3554 3555 3556 3557
    // for the relation, add an extra input
    if ( fRelation )
    {
        Abc_Obj_t * pObj;
        pObj = Abc_NtkCreatePi( pNtkOff );
        Abc_ObjAssignName( pObj, "New", NULL );
    }
Alan Mishchenko committed
3558
    // create logic network
Alan Mishchenko committed
3559
    pNtkAig = Abc_NtkFromDar( pNtkOff, pManAig );
Alan Mishchenko committed
3560 3561 3562 3563
    Aig_ManStop( pManAig );
    return pNtkAig;
}

Alan Mishchenko committed
3564 3565 3566 3567 3568 3569 3570 3571 3572 3573 3574 3575 3576 3577 3578 3579
/**Function*************************************************************

  Synopsis    [Fast interpolation.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_NtkInterFast( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbose )
{
    extern void Aig_ManInterFast( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fVerbose );
    Aig_Man_t * pManOn, * pManOff;
    // create internal AIGs
Alan Mishchenko committed
3580
    pManOn = Abc_NtkToDar( pNtkOn, 0, 0 );
Alan Mishchenko committed
3581 3582
    if ( pManOn == NULL )
        return;
Alan Mishchenko committed
3583
    pManOff = Abc_NtkToDar( pNtkOff, 0, 0 );
Alan Mishchenko committed
3584 3585 3586 3587 3588 3589
    if ( pManOff == NULL )
        return;
    Aig_ManInterFast( pManOn, pManOff, fVerbose );
    Aig_ManStop( pManOn );
    Aig_ManStop( pManOff );
}
Alan Mishchenko committed
3590

3591 3592 3593
abctime timeCnf;
abctime timeSat;
abctime timeInt;
Alan Mishchenko committed
3594

Alan Mishchenko committed
3595 3596 3597 3598 3599 3600 3601 3602 3603 3604 3605
/**Function*************************************************************

  Synopsis    [Interplates two networks.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
3606
Abc_Ntk_t * Abc_NtkInter( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fRelation, int fVerbose )
Alan Mishchenko committed
3607 3608 3609
{
    Abc_Ntk_t * pNtkOn1, * pNtkOff1, * pNtkInter1, * pNtkInter;
    Abc_Obj_t * pObj;
3610
    int i; //, clk = Abc_Clock();
Alan Mishchenko committed
3611 3612
    if ( Abc_NtkCoNum(pNtkOn) != Abc_NtkCoNum(pNtkOff) )
    {
3613
        Abc_Print( 1, "Currently works only for networks with equal number of POs.\n" );
Alan Mishchenko committed
3614 3615
        return NULL;
    }
Alan Mishchenko committed
3616 3617 3618
    // compute the fast interpolation time
//    Abc_NtkInterFast( pNtkOn, pNtkOff, fVerbose );
    // consider the case of one output
Alan Mishchenko committed
3619
    if ( Abc_NtkCoNum(pNtkOn) == 1 )
Alan Mishchenko committed
3620
        return Abc_NtkInterOne( pNtkOn, pNtkOff, fRelation, fVerbose );
Alan Mishchenko committed
3621
    // start the new network
Alan Mishchenko committed
3622 3623 3624 3625 3626
    pNtkInter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
    pNtkInter->pName = Extra_UtilStrsav(pNtkOn->pName);
    Abc_NtkForEachPi( pNtkOn, pObj, i )
        Abc_NtkDupObj( pNtkInter, pObj, 1 );
    // process each POs separately
Alan Mishchenko committed
3627 3628 3629
timeCnf = 0;
timeSat = 0;
timeInt = 0;
Alan Mishchenko committed
3630 3631 3632 3633 3634 3635 3636 3637 3638 3639 3640 3641 3642 3643 3644 3645 3646 3647 3648
    Abc_NtkForEachCo( pNtkOn, pObj, i )
    {
        pNtkOn1 = Abc_NtkCreateCone( pNtkOn, Abc_ObjFanin0(pObj), Abc_ObjName(pObj), 1 );
        if ( Abc_ObjFaninC0(pObj) )
            Abc_ObjXorFaninC( Abc_NtkPo(pNtkOn1, 0), 0 );

        pObj   = Abc_NtkCo(pNtkOff, i);
        pNtkOff1 = Abc_NtkCreateCone( pNtkOff, Abc_ObjFanin0(pObj), Abc_ObjName(pObj), 1 );
        if ( Abc_ObjFaninC0(pObj) )
            Abc_ObjXorFaninC( Abc_NtkPo(pNtkOff1, 0), 0 );

        if ( Abc_NtkNodeNum(pNtkOn1) == 0 )
            pNtkInter1 = Abc_NtkDup( pNtkOn1 );
        else if ( Abc_NtkNodeNum(pNtkOff1) == 0 )
        {
            pNtkInter1 = Abc_NtkDup( pNtkOff1 );
            Abc_ObjXorFaninC( Abc_NtkPo(pNtkInter1, 0), 0 );
        }
        else
Alan Mishchenko committed
3649
            pNtkInter1 = Abc_NtkInterOne( pNtkOn1, pNtkOff1, 0, fVerbose );
Alan Mishchenko committed
3650 3651 3652 3653 3654
        if ( pNtkInter1 )
        {
            Abc_NtkAppend( pNtkInter, pNtkInter1, 1 );
            Abc_NtkDelete( pNtkInter1 );
        }
Alan Mishchenko committed
3655 3656 3657 3658

        Abc_NtkDelete( pNtkOn1 );
        Abc_NtkDelete( pNtkOff1 );
    }
Alan Mishchenko committed
3659 3660 3661
//    ABC_PRT( "CNF", timeCnf );
//    ABC_PRT( "SAT", timeSat );
//    ABC_PRT( "Int", timeInt );
3662
//    ABC_PRT( "Slow interpolation time", Abc_Clock() - clk );
Alan Mishchenko committed
3663

Alan Mishchenko committed
3664 3665
    // return the network
    if ( !Abc_NtkCheck( pNtkInter ) )
3666
        Abc_Print( 1, "Abc_NtkAttachBottom(): Network check has failed.\n" );
Alan Mishchenko committed
3667 3668 3669 3670 3671
    return pNtkInter;
}

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

Alan Mishchenko committed
3672
  Synopsis    []
Alan Mishchenko committed
3673 3674 3675 3676 3677 3678 3679 3680

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
3681 3682
void Abc_NtkPrintSccs( Abc_Ntk_t * pNtk, int fVerbose )
{
Alan Mishchenko committed
3683
//    extern Vec_Ptr_t * Aig_ManRegPartitionLinear( Aig_Man_t * pAig, int nPartSize );
Alan Mishchenko committed
3684
    Aig_Man_t * pMan;
Alan Mishchenko committed
3685
    pMan = Abc_NtkToDar( pNtk, 0, 1 );
Alan Mishchenko committed
3686 3687 3688
    if ( pMan == NULL )
        return;
    Aig_ManComputeSccs( pMan );
Alan Mishchenko committed
3689
//    Aig_ManRegPartitionLinear( pMan, 1000 );
Alan Mishchenko committed
3690 3691 3692
    Aig_ManStop( pMan );
}

Alan Mishchenko committed
3693 3694
/**Function*************************************************************

Alan Mishchenko committed
3695 3696 3697 3698 3699 3700 3701 3702 3703
  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
3704
int Abc_NtkDarPrintCone( Abc_Ntk_t * pNtk )
Alan Mishchenko committed
3705 3706 3707 3708 3709
{
    extern void Saig_ManPrintCones( Aig_Man_t * pAig );
    Aig_Man_t * pMan;
    pMan = Abc_NtkToDar( pNtk, 0, 1 );
    if ( pMan == NULL )
3710
        return 0;
Alan Mishchenko committed
3711 3712 3713
    assert( Aig_ManRegNum(pMan) > 0 );
    Saig_ManPrintCones( pMan );
    Aig_ManStop( pMan );
3714
    return 1;
Alan Mishchenko committed
3715 3716 3717 3718 3719
}

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

  Synopsis    []
Alan Mishchenko committed
3720 3721 3722 3723 3724 3725 3726 3727 3728 3729 3730 3731 3732 3733 3734 3735 3736 3737 3738 3739 3740 3741 3742 3743 3744 3745 3746 3747 3748 3749 3750

  Description []
               
  SideEffects []

  SeeAlso     []
 
***********************************************************************/
Abc_Ntk_t * Abc_NtkBalanceExor( Abc_Ntk_t * pNtk, int fUpdateLevel, int fVerbose )
{
    extern void Dar_BalancePrintStats( Aig_Man_t * p );
    Abc_Ntk_t * pNtkAig;
    Aig_Man_t * pMan, * pTemp;//, * pTemp2;
    assert( Abc_NtkIsStrash(pNtk) );
    // derive AIG with EXORs
    pMan = Abc_NtkToDar( pNtk, 1, 0 );
    if ( pMan == NULL )
        return NULL;
//    Aig_ManPrintStats( pMan );
    if ( fVerbose )
        Dar_BalancePrintStats( pMan );
    // perform balancing
    pTemp = Dar_ManBalance( pMan, fUpdateLevel );
//    Aig_ManPrintStats( pTemp );
    // create logic network
    pNtkAig = Abc_NtkFromDar( pNtk, pTemp );
    Aig_ManStop( pTemp );
    Aig_ManStop( pMan );
    return pNtkAig;
}

Alan Mishchenko committed
3751 3752 3753 3754 3755 3756 3757 3758 3759 3760 3761
/**Function*************************************************************

  Synopsis    [Performs phase abstraction.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
3762
Abc_Ntk_t * Abc_NtkPhaseAbstract( Abc_Ntk_t * pNtk, int nFrames, int nPref, int fIgnore, int fPrint, int fVerbose )
Alan Mishchenko committed
3763
{
Alan Mishchenko committed
3764
    extern Aig_Man_t * Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrames, int nPref, int fIgnore, int fPrint, int fVerbose );
Alan Mishchenko committed
3765 3766 3767
    Vec_Int_t * vInits;
    Abc_Ntk_t * pNtkAig;
    Aig_Man_t * pMan, * pTemp;
Alan Mishchenko committed
3768
    pMan = Abc_NtkToDar( pNtk, 0, 1 );
Alan Mishchenko committed
3769 3770 3771
    if ( pMan == NULL )
        return NULL;
    vInits = Abc_NtkGetLatchValues(pNtk);
Alan Mishchenko committed
3772
    pMan = Saig_ManPhaseAbstract( pTemp = pMan, vInits, nFrames, nPref, fIgnore, fPrint, fVerbose );
Alan Mishchenko committed
3773 3774 3775 3776 3777
    Vec_IntFree( vInits );
    Aig_ManStop( pTemp );
    if ( pMan == NULL )
        return NULL;
    pNtkAig = Abc_NtkFromAigPhase( pMan );
Alan Mishchenko committed
3778 3779
//    pNtkAig->pName = Extra_UtilStrsav(pNtk->pName);
//    pNtkAig->pSpec = Extra_UtilStrsav(pNtk->pSpec);
Alan Mishchenko committed
3780 3781 3782 3783
    Aig_ManStop( pMan );
    return pNtkAig;
}

Alan Mishchenko committed
3784 3785
/**Function*************************************************************

Alan Mishchenko committed
3786 3787 3788 3789 3790 3791 3792 3793 3794
  Synopsis    [Performs phase abstraction.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
3795 3796 3797 3798 3799 3800 3801 3802 3803 3804 3805 3806 3807 3808 3809 3810 3811 3812 3813 3814 3815 3816 3817 3818 3819 3820 3821
int Abc_NtkPhaseFrameNum( Abc_Ntk_t * pNtk )
{
    extern int Saig_ManPhaseFrameNum( Aig_Man_t * p, Vec_Int_t * vInits );
    Vec_Int_t * vInits;
    Aig_Man_t * pMan;
    int nFrames;
    pMan = Abc_NtkToDar( pNtk, 0, 1 );
    if ( pMan == NULL )
        return 1;
    vInits = Abc_NtkGetLatchValues(pNtk);
    nFrames = Saig_ManPhaseFrameNum( pMan, vInits );
    Vec_IntFree( vInits );
    Aig_ManStop( pMan );
    return nFrames;
}

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

  Synopsis    [Performs phase abstraction.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
3822 3823 3824 3825 3826 3827 3828 3829 3830 3831 3832 3833 3834 3835 3836 3837 3838 3839 3840 3841 3842 3843 3844 3845 3846 3847 3848 3849 3850 3851 3852 3853 3854 3855 3856 3857 3858 3859 3860 3861 3862 3863 3864 3865 3866 3867 3868 3869
Abc_Ntk_t * Abc_NtkDarSynchOne( Abc_Ntk_t * pNtk, int nWords, int fVerbose )
{
    extern Aig_Man_t * Saig_SynchSequenceApply( Aig_Man_t * pAig, int nWords, int fVerbose );
    Abc_Ntk_t * pNtkAig;
    Aig_Man_t * pMan, * pTemp;
    pMan = Abc_NtkToDar( pNtk, 0, 1 );
    if ( pMan == NULL )
        return NULL;
    pMan = Saig_SynchSequenceApply( pTemp = pMan, nWords, fVerbose );
    Aig_ManStop( pTemp );
    if ( pMan == NULL )
        return NULL;
    pNtkAig = Abc_NtkFromDar( pNtk, pMan );
    Aig_ManStop( pMan );
    return pNtkAig;
}

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

  Synopsis    [Performs phase abstraction.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Abc_Ntk_t * Abc_NtkDarSynch( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nWords, int fVerbose )
{
    extern Aig_Man_t * Saig_Synchronize( Aig_Man_t * pAig1, Aig_Man_t * pAig2, int nWords, int fVerbose );
    Abc_Ntk_t * pNtkAig;
    Aig_Man_t * pMan1, * pMan2, * pMan;
    pMan1 = Abc_NtkToDar( pNtk1, 0, 1 );
    if ( pMan1 == NULL )
        return NULL;
    pMan2 = Abc_NtkToDar( pNtk2, 0, 1 );
    if ( pMan2 == NULL )
    {
        Aig_ManStop( pMan1 );
        return NULL;
    }
    pMan = Saig_Synchronize( pMan1, pMan2, nWords, fVerbose );
    Aig_ManStop( pMan1 );
    Aig_ManStop( pMan2 );
    if ( pMan == NULL )
        return NULL;
    pNtkAig = Abc_NtkFromAigPhase( pMan );
Alan Mishchenko committed
3870 3871
//    pNtkAig->pName = Extra_UtilStrsav("miter");
//    pNtkAig->pSpec = NULL;
Alan Mishchenko committed
3872 3873 3874 3875 3876 3877 3878 3879 3880 3881 3882 3883 3884 3885 3886
    Aig_ManStop( pMan );
    return pNtkAig;
}

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

  Synopsis    [Performs phase abstraction.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
3887 3888 3889 3890 3891 3892 3893 3894 3895 3896 3897 3898 3899 3900 3901 3902 3903 3904 3905 3906 3907 3908 3909 3910 3911 3912 3913 3914 3915 3916 3917 3918 3919 3920 3921 3922 3923 3924
Abc_Ntk_t * Abc_NtkDarClockGate( Abc_Ntk_t * pNtk, Abc_Ntk_t * pCare, Cgt_Par_t * pPars )
{
    Abc_Ntk_t * pNtkAig;
    Aig_Man_t * pMan1, * pMan2 = NULL, * pMan;
    pMan1 = Abc_NtkToDar( pNtk, 0, 1 );
    if ( pMan1 == NULL )
        return NULL;
    if ( pCare )
    {
        pMan2 = Abc_NtkToDar( pCare, 0, 0 );
        if ( pMan2 == NULL )
        {
            Aig_ManStop( pMan1 );
            return NULL;
        }
    }
    pMan = Cgt_ClockGating( pMan1, pMan2, pPars );
    Aig_ManStop( pMan1 );
    if ( pMan2 )
        Aig_ManStop( pMan2 );
    if ( pMan == NULL )
        return NULL;
    pNtkAig = Abc_NtkFromDar( pNtk, pMan );
    Aig_ManStop( pMan );
    return pNtkAig;
}

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

  Synopsis    [Performs phase abstraction.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
3925 3926 3927 3928 3929 3930 3931 3932 3933 3934 3935
Abc_Ntk_t * Abc_NtkDarExtWin( Abc_Ntk_t * pNtk, int nObjId, int nDist, int fVerbose )
{
    Abc_Ntk_t * pNtkAig;
    Aig_Man_t * pMan1, * pMan;
    Aig_Obj_t * pObj;
    pMan1 = Abc_NtkToDar( pNtk, 0, 1 );
    if ( pMan1 == NULL )
        return NULL;
    if ( nObjId == -1 )
    {
        pObj = Saig_ManFindPivot( pMan1 );
3936
        Abc_Print( 1, "Selected object %d as a window pivot.\n", pObj->Id );
Alan Mishchenko committed
3937 3938 3939 3940 3941 3942
    }
    else
    {
        if ( nObjId >= Aig_ManObjNumMax(pMan1) )
        {
            Aig_ManStop( pMan1 );
3943
            Abc_Print( 1, "The ID is too large.\n" );
Alan Mishchenko committed
3944 3945 3946 3947 3948 3949
            return NULL;
        }
        pObj = Aig_ManObj( pMan1, nObjId );
        if ( pObj == NULL )
        {
            Aig_ManStop( pMan1 );
3950
            Abc_Print( 1, "Object with ID %d does not exist.\n", nObjId );
Alan Mishchenko committed
3951 3952 3953 3954 3955
            return NULL;
        }
        if ( !Saig_ObjIsLo(pMan1, pObj) && !Aig_ObjIsNode(pObj) )
        {
            Aig_ManStop( pMan1 );
3956
            Abc_Print( 1, "Object with ID %d is not a node or reg output.\n", nObjId );
Alan Mishchenko committed
3957 3958 3959 3960 3961 3962 3963 3964 3965 3966 3967 3968 3969 3970 3971 3972 3973 3974 3975 3976 3977 3978 3979 3980 3981 3982 3983 3984 3985 3986 3987 3988 3989 3990 3991 3992
            return NULL;
        }
    }
    pMan = Saig_ManWindowExtract( pMan1, pObj, nDist );
    Aig_ManStop( pMan1 );
    if ( pMan == NULL )
        return NULL;
    pNtkAig = Abc_NtkFromAigPhase( pMan );
    pNtkAig->pName = Extra_UtilStrsav(pNtk->pName);
    pNtkAig->pSpec = Extra_UtilStrsav(pNtk->pSpec);
    Aig_ManStop( pMan );
    return pNtkAig;
}

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

  Synopsis    [Performs phase abstraction.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Abc_Ntk_t * Abc_NtkDarInsWin( Abc_Ntk_t * pNtk, Abc_Ntk_t * pCare, int nObjId, int nDist, int fVerbose )
{
    Abc_Ntk_t * pNtkAig;
    Aig_Man_t * pMan1, * pMan2 = NULL, * pMan;
    Aig_Obj_t * pObj;
    pMan1 = Abc_NtkToDar( pNtk, 0, 1 );
    if ( pMan1 == NULL )
        return NULL;
    if ( nObjId == -1 )
    {
        pObj = Saig_ManFindPivot( pMan1 );
3993
        Abc_Print( 1, "Selected object %d as a window pivot.\n", pObj->Id );
Alan Mishchenko committed
3994 3995 3996 3997 3998 3999
    }
    else
    {
        if ( nObjId >= Aig_ManObjNumMax(pMan1) )
        {
            Aig_ManStop( pMan1 );
4000
            Abc_Print( 1, "The ID is too large.\n" );
Alan Mishchenko committed
4001 4002 4003 4004 4005 4006
            return NULL;
        }
        pObj = Aig_ManObj( pMan1, nObjId );
        if ( pObj == NULL )
        {
            Aig_ManStop( pMan1 );
4007
            Abc_Print( 1, "Object with ID %d does not exist.\n", nObjId );
Alan Mishchenko committed
4008 4009 4010 4011 4012
            return NULL;
        }
        if ( !Saig_ObjIsLo(pMan1, pObj) && !Aig_ObjIsNode(pObj) )
        {
            Aig_ManStop( pMan1 );
4013
            Abc_Print( 1, "Object with ID %d is not a node or reg output.\n", nObjId );
Alan Mishchenko committed
4014 4015 4016 4017 4018 4019 4020 4021 4022 4023 4024 4025 4026 4027 4028 4029 4030 4031 4032 4033 4034 4035 4036 4037 4038 4039 4040 4041 4042 4043 4044 4045 4046 4047
            return NULL;
        }
    }
    if ( pCare )
    {
        pMan2 = Abc_NtkToDar( pCare, 0, 0 );
        if ( pMan2 == NULL )
        {
            Aig_ManStop( pMan1 );
            return NULL;
        }
    }
    pMan = Saig_ManWindowInsert( pMan1, pObj, nDist, pMan2 );
    Aig_ManStop( pMan1 );
    if ( pMan2 )
        Aig_ManStop( pMan2 );
    if ( pMan == NULL )
        return NULL;
    pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
    Aig_ManStop( pMan );
    return pNtkAig;
}

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

  Synopsis    [Performs phase abstraction.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
4048 4049 4050 4051
Abc_Ntk_t * Abc_NtkDarFrames( Abc_Ntk_t * pNtk, int nPrefix, int nFrames, int fInit, int fVerbose )
{
    Abc_Ntk_t * pNtkAig;
    Aig_Man_t * pMan, * pTemp;
Alan Mishchenko committed
4052
    pMan = Abc_NtkToDar( pNtk, 0, 1 );
Alan Mishchenko committed
4053 4054 4055 4056 4057 4058 4059 4060 4061 4062 4063 4064 4065 4066 4067
    if ( pMan == NULL )
        return NULL;
    pMan = Saig_ManTimeframeSimplify( pTemp = pMan, nPrefix, nFrames, fInit, fVerbose );
    Aig_ManStop( pTemp );
    if ( pMan == NULL )
        return NULL;
    pNtkAig = Abc_NtkFromAigPhase( pMan );
    pNtkAig->pName = Extra_UtilStrsav(pNtk->pName);
    pNtkAig->pSpec = Extra_UtilStrsav(pNtk->pSpec);
    Aig_ManStop( pMan );
    return pNtkAig;
}

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

Alan Mishchenko committed
4068 4069 4070 4071 4072 4073 4074 4075 4076 4077 4078 4079 4080 4081 4082 4083 4084 4085
  Synopsis    [Performs phase abstraction.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Abc_Ntk_t * Abc_NtkDarCleanupAig( Abc_Ntk_t * pNtk, int fCleanupPis, int fCleanupPos, int fVerbose )
{
    Abc_Ntk_t * pNtkAig;
    Aig_Man_t * pMan;
    pMan = Abc_NtkToDar( pNtk, 0, 1 );
    if ( pMan == NULL )
        return NULL;
    if ( fCleanupPis )
    {
4086
        int Temp = Aig_ManCiCleanup( pMan );
Alan Mishchenko committed
4087
        if ( fVerbose )
4088
            Abc_Print( 1, "Cleanup removed %d primary inputs without fanout.\n", Temp );                                                                     
Alan Mishchenko committed
4089 4090 4091
    }
    if ( fCleanupPos )
    {
4092
        int Temp = Aig_ManCoCleanup( pMan );
Alan Mishchenko committed
4093
        if ( fVerbose )
4094
            Abc_Print( 1, "Cleanup removed %d primary outputs driven by const-0.\n", Temp );                                                                     
Alan Mishchenko committed
4095 4096 4097 4098 4099 4100 4101 4102 4103 4104
    }
    pNtkAig = Abc_NtkFromAigPhase( pMan );
    pNtkAig->pName = Extra_UtilStrsav(pNtk->pName);
    pNtkAig->pSpec = Extra_UtilStrsav(pNtk->pSpec);
    Aig_ManStop( pMan );
    return pNtkAig;
}

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

Alan Mishchenko committed
4105 4106 4107 4108 4109 4110 4111 4112 4113
  Synopsis    [Performs BDD-based reachability analysis.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
4114
int Abc_NtkDarReach( Abc_Ntk_t * pNtk, Saig_ParBbr_t * pPars )
Alan Mishchenko committed
4115 4116
{
    Aig_Man_t * pMan;
4117
    int RetValue;
Alan Mishchenko committed
4118
    pMan = Abc_NtkToDar( pNtk, 0, 1 );
Alan Mishchenko committed
4119
    if ( pMan == NULL )
4120 4121
        return -1;
    RetValue = Aig_ManVerifyUsingBdds( pMan, pPars );
Alan Mishchenko committed
4122 4123
    ABC_FREE( pNtk->pModel );
    ABC_FREE( pNtk->pSeqModel );
Alan Mishchenko committed
4124
    pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
Alan Mishchenko committed
4125
    Aig_ManStop( pMan );
4126
    return RetValue;
Alan Mishchenko committed
4127 4128
}

4129 4130
ABC_NAMESPACE_IMPL_END

4131 4132
#include "map/amap/amap.h"
#include "map/mio/mio.h"
Alan Mishchenko committed
4133

4134 4135 4136
ABC_NAMESPACE_IMPL_START


Alan Mishchenko committed
4137 4138 4139 4140 4141 4142 4143 4144 4145 4146 4147 4148 4149
/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Abc_Ntk_t * Amap_ManProduceNetwork( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMapping )
{
4150 4151
//    extern void * Abc_FrameReadLibGen();
    Mio_Library_t * pLib = (Mio_Library_t *)Abc_FrameReadLibGen();
Alan Mishchenko committed
4152 4153 4154 4155 4156 4157
    Amap_Out_t * pRes;
    Vec_Ptr_t * vNodesNew;
    Abc_Ntk_t * pNtkNew;
    Abc_Obj_t * pNodeNew, * pFaninNew;
    int i, k, iPis, iPos, nDupGates;
    // make sure gates exist in the current library
4158
    Vec_PtrForEachEntry( Amap_Out_t *, vMapping, pRes, i )
4159
        if ( pRes->pName && Mio_LibraryReadGateByName( pLib, pRes->pName, NULL ) == NULL )
Alan Mishchenko committed
4160
        {
4161
            Abc_Print( 1, "Current library does not contain gate \"%s\".\n", pRes->pName );
Alan Mishchenko committed
4162 4163 4164 4165 4166 4167 4168
            return NULL;
        }
    // create the network
    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_MAP );
    pNtkNew->pManFunc = pLib;
    iPis = iPos = 0;
    vNodesNew = Vec_PtrAlloc( Vec_PtrSize(vMapping) );
4169
    Vec_PtrForEachEntry( Amap_Out_t *, vMapping, pRes, i )
Alan Mishchenko committed
4170 4171 4172 4173 4174 4175 4176 4177
    {
        if ( pRes->Type == -1 )
            pNodeNew = Abc_NtkCi( pNtkNew, iPis++ );
        else if ( pRes->Type == 1 )
            pNodeNew = Abc_NtkCo( pNtkNew, iPos++ );
        else
        {
            pNodeNew = Abc_NtkCreateNode( pNtkNew );
4178
            pNodeNew->pData = Mio_LibraryReadGateByName( pLib, pRes->pName, NULL );
Alan Mishchenko committed
4179 4180 4181
        }
        for ( k = 0; k < pRes->nFans; k++ )
        {
4182
            pFaninNew = (Abc_Obj_t *)Vec_PtrEntry( vNodesNew, pRes->pFans[k] );
Alan Mishchenko committed
4183 4184 4185 4186 4187 4188 4189 4190
            Abc_ObjAddFanin( pNodeNew, pFaninNew );
        }
        Vec_PtrPush( vNodesNew, pNodeNew );
    }
    Vec_PtrFree( vNodesNew );
    assert( iPis == Abc_NtkCiNum(pNtkNew) );
    assert( iPos == Abc_NtkCoNum(pNtkNew) );
    // decouple the PO driver nodes to reduce the number of levels
4191
    nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
Alan Mishchenko committed
4192
//    if ( nDupGates && Map_ManReadVerbose(pMan) )
4193
//        Abc_Print( 1, "Duplicated %d gates to decouple the CO drivers.\n", nDupGates );
Alan Mishchenko committed
4194 4195 4196 4197 4198 4199 4200 4201 4202 4203 4204 4205 4206 4207 4208 4209
    return pNtkNew;
}

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

  Synopsis    [Gives the current ABC network to AIG manager for processing.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Abc_Ntk_t * Abc_NtkDarAmap( Abc_Ntk_t * pNtk, Amap_Par_t * pPars )
{
Alan Mishchenko committed
4210
    extern Vec_Ptr_t * Amap_ManTest( Aig_Man_t * pAig, Amap_Par_t * pPars );
Alan Mishchenko committed
4211 4212 4213 4214 4215 4216 4217 4218 4219 4220 4221 4222 4223 4224 4225 4226
    Vec_Ptr_t * vMapping;
    Abc_Ntk_t * pNtkAig = NULL;
    Aig_Man_t * pMan;
    Aig_MmFlex_t * pMem;

    assert( Abc_NtkIsStrash(pNtk) );
    // convert to the AIG manager
    pMan = Abc_NtkToDarChoices( pNtk );
    if ( pMan == NULL )
        return NULL;

    // perform computation
    vMapping = Amap_ManTest( pMan, pPars );
    Aig_ManStop( pMan );
    if ( vMapping == NULL )
        return NULL;
4227
    pMem = (Aig_MmFlex_t *)Vec_PtrPop( vMapping );
Alan Mishchenko committed
4228 4229 4230 4231 4232 4233 4234
    pNtkAig = Amap_ManProduceNetwork( pNtk, vMapping );
    Aig_MmFlexStop( pMem, 0 );
    Vec_PtrFree( vMapping );

    // make sure everything is okay
    if ( pNtkAig && !Abc_NtkCheck( pNtkAig ) )
    {
4235
        Abc_Print( 1, "Abc_NtkDar: The network check has failed.\n" );
Alan Mishchenko committed
4236 4237 4238 4239 4240
        Abc_NtkDelete( pNtkAig );
        return NULL;
    }
    return pNtkAig;
}
Alan Mishchenko committed
4241

Alan Mishchenko committed
4242 4243 4244 4245 4246 4247 4248 4249 4250 4251 4252
/**Function*************************************************************

  Synopsis    [Performs BDD-based reachability analysis.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
4253 4254 4255 4256 4257 4258 4259 4260 4261 4262 4263 4264 4265 4266 4267 4268 4269 4270 4271 4272 4273
void Abc_NtkDarConstr( Abc_Ntk_t * pNtk, int nFrames, int nConfs, int nProps, int fStruct, int fOldAlgo, int fVerbose )
{
    Aig_Man_t * pMan;//, * pMan2;//, * pTemp;
    assert( Abc_NtkIsStrash(pNtk) );
    pMan = Abc_NtkToDar( pNtk, 0, 1 );
    if ( pMan == NULL )
        return;
    if ( fStruct )
        Saig_ManDetectConstrTest( pMan );
    else
        Saig_ManDetectConstrFuncTest( pMan, nFrames, nConfs, nProps, fOldAlgo, fVerbose );
    Aig_ManStop( pMan );
}

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

  Synopsis    [Performs BDD-based reachability analysis.]

  Description []
               
  SideEffects []
4274 4275 4276 4277 4278 4279 4280 4281 4282 4283 4284 4285 4286 4287 4288 4289 4290 4291 4292 4293 4294 4295 4296 4297 4298 4299 4300 4301 4302 4303

  SeeAlso     []

***********************************************************************/
Abc_Ntk_t * Abc_NtkDarOutdec( Abc_Ntk_t * pNtk, int nLits, int fVerbose )
{
    Abc_Ntk_t * pNtkAig;
    Aig_Man_t * pMan, * pTemp;
    assert( Abc_NtkIsStrash(pNtk) );
    pMan = Abc_NtkToDar( pNtk, 0, 1 );
    if ( pMan == NULL )
        return NULL;
    pMan = Saig_ManDecPropertyOutput( pTemp = pMan, nLits, fVerbose );
    Aig_ManStop( pTemp );
    if ( pMan == NULL )
        return NULL;
    pNtkAig = Abc_NtkFromAigPhase( pMan );
    pNtkAig->pName = Extra_UtilStrsav(pMan->pName);
    pNtkAig->pSpec = Extra_UtilStrsav(pMan->pSpec);
    Aig_ManStop( pMan );
    return pNtkAig;
}

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

  Synopsis    [Performs BDD-based reachability analysis.]

  Description []
               
  SideEffects []
4304 4305 4306 4307 4308 4309 4310 4311 4312 4313 4314 4315 4316 4317 4318 4319 4320 4321 4322 4323 4324 4325 4326 4327 4328 4329 4330 4331 4332 4333 4334 4335 4336 4337 4338 4339 4340 4341 4342 4343 4344 4345 4346 4347 4348 4349 4350 4351 4352 4353 4354 4355 4356 4357 4358 4359 4360 4361 4362 4363 4364 4365 4366 4367 4368 4369 4370 4371 4372 4373 4374 4375 4376 4377 4378 4379 4380 4381 4382 4383 4384 4385 4386 4387 4388 4389 4390 4391

  SeeAlso     []

***********************************************************************/
Abc_Ntk_t * Abc_NtkDarUnfold( Abc_Ntk_t * pNtk, int nFrames, int nConfs, int nProps, int fStruct, int fOldAlgo, int fVerbose )
{
    Abc_Ntk_t * pNtkAig;
    Aig_Man_t * pMan, * pTemp;
    assert( Abc_NtkIsStrash(pNtk) );
    pMan = Abc_NtkToDar( pNtk, 0, 1 );
    if ( pMan == NULL )
        return NULL;
    if ( fStruct )
        pMan = Saig_ManDupUnfoldConstrs( pTemp = pMan );
    else
        pMan = Saig_ManDupUnfoldConstrsFunc( pTemp = pMan, nFrames, nConfs, nProps, fOldAlgo, fVerbose );
    Aig_ManStop( pTemp );
    if ( pMan == NULL )
        return NULL;
    pNtkAig = Abc_NtkFromAigPhase( pMan );
    pNtkAig->pName = Extra_UtilStrsav(pMan->pName);
    pNtkAig->pSpec = Extra_UtilStrsav(pMan->pSpec);
    Aig_ManStop( pMan );
    return pNtkAig;
}

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

  Synopsis    [Performs BDD-based reachability analysis.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Abc_Ntk_t * Abc_NtkDarFold( Abc_Ntk_t * pNtk, int fCompl, int fVerbose )
{
    Abc_Ntk_t * pNtkAig;
    Aig_Man_t * pMan, * pTemp;
    assert( Abc_NtkIsStrash(pNtk) );
    pMan = Abc_NtkToDar( pNtk, 0, 1 );
    if ( pMan == NULL )
        return NULL;
    pMan = Saig_ManDupFoldConstrsFunc( pTemp = pMan, fCompl, fVerbose );
    Aig_ManStop( pTemp );
    pNtkAig = Abc_NtkFromAigPhase( pMan );
    pNtkAig->pName = Extra_UtilStrsav(pMan->pName);
    pNtkAig->pSpec = Extra_UtilStrsav(pMan->pSpec);
    Aig_ManStop( pMan );
    return pNtkAig;
}

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

  Synopsis    [Performs BDD-based reachability analysis.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_NtkDarConstrProfile( Abc_Ntk_t * pNtk, int fVerbose )
{
    extern int Ssw_ManProfileConstraints( Aig_Man_t * p, int nWords, int nFrames, int fVerbose );
    extern Vec_Int_t * Saig_ManComputeSwitchProbs( Aig_Man_t * p, int nFrames, int nPref, int fProbOne );
    Aig_Man_t * pMan;
//    Vec_Int_t * vProbOne;
//    Aig_Obj_t * pObj;
//    int i, Entry;
    assert( Abc_NtkIsStrash(pNtk) );
    assert( Abc_NtkConstrNum(pNtk) );
    pMan = Abc_NtkToDar( pNtk, 0, 1 );
    if ( pMan == NULL )
        return;
    // value in the init state
//    Abc_AigSetNodePhases( pNtk );
/*
    // derive probabilities
    vProbOne = Saig_ManComputeSwitchProbs( pMan, 48, 16, 1 );
    // iterate over the constraint outputs
    Saig_ManForEachPo( pMan, pObj, i )
    {
        Entry = Vec_IntEntry( vProbOne, Aig_ObjId(pObj) );
        if ( i < Saig_ManPoNum(pMan) - Saig_ManConstrNum(pMan) )
4392
            Abc_Print( 1, "Primary output :  ", i );
4393
        else
4394 4395 4396 4397
            Abc_Print( 1, "Constraint %3d :  ", i-(Saig_ManPoNum(pMan) - Saig_ManConstrNum(pMan)) );
        Abc_Print( 1, "ProbOne = %f  ", Abc_Int2Float(Entry) );
        Abc_Print( 1, "AllZeroValue = %d ", Aig_ObjPhase(pObj) );
        Abc_Print( 1, "\n" );
4398 4399 4400 4401
    }
*/
    // double-check
    Ssw_ManProfileConstraints( pMan, 16, 64, 1 );
4402
    Abc_Print( 1, "TwoFrameSatValue = %d.\n", Ssw_ManSetConstrPhases(pMan, 2, NULL) );
4403 4404 4405 4406 4407 4408 4409 4410 4411 4412 4413 4414 4415 4416 4417 4418
    // clean up
//    Vec_IntFree( vProbOne );
    Aig_ManStop( pMan );
}

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

  Synopsis    [Performs BDD-based reachability analysis.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
4419
void Abc_NtkDarTest( Abc_Ntk_t * pNtk, int Num )
Alan Mishchenko committed
4420
{
4421 4422
//    extern void Saig_ManDetectConstr( Aig_Man_t * p );
//    extern void Saig_ManDetectConstrFuncTest( Aig_Man_t * p );
4423 4424 4425
//    extern void Saig_ManFoldConstrTest( Aig_Man_t * pAig );
    extern void Llb_ManComputeDomsTest( Aig_Man_t * pAig, int Num );

4426 4427


Alan Mishchenko committed
4428
//    extern void Fsim_ManTest( Aig_Man_t * pAig );
Alan Mishchenko committed
4429 4430 4431
    extern Vec_Int_t * Saig_StrSimPerformMatching( Aig_Man_t * p0, Aig_Man_t * p1, int nDist, int fVerbose, Aig_Man_t ** ppMiter );
//    Vec_Int_t * vPairs;
    Aig_Man_t * pMan;//, * pMan2;//, * pTemp;
Alan Mishchenko committed
4432 4433 4434 4435
    assert( Abc_NtkIsStrash(pNtk) );
    pMan = Abc_NtkToDar( pNtk, 0, 1 );
    if ( pMan == NULL )
        return;
Alan Mishchenko committed
4436
/*
Alan Mishchenko committed
4437 4438 4439 4440 4441 4442
Aig_ManSetRegNum( pMan, pMan->nRegs );
Aig_ManPrintStats( pMan );
Saig_ManDumpBlif( pMan, "_temp_.blif" );
Aig_ManStop( pMan );
pMan = Saig_ManReadBlif( "_temp_.blif" );
Aig_ManPrintStats( pMan );
Alan Mishchenko committed
4443
*/
Alan Mishchenko committed
4444
/*
Alan Mishchenko committed
4445 4446 4447
    Aig_ManSetRegNum( pMan, pMan->nRegs );
    pTemp = Ssw_SignalCorrespondeceTestPairs( pMan );
    Aig_ManStop( pTemp );
Alan Mishchenko committed
4448 4449
*/

Alan Mishchenko committed
4450 4451 4452 4453 4454
/*
//    Ssw_SecSpecialMiter( pMan, NULL, 2, 1 );
    pMan2 = Aig_ManDupSimple(pMan);
    vPairs = Saig_StrSimPerformMatching( pMan, pMan2, 0, 1, NULL );
    Vec_IntFree( vPairs );
Alan Mishchenko committed
4455
    Aig_ManStop( pMan );
Alan Mishchenko committed
4456 4457
    Aig_ManStop( pMan2 );
*/
4458 4459 4460 4461 4462 4463 4464 4465 4466 4467 4468 4469 4470
//    Ioa_WriteAigerBufferTest( pMan, "test.aig", 0, 0 );
//    Saig_ManFoldConstrTest( pMan );
    {
    extern void Saig_ManBmcSectionsTest( Aig_Man_t * p );
    extern void Saig_ManBmcTerSimTest( Aig_Man_t * p );
    extern void Saig_ManBmcSupergateTest( Aig_Man_t * p );
    extern void Saig_ManBmcMappingTest( Aig_Man_t * p );
//    Saig_ManBmcSectionsTest( pMan );
//    Saig_ManBmcTerSimTest( pMan );
//    Saig_ManBmcSupergateTest( pMan );
//    Saig_ManBmcMappingTest( pMan );
    }

4471 4472 4473 4474
    {
//        void Pdr_ManEquivClasses( Aig_Man_t * pMan );
//        Pdr_ManEquivClasses( pMan );
    }
4475

4476 4477 4478 4479 4480 4481 4482 4483 4484
//    Llb_ManComputeDomsTest( pMan, Num );
    {
        extern void Llb_ManMinCutTest( Aig_Man_t * pMan, int Num );
        extern void Llb_BddStructAnalysis( Aig_Man_t * pMan );
        extern void Llb_NonlinExperiment( Aig_Man_t * pAig, int Num );
//        Llb_BddStructAnalysis( pMan );
        Llb_ManMinCutTest( pMan, Num );
//        Llb_NonlinExperiment( pMan, Num );
    }
Alan Mishchenko committed
4485 4486

//    Saig_MvManSimulate( pMan, 1 );
4487 4488
//    Saig_ManDetectConstr( pMan );
//    Saig_ManDetectConstrFuncTest( pMan );
Alan Mishchenko committed
4489

Alan Mishchenko committed
4490
//    Fsim_ManTest( pMan );
Alan Mishchenko committed
4491 4492
    Aig_ManStop( pMan );

Alan Mishchenko committed
4493
}
Alan Mishchenko committed
4494

Alan Mishchenko committed
4495 4496 4497 4498 4499 4500 4501 4502 4503 4504 4505 4506 4507
/**Function*************************************************************

  Synopsis    [Performs BDD-based reachability analysis.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk )
{
Alan Mishchenko committed
4508
//    extern Aig_Man_t * Saig_ManDualRail( Aig_Man_t * p, int fMiter );
Alan Mishchenko committed
4509

Alan Mishchenko committed
4510
/*
Alan Mishchenko committed
4511 4512 4513 4514 4515 4516 4517 4518 4519 4520 4521 4522
    extern Aig_Man_t * Ssw_SignalCorrespondeceTestPairs( Aig_Man_t * pAig );

    Abc_Ntk_t * pNtkAig;
    Aig_Man_t * pMan, * pTemp;
    assert( Abc_NtkIsStrash(pNtk) );
    pMan = Abc_NtkToDar( pNtk, 0, 1 );
    if ( pMan == NULL )
        return NULL;

    Aig_ManSetRegNum( pMan, pMan->nRegs );
    pMan = Ssw_SignalCorrespondeceTestPairs( pTemp = pMan );
    Aig_ManStop( pTemp );
Alan Mishchenko committed
4523 4524
    if ( pMan == NULL )
        return NULL;
Alan Mishchenko committed
4525 4526 4527 4528

    pNtkAig = Abc_NtkFromAigPhase( pMan );
    pNtkAig->pName = Extra_UtilStrsav(pNtk->pName);
    pNtkAig->pSpec = Extra_UtilStrsav(pNtk->pSpec);
Alan Mishchenko committed
4529
    Aig_ManStop( pMan );
Alan Mishchenko committed
4530
    return pNtkAig;
Alan Mishchenko committed
4531 4532
*/
    Abc_Ntk_t * pNtkAig;
Alan Mishchenko committed
4533
    Aig_Man_t * pMan;//, * pTemp;
Alan Mishchenko committed
4534 4535 4536 4537
    assert( Abc_NtkIsStrash(pNtk) );
    pMan = Abc_NtkToDar( pNtk, 0, 1 );
    if ( pMan == NULL )
        return NULL;
4538

Alan Mishchenko committed
4539
/*
Alan Mishchenko committed
4540
    Aig_ManSetRegNum( pMan, pMan->nRegs );
Alan Mishchenko committed
4541
    pMan = Saig_ManDualRail( pTemp = pMan, 1 );
Alan Mishchenko committed
4542
    Aig_ManStop( pTemp );
Alan Mishchenko committed
4543 4544
    if ( pMan == NULL )
        return NULL;
Alan Mishchenko committed
4545 4546 4547 4548 4549

    pNtkAig = Abc_NtkFromAigPhase( pMan );
    pNtkAig->pName = Extra_UtilStrsav(pNtk->pName);
    pNtkAig->pSpec = Extra_UtilStrsav(pNtk->pSpec);
    Aig_ManStop( pMan );
Alan Mishchenko committed
4550 4551 4552 4553 4554
*/

    pNtkAig = Abc_NtkFromDar( pNtk, pMan );
    Aig_ManStop( pMan );

Alan Mishchenko committed
4555 4556
    return pNtkAig;

Alan Mishchenko committed
4557 4558
}

Alan Mishchenko committed
4559 4560 4561 4562
////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////

Jiang Long committed
4563
#include "abcDarUnfold2.c"
4564 4565
ABC_NAMESPACE_IMPL_END