saigHaig.c 23 KB
Newer Older
Alan Mishchenko committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24
/**CFile****************************************************************

  FileName    [saigHaig.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Sequential AIG package.]

  Synopsis    [Experiments with history AIG recording.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - April 28, 2007.]

  Revision    [$Id: saigHaig.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]

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

#include "saig.h"
#include "satSolver.h"
#include "cnf.h"

25 26 27
ABC_NAMESPACE_IMPL_START


Alan Mishchenko committed
28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48
////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

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

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

  Synopsis    [Prepares the inductive case with speculative reduction.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Aig_ManHaigSpeculate( Aig_Man_t * pFrames, Aig_Obj_t * pObj )
{
Alan Mishchenko committed
49 50
    Aig_Obj_t * pObjNew, * pObjNew2, * pObjRepr, * pObjReprNew;//, * pMiter;
    Aig_Obj_t * pPo;
Alan Mishchenko committed
51 52 53 54
    // skip nodes without representative
    pObjRepr = pObj->pHaig;
    if ( pObjRepr == NULL )
        return;
Alan Mishchenko committed
55
//    assert( pObjRepr->Id < pObj->Id );
Alan Mishchenko committed
56
    // get the new node 
57
    pObjNew = (Aig_Obj_t *)pObj->pData;
Alan Mishchenko committed
58
    // get the new node of the representative
59
    pObjReprNew = (Aig_Obj_t *)pObjRepr->pData;
Alan Mishchenko committed
60
    // if this is the same node, no need to add constraints
Alan Mishchenko committed
61
    assert( pObjNew != NULL && pObjReprNew != NULL );
Alan Mishchenko committed
62 63 64 65 66 67 68
    if ( Aig_Regular(pObjNew) == Aig_Regular(pObjReprNew) )
        return;
    // these are different nodes - perform speculative reduction
    pObjNew2 = Aig_NotCond( pObjReprNew, pObj->fPhase ^ pObjRepr->fPhase );
    // set the new node
    pObj->pData = pObjNew2;
    // add the constraint
Alan Mishchenko committed
69 70 71 72 73 74 75 76 77 78 79 80 81
    if ( pObj->fMarkA )
        return;
//    pMiter = Aig_Exor( pFrames, pObjNew, pObjReprNew );
//    pMiter = Aig_NotCond( pMiter, !Aig_ObjPhaseReal(pMiter) );
//    assert( Aig_ObjPhaseReal(pMiter) == 1 );
//    Aig_ObjCreatePo( pFrames, pMiter );
    if ( Aig_ObjPhaseReal(pObjNew) != Aig_ObjPhaseReal(pObjReprNew) )
        pObjReprNew = Aig_Not(pObjReprNew);
    pPo = Aig_ObjCreatePo( pFrames, pObjNew );
    Aig_ObjCreatePo( pFrames, pObjReprNew );

    // remember the node corresponding to this PO
    pPo->pData = pObj;
Alan Mishchenko committed
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
}

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

  Synopsis    [Prepares the inductive case with speculative reduction.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Aig_Man_t * Aig_ManHaigFrames( Aig_Man_t * pHaig, int nFrames )
{
    Aig_Man_t * pFrames;
    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
    int i, f, nAssumptions = 0;
    assert( nFrames == 1 || nFrames == 2 );
    assert( nFrames == 1 || Saig_ManRegNum(pHaig) > 0 );
    // start AIG manager for timeframes
    pFrames = Aig_ManStart( Aig_ManNodeNum(pHaig) * nFrames );
    pFrames->pName = Aig_UtilStrsav( pHaig->pName );
    pFrames->pSpec = Aig_UtilStrsav( pHaig->pSpec );
    // map the constant node
    Aig_ManConst1(pHaig)->pData = Aig_ManConst1( pFrames );
    // create variables for register outputs
    Saig_ManForEachLo( pHaig, pObj, i )
        pObj->pData = Aig_ObjCreatePi( pFrames );
    // add timeframes
    Aig_ManSetPioNumbers( pHaig );
    for ( f = 0; f < nFrames; f++ )
    {
Alan Mishchenko committed
115 116 117 118 119 120 121 122
        // create primary inputs
        Saig_ManForEachPi( pHaig, pObj, i )
            pObj->pData = Aig_ObjCreatePi( pFrames );
        // create internal nodes
        Aig_ManForEachNode( pHaig, pObj, i )
        {        
            pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
            Aig_ManHaigSpeculate( pFrames, pObj );
Alan Mishchenko committed
123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151
        }
        if ( f == nFrames - 2 )
            nAssumptions = Aig_ManPoNum(pFrames);
        if ( f == nFrames - 1 )
            break;
        // save register inputs
        Saig_ManForEachLi( pHaig, pObj, i )
            pObj->pData = Aig_ObjChild0Copy(pObj);
        // transfer to register outputs
        Saig_ManForEachLiLo(  pHaig, pObjLi, pObjLo, i )
            pObjLo->pData = pObjLi->pData;
    }
    Aig_ManCleanup( pFrames );
    pFrames->nAsserts = Aig_ManPoNum(pFrames) - nAssumptions;
    Aig_ManSetRegNum( pFrames, 0 );
    return pFrames;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200
int Aig_ManMapHaigNodes( Aig_Man_t * pHaig )
{
    Aig_Obj_t * pObj1, * pObj2;
    int Id1, Id2, i, Counter = 0;
    Aig_ManForEachObj( pHaig, pObj1, i )
        pObj1->pHaig = NULL;
    Vec_IntForEachEntry( pHaig->vEquPairs, Id1, i )
    {
        Id2 = Vec_IntEntry( pHaig->vEquPairs, ++i );
        pObj1 = Aig_ManObj( pHaig, Id1 );
        pObj2 = Aig_ManObj( pHaig, Id2 );
        assert( pObj1 != pObj2 );
        assert( !Aig_ObjIsPi(pObj1) || !Aig_ObjIsPi(pObj2) );
        if ( Aig_ObjIsPi(pObj1) )
        {
            Counter += (int)(pObj2->pHaig != NULL);
            pObj2->pHaig = pObj1;
        }
        else if ( Aig_ObjIsPi(pObj2) )
        {
            Counter += (int)(pObj1->pHaig != NULL);
            pObj1->pHaig = pObj2;
        }
        else if ( pObj1->Id < pObj2->Id )
        {
            Counter += (int)(pObj2->pHaig != NULL);
            pObj2->pHaig = pObj1;
        }
        else 
        {
            Counter += (int)(pObj1->pHaig != NULL);
            pObj1->pHaig = pObj2;
        }
    }
//    printf( "Overwrites %d out of %d.\n", Counter, Vec_IntSize(pHaig->vEquPairs)/2 );
    return Counter;
}
 
/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
201
int Aig_ManHaigVerify( Aig_Man_t * p, Aig_Man_t * pAig, Aig_Man_t * pHaig, int nFrames, int clkSynth )
Alan Mishchenko committed
202 203
{
    int nBTLimit = 0;
Alan Mishchenko committed
204
    Aig_Man_t * pFrames, * pTemp;
Alan Mishchenko committed
205 206
    Cnf_Dat_t * pCnf;
    sat_solver * pSat;
Alan Mishchenko committed
207
    Aig_Obj_t * pObj1, * pObj2;
Alan Mishchenko committed
208
    int i, RetValue1, RetValue2, Counter, Lits[2], nOvers;
Alan Mishchenko committed
209
    int clk = clock(), clkVerif;
Alan Mishchenko committed
210

Alan Mishchenko committed
211
    nOvers = Aig_ManMapHaigNodes( pHaig );
Alan Mishchenko committed
212

Alan Mishchenko committed
213 214
    // create time frames with speculative reduction and convert them into CNF
clk = clock();
Alan Mishchenko committed
215 216
    pFrames = Aig_ManHaigFrames( pHaig, nFrames );
    Aig_ManCleanMarkA( pHaig );
Alan Mishchenko committed
217 218

    printf( "Frames:     " );
Alan Mishchenko committed
219
    Aig_ManPrintStats( pFrames );
Alan Mishchenko committed
220

Alan Mishchenko committed
221 222
    pFrames = Dar_ManRwsat( pTemp = pFrames, 1, 0 );
    Aig_ManStop( pTemp );
Alan Mishchenko committed
223

Alan Mishchenko committed
224
    printf( "Frames synt:" );
Alan Mishchenko committed
225 226
    Aig_ManPrintStats( pFrames );

Alan Mishchenko committed
227 228
    printf( "Additional frames stats: Assumptions = %d. Assertions = %d. Pairs = %d. Over = %d.\n", 
        Aig_ManPoNum(pFrames)/2 - pFrames->nAsserts/2, pFrames->nAsserts/2, Vec_IntSize(pHaig->vEquPairs)/2, nOvers );
Alan Mishchenko committed
229 230
//    pCnf = Cnf_DeriveSimple( pFrames, Aig_ManPoNum(pFrames) );
    pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) );
Alan Mishchenko committed
231

Alan Mishchenko committed
232 233 234 235 236 237 238


//    pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) - pFrames->nAsserts );
//Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 );
//    Saig_ManDumpBlif( pHaig, "haig_temp.blif" );
//    Saig_ManDumpBlif( pFrames, "haig_temp_frames.blif" );
    // create the SAT solver to be used for this problem
239
    pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
Alan Mishchenko committed
240
    if ( pSat == NULL )
Alan Mishchenko committed
241
    {
Alan Mishchenko committed
242 243 244 245 246 247 248 249
        printf( "Aig_ManHaigVerify(): Computed CNF is not valid.\n" );
        return 0;
    }

    if ( nFrames == 2 )
    {
        // add clauses for the first frame
        Aig_ManForEachPo( pFrames, pObj1, i )
Alan Mishchenko committed
250
        {
Alan Mishchenko committed
251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270
            if ( i >= Aig_ManPoNum(pFrames) - pFrames->nAsserts )
                break;

            pObj2 = Aig_ManPo( pFrames, ++i );
            assert( pObj1->fPhase == pObj2->fPhase );

            Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id], 0 );
            Lits[1] = toLitCond( pCnf->pVarNums[pObj2->Id], 1 );
            if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
            {
                sat_solver_delete( pSat );
                return 0;
            }
            Lits[0]++;
            Lits[1]--;
            if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
            {
                sat_solver_delete( pSat );
                return 0;
            }
Alan Mishchenko committed
271
        }
Alan Mishchenko committed
272 273 274 275 276 277 278

        if ( !sat_solver_simplify(pSat) )
        {
            sat_solver_delete( pSat );
            return 0;
        }
    }
Alan Mishchenko committed
279
ABC_PRT( "Preparation", clock() - clk );
Alan Mishchenko committed
280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296


    // check in the second timeframe
clk = clock();
    Counter = 0;
    printf( "Started solving ...\r" );
    Aig_ManForEachPo( pFrames, pObj1, i )
    {
        if ( i < Aig_ManPoNum(pFrames) - pFrames->nAsserts )
            continue;

        pObj2 = Aig_ManPo( pFrames, ++i );
        assert( pObj1->fPhase == pObj2->fPhase );

        Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id], 0 );
        Lits[1] = toLitCond( pCnf->pVarNums[pObj2->Id], 1 );

Alan Mishchenko committed
297
        RetValue1 = sat_solver_solve( pSat, Lits, Lits + 2, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
Alan Mishchenko committed
298 299 300 301 302 303 304 305 306 307 308
        if ( RetValue1 == l_False )
        {
            Lits[0] = lit_neg( Lits[0] );
            Lits[1] = lit_neg( Lits[1] );
//            RetValue = sat_solver_addclause( pSat, Lits, Lits + 2 );
//            assert( RetValue );
        }

        Lits[0]++;
        Lits[1]--;

Alan Mishchenko committed
309
        RetValue2 = sat_solver_solve( pSat, Lits, Lits + 2, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
Alan Mishchenko committed
310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326
        if ( RetValue2 == l_False )
        {
            Lits[0] = lit_neg( Lits[0] );
            Lits[1] = lit_neg( Lits[1] );
//            RetValue = sat_solver_addclause( pSat, Lits, Lits + 2 );
//            assert( RetValue );
        }

        if ( RetValue1 != l_False || RetValue2 != l_False )
            Counter++;

        if ( i % 50 == 1 )
            printf( "Solving assertion %6d out of %6d.\r", 
                (i - (Aig_ManPoNum(pFrames) - pFrames->nAsserts))/2, 
                pFrames->nAsserts/2 );
//        if ( nClasses == 1000 )
//            break;
Alan Mishchenko committed
327
    }
Alan Mishchenko committed
328
    printf( "                                                          \r" );
Alan Mishchenko committed
329
ABC_PRT( "Solving    ", clock() - clk );
Alan Mishchenko committed
330
clkVerif = clock() - clk;
Alan Mishchenko committed
331 332 333 334
    if ( Counter )
        printf( "Verification failed for %d out of %d assertions.\n", Counter, pFrames->nAsserts/2 );
    else
        printf( "Verification is successful for all %d assertions.\n", pFrames->nAsserts/2 );
Alan Mishchenko committed
335

Alan Mishchenko committed
336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389
    // print the statistic into a file
    {
        FILE * pTable;
        Aig_Man_t * pTemp, * pHaig2;

        pHaig2 = pAig->pManHaig; 
        pAig->pManHaig = NULL;
        pTemp = Aig_ManDupDfs( pAig );
        pAig->pManHaig = pHaig2;

        Aig_ManSeqCleanup( pTemp );

        pTable = fopen( "stats.txt", "a+" );
        fprintf( pTable, "%s ",  p->pName );
        fprintf( pTable, "%d ", Saig_ManPiNum(p) );
        fprintf( pTable, "%d ", Saig_ManPoNum(p) );

        fprintf( pTable, "%d ", Saig_ManRegNum(p) );
        fprintf( pTable, "%d ", Aig_ManNodeNum(p) );
        fprintf( pTable, "%d ", Aig_ManLevelNum(p) );

        fprintf( pTable, "%d ", Saig_ManRegNum(pTemp) );
        fprintf( pTable, "%d ", Aig_ManNodeNum(pTemp) );
        fprintf( pTable, "%d ", Aig_ManLevelNum(pTemp) );

        fprintf( pTable, "%d ", Saig_ManRegNum(pHaig) );
        fprintf( pTable, "%d ", Aig_ManNodeNum(pHaig) );
        fprintf( pTable, "%d ", Aig_ManLevelNum(pHaig) );

        fprintf( pTable, "%.2f", (float)(clkSynth)/(float)(CLOCKS_PER_SEC) );
        fprintf( pTable, "\n" );
        fclose( pTable );


        pTable = fopen( "stats2.txt", "a+" );
        fprintf( pTable, "%s ",  p->pName );
        fprintf( pTable, "%d ", Aig_ManNodeNum(pFrames) );
        fprintf( pTable, "%d ", Aig_ManLevelNum(pFrames) );

        fprintf( pTable, "%d ", pCnf->nVars );
        fprintf( pTable, "%d ", pCnf->nClauses );
        fprintf( pTable, "%d ", pCnf->nLiterals );

        fprintf( pTable, "%d ", Aig_ManPoNum(pFrames)/2 - pFrames->nAsserts/2 );
        fprintf( pTable, "%d ", pFrames->nAsserts/2 );
        fprintf( pTable, "%d ", Vec_IntSize(pHaig->vEquPairs)/2 );

        fprintf( pTable, "%.2f", (float)(clkVerif)/(float)(CLOCKS_PER_SEC) );
        fprintf( pTable, "\n" );
        fclose( pTable );

        Aig_ManStop( pTemp );
    }

Alan Mishchenko committed
390 391 392 393
    // clean up
    Aig_ManStop( pFrames );
    Cnf_DataFree( pCnf );
    sat_solver_delete( pSat );
Alan Mishchenko committed
394
    return 1;
Alan Mishchenko committed
395 396 397 398 399 400 401 402 403 404 405 406 407
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
408
int Aig_ManHaigVerify2( Aig_Man_t * p, Aig_Man_t * pAig, Aig_Man_t * pHaig, int nFrames )
Alan Mishchenko committed
409 410 411 412
{
    int nBTLimit = 0;
    Cnf_Dat_t * pCnf;
    sat_solver * pSat;
Alan Mishchenko committed
413 414
    Aig_Obj_t * pObj1, * pObj2;
    int i, RetValue1, RetValue2, Counter, Lits[2];
Alan Mishchenko committed
415
    int clk = clock();
Alan Mishchenko committed
416 417
    int Delta;
    int Id1, Id2;
Alan Mishchenko committed
418 419 420 421 422

    assert( nFrames == 1 || nFrames == 2 );

clk = clock();
    pCnf = Cnf_DeriveSimple( pHaig, Aig_ManPoNum(pHaig) );
Alan Mishchenko committed
423 424 425 426
//    Aig_ManForEachObj( pHaig, pObj, i )
//        printf( "%d=%d  ", pObj->Id, pCnf->pVarNums[pObj->Id] );
//    printf( "\n" );

Alan Mishchenko committed
427
    // create the SAT solver to be used for this problem
428
    pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, nFrames, 0 );
Alan Mishchenko committed
429
//Sat_SolverWriteDimacs( pSat, "1.cnf", NULL, NULL, 0 );
Alan Mishchenko committed
430 431 432 433 434 435 436 437
    if ( pSat == NULL )
    {
        printf( "Aig_ManHaigVerify(): Computed CNF is not valid.\n" );
        return -1;
    }

    if ( nFrames == 2 )
    {
Alan Mishchenko committed
438
        Vec_IntForEachEntry( pHaig->vEquPairs, Id1, i )
Alan Mishchenko committed
439
        {
Alan Mishchenko committed
440 441 442 443
            Id2 = Vec_IntEntry( pHaig->vEquPairs, ++i );
            pObj1 = Aig_ManObj( pHaig, Id1 );
            pObj2 = Aig_ManObj( pHaig, Id2 );
            if ( pObj1->fPhase ^ pObj2->fPhase )
Alan Mishchenko committed
444
            {
Alan Mishchenko committed
445 446
                Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id], 0 );
                Lits[1] = toLitCond( pCnf->pVarNums[pObj2->Id], 0 );
Alan Mishchenko committed
447 448 449 450 451 452 453 454 455 456 457 458 459 460 461
                if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
                {
                    sat_solver_delete( pSat );
                    return 0;
                }
                Lits[0]++;
                Lits[1]++;
                if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
                {
                    sat_solver_delete( pSat );
                    return 0;
                }
            }
            else
            {
Alan Mishchenko committed
462 463
                Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id], 0 );
                Lits[1] = toLitCond( pCnf->pVarNums[pObj2->Id], 1 );
Alan Mishchenko committed
464 465 466 467 468 469 470 471 472 473 474 475 476 477 478
                if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
                {
                    sat_solver_delete( pSat );
                    return 0;
                }
                Lits[0]++;
                Lits[1]--;
                if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
                {
                    sat_solver_delete( pSat );
                    return 0;
                }
            }
        }

Alan Mishchenko committed
479 480 481 482
        if ( !sat_solver_simplify(pSat) )
        {
            sat_solver_delete( pSat );
            return 0;
Alan Mishchenko committed
483 484
        }
    }
Alan Mishchenko committed
485
ABC_PRT( "Preparation", clock() - clk );
Alan Mishchenko committed
486 487 488 489 490


    // check in the second timeframe
clk = clock();
    Counter = 0;
Alan Mishchenko committed
491 492
    Delta = (nFrames == 2)? pCnf->nVars : 0;
    Vec_IntForEachEntry( pHaig->vEquPairs, Id1, i )
Alan Mishchenko committed
493
    {
Alan Mishchenko committed
494 495 496 497
        Id2 = Vec_IntEntry( pHaig->vEquPairs, ++i );
        pObj1 = Aig_ManObj( pHaig, Id1 );
        pObj2 = Aig_ManObj( pHaig, Id2 );
        if ( pObj1->fPhase ^ pObj2->fPhase )
Alan Mishchenko committed
498
        {
Alan Mishchenko committed
499 500
            Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id]+Delta, 0 );
            Lits[1] = toLitCond( pCnf->pVarNums[pObj2->Id]+Delta, 0 );
Alan Mishchenko committed
501

Alan Mishchenko committed
502
            RetValue1 = sat_solver_solve( pSat, Lits, Lits + 2, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
Alan Mishchenko committed
503 504 505 506

            Lits[0]++;
            Lits[1]++;

Alan Mishchenko committed
507
            RetValue2 = sat_solver_solve( pSat, Lits, Lits + 2, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
Alan Mishchenko committed
508 509

            if ( RetValue1 != l_False || RetValue2 != l_False )
Alan Mishchenko committed
510 511 512 513
                Counter++;
        }
        else
        {
Alan Mishchenko committed
514 515
            Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id]+Delta, 0 );
            Lits[1] = toLitCond( pCnf->pVarNums[pObj2->Id]+Delta, 1 );
Alan Mishchenko committed
516

Alan Mishchenko committed
517
            RetValue1 = sat_solver_solve( pSat, Lits, Lits + 2, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
Alan Mishchenko committed
518 519 520 521

            Lits[0]++;
            Lits[1]--;

Alan Mishchenko committed
522
            RetValue2 = sat_solver_solve( pSat, Lits, Lits + 2, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
Alan Mishchenko committed
523 524

            if ( RetValue1 != l_False || RetValue2 != l_False )
Alan Mishchenko committed
525 526
                Counter++;
        }
Alan Mishchenko committed
527 528 529 530 531
        if ( i % 50 == 1 )
            printf( "Solving assertion %6d out of %6d.\r", i/2, Vec_IntSize(pHaig->vEquPairs)/2 );

//        if ( i / 2 > 1000 )
//            break;
Alan Mishchenko committed
532
    }
Alan Mishchenko committed
533
ABC_PRT( "Solving    ", clock() - clk );
Alan Mishchenko committed
534
    if ( Counter )
Alan Mishchenko committed
535
        printf( "Verification failed for %d out of %d classes.\n", Counter, Vec_IntSize(pHaig->vEquPairs)/2 );
Alan Mishchenko committed
536
    else
Alan Mishchenko committed
537
        printf( "Verification is successful for all %d classes.\n", Vec_IntSize(pHaig->vEquPairs)/2 );
Alan Mishchenko committed
538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554

    Cnf_DataFree( pCnf );
    sat_solver_delete( pSat );
    return 1;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591
Aig_Man_t * Saig_ManHaigDump( Aig_Man_t * pHaig )
{
    Vec_Ptr_t * vTemp;
    Aig_Obj_t * pObj, * pObj1, * pObj2, * pMiter;
    int Id1, Id2, i;
    // remove regular POs
    Aig_ManSetPioNumbers( pHaig );
    vTemp = Vec_PtrAlloc( Saig_ManRegNum(pHaig) );
    Aig_ManForEachPo( pHaig, pObj, i )
    {
        if ( Saig_ObjIsPo(pHaig, pObj) )
        {
            Aig_ObjDisconnect( pHaig, pObj );
            Vec_PtrWriteEntry( pHaig->vObjs, pObj->Id, NULL );
        }
        else
        {
            Vec_PtrPush( vTemp, pObj );
        }
    }
    Vec_PtrShrink( pHaig->vPos, 0 ); 
    pHaig->nObjs[AIG_OBJ_PO] = Vec_PtrSize( vTemp );
    // add new POs
    Vec_IntForEachEntry( pHaig->vEquPairs, Id1, i )
    {
        Id2 = Vec_IntEntry( pHaig->vEquPairs, ++i );
        pObj1 = Aig_ManObj( pHaig, Id1 );
        pObj2 = Aig_ManObj( pHaig, Id2 );
        assert( pObj1 != pObj2 );
        assert( !Aig_ObjIsPi(pObj1) || !Aig_ObjIsPi(pObj2) );
        pMiter = Aig_Exor( pHaig, pObj1, pObj2 );
        pMiter = Aig_NotCond( pMiter, Aig_ObjPhaseReal(pMiter) );
        assert( Aig_ObjPhaseReal(pMiter) == 0 );
        Aig_ObjCreatePo( pHaig, pMiter );
    }
    printf( "Added %d property outputs.\n", Vec_IntSize(pHaig->vEquPairs)/2 );
    // add the registers
592
    Vec_PtrForEachEntry( Aig_Obj_t *, vTemp, pObj, i )
Alan Mishchenko committed
593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621
        Vec_PtrPush( pHaig->vPos, pObj );
    Vec_PtrFree( vTemp );
    assert( pHaig->nObjs[AIG_OBJ_PO] ==  Vec_PtrSize(pHaig->vPos) ); 
    Aig_ManCleanup( pHaig );
    Aig_ManSetRegNum( pHaig, pHaig->nRegs );
//    return pHaig;

    printf( "HAIG:       " );
    Aig_ManPrintStats( pHaig );
    printf( "HAIG is written into file \"haig.blif\".\n" );
    Saig_ManDumpBlif( pHaig, "haig.blif" );

    Vec_IntFree( pHaig->vEquPairs );
    Aig_ManStop( pHaig );
    return NULL;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Aig_Man_t * Saig_ManHaigRecord( Aig_Man_t * p, int nIters, int nSteps, int fRetimingOnly, int fAddBugs, int fUseCnf, int fVerbose )
Alan Mishchenko committed
622
{
Alan Mishchenko committed
623
    int fSeqHaig = (int)( Aig_ManRegNum(p) > 0 );
Alan Mishchenko committed
624 625 626
    Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
    Aig_Man_t * pNew, * pTemp;
    Aig_Obj_t * pObj;
Alan Mishchenko committed
627
    int i, k, nStepsReal, clk = clock(), clkSynth;
Alan Mishchenko committed
628
    Dar_ManDefaultRwrParams( pParsRwr );
Alan Mishchenko committed
629 630

clk = clock();
Alan Mishchenko committed
631 632 633 634 635
    // duplicate this manager
    pNew = Aig_ManDupSimple( p );
    // create its history AIG
    pNew->pManHaig = Aig_ManDupSimple( pNew );
    Aig_ManForEachObj( pNew, pObj, i )
636
        pObj->pHaig = (Aig_Obj_t *)pObj->pData;
Alan Mishchenko committed
637 638
    // remove structural hashing table
    Aig_TableClear( pNew->pManHaig );
Alan Mishchenko committed
639
    pNew->pManHaig->vEquPairs = Vec_IntAlloc( 10000 );
Alan Mishchenko committed
640
ABC_PRT( "HAIG setup time", clock() - clk );
Alan Mishchenko committed
641

Alan Mishchenko committed
642 643
clk = clock();
    if ( fSeqHaig )
Alan Mishchenko committed
644
    {
Alan Mishchenko committed
645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672
        if ( fRetimingOnly )
        {
            // perform retiming
            nStepsReal = Saig_ManRetimeSteps( pNew, nSteps, 1, fAddBugs ); 
            pNew = Aig_ManDupSimpleDfs( pTemp = pNew ); 
            Aig_ManStop( pTemp );
            printf( "Performed %d retiming moves.\n", nStepsReal );
        }
        else
        {
            for ( k = 0; k < nIters; k++ )
            {
                // perform balancing
                pNew = Dar_ManBalance( pTemp = pNew, 0 );
                Aig_ManStop( pTemp );

                // perform rewriting
                Dar_ManRewrite( pNew, pParsRwr );
                pNew = Aig_ManDupDfs( pTemp = pNew ); 
                Aig_ManStop( pTemp );

                // perform retiming
                nStepsReal = Saig_ManRetimeSteps( pNew, nSteps, 1, fAddBugs ); 
                pNew = Aig_ManDupSimpleDfs( pTemp = pNew ); 
                Aig_ManStop( pTemp );
                printf( "Performed %d retiming moves.\n", nStepsReal );
            }
        }
Alan Mishchenko committed
673 674 675
    }
    else
    {
Alan Mishchenko committed
676 677 678 679 680 681 682 683 684 685 686
        for ( k = 0; k < nIters; k++ )
        {
            // perform balancing
            pNew = Dar_ManBalance( pTemp = pNew, 0 );
            Aig_ManStop( pTemp );

            // perform rewriting
            Dar_ManRewrite( pNew, pParsRwr );
            pNew = Aig_ManDupDfs( pTemp = pNew ); 
            Aig_ManStop( pTemp );
        }
Alan Mishchenko committed
687
    } 
Alan Mishchenko committed
688
ABC_PRT( "Synthesis time ", clock() - clk );
Alan Mishchenko committed
689
clkSynth = clock() - clk;
Alan Mishchenko committed
690 691

    // use the haig for verification
Alan Mishchenko committed
692
//    Aig_ManAntiCleanup( pNew->pManHaig );
Alan Mishchenko committed
693 694 695
    Aig_ManSetRegNum( pNew->pManHaig, pNew->pManHaig->nRegs );
//Aig_ManShow( pNew->pManHaig, 0, NULL ); 

Alan Mishchenko committed
696 697 698
    printf( "AIG before: " );
    Aig_ManPrintStats( p );
    printf( "AIG after:  " );
Alan Mishchenko committed
699
    Aig_ManPrintStats( pNew );
Alan Mishchenko committed
700
    printf( "HAIG:       " );
Alan Mishchenko committed
701 702
    Aig_ManPrintStats( pNew->pManHaig );

Alan Mishchenko committed
703 704
    if ( fUseCnf )
    {
Alan Mishchenko committed
705
        if ( !Aig_ManHaigVerify2( p, pNew, pNew->pManHaig, 1+fSeqHaig ) )
Alan Mishchenko committed
706 707 708 709
            printf( "Constructing SAT solver has failed.\n" );         
    }
    else
    {
Alan Mishchenko committed
710
        if ( !Aig_ManHaigVerify( p, pNew, pNew->pManHaig, 1+fSeqHaig, clkSynth ) )
Alan Mishchenko committed
711 712
            printf( "Constructing SAT solver has failed.\n" );         
    }
Alan Mishchenko committed
713

Alan Mishchenko committed
714 715 716 717
    Saig_ManHaigDump( pNew->pManHaig );
    pNew->pManHaig = NULL;
    return pNew;
/*
Alan Mishchenko committed
718
    // cleanup
Alan Mishchenko committed
719
    Vec_IntFree( pNew->pManHaig->vEquPairs );
Alan Mishchenko committed
720 721
    Aig_ManStop( pNew->pManHaig );
    pNew->pManHaig = NULL;
Alan Mishchenko committed
722 723
    return pNew;
*/
Alan Mishchenko committed
724 725 726 727 728 729 730
}

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


731 732
ABC_NAMESPACE_IMPL_END