giaCCof.c 10.8 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21
/**CFile****************************************************************

  FileName    [giaCCof.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Scalable AIG package.]

  Synopsis    [Backward reachability using circuit cofactoring.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

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

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

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

#include "gia.h"
22
#include "sat/bsat/satSolver.h"
23 24 25 26 27 28 29 30 31 32 33 34

ABC_NAMESPACE_IMPL_START


////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

typedef struct Ccf_Man_t_ Ccf_Man_t; // manager
struct Ccf_Man_t_
{
    // user data
35 36 37 38 39
    Gia_Man_t *  pGia;       // single-output AIG manager
    int          nFrameMax;  // maximum number of frames
    int          nConfMax;   // maximum number of conflicts
    int          nTimeMax;   // maximum runtime in seconds
    int          fVerbose;   // verbose flag
40
    // internal data
41 42 43 44
    void *       pUnr;       // unrolling manager
    Gia_Man_t *  pFrames;    // unrolled timeframes
    Vec_Int_t *  vCopies;    // copy pointers of the AIG
    sat_solver * pSat;       // SAT solver
45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63
};

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

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

  Synopsis    [Create manager.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Ccf_Man_t * Ccf_ManStart( Gia_Man_t * pGia, int nFrameMax, int nConfMax, int nTimeMax, int fVerbose )
{
64
    static Gia_ParFra_t Pars, * pPars = &Pars;
65 66 67
    Ccf_Man_t * p;
    assert( nFrameMax > 0 );
    p = ABC_CALLOC( Ccf_Man_t, 1 );
68 69 70 71 72 73 74 75 76 77 78 79
    p->pGia      = pGia;
    p->nFrameMax = nFrameMax;    
    p->nConfMax  = nConfMax;
    p->nTimeMax  = nTimeMax;
    p->fVerbose  = fVerbose;
    // create unrolling manager
    memset( pPars, 0, sizeof(Gia_ParFra_t) );
    pPars->fVerbose     = fVerbose;
    pPars->nFrames      = nFrameMax;
    pPars->fSaveLastLit = 1;
    p->pUnr = Gia_ManUnrollStart( pGia, pPars );
    p->vCopies = Vec_IntAlloc( 1000 );
80
    // internal data
81 82
    p->pSat = sat_solver_new();
//    sat_solver_setnvars( p->pSat, 10000 );
83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98
    return p;
}

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

  Synopsis    [Delete manager.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ccf_ManStop( Ccf_Man_t * p )
{
99 100
    Vec_IntFree( p->vCopies );
    Gia_ManUnrollStop( p->pUnr );
101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124
    sat_solver_delete( p->pSat );
    Gia_ManStopP( &p->pFrames );
    ABC_FREE( p );
}


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

  Synopsis    [Extends the solver.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Gia_ManCofExtendSolver( Ccf_Man_t * p )
{
    Gia_Obj_t * pObj;
    int i;
    // add SAT clauses
    for ( i = sat_solver_nvars(p->pSat); i < Gia_ManObjNum(p->pFrames); i++ )
    {
125
        pObj = Gia_ManObj( p->pFrames, i );
126 127 128 129 130
        if ( Gia_ObjIsAnd(pObj) )
            sat_solver_add_and( p->pSat, i, 
                Gia_ObjFaninId0(pObj, i), 
                Gia_ObjFaninId1(pObj, i), 
                Gia_ObjFaninC0(pObj), 
131
                Gia_ObjFaninC1(pObj), 0 ); 
132
    }
133
    sat_solver_setnvars( p->pSat, Gia_ManObjNum(p->pFrames) );
134 135
}

136
static inline int Gia_Obj0Copy( Vec_Int_t * vCopies, int Fan0, int fCompl0 )  
137
{ return Abc_LitNotCond( Vec_IntEntry(vCopies, Fan0), fCompl0 ); }
138

139
static inline int Gia_Obj1Copy( Vec_Int_t * vCopies, int Fan1, int fCompl1 )  
140
{ return Abc_LitNotCond( Vec_IntEntry(vCopies, Fan1), fCompl1 ); }
141
 
142 143 144 145 146 147 148 149 150 151 152
/**Function*************************************************************

  Synopsis    [Cofactor the circuit w.r.t. the given assignment.]

  Description [Assumes that the solver has just returned SAT.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
153
void Gia_ManCofOneDerive_rec( Ccf_Man_t * p, int Id )
154
{
155 156
    Gia_Obj_t * pObj;
    int Res;
157 158
    if ( Vec_IntEntry(p->vCopies, Id) != -1 )
        return;
159
    pObj = Gia_ManObj(p->pFrames, Id);
160 161 162
    assert( Gia_ObjIsCi(pObj) || Gia_ObjIsAnd(pObj) );
    if ( Gia_ObjIsAnd(pObj) )
    {
163 164 165 166 167 168
        int fCompl0 = Gia_ObjFaninC0(pObj);
        int fCompl1 = Gia_ObjFaninC1(pObj);
        int Fan0 = Gia_ObjFaninId0p(p->pFrames, pObj);
        int Fan1 = Gia_ObjFaninId1p(p->pFrames, pObj);
        Gia_ManCofOneDerive_rec( p, Fan0 );
        Gia_ManCofOneDerive_rec( p, Fan1 );
169
        Res = Gia_ManHashAnd( p->pFrames, 
170 171
            Gia_Obj0Copy(p->vCopies, Fan0, fCompl0), 
            Gia_Obj1Copy(p->vCopies, Fan1, fCompl1) );
172
    }
173 174
    else if ( Gia_ObjCioId(pObj) >= Gia_ManRegNum(p->pGia) ) // PI
        Res = sat_solver_var_value( p->pSat, Id );
175
    else
176
        Res = Abc_Var2Lit( Id, 0 );
177
    Vec_IntWriteEntry( p->vCopies, Id, Res );
178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193
}

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

  Synopsis    [Cofactor the circuit w.r.t. the given assignment.]

  Description [Assumes that the solver has just returned SAT.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Gia_ManCofOneDerive( Ccf_Man_t * p, int LitProp )
{
    int LitOut;
194
    // derive the cofactor of the property node
195
    Vec_IntFill( p->vCopies, Gia_ManObjNum(p->pFrames), -1 );
196 197 198
    Gia_ManCofOneDerive_rec( p, Abc_Lit2Var(LitProp) );
    LitOut = Vec_IntEntry( p->vCopies, Abc_Lit2Var(LitProp) );
    LitOut = Abc_LitNotCond( LitOut, Abc_LitIsCompl(LitProp) );
199 200 201 202 203
    // add new PO for the cofactor
    Gia_ManAppendCo( p->pFrames, LitOut );
    // add SAT clauses
    Gia_ManCofExtendSolver( p );
    // return negative literal of the cofactor
204
    return Abc_LitNot(LitOut);
205
} 
206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221

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

  Synopsis    [Enumerates backward reachable states.]

  Description [Return -1 if resource limit is reached. Returns 1 
  if computation converged (there is no more reachable states).
  Returns 0 if no more states to enumerate.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Gia_ManCofGetReachable( Ccf_Man_t * p, int Lit )
{
222
    int ObjPrev = 0, ConfPrev = 0;
223
    int Count = 0, LitOut, RetValue;
224
    abctime clk;
225 226 227 228 229
    // try solving for the first time and quit if converged
    RetValue = sat_solver_solve( p->pSat, &Lit, &Lit + 1, p->nConfMax, 0, 0, 0 );
    if ( RetValue == l_False )
        return 1;
    // iterate circuit cofactoring
230
    while ( RetValue == l_True )
231
    {
232
        clk = Abc_Clock();
233
        // derive cofactor
234
        LitOut = Gia_ManCofOneDerive( p, Lit );
235 236 237 238 239
        // add the blocking clause
        RetValue = sat_solver_addclause( p->pSat, &LitOut, &LitOut + 1 );
        assert( RetValue );
        // try solving again
        RetValue = sat_solver_solve( p->pSat, &Lit, &Lit + 1, p->nConfMax, 0, 0, 0 );
240 241 242 243 244
        // derive cofactors
        if ( p->fVerbose ) 
        {
            printf( "%3d : AIG =%7d  Conf =%7d.  ", Count++, 
                Gia_ManObjNum(p->pFrames) - ObjPrev, sat_solver_nconflicts(p->pSat) - ConfPrev );
245
            Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
246 247 248
            ObjPrev = Gia_ManObjNum(p->pFrames);
            ConfPrev = sat_solver_nconflicts(p->pSat);
        }
249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266
    }
    if ( RetValue == l_Undef )
        return -1;
    return 0;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Gia_Man_t * Gia_ManCofTest( Gia_Man_t * pGia, int nFrameMax, int nConfMax, int nTimeMax, int fVerbose )
267
{ 
268 269
    Gia_Man_t * pNew;
    Ccf_Man_t * p;
270
    Gia_Obj_t * pObj;
271
    int f, i, Lit, RetValue = -1, fFailed = 0;
272 273
    abctime nTimeToStop = Abc_Clock() + nTimeMax * CLOCKS_PER_SEC;
    abctime clk = Abc_Clock();
274
    assert( Gia_ManPoNum(pGia) == 1 );
275

276 277
    // create reachability manager
    p = Ccf_ManStart( pGia, nFrameMax, nConfMax, nTimeMax, fVerbose );
278 279 280 281 282

    // set runtime limit
    if ( nTimeMax )
        sat_solver_set_runtime_limit( p->pSat, nTimeToStop );

283 284 285
    // perform backward image computation
    for ( f = 0; f < nFrameMax; f++ )
    {
286
        if ( fVerbose ) 
287
            printf( "ITER %3d :\n", f );
288 289 290 291 292 293
        // add to the mapping of nodes
        p->pFrames = (Gia_Man_t *)Gia_ManUnrollAdd( p->pUnr, f+1 );
        // add SAT clauses
        Gia_ManCofExtendSolver( p );
        // return output literal
        Lit = Gia_ManUnrollLastLit( p->pUnr );
294 295 296 297
        // derives cofactors of the property literal till all states are blocked
        RetValue = Gia_ManCofGetReachable( p, Lit );
        if ( RetValue )
            break;
298 299 300 301 302 303 304 305 306 307 308 309

        // check the property output
        Gia_ManSetPhase( p->pFrames );
        Gia_ManForEachPo( p->pFrames, pObj, i )
            if ( pObj->fPhase )
            {
                printf( "Property failed in frame %d.\n", f );
                fFailed = 1;
                break;
            }
        if ( i < Gia_ManPoNum(p->pFrames) )
            break;
310
    }
311

312
    // report the result
313
    if ( nTimeToStop && Abc_Clock() > nTimeToStop )
314 315
        printf( "Runtime limit (%d sec) is reached after %d frames.  ", nTimeMax, f );
    else if ( f == nFrameMax )
316
        printf( "Completed %d frames without converging.  ", f );
317
    else if ( RetValue == 1 )
318
        printf( "Backward reachability converged after %d iterations.  ", f-1 );
319
    else if ( RetValue == -1 )
320
        printf( "Conflict limit or timeout is reached after %d frames.  ", f-1 );
321
    Abc_PrintTime( 1, "Runtime", Abc_Clock() - clk );
322

323 324 325 326 327
    if ( !fFailed && RetValue == 1 )
        printf( "Property holds.\n" );
    else if ( !fFailed )
        printf( "Property is undecided.\n" );

328 329 330 331
    // get the resulting AIG manager
    Gia_ManHashStop( p->pFrames );
    pNew = p->pFrames;  p->pFrames = NULL;
    Ccf_ManStop( p );
332 333 334 335

    // cleanup
//    if ( fVerbose )
//        Gia_ManPrintStats( pNew, 0 );
336 337 338
    pNew = Gia_ManCleanup( pGia = pNew );
    Gia_ManStop( pGia );
//    if ( fVerbose )
339
//        Gia_ManPrintStats( pNew, 0 );
340 341 342 343 344 345 346 347 348 349
    return pNew;   
}

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


ABC_NAMESPACE_IMPL_END