sswDyn.c 15.8 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
/**CFile****************************************************************

  FileName    [sswDyn.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Inductive prover with constraints.]

  Synopsis    [Dynamic loading of constraints.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - September 1, 2008.]

  Revision    [$Id: sswDyn.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]

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

#include "sswInt.h"
22
#include "misc/bar/bar.h"
Alan Mishchenko committed
23

24 25 26
ABC_NAMESPACE_IMPL_START


Alan Mishchenko committed
27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56
////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

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

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

  Synopsis    [Label PIs nodes of the frames corresponding to PIs of AIG.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ssw_ManLabelPiNodes( Ssw_Man_t * p )
{
    Aig_Obj_t * pObj, * pObjFrames;
    int f, i;
    Aig_ManConst1( p->pFrames )->fMarkA = 1;
    Aig_ManConst1( p->pFrames )->fMarkB = 1;
    for ( f = 0; f < p->nFrames; f++ )
    {
        Saig_ManForEachPi( p->pAig, pObj, i )
        {
            pObjFrames = Ssw_ObjFrame( p, pObj, f );
57
            assert( Aig_ObjIsCi(pObjFrames) );
Alan Mishchenko committed
58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81
            assert( pObjFrames->fMarkB == 0 );
            pObjFrames->fMarkA = 1;
            pObjFrames->fMarkB = 1;
        }
    }
}

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

  Synopsis    [Collects new POs in p->vNewPos.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ssw_ManCollectPis_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vNewPis )
{
    assert( !Aig_IsComplement(pObj) );
    if ( pObj->fMarkA )
        return;
    pObj->fMarkA = 1;
82
    if ( Aig_ObjIsCi(pObj) )
Alan Mishchenko committed
83 84 85 86 87 88 89 90 91 92 93 94 95 96
    {
        Vec_PtrPush( vNewPis, pObj );
        return;
    }
    assert( Aig_ObjIsNode(pObj) );
    Ssw_ManCollectPis_rec( Aig_ObjFanin0(pObj), vNewPis );
    Ssw_ManCollectPis_rec( Aig_ObjFanin1(pObj), vNewPis );
}

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

  Synopsis    [Collects new POs in p->vNewPos.]

  Description []
97

Alan Mishchenko committed
98 99 100 101 102 103 104 105 106 107 108 109 110 111 112
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ssw_ManCollectPos_rec( Ssw_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t * vNewPos )
{
    Aig_Obj_t * pFanout;
    int iFanout = -1, i;
    assert( !Aig_IsComplement(pObj) );
    if ( pObj->fMarkB )
        return;
    pObj->fMarkB = 1;
    if ( pObj->Id > p->nSRMiterMaxId )
        return;
113
    if ( Aig_ObjIsCo(pObj) )
Alan Mishchenko committed
114 115
    {
        // skip if it is a register input PO
116
        if ( Aig_ObjCioId(pObj) >= Aig_ManCoNum(p->pFrames)-Aig_ManRegNum(p->pAig) )
Alan Mishchenko committed
117 118
            return;
        // add the number of this constraint
119
        Vec_IntPush( vNewPos, Aig_ObjCioId(pObj)/2 );
Alan Mishchenko committed
120 121 122 123 124 125 126 127 128 129 130 131
        return;
    }
    // visit the fanouts
    assert( p->pFrames->pFanData != NULL );
    Aig_ObjForEachFanout( p->pFrames, pObj, pFanout, iFanout, i )
        Ssw_ManCollectPos_rec( p, pFanout, vNewPos );
}

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

  Synopsis    [Loads logic cones and relevant constraints.]

132
  Description [Both pRepr and pObj are objects of the AIG.
Alan Mishchenko committed
133
  The result is the current SAT solver loaded with the logic cones
134
  for pRepr and pObj corresponding to them in the frames,
Alan Mishchenko committed
135
  as well as all the relevant constraints.]
136

Alan Mishchenko committed
137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ssw_ManLoadSolver( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj )
{
    Aig_Obj_t * pObjFrames, * pReprFrames;
    Aig_Obj_t * pTemp, * pObj0, * pObj1;
    int i, iConstr, RetValue;

    assert( pRepr != pObj );
    // get the corresponding frames nodes
    pReprFrames = Aig_Regular( Ssw_ObjFrame( p, pRepr, p->pPars->nFramesK ) );
    pObjFrames  = Aig_Regular( Ssw_ObjFrame( p, pObj,  p->pPars->nFramesK ) );
    assert( pReprFrames != pObjFrames );
 /*
154
    // compute the AIG support
Alan Mishchenko committed
155 156 157 158
    Vec_PtrClear( p->vNewLos );
    Ssw_ManCollectPis_rec( pRepr, p->vNewLos );
    Ssw_ManCollectPis_rec( pObj,  p->vNewLos );
    // add logic cones for register outputs
159
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vNewLos, pTemp, i )
Alan Mishchenko committed
160 161 162 163 164 165 166 167 168
    {
        pObj0 = Aig_Regular( Ssw_ObjFrame( p, pTemp, p->pPars->nFramesK ) );
        Ssw_CnfNodeAddToSolver( p->pMSat, pObj0 );
    }
*/
    // add cones for the nodes
    Ssw_CnfNodeAddToSolver( p->pMSat, pReprFrames );
    Ssw_CnfNodeAddToSolver( p->pMSat, pObjFrames );

169
    // compute the frames support
Alan Mishchenko committed
170 171 172 173 174 175 176 177
    Vec_PtrClear( p->vNewLos );
    Ssw_ManCollectPis_rec( pReprFrames, p->vNewLos );
    Ssw_ManCollectPis_rec( pObjFrames,  p->vNewLos );
    // these nodes include both nodes corresponding to PIs and LOs
    // (the nodes corresponding to PIs should be labeled with fMarkB!)

    // collect the related constraint POs
    Vec_IntClear( p->vNewPos );
178
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vNewLos, pTemp, i )
Alan Mishchenko committed
179 180 181 182
        Ssw_ManCollectPos_rec( p, pTemp, p->vNewPos );
    // check if the corresponding pairs are added
    Vec_IntForEachEntry( p->vNewPos, iConstr, i )
    {
183 184
        pObj0 = Aig_ManCo( p->pFrames, 2*iConstr   );
        pObj1 = Aig_ManCo( p->pFrames, 2*iConstr+1 );
Alan Mishchenko committed
185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204
//        if ( pObj0->fMarkB && pObj1->fMarkB )
        if ( pObj0->fMarkB || pObj1->fMarkB )
        {
            pObj0->fMarkB = 1;
            pObj1->fMarkB = 1;
            Ssw_NodesAreConstrained( p, Aig_ObjChild0(pObj0), Aig_ObjChild0(pObj1) );
        }
    }
    if ( p->pMSat->pSat->qtail != p->pMSat->pSat->qhead )
    {
        RetValue = sat_solver_simplify(p->pMSat->pSat);
        assert( RetValue != 0 );
    }
}

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

  Synopsis    [Tranfers simulation information from FRAIG to AIG.]

  Description []
205

Alan Mishchenko committed
206 207 208 209 210 211 212 213 214 215 216 217
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ssw_ManSweepTransferDyn( Ssw_Man_t * p )
{
    Aig_Obj_t * pObj, * pObjFraig;
    unsigned * pInfo;
    int i, f, nFrames;

    // transfer simulation information
218
    Aig_ManForEachCi( p->pAig, pObj, i )
Alan Mishchenko committed
219 220 221 222 223 224 225 226
    {
        pObjFraig = Ssw_ObjFrame( p, pObj, 0 );
        if ( pObjFraig == Aig_ManConst0(p->pFrames) )
        {
            Ssw_SmlObjAssignConst( p->pSml, pObj, 0, 0 );
            continue;
        }
        assert( !Aig_IsComplement(pObjFraig) );
227
        assert( Aig_ObjIsCi(pObjFraig) );
228
        pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjCioId(pObjFraig) );
Alan Mishchenko committed
229 230 231 232 233 234 235 236 237
        Ssw_SmlObjSetWord( p->pSml, pObj, pInfo[0], 0, 0 );
    }
    // set random simulation info for the second frame
    for ( f = 1; f < p->nFrames; f++ )
    {
        Saig_ManForEachPi( p->pAig, pObj, i )
        {
            pObjFraig = Ssw_ObjFrame( p, pObj, f );
            assert( !Aig_IsComplement(pObjFraig) );
238
            assert( Aig_ObjIsCi(pObjFraig) );
239
            pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjCioId(pObjFraig) );
Alan Mishchenko committed
240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256
            Ssw_SmlObjSetWord( p->pSml, pObj, pInfo[0], 0, f );
        }
    }
    // create random info
    nFrames = Ssw_SmlNumFrames( p->pSml );
    for ( ; f < nFrames; f++ )
    {
        Saig_ManForEachPi( p->pAig, pObj, i )
            Ssw_SmlAssignRandomFrame( p->pSml, pObj, f );
    }
}

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

  Synopsis    [Performs one round of simulation with counter-examples.]

  Description []
257

Alan Mishchenko committed
258 259 260 261 262 263 264
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Ssw_ManSweepResimulateDyn( Ssw_Man_t * p, int f )
{
265
    int RetValue1, RetValue2;
266
    abctime clk = Abc_Clock();
Alan Mishchenko committed
267 268 269 270 271 272 273 274 275 276 277 278 279
    // transfer PI simulation information from storage
//    Ssw_SmlAssignDist1Plus( p->pSml, p->pPatWords );
    Ssw_ManSweepTransferDyn( p );
    // simulate internal nodes
//    Ssw_SmlSimulateOneFrame( p->pSml );
    Ssw_SmlSimulateOne( p->pSml );
    // check equivalence classes
    RetValue1 = Ssw_ClassesRefineConst1( p->ppClasses, 1 );
    RetValue2 = Ssw_ClassesRefine( p->ppClasses, 1 );
    // prepare simulation info for the next round
    Vec_PtrCleanSimInfo( p->vSimInfo, 0, 1 );
    p->nPatterns = 0;
    p->nSimRounds++;
280
p->timeSimSat += Abc_Clock() - clk;
Alan Mishchenko committed
281 282 283 284 285
    return RetValue1 > 0 || RetValue2 > 0;
}

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

Alan Mishchenko committed
286 287 288
  Synopsis    [Performs one round of simulation with counter-examples.]

  Description []
289

Alan Mishchenko committed
290 291 292 293 294 295 296 297
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Ssw_ManSweepResimulateDynLocal( Ssw_Man_t * p, int f )
{
    Aig_Obj_t * pObj, * pRepr, ** ppClass;
298
    int i, k, nSize, RetValue1, RetValue2;
299
    abctime clk = Abc_Clock();
Alan Mishchenko committed
300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334
    p->nSimRounds++;
    // transfer PI simulation information from storage
//    Ssw_SmlAssignDist1Plus( p->pSml, p->pPatWords );
    Ssw_ManSweepTransferDyn( p );
    // determine const1 cands and classes to be simulated
    Vec_PtrClear( p->vResimConsts );
    Vec_PtrClear( p->vResimClasses );
    Aig_ManIncrementTravId( p->pAig );
    for ( i = p->iNodeStart; i < p->iNodeLast + p->pPars->nResimDelta; i++ )
    {
        if ( i >= Aig_ManObjNumMax( p->pAig ) )
            break;
        pObj = Aig_ManObj( p->pAig, i );
        if ( pObj == NULL )
            continue;
        if ( Ssw_ObjIsConst1Cand(p->pAig, pObj) )
        {
            Vec_PtrPush( p->vResimConsts, pObj );
            continue;
        }
        pRepr = Aig_ObjRepr(p->pAig, pObj);
        if ( pRepr == NULL )
            continue;
        if ( Aig_ObjIsTravIdCurrent(p->pAig, pRepr) )
            continue;
        Aig_ObjSetTravIdCurrent(p->pAig, pRepr);
        Vec_PtrPush( p->vResimClasses, pRepr );
    }
    // simulate internal nodes
//    Ssw_SmlSimulateOneFrame( p->pSml );
//    Ssw_SmlSimulateOne( p->pSml );
    // resimulate dynamically
//    Aig_ManIncrementTravId( p->pAig );
//    Aig_ObjIsTravIdCurrent( p->pAig, Aig_ManConst1(p->pAig) );
    p->nVisCounter++;
335
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vResimConsts, pObj, i )
Alan Mishchenko committed
336 337
        Ssw_SmlSimulateOneDyn_rec( p->pSml, pObj, p->nFrames-1, p->pVisited, p->nVisCounter );
    // resimulate the cone of influence of the cand classes
338
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vResimClasses, pRepr, i )
Alan Mishchenko committed
339 340 341 342 343 344 345 346 347 348 349 350
    {
        ppClass = Ssw_ClassesReadClass( p->ppClasses, pRepr, &nSize );
        for ( k = 0; k < nSize; k++ )
            Ssw_SmlSimulateOneDyn_rec( p->pSml, ppClass[k], p->nFrames-1, p->pVisited, p->nVisCounter );
    }

    // check equivalence classes
//    RetValue1 = Ssw_ClassesRefineConst1( p->ppClasses, 1 );
//    RetValue2 = Ssw_ClassesRefine( p->ppClasses, 1 );
    // refine these nodes
    RetValue1 = Ssw_ClassesRefineConst1Group( p->ppClasses, p->vResimConsts, 1 );
    RetValue2 = 0;
351
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vResimClasses, pRepr, i )
Alan Mishchenko committed
352 353 354 355 356 357
        RetValue2 += Ssw_ClassesRefineOneClass( p->ppClasses, pRepr, 1 );

    // prepare simulation info for the next round
    Vec_PtrCleanSimInfo( p->vSimInfo, 0, 1 );
    p->nPatterns = 0;
    p->nSimRounds++;
358
p->timeSimSat += Abc_Clock() - clk;
Alan Mishchenko committed
359 360 361 362 363
    return RetValue1 > 0 || RetValue2 > 0;
}

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

Alan Mishchenko committed
364 365 366
  Synopsis    [Performs fraiging for the internal nodes.]

  Description []
367

Alan Mishchenko committed
368 369 370 371 372 373
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Ssw_ManSweepDyn( Ssw_Man_t * p )
374
{
Alan Mishchenko committed
375 376
    Bar_Progress_t * pProgress = NULL;
    Aig_Obj_t * pObj, * pObjNew;
377
    int i, f;
378
    abctime clk;
Alan Mishchenko committed
379 380

    // perform speculative reduction
381
clk = Abc_Clock();
Alan Mishchenko committed
382 383 384 385 386 387 388 389 390
    // create timeframes
    p->pFrames = Ssw_FramesWithClasses( p );
    Aig_ManFanoutStart( p->pFrames );
    p->nSRMiterMaxId = Aig_ManObjNumMax( p->pFrames );

    // map constants and PIs of the last frame
    f = p->pPars->nFramesK;
    Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
    Saig_ManForEachPi( p->pAig, pObj, i )
391
        Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreateCi(p->pFrames) );
392
    Aig_ManSetCioIds( p->pFrames );
Alan Mishchenko committed
393 394
    // label nodes corresponding to primary inputs
    Ssw_ManLabelPiNodes( p );
395
p->timeReduce += Abc_Clock() - clk;
Alan Mishchenko committed
396 397 398

    // prepare simulation info
    assert( p->vSimInfo == NULL );
399
    p->vSimInfo = Vec_PtrAllocSimInfo( Aig_ManCiNum(p->pFrames), 1 );
Alan Mishchenko committed
400 401 402 403 404 405 406
    Vec_PtrCleanSimInfo( p->vSimInfo, 0, 1 );

    // sweep internal nodes
    p->fRefined = 0;
    Ssw_ClassesClearRefined( p->ppClasses );
    if ( p->pPars->fVerbose )
        pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) );
Alan Mishchenko committed
407
    p->iNodeStart = 0;
Alan Mishchenko committed
408 409
    Aig_ManForEachObj( p->pAig, pObj, i )
    {
Alan Mishchenko committed
410 411
        if ( p->iNodeStart == 0 )
            p->iNodeStart = i;
Alan Mishchenko committed
412 413 414
        if ( p->pPars->fVerbose )
            Bar_ProgressUpdate( pProgress, i, NULL );
        if ( Saig_ObjIsLo(p->pAig, pObj) )
415
            p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0, NULL );
Alan Mishchenko committed
416
        else if ( Aig_ObjIsNode(pObj) )
417
        {
Alan Mishchenko committed
418 419
            pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
            Ssw_ObjSetFrame( p, pObj, f, pObjNew );
420
            p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0, NULL );
Alan Mishchenko committed
421 422
        }
        // check if it is time to recycle the solver
423 424 425
        if ( p->pMSat->pSat == NULL ||
            (p->pPars->nSatVarMax2 &&
             p->pMSat->nSatVars > p->pPars->nSatVarMax2 &&
Alan Mishchenko committed
426 427 428 429
             p->nRecycleCalls > p->pPars->nRecycleCalls2) )
        {
            // resimulate
            if ( p->nPatterns > 0 )
Alan Mishchenko committed
430 431 432 433 434 435 436 437
            {
                p->iNodeLast = i;
                if ( p->pPars->fLocalSim )
                    Ssw_ManSweepResimulateDynLocal( p, f );
                else
                    Ssw_ManSweepResimulateDyn( p, f );
                p->iNodeStart = i+1;
            }
438
//                Abc_Print( 1, "Recycling SAT solver with %d vars and %d calls.\n", 
Alan Mishchenko committed
439 440 441 442 443 444 445 446
//                    p->pMSat->nSatVars, p->nRecycleCalls );
//            Aig_ManCleanMarkAB( p->pAig );
            Aig_ManCleanMarkAB( p->pFrames );
            // label nodes corresponding to primary inputs
            Ssw_ManLabelPiNodes( p );
            // replace the solver
            if ( p->pMSat )
            {
447 448
                p->nVarsMax  = Abc_MaxInt( p->nVarsMax,  p->pMSat->nSatVars );
                p->nCallsMax = Abc_MaxInt( p->nCallsMax, p->pMSat->nSolverCalls );
Alan Mishchenko committed
449 450 451 452 453 454 455 456 457 458
                Ssw_SatStop( p->pMSat );
                p->nRecycles++;
                p->nRecyclesTotal++;
                p->nRecycleCalls = 0;
            }
            p->pMSat = Ssw_SatStart( 0 );
            assert( p->nPatterns == 0 );
        }
        // resimulate
        if ( p->nPatterns == 32 )
Alan Mishchenko committed
459 460 461 462 463 464 465 466
        {
            p->iNodeLast = i;
            if ( p->pPars->fLocalSim )
                Ssw_ManSweepResimulateDynLocal( p, f );
            else
                Ssw_ManSweepResimulateDyn( p, f );
            p->iNodeStart = i+1;
        }
Alan Mishchenko committed
467 468 469
    }
    // resimulate
    if ( p->nPatterns > 0 )
Alan Mishchenko committed
470 471 472 473 474 475 476
    {
        p->iNodeLast = i;
        if ( p->pPars->fLocalSim )
            Ssw_ManSweepResimulateDynLocal( p, f );
        else
            Ssw_ManSweepResimulateDyn( p, f );
    }
Alan Mishchenko committed
477 478 479 480 481 482 483 484 485 486 487 488 489 490
    // collect stats
    if ( p->pPars->fVerbose )
        Bar_ProgressStop( pProgress );

    // cleanup
//    Ssw_ClassesCheck( p->ppClasses );
    return p->fRefined;
}

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


491
ABC_NAMESPACE_IMPL_END