saigBmc2.c 29.9 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    [saigBmc.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Sequential AIG package.]

  Synopsis    [Simple BMC package.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

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

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

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

#include "saig.h"
22 23 24
#include "sat/cnf/cnf.h"
#include "sat/bsat/satStore.h"
#include "proof/ssw/ssw.h"
25 26 27

ABC_NAMESPACE_IMPL_START

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

32
//#define AIG_VISITED       ((Aig_Obj_t *)(ABC_PTRUINT_T)1)
33 34 35 36 37 38 39 40 41 42 43 44 45

typedef struct Saig_Bmc_t_ Saig_Bmc_t;
struct Saig_Bmc_t_
{
    // parameters
    int                   nFramesMax;     // the max number of timeframes to consider
    int                   nNodesMax;      // the max number of nodes to add
    int                   nConfMaxOne;    // the max number of conflicts at a target
    int                   nConfMaxAll;    // the max number of conflicts for all targets
    int                   fVerbose;       // enables verbose output
    // AIG managers
    Aig_Man_t *           pAig;           // the user's AIG manager
    Aig_Man_t *           pFrm;           // Frames manager
46
    Vec_Int_t *           vVisited;       // nodes visited in Frames
47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63
    // node mapping
    int                   nObjs;          // the largest number of an AIG object
    Vec_Ptr_t *           vAig2Frm;       // mapping of AIG nodees into Frames nodes
    // SAT solver
    sat_solver *          pSat;           // SAT solver
    int                   nSatVars;       // the number of used SAT variables
    Vec_Int_t *           vObj2Var;       // mapping of frames objects in CNF variables
    int                   nStitchVars;
    // subproblems
    Vec_Ptr_t *           vTargets;       // targets to be solved in this interval
    int                   iFramePrev;     // previous frame  
    int                   iFrameLast;     // last frame  
    int                   iOutputLast;    // last output
    int                   iFrameFail;     // failed frame 
    int                   iOutputFail;    // failed output
};

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
static inline Aig_Obj_t * Saig_BmcObjFrame( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i )                       
{ 
//    return (Aig_Obj_t *)Vec_PtrGetEntry( p->vAig2Frm, p->nObjs*i+pObj->Id );     
    Aig_Obj_t * pRes;
    Vec_Int_t * vFrame = (Vec_Int_t *)Vec_PtrEntry( p->vAig2Frm, i );
    int iObjLit = Vec_IntEntry( vFrame, Aig_ObjId(pObj) );
    if ( iObjLit == -1 )
        return NULL;
    pRes = Aig_ManObj( p->pFrm, Abc_Lit2Var(iObjLit) );
    if ( pRes == NULL )
        Vec_IntWriteEntry( vFrame, Aig_ObjId(pObj), -1 );
    else
        pRes = Aig_NotCond( pRes, Abc_LitIsCompl(iObjLit) );
    return pRes;
}
static inline void        Saig_BmcObjSetFrame( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) 
{
//    Vec_PtrSetEntry( p->vAig2Frm, p->nObjs*i+pObj->Id, pNode );     
    Vec_Int_t * vFrame;
    int iObjLit;
    if ( i == Vec_PtrSize(p->vAig2Frm) )
        Vec_PtrPush( p->vAig2Frm, Vec_IntStartFull(p->nObjs) );
    assert( i < Vec_PtrSize(p->vAig2Frm) );
    vFrame = (Vec_Int_t *)Vec_PtrEntry( p->vAig2Frm, i );
    if ( pNode == NULL )
        iObjLit = -1;
    else
        iObjLit = Abc_Var2Lit( Aig_ObjId(Aig_Regular(pNode)), Aig_IsComplement(pNode) );
    Vec_IntWriteEntry( vFrame, Aig_ObjId(pObj), iObjLit );
}
94 95 96 97

static inline Aig_Obj_t * Saig_BmcObjChild0( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i )                   { assert( !Aig_IsComplement(pObj) ); return Aig_NotCond(Saig_BmcObjFrame(p, Aig_ObjFanin0(pObj), i), Aig_ObjFaninC0(pObj));  }
static inline Aig_Obj_t * Saig_BmcObjChild1( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i )                   { assert( !Aig_IsComplement(pObj) ); return Aig_NotCond(Saig_BmcObjFrame(p, Aig_ObjFanin1(pObj), i), Aig_ObjFaninC1(pObj));  }

98 99 100
static inline int         Saig_BmcSatNum( Saig_Bmc_t * p, Aig_Obj_t * pObj )                             { return Vec_IntGetEntry( p->vObj2Var, pObj->Id );  }
static inline void        Saig_BmcSetSatNum( Saig_Bmc_t * p, Aig_Obj_t * pObj, int Num )                 { Vec_IntSetEntry(p->vObj2Var, pObj->Id, Num);      }

Alan Mishchenko committed
101 102 103 104
////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////

105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140
#define ABS_ZER 1
#define ABS_ONE 2
#define ABS_UND 3

static inline int Abs_ManSimInfoNot( int Value )
{
    if ( Value == ABS_ZER )
        return ABS_ONE;
    if ( Value == ABS_ONE )
        return ABS_ZER;
    return ABS_UND;
}

static inline int Abs_ManSimInfoAnd( int Value0, int Value1 )
{
    if ( Value0 == ABS_ZER || Value1 == ABS_ZER )
        return ABS_ZER;
    if ( Value0 == ABS_ONE && Value1 == ABS_ONE )
        return ABS_ONE;
    return ABS_UND;
}

static inline int Abs_ManSimInfoGet( Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj, int iFrame )
{
    unsigned * pInfo = (unsigned *)Vec_PtrEntry( vSimInfo, iFrame );
    return 3 & (pInfo[Aig_ObjId(pObj) >> 4] >> ((Aig_ObjId(pObj) & 15) << 1));
}

static inline void Abs_ManSimInfoSet( Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj, int iFrame, int Value )
{
    unsigned * pInfo = (unsigned *)Vec_PtrEntry( vSimInfo, iFrame );
    assert( Value >= ABS_ZER && Value <= ABS_UND );
    Value ^= Abs_ManSimInfoGet( vSimInfo, pObj, iFrame );
    pInfo[Aig_ObjId(pObj) >> 4] ^= (Value << ((Aig_ObjId(pObj) & 15) << 1));
}

Alan Mishchenko committed
141 142
/**Function*************************************************************

143
  Synopsis    [Performs ternary simulation for one node.]
Alan Mishchenko committed
144

145
  Description []
Alan Mishchenko committed
146 147 148 149 150 151
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
152
int Abs_ManExtendOneEval_rec( Vec_Ptr_t * vSimInfo, Aig_Man_t * p, Aig_Obj_t * pObj, int iFrame )
Alan Mishchenko committed
153
{
154 155 156 157
    int Value0, Value1, Value;
    Value = Abs_ManSimInfoGet( vSimInfo, pObj, iFrame );
    if ( Value )
        return Value;
158
    if ( Aig_ObjIsCi(pObj) )
Alan Mishchenko committed
159
    {
160 161 162 163 164 165 166 167
        assert( Saig_ObjIsLo(p, pObj) );
        Value = Abs_ManExtendOneEval_rec( vSimInfo, p, Saig_ObjLoToLi(p, pObj), iFrame-1 );
        Abs_ManSimInfoSet( vSimInfo, pObj, iFrame, Value );
        return Value;
    }
    Value0 = Abs_ManExtendOneEval_rec( vSimInfo, p, Aig_ObjFanin0(pObj), iFrame );
    if ( Aig_ObjFaninC0(pObj) )
        Value0 = Abs_ManSimInfoNot( Value0 );
168
    if ( Aig_ObjIsCo(pObj) )
169 170 171
    {
        Abs_ManSimInfoSet( vSimInfo, pObj, iFrame, Value0 );
        return Value0;
Alan Mishchenko committed
172
    }
173 174 175 176 177 178 179 180 181 182 183 184 185
    assert( Aig_ObjIsNode(pObj) );
    if ( Value0 == ABS_ZER )
        Value = ABS_ZER;
    else
    {
        Value1 = Abs_ManExtendOneEval_rec( vSimInfo, p, Aig_ObjFanin1(pObj), iFrame );
        if ( Aig_ObjFaninC1(pObj) )
            Value1 = Abs_ManSimInfoNot( Value1 );
        Value = Abs_ManSimInfoAnd( Value0, Value1 );
    }
    Abs_ManSimInfoSet( vSimInfo, pObj, iFrame, Value );
    assert( Value );
    return Value;
Alan Mishchenko committed
186 187 188 189
}

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

190 191 192 193 194 195 196 197 198 199 200 201 202 203 204
  Synopsis    [Performs ternary simulation for one design.]

  Description [The returned array contains the result of ternary 
  simulation for all the frames where the output could be proved 0.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Ptr_t * Abs_ManTernarySimulate( Aig_Man_t * p, int nFramesMax, int fVerbose )
{
    Vec_Ptr_t * vSimInfo;
    Aig_Obj_t * pObj;
    int i, f, nFramesLimit, nFrameWords;
205
    clock_t clk = clock();
206 207 208
    assert( Aig_ManRegNum(p) > 0 );
    // the maximum number of frames will be determined to use at most 200Mb of RAM
    nFramesLimit = 1 + (200000000 * 4)/Aig_ManObjNum(p);
209 210
    nFramesLimit = Abc_MinInt( nFramesLimit, nFramesMax );
    nFrameWords  = Abc_BitWordNum( 2 * Aig_ManObjNum(p) );
211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231
    // allocate simulation info
    vSimInfo = Vec_PtrAlloc( nFramesLimit );
    for ( f = 0; f < nFramesLimit; f++ )
    {
        Vec_PtrPush( vSimInfo, ABC_CALLOC(unsigned, nFrameWords) );
        if ( f == 0 ) 
        {
            Saig_ManForEachLo( p, pObj, i )
                Abs_ManSimInfoSet( vSimInfo, pObj, 0, ABS_ZER );
        }
        Abs_ManSimInfoSet( vSimInfo, Aig_ManConst1(p), f, ABS_ONE );
        Saig_ManForEachPi( p, pObj, i )
            Abs_ManSimInfoSet( vSimInfo, pObj, f, ABS_UND );
        Saig_ManForEachPo( p, pObj, i )
            Abs_ManExtendOneEval_rec( vSimInfo, p, pObj, f );
        // check if simulation has derived at least one fail or unknown
        Saig_ManForEachPo( p, pObj, i )
            if ( Abs_ManSimInfoGet(vSimInfo, pObj, f) != ABS_ZER )
            {
                if ( fVerbose )
                {
232
                    printf( "Ternary sim found non-zero output in frame %d.  Used %5.2f MB.  ", 
233 234 235 236 237 238 239 240
                        f, 0.25 * (f+1) * Aig_ManObjNum(p) / (1<<20) );
                    ABC_PRT( "Time", clock() - clk );
                }
                return vSimInfo;
            }
    }
    if ( fVerbose )
    {
241
        printf( "Ternary sim proved all outputs in the first %d frames.  Used %5.2f MB.  ", 
242 243 244 245 246 247 248 249 250
            nFramesLimit, 0.25 * nFramesLimit * Aig_ManObjNum(p) / (1<<20) );
        ABC_PRT( "Time", clock() - clk );
    }
    return vSimInfo;
}

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

  Synopsis    [Free the array of simulation info.]
Alan Mishchenko committed
251 252 253 254 255 256 257 258

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
259
void Abs_ManFreeAray( Vec_Ptr_t * p )
Alan Mishchenko committed
260
{
261 262 263 264 265
    void * pTemp;
    int i;
    Vec_PtrForEachEntry( void *, p, pTemp, i )
        ABC_FREE( pTemp );
    Vec_PtrFree( p );
Alan Mishchenko committed
266 267
}

268

Alan Mishchenko committed
269 270
/**Function*************************************************************

271
  Synopsis    [Create manager.]
Alan Mishchenko committed
272

273
  Description []
Alan Mishchenko committed
274 275 276 277 278 279
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
280
Saig_Bmc_t * Saig_BmcManStart( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConfMaxOne, int nConfMaxAll, int fVerbose )
Alan Mishchenko committed
281
{
282 283 284 285 286 287 288 289 290 291 292 293 294 295 296
    Saig_Bmc_t * p;
    Aig_Obj_t * pObj;
    int i, Lit;
//    assert( Aig_ManRegNum(pAig) > 0 );
    p = (Saig_Bmc_t *)ABC_ALLOC( char, sizeof(Saig_Bmc_t) );
    memset( p, 0, sizeof(Saig_Bmc_t) );
    // set parameters
    p->nFramesMax   = nFramesMax;
    p->nNodesMax    = nNodesMax;
    p->nConfMaxOne  = nConfMaxOne;
    p->nConfMaxAll  = nConfMaxAll;
    p->fVerbose     = fVerbose;
    p->pAig         = pAig;
    p->nObjs        = Aig_ManObjNumMax(pAig);
    // create node and variable mappings
297
    p->vAig2Frm     = Vec_PtrAlloc( 100 );
298
    p->vObj2Var     = Vec_IntAlloc( 0 );
299
    Vec_IntFill( p->vObj2Var, p->nObjs, 0 );
300
    // start the AIG manager and map primary inputs
301
    p->pFrm         = Aig_ManStart( p->nObjs );
Alan Mishchenko committed
302
    Saig_ManForEachLo( pAig, pObj, i )
303 304 305 306 307 308 309 310 311
        Saig_BmcObjSetFrame( p, pObj, 0, Aig_ManConst0(p->pFrm) ); 
    // create SAT solver
    p->nSatVars     = 1;
    p->pSat         = sat_solver_new();
    sat_solver_setnvars( p->pSat, 2000 );
    Lit = toLit( p->nSatVars );
    sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
    Saig_BmcSetSatNum( p, Aig_ManConst1(p->pFrm), p->nSatVars++ );
    // other data structures
312 313
    p->vTargets     = Vec_PtrAlloc( 1000 );
    p->vVisited     = Vec_IntAlloc( 1000 );
314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332
    p->iOutputFail  = -1;
    p->iFrameFail   = -1;
    return p;
}

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

  Synopsis    [Delete manager.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Saig_BmcManStop( Saig_Bmc_t * p )
{
    Aig_ManStop( p->pFrm  );
333
    Vec_VecFree( (Vec_Vec_t *)p->vAig2Frm );
334 335 336
    Vec_IntFree( p->vObj2Var );
    sat_solver_delete( p->pSat );
    Vec_PtrFree( p->vTargets );
337
    Vec_IntFree( p->vVisited );
338 339 340 341 342 343 344 345 346 347 348 349 350 351
    ABC_FREE( p );
}

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

  Synopsis    [Explores the possibility of constructing the output.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
352
/*
353 354 355 356 357 358 359 360 361 362
Aig_Obj_t * Saig_BmcIntervalExplore_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i )
{
    Aig_Obj_t * pRes, * p0, * p1, * pConst1 = Aig_ManConst1(p->pAig);
    pRes = Saig_BmcObjFrame( p, pObj, i );
    if ( pRes != NULL )
        return pRes;
    if ( Saig_ObjIsPi( p->pAig, pObj ) )
        pRes = AIG_VISITED;
    else if ( Saig_ObjIsLo( p->pAig, pObj ) )
        pRes = Saig_BmcIntervalExplore_rec( p, Saig_ObjLoToLi(p->pAig, pObj), i-1 );
363
    else if ( Aig_ObjIsCo( pObj ) )
364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392
    {
        pRes = Saig_BmcIntervalExplore_rec( p, Aig_ObjFanin0(pObj), i );
        if ( pRes != AIG_VISITED )
            pRes = Saig_BmcObjChild0( p, pObj, i );
    }
    else 
    {
        p0 = Saig_BmcIntervalExplore_rec( p, Aig_ObjFanin0(pObj), i );
        if ( p0 != AIG_VISITED )
            p0 = Saig_BmcObjChild0( p, pObj, i );
        p1 = Saig_BmcIntervalExplore_rec( p, Aig_ObjFanin1(pObj), i );
        if ( p1 != AIG_VISITED )
            p1 = Saig_BmcObjChild1( p, pObj, i );

        if ( p0 == Aig_Not(p1) )
            pRes = Aig_ManConst0(p->pFrm);
        else if ( Aig_Regular(p0) == pConst1 )
            pRes = (p0 == pConst1) ? p1 : Aig_ManConst0(p->pFrm);
        else if ( Aig_Regular(p1) == pConst1 )
            pRes = (p1 == pConst1) ? p0 : Aig_ManConst0(p->pFrm);
        else 
            pRes = AIG_VISITED;

        if ( pRes != AIG_VISITED && !Aig_ObjIsConst1(Aig_Regular(pRes)) )
            pRes = AIG_VISITED;
    }
    Saig_BmcObjSetFrame( p, pObj, i, pRes );
    return pRes;
}
393
*/
394 395 396 397 398 399 400 401 402 403 404 405

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

  Synopsis    [Performs the actual construction of the output.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
406
Aig_Obj_t * Saig_BmcIntervalConstruct_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i, Vec_Int_t * vVisited )
407 408 409 410 411 412
{
    Aig_Obj_t * pRes;
    pRes = Saig_BmcObjFrame( p, pObj, i );
    if ( pRes != NULL )
        return pRes;
    if ( Saig_ObjIsPi( p->pAig, pObj ) )
413
        pRes = Aig_ObjCreateCi(p->pFrm);
414 415
    else if ( Saig_ObjIsLo( p->pAig, pObj ) )
        pRes = Saig_BmcIntervalConstruct_rec( p, Saig_ObjLoToLi(p->pAig, pObj), i-1, vVisited );
416
    else if ( Aig_ObjIsCo( pObj ) )
417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433
    {
        Saig_BmcIntervalConstruct_rec( p, Aig_ObjFanin0(pObj), i, vVisited );
        pRes = Saig_BmcObjChild0( p, pObj, i );
    }
    else 
    {
        Saig_BmcIntervalConstruct_rec( p, Aig_ObjFanin0(pObj), i, vVisited );
        if ( Saig_BmcObjChild0(p, pObj, i) == Aig_ManConst0(p->pFrm) )
            pRes = Aig_ManConst0(p->pFrm);
        else
        {
            Saig_BmcIntervalConstruct_rec( p, Aig_ObjFanin1(pObj), i, vVisited );
            pRes = Aig_And( p->pFrm, Saig_BmcObjChild0(p, pObj, i), Saig_BmcObjChild1(p, pObj, i) );
        }
    }
    assert( pRes != NULL );
    Saig_BmcObjSetFrame( p, pObj, i, pRes );
434 435
    Vec_IntPush( vVisited, Aig_ObjId(pObj) );
    Vec_IntPush( vVisited, i );
436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452
    return pRes;
}

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

  Synopsis    [Adds new AIG nodes to the frames.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Saig_BmcInterval( Saig_Bmc_t * p )
{
    Aig_Obj_t * pTarget;
453
    int i, iObj, iFrame;
454 455 456 457
    int nNodes = Aig_ManObjNum( p->pFrm );
    Vec_PtrClear( p->vTargets );
    p->iFramePrev = p->iFrameLast;
    for ( ; p->iFrameLast < p->nFramesMax; p->iFrameLast++, p->iOutputLast = 0 )
458
    { 
459
        if ( p->iOutputLast == 0 )
Alan Mishchenko committed
460
        {
461
            Saig_BmcObjSetFrame( p, Aig_ManConst1(p->pAig), p->iFrameLast, Aig_ManConst1(p->pFrm) );
Alan Mishchenko committed
462
        }
463
        for ( ; p->iOutputLast < Saig_ManPoNum(p->pAig); p->iOutputLast++ )
Alan Mishchenko committed
464
        {
465 466
            if ( Aig_ManObjNum(p->pFrm) >= nNodes + p->nNodesMax )
                return;
467
//            Saig_BmcIntervalExplore_rec( p, Aig_ManCo(p->pAig, p->iOutputLast), p->iFrameLast );
468
            Vec_IntClear( p->vVisited );
469
            pTarget = Saig_BmcIntervalConstruct_rec( p, Aig_ManCo(p->pAig, p->iOutputLast), p->iFrameLast, p->vVisited );
470
            Vec_PtrPush( p->vTargets, pTarget );
471
            Aig_ObjCreateCo( p->pFrm, pTarget );
472
            Aig_ManCleanup( p->pFrm ); // it is not efficient to cleanup the whole manager!!!
473
            // check if the node is gone
474 475
            Vec_IntForEachEntryDouble( p->vVisited, iObj, iFrame, i )
                Saig_BmcObjFrame( p, Aig_ManObj(p->pAig, iObj), iFrame );
476
            // it is not efficient to remove nodes, which may be used later!!!
Alan Mishchenko committed
477
        }
478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495
    }
}

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

  Synopsis    [Performs the actual construction of the output.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Aig_Obj_t * Saig_BmcIntervalToAig_rec( Saig_Bmc_t * p, Aig_Man_t * pNew, Aig_Obj_t * pObj )
{
    if ( pObj->pData )
        return (Aig_Obj_t *)pObj->pData;
496
    Vec_IntPush( p->vVisited, Aig_ObjId(pObj) );
497
    if ( Saig_BmcSatNum(p, pObj) || Aig_ObjIsCi(pObj) )
498
    {
499
        p->nStitchVars += !Aig_ObjIsCi(pObj);
500
        return (Aig_Obj_t *)(pObj->pData = Aig_ObjCreateCi(pNew));
501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528
    }
    Saig_BmcIntervalToAig_rec( p, pNew, Aig_ObjFanin0(pObj) );
    Saig_BmcIntervalToAig_rec( p, pNew, Aig_ObjFanin1(pObj) );
    assert( pObj->pData == NULL );
    return (Aig_Obj_t *)(pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ));
}

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

  Synopsis    [Creates AIG of the newly added nodes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Aig_Man_t * Saig_BmcIntervalToAig( Saig_Bmc_t * p )
{
    Aig_Man_t * pNew;
    Aig_Obj_t * pObj, * pObjNew;
    int i;
    Aig_ManForEachObj( p->pFrm, pObj, i )
        assert( pObj->pData == NULL );

    pNew = Aig_ManStart( p->nNodesMax );
    Aig_ManConst1(p->pFrm)->pData = Aig_ManConst1(pNew);
529 530
    Vec_IntClear( p->vVisited );
    Vec_IntPush( p->vVisited, Aig_ObjId(Aig_ManConst1(p->pFrm)) );
531 532 533 534 535
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vTargets, pObj, i )
    {
//        assert( !Aig_ObjIsConst1(Aig_Regular(pObj)) );
        pObjNew = Saig_BmcIntervalToAig_rec( p, pNew, Aig_Regular(pObj) );
        assert( !Aig_IsComplement(pObjNew) );
536
        Aig_ObjCreateCo( pNew, pObjNew );
537
    } 
538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555
    return pNew;
}

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

  Synopsis    [Derives CNF for the newly added nodes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Saig_BmcLoadCnf( Saig_Bmc_t * p, Cnf_Dat_t * pCnf )
{
    Aig_Obj_t * pObj, * pObjNew;
    int i, Lits[2], VarNumOld, VarNumNew;
556
    Aig_ManForEachObjVec( p->vVisited, p->pFrm, pObj, i )
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
    {
        // get the new variable of this node
        pObjNew     = (Aig_Obj_t *)pObj->pData;
        pObj->pData = NULL;
        VarNumNew   = pCnf->pVarNums[ pObjNew->Id ];
        if ( VarNumNew == -1 )
            continue;
        // get the old variable of this node
        VarNumOld   = Saig_BmcSatNum( p, pObj );
        if ( VarNumOld == 0 )
        {
            Saig_BmcSetSatNum( p, pObj, VarNumNew );
            continue;
        }
        // add clauses connecting existing variables
        Lits[0] = toLitCond( VarNumOld, 0 );
        Lits[1] = toLitCond( VarNumNew, 1 );
        if ( !sat_solver_addclause( p->pSat, Lits, Lits+2 ) )
            assert( 0 );
        Lits[0] = toLitCond( VarNumOld, 1 );
        Lits[1] = toLitCond( VarNumNew, 0 );
        if ( !sat_solver_addclause( p->pSat, Lits, Lits+2 ) )
            assert( 0 );
    }
    // add CNF to the SAT solver
    for ( i = 0; i < pCnf->nClauses; i++ )
        if ( !sat_solver_addclause( p->pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
Alan Mishchenko committed
584
            break;
585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612
    if ( i < pCnf->nClauses )
        printf( "SAT solver became UNSAT after adding clauses.\n" );
}

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

  Synopsis    [Solves targets with the given resource limit.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Saig_BmcDeriveFailed( Saig_Bmc_t * p, int iTargetFail )
{
    int k;
    p->iOutputFail = p->iOutputLast;
    p->iFrameFail  = p->iFrameLast;
    for ( k = Vec_PtrSize(p->vTargets); k > iTargetFail; k-- )
    {
        if ( p->iOutputFail == 0 )
        {
            p->iOutputFail = Saig_ManPoNum(p->pAig);
            p->iFrameFail--;
        }
        p->iOutputFail--;
Alan Mishchenko committed
613 614 615
    }
}

616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632
/**Function*************************************************************

  Synopsis    [Solves targets with the given resource limit.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Abc_Cex_t * Saig_BmcGenerateCounterExample( Saig_Bmc_t * p )
{
    Abc_Cex_t * pCex;
    Aig_Obj_t * pObj, * pObjFrm;
    int i, f, iVarNum;
    // start the counter-example
633
    pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), p->iFrameFail+1 );
634 635 636 637 638 639 640 641 642 643 644 645 646 647
    pCex->iFrame = p->iFrameFail;
    pCex->iPo    = p->iOutputFail;
    // copy the bit data
    for ( f = 0; f <= p->iFrameFail; f++ )
    {
        Saig_ManForEachPi( p->pAig, pObj, i )
        {
            pObjFrm = Saig_BmcObjFrame( p, pObj, f );
            if ( pObjFrm == NULL )
                continue;
            iVarNum = Saig_BmcSatNum( p, pObjFrm );
            if ( iVarNum == 0 )
                continue;
            if ( sat_solver_var_value( p->pSat, iVarNum ) )
648
                Abc_InfoSetBit( pCex->pData, pCex->nRegs + Saig_ManPiNum(p->pAig) * f + i );
649 650 651
        }
    }
    // verify the counter example
652
    if ( !Saig_ManVerifyCex( p->pAig, pCex ) )
653 654
    {
        printf( "Saig_BmcGenerateCounterExample(): Counter-example is invalid.\n" );
655
        Abc_CexFree( pCex );
656 657 658 659
        pCex = NULL;
    }
    return pCex;
}
Alan Mishchenko committed
660

Alan Mishchenko committed
661 662
/**Function*************************************************************

663
  Synopsis    [Solves targets with the given resource limit.]
Alan Mishchenko committed
664 665 666 667 668 669 670 671

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
672
int Saig_BmcSolveTargets( Saig_Bmc_t * p, int nStart, int * pnOutsSolved )
Alan Mishchenko committed
673 674
{
    Aig_Obj_t * pObj;
675
    int i, k, VarNum, Lit, status, RetValue;
676 677
    assert( Vec_PtrSize(p->vTargets) > 0 );
    if ( p->pSat->qtail != p->pSat->qhead )
Alan Mishchenko committed
678
    {
679 680
        RetValue = sat_solver_simplify(p->pSat);
        assert( RetValue != 0 );
Alan Mishchenko committed
681
    }
682
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vTargets, pObj, i )
Alan Mishchenko committed
683
    {
684 685 686 687 688 689 690 691
        if ( ((*pnOutsSolved)++ / Saig_ManPoNum(p->pAig)) < nStart )
            continue;
        if ( p->nConfMaxAll && p->pSat->stats.conflicts > p->nConfMaxAll )
            return l_Undef;
        VarNum = Saig_BmcSatNum( p, Aig_Regular(pObj) );
        Lit = toLitCond( VarNum, Aig_IsComplement(pObj) );
        RetValue = sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)p->nConfMaxOne, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
        if ( RetValue == l_False ) // unsat
692 693 694 695 696 697 698 699 700 701 702 703 704 705 706
        {
            // add final unit clause
            Lit = lit_neg( Lit );
            status = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
            assert( status );
            // add learned units
            for ( k = 0; k < veci_size(&p->pSat->unit_lits); k++ )
            {
                Lit = veci_begin(&p->pSat->unit_lits)[k];
                status = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
                assert( status );
            }
            veci_resize(&p->pSat->unit_lits, 0);
            // propagate units
            sat_solver_compress( p->pSat );
707
            continue;
708
        }
709 710 711 712 713 714 715 716 717 718 719
        if ( RetValue == l_Undef ) // undecided
            return l_Undef;
        // generate counter-example
        Saig_BmcDeriveFailed( p, i );
        p->pAig->pSeqModel = Saig_BmcGenerateCounterExample( p );

        {
//            extern Vec_Int_t * Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iFirstPi, void * pCex );
//            Saig_ManExtendCounterExampleTest( p->pAig, 0, p->pAig->pSeqModel );
        }
        return l_True;
Alan Mishchenko committed
720
    }
721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739
    return l_False;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Saig_BmcAddTargetsAsPos( Saig_Bmc_t * p )
{
    Aig_Obj_t * pObj;
    int i;
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vTargets, pObj, i )
740
        Aig_ObjCreateCo( p->pFrm, pObj );
741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756
    Aig_ManPrintStats( p->pFrm );
    Aig_ManCleanup( p->pFrm );
    Aig_ManPrintStats( p->pFrm );
} 

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

  Synopsis    [Performs BMC with the given parameters.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
757
int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames, int fSilent )
758 759 760 761 762
{
    Saig_Bmc_t * p;
    Aig_Man_t * pNew;
    Cnf_Dat_t * pCnf;
    int nOutsSolved = 0;
763 764 765
    int Iter, RetValue = -1;
    clock_t nTimeToStop = nTimeOut ? nTimeOut * CLOCKS_PER_SEC + clock(): 0;
    clock_t clk = clock(), clk2, clkTotal = clock();
766 767 768 769 770 771
    int Status = -1;
/*
    Vec_Ptr_t * vSimInfo;
    vSimInfo = Abs_ManTernarySimulate( pAig, nFramesMax, fVerbose );
    Abs_ManFreeAray( vSimInfo );
*/
Alan Mishchenko committed
772 773
    if ( fVerbose )
    {
774
        printf( "Running \"bmc2\". AIG:  PI/PO/Reg = %d/%d/%d.  Node = %6d. Lev = %5d.\n", 
Alan Mishchenko committed
775 776
            Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), Saig_ManRegNum(pAig),
            Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) );
777 778 779
        printf( "Params: FramesMax = %d. NodesDelta = %d. ConfMaxOne = %d. ConfMaxAll = %d.\n", 
            nFramesMax, nNodesMax, nConfMaxOne, nConfMaxAll );
    } 
780 781
    nFramesMax = nFramesMax ? nFramesMax : ABC_INFINITY;
    p = Saig_BmcManStart( pAig, nFramesMax, nNodesMax, nConfMaxOne, nConfMaxAll, fVerbose );
782 783
    // set runtime limit
    if ( nTimeOut )
784
        sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
785
    for ( Iter = 0; ; Iter++ )
Alan Mishchenko committed
786
    {
787 788 789 790 791 792 793 794 795 796
        clk2 = clock();
        // add new logic interval to frames
        Saig_BmcInterval( p );
//        Saig_BmcAddTargetsAsPos( p );
        if ( Vec_PtrSize(p->vTargets) == 0 )
            break;
        // convert logic slice into new AIG
        pNew = Saig_BmcIntervalToAig( p );
//printf( "StitchVars = %d.\n", p->nStitchVars );
        // derive CNF for the new AIG
797
        pCnf = Cnf_Derive( pNew, Aig_ManCoNum(pNew) );
798 799 800 801 802 803 804 805
        Cnf_DataLift( pCnf, p->nSatVars );
        p->nSatVars += pCnf->nVars;
        // add this CNF to the solver
        Saig_BmcLoadCnf( p, pCnf );
        Cnf_DataFree( pCnf );
        Aig_ManStop( pNew );
        // solve the targets
        RetValue = Saig_BmcSolveTargets( p, nStart, &nOutsSolved );
Alan Mishchenko committed
806 807
        if ( fVerbose )
        {
808
            printf( "%4d : F =%5d. O =%4d.  And =%8d. Var =%8d. Conf =%7d. ", 
809
                Iter, p->iFrameLast, p->iOutputLast, Aig_ManNodeNum(p->pFrm), p->nSatVars, (int)p->pSat->stats.conflicts );   
810
            printf( "%4.0f MB",     4.0*(p->iFrameLast+1)*p->nObjs/(1<<20) );
811 812
            printf( "%9.2f sec", (float)(clock() - clkTotal)/(float)(CLOCKS_PER_SEC) );
            printf( "\n" );
813
            fflush( stdout );
814 815 816 817
        }
        if ( RetValue != l_False )
            break;
        // check the timeout
818
        if ( nTimeOut && clock() > nTimeToStop )
819
        {
820 821
            if ( !fSilent )
                printf( "Reached timeout (%d seconds).\n",  nTimeOut );
822 823
            if ( piFrames )
                *piFrames = p->iFrameLast-1;
824
            Saig_BmcManStop( p );
825
            return Status;
Alan Mishchenko committed
826 827
        }
    }
828
    if ( RetValue == l_True )
Alan Mishchenko committed
829
    {
830
        assert( p->iFrameFail * Saig_ManPoNum(p->pAig) + p->iOutputFail + 1 == nOutsSolved );
831
        if ( !fSilent )
832 833
            Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", 
                p->iOutputFail, p->pAig->pName, p->iFrameFail );
834 835
        Status = 0;
        if ( piFrames )
836
            *piFrames = p->iFrameFail - 1;
Alan Mishchenko committed
837
    }
838
    else // if ( RetValue == l_False || RetValue == l_Undef )
Alan Mishchenko committed
839
    {
840
        if ( !fSilent )
841
            Abc_Print( 1, "No output failed in %d frames.  ", Abc_MaxInt(p->iFramePrev-1, 0) );
842
        if ( piFrames )
843 844
        {
            if ( p->iOutputLast > 0 )
845
                *piFrames = p->iFramePrev - 2;
846
            else
847
                *piFrames = p->iFramePrev - 1;
848
        }
Alan Mishchenko committed
849
    }
850
    if ( !fSilent )
Alan Mishchenko committed
851
    {
852 853 854 855
        if ( fVerbOverwrite )
        {
            ABC_PRTr( "Time", clock() - clk );
        }
856
        else
857 858 859 860 861 862 863 864 865 866 867 868 869 870
        {
            ABC_PRT( "Time", clock() - clk );
        }
        if ( RetValue != l_True )
        {
            if ( p->iFrameLast >= p->nFramesMax )
                printf( "Reached limit on the number of timeframes (%d).\n", p->nFramesMax );
            else if ( p->nConfMaxAll && p->pSat->stats.conflicts > p->nConfMaxAll )
                printf( "Reached global conflict limit (%d).\n", p->nConfMaxAll );
            else if ( nTimeOut && clock() > nTimeToStop )
                printf( "Reached timeout (%d seconds).\n", nTimeOut );
            else
                printf( "Reached local conflict limit (%d).\n", p->nConfMaxOne );
        }
871 872
    }
    Saig_BmcManStop( p );
873
    fflush( stdout );
874
    return Status;
Alan Mishchenko committed
875 876
}

877

Alan Mishchenko committed
878 879 880 881 882
////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////


883 884
ABC_NAMESPACE_IMPL_END