sswBmc.c 7.08 KB
Newer Older
Alan Mishchenko committed
1 2 3 4 5 6 7 8
/**CFile****************************************************************

  FileName    [sswBmc.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Inductive prover with constraints.]

Alan Mishchenko committed
9
  Synopsis    [Bounded model checker using dynamic unrolling.]
Alan Mishchenko committed
10 11 12 13 14 15 16 17 18 19 20 21 22

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

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

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

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

#include "sswInt.h"

23 24 25
ABC_NAMESPACE_IMPL_START


Alan Mishchenko committed
26 27 28 29 30 31 32 33 34 35
////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

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

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

Alan Mishchenko committed
36
  Synopsis    [Incrementally unroll the timeframes.]
Alan Mishchenko committed
37 38 39 40 41 42 43 44

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
45
Aig_Obj_t * Ssw_BmcUnroll_rec( Ssw_Frm_t * pFrm, Aig_Obj_t * pObj, int f )
Alan Mishchenko committed
46
{
Alan Mishchenko committed
47 48 49 50 51 52
    Aig_Obj_t * pRes, * pRes0, * pRes1;
    if ( (pRes = Ssw_ObjFrame_(pFrm, pObj, f)) )
        return pRes;
    if ( Aig_ObjIsConst1(pObj) )
        pRes = Aig_ManConst1( pFrm->pFrames );
    else if ( Saig_ObjIsPi(pFrm->pAig, pObj) )
53
        pRes = Aig_ObjCreateCi( pFrm->pFrames );
54
    else if ( Aig_ObjIsCo(pObj) )
Alan Mishchenko committed
55 56 57 58 59 60 61 62
    {
        Ssw_BmcUnroll_rec( pFrm, Aig_ObjFanin0(pObj), f );
        pRes = Ssw_ObjChild0Fra_( pFrm, pObj, f );
    }
    else if ( Saig_ObjIsLo(pFrm->pAig, pObj) )
    {
        if ( f == 0 )
            pRes = Aig_ManConst0( pFrm->pFrames );
63
        else
Alan Mishchenko committed
64 65
            pRes = Ssw_BmcUnroll_rec( pFrm, Saig_ObjLoToLi(pFrm->pAig, pObj), f-1 );
    }
66
    else
Alan Mishchenko committed
67 68 69 70 71 72 73 74 75 76
    {
        assert( Aig_ObjIsNode(pObj) );
        Ssw_BmcUnroll_rec( pFrm, Aig_ObjFanin0(pObj), f );
        Ssw_BmcUnroll_rec( pFrm, Aig_ObjFanin1(pObj), f );
        pRes0 = Ssw_ObjChild0Fra_( pFrm, pObj, f );
        pRes1 = Ssw_ObjChild1Fra_( pFrm, pObj, f );
        pRes = Aig_And( pFrm->pFrames, pRes0, pRes1 );
    }
    Ssw_ObjSetFrame_( pFrm, pObj, f, pRes );
    return pRes;
Alan Mishchenko committed
77 78 79 80
}

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

Alan Mishchenko committed
81
  Synopsis    [Derives counter-example.]
Alan Mishchenko committed
82 83

  Description []
84

Alan Mishchenko committed
85 86 87 88 89
  SideEffects []

  SeeAlso     []

***********************************************************************/
90
Abc_Cex_t * Ssw_BmcGetCounterExample( Ssw_Frm_t * pFrm, Ssw_Sat_t * pSat, int iPo, int iFrame )
Alan Mishchenko committed
91
{
92
    Abc_Cex_t * pCex;
Alan Mishchenko committed
93 94 95 96
    Aig_Obj_t * pObj, * pObjFrames;
    int f, i, nShift;
    assert( Saig_ManRegNum(pFrm->pAig) > 0 );
    // allocate the counter example
97
    pCex = Abc_CexAlloc( Saig_ManRegNum(pFrm->pAig), Saig_ManPiNum(pFrm->pAig), iFrame + 1 );
Alan Mishchenko committed
98 99 100 101 102 103 104 105 106 107 108
    pCex->iPo    = iPo;
    pCex->iFrame = iFrame;
    // create data-bits
    nShift = Saig_ManRegNum(pFrm->pAig);
    for ( f = 0; f <= iFrame; f++, nShift += Saig_ManPiNum(pFrm->pAig) )
        Saig_ManForEachPi( pFrm->pAig, pObj, i )
        {
            pObjFrames = Ssw_ObjFrame_(pFrm, pObj, f);
            if ( pObjFrames == NULL )
                continue;
            if ( Ssw_CnfGetNodeValue( pSat, pObjFrames ) )
109
                Abc_InfoSetBit( pCex->pData, nShift + i );
Alan Mishchenko committed
110 111
        }
    return pCex;
Alan Mishchenko committed
112 113 114 115 116
}


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

Alan Mishchenko committed
117
  Synopsis    [Performs BMC for the given AIG.]
Alan Mishchenko committed
118 119 120 121 122 123 124 125

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
126
int Ssw_BmcDynamic( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int fVerbose, int * piFrame )
Alan Mishchenko committed
127
{
Alan Mishchenko committed
128 129 130
    Ssw_Frm_t * pFrm;
    Ssw_Sat_t * pSat;
    Aig_Obj_t * pObj, * pObjFrame;
131
    int status, Lit, i, f, RetValue;
132
    abctime clkPart;
Alan Mishchenko committed
133 134 135

    // start managers
    assert( Saig_ManRegNum(pAig) > 0 );
136
    Aig_ManSetCioIds( pAig );
Alan Mishchenko committed
137 138 139 140 141
    pSat = Ssw_SatStart( 0 );
    pFrm = Ssw_FrmStart( pAig );
    pFrm->pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) * 3 );
    // report statistics
    if ( fVerbose )
Alan Mishchenko committed
142
    {
143
        Abc_Print( 1, "AIG:  PI/PO/Reg = %d/%d/%d.  Node = %6d. Lev = %5d.\n",
Alan Mishchenko committed
144 145 146
            Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), Saig_ManRegNum(pAig),
            Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) );
        fflush( stdout );
Alan Mishchenko committed
147
    }
Alan Mishchenko committed
148 149 150
    // perform dynamic unrolling
    RetValue = -1;
    for ( f = 0; f < nFramesMax; f++ )
Alan Mishchenko committed
151
    {
152
        clkPart = Abc_Clock();
Alan Mishchenko committed
153
        Saig_ManForEachPo( pAig, pObj, i )
Alan Mishchenko committed
154
        {
Alan Mishchenko committed
155 156 157 158 159 160 161 162 163 164
            // unroll the circuit for this output
            Ssw_BmcUnroll_rec( pFrm, pObj, f );
            pObjFrame = Ssw_ObjFrame_( pFrm, pObj, f );
            Ssw_CnfNodeAddToSolver( pSat, Aig_Regular(pObjFrame) );
            status = sat_solver_simplify(pSat->pSat);
            assert( status );
            // solve
            Lit = toLitCond( Ssw_ObjSatNum(pSat,pObjFrame), Aig_IsComplement(pObjFrame) );
            if ( fVerbose )
            {
165
                Abc_Print( 1, "Solving output %2d of frame %3d ... \r",
Alan Mishchenko committed
166 167
                    i % Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) );
            }
Alan Mishchenko committed
168
            status = sat_solver_solve( pSat->pSat, &Lit, &Lit + 1, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
Alan Mishchenko committed
169
            if ( status == l_False )
Alan Mishchenko committed
170
            {
Alan Mishchenko committed
171 172 173 174 175
/*
                Lit = lit_neg( Lit );
                RetValue = sat_solver_addclause( pSat->pSat, &Lit, &Lit + 1 );
                assert( RetValue );
                if ( pSat->pSat->qtail != pSat->pSat->qhead )
Alan Mishchenko committed
176
                {
Alan Mishchenko committed
177 178 179 180 181 182
                    RetValue = sat_solver_simplify(pSat->pSat);
                    assert( RetValue );
                }
*/
                RetValue = 1;
                continue;
Alan Mishchenko committed
183
            }
Alan Mishchenko committed
184
            else if ( status == l_True )
Alan Mishchenko committed
185
            {
Alan Mishchenko committed
186 187 188 189 190 191 192 193 194 195
                pAig->pSeqModel = Ssw_BmcGetCounterExample( pFrm, pSat, i, f );
                if ( piFrame )
                    *piFrame = f;
                RetValue = 0;
                break;
            }
            else
            {
                if ( piFrame )
                    *piFrame = f;
Alan Mishchenko committed
196 197 198 199 200 201
                RetValue = -1;
                break;
            }
        }
        if ( fVerbose )
        {
202 203 204
            Abc_Print( 1, "Solved %2d outputs of frame %3d.  ", Saig_ManPoNum(pAig), f );
            Abc_Print( 1, "Conf =%8.0f. Var =%8d. AIG=%9d. ",
                (double)pSat->pSat->stats.conflicts,
Alan Mishchenko committed
205
                pSat->nSatVars, Aig_ManNodeNum(pFrm->pFrames) );
206 207
            ABC_PRT( "T", Abc_Clock() - clkPart );
            clkPart = Abc_Clock();
Alan Mishchenko committed
208
            fflush( stdout );
Alan Mishchenko committed
209
        }
Alan Mishchenko committed
210
        if ( RetValue != 1 )
Alan Mishchenko committed
211 212
            break;
    }
Alan Mishchenko committed
213 214 215

    Ssw_SatStop( pSat );
    Ssw_FrmStop( pFrm );
Alan Mishchenko committed
216 217 218 219 220 221 222 223
    return RetValue;
}

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


224
ABC_NAMESPACE_IMPL_END