saigTempor.c 8.42 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    [saigTempor.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Sequential AIG package.]

  Synopsis    [Temporal decomposition.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

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

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

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

#include "saig.h"
22
#include "sat/bmc/bmc.h"
23 24 25 26 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

ABC_NAMESPACE_IMPL_START


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

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

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

  Synopsis    [Creates initialized timeframes for temporal decomposition.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Aig_Man_t * Saig_ManTemporFrames( Aig_Man_t * pAig, int nFrames )
{
    Aig_Man_t * pFrames;
    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
    int i, f;
    // start the frames package
    Aig_ManCleanData( pAig );
    pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) * nFrames );
54
    pFrames->pName = Abc_UtilStrsav( pAig->pName );
55 56 57 58 59 60 61 62
    // initiliaze the flops
    Saig_ManForEachLo( pAig, pObj, i )
        pObj->pData = Aig_ManConst0(pFrames);
    // for each timeframe
    for ( f = 0; f < nFrames; f++ )
    {
        Aig_ManConst1(pAig)->pData = Aig_ManConst1(pFrames);
        Saig_ManForEachPi( pAig, pObj, i )
63
            pObj->pData = Aig_ObjCreateCi(pFrames);
64 65
        Aig_ManForEachNode( pAig, pObj, i )
            pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
66
        Aig_ManForEachCo( pAig, pObj, i )
67 68 69 70 71 72
            pObj->pData = Aig_ObjChild0Copy(pObj);
        Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
            pObjLo->pData = pObjLi->pData;
    }
    // create POs for the flop inputs
    Saig_ManForEachLi( pAig, pObj, i )
73
        Aig_ObjCreateCo( pFrames, (Aig_Obj_t *)pObj->pData );
74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101
    Aig_ManCleanup( pFrames );
    return pFrames;
}


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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Aig_Man_t * Saig_ManTemporDecompose( Aig_Man_t * pAig, int nFrames )
{
    Aig_Man_t * pAigNew, * pFrames;
    Aig_Obj_t * pObj, * pReset;
    int i;
    if ( pAig->nConstrs > 0 )
    {
        printf( "The AIG manager should have no constraints.\n" );
        return NULL;
    }
    // create initialized timeframes
    pFrames = Saig_ManTemporFrames( pAig, nFrames );
102
    assert( Aig_ManCoNum(pFrames) == Aig_ManRegNum(pAig) );
103 104 105 106

    // start the new manager
    Aig_ManCleanData( pAig );
    pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
107
    pAigNew->pName = Abc_UtilStrsav( pAig->pName );
108 109 110
    // map the constant node and primary inputs
    Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
    Saig_ManForEachPi( pAig, pObj, i )
111
        pObj->pData = Aig_ObjCreateCi( pAigNew );
112 113 114

    // insert initialization logic
    Aig_ManConst1(pFrames)->pData = Aig_ManConst1( pAigNew );
115 116
    Aig_ManForEachCi( pFrames, pObj, i )
        pObj->pData = Aig_ObjCreateCi( pAigNew );
117 118
    Aig_ManForEachNode( pFrames, pObj, i )
        pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
119
    Aig_ManForEachCo( pFrames, pObj, i )
120 121 122
        pObj->pData = Aig_ObjChild0Copy(pObj);

    // create reset latch (the first one among the latches)
123
    pReset = Aig_ObjCreateCi( pAigNew );
124 125 126

    // create flop output values
    Saig_ManForEachLo( pAig, pObj, i )
127
        pObj->pData = Aig_Mux( pAigNew, pReset, Aig_ObjCreateCi(pAigNew), (Aig_Obj_t *)Aig_ManCo(pFrames, i)->pData );
128 129 130 131 132 133 134
    Aig_ManStop( pFrames );

    // add internal nodes of this frame
    Aig_ManForEachNode( pAig, pObj, i )
        pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
    // create primary outputs
    Saig_ManForEachPo( pAig, pObj, i )
135
        Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
136 137

    // create reset latch (the first one among the latches)
138
    Aig_ObjCreateCo( pAigNew, Aig_ManConst1(pAigNew) );
139 140
    // create latch inputs
    Saig_ManForEachLi( pAig, pObj, i )
141
        Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
142 143 144 145 146 147 148 149 150

    // finalize
    Aig_ManCleanup( pAigNew );
    Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig)+1 ); // + reset latch (011111...)
    return pAigNew;
}

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

151 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
  Synopsis    [Find index of first non-zero entry.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Vec_IntLastNonZeroBeforeLimit( Vec_Int_t * vTemp, int Limit )
{
    int Entry, i;
    if ( vTemp == NULL )
        return -1;
    Vec_IntForEachEntryReverse( vTemp, Entry, i )
    {
        if ( i >= Limit )
            continue;
        if ( Entry )
            return i;
    }
    return -1;
}

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

177 178 179 180 181 182 183 184 185
  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
186
Aig_Man_t * Saig_ManTempor( Aig_Man_t * pAig, int nFrames, int TimeOut, int nConfLimit, int fUseBmc, int fUseTransSigs, int fVerbose, int fVeryVerbose )
187
{ 
188 189 190
    extern int Saig_ManPhasePrefixLength( Aig_Man_t * p, int fVerbose, int fVeryVerbose, Vec_Int_t ** pvTrans );

    Vec_Int_t * vTransSigs = NULL;
191 192 193 194
    int RetValue, nFramesFinished = -1;
    assert( nFrames >= 0 ); 
    if ( nFrames == 0 )
    {
195
        nFrames = Saig_ManPhasePrefixLength( pAig, fVerbose, fVeryVerbose, &vTransSigs );
196 197 198 199 200 201
        if ( nFrames == 0 )
        {
            Vec_IntFreeP( &vTransSigs );
            printf( "The leading sequence has length 0. Temporal decomposition is not performed.\n" );
            return NULL;
        }
202 203
        if ( nFrames == 1 )
        {
204
            Vec_IntFreeP( &vTransSigs );
205 206 207
            printf( "The leading sequence has length 1. Temporal decomposition is not performed.\n" );
            return NULL;
        }
208 209 210 211 212 213 214 215 216 217 218
        if ( fUseTransSigs )
        {
            int Entry, i, iLast = -1;
            Vec_IntForEachEntry( vTransSigs, Entry, i )
                iLast = Entry ? i :iLast;
            if ( iLast > 0 && iLast < nFrames )
            {
                Abc_Print( 1, "Reducing frame count from %d to %d to fit the last transient.\n", nFrames, iLast );
                nFrames = iLast;
            }
        }
219 220 221 222 223 224 225
        Abc_Print( 1, "Using computed frame number (%d).\n", nFrames );
    }
    else
        Abc_Print( 1, "Using user-given frame number (%d).\n", nFrames );
    // run BMC2
    if ( fUseBmc )
    {
226
        RetValue = Saig_BmcPerform( pAig, 0, nFrames, 2000, TimeOut, nConfLimit, 0, fVerbose, 0, &nFramesFinished, 0, 0 );
227 228
        if ( RetValue == 0 )
        {
229
            Vec_IntFreeP( &vTransSigs );
230 231 232
            printf( "A cex found in the first %d frames.\n", nFrames );
            return NULL;
        }
233
        if ( nFramesFinished + 1 < nFrames )
234
        {
235 236 237 238 239 240 241 242 243
            int iLastBefore = Vec_IntLastNonZeroBeforeLimit( vTransSigs, nFramesFinished );
            if ( iLastBefore < 1 || !fUseTransSigs )
            {
                Vec_IntFreeP( &vTransSigs );
                printf( "BMC for %d frames could not be completed. A cex may exist!\n", nFrames );
                return NULL;
            }
            assert( iLastBefore < nFramesFinished );
            printf( "BMC succeeded to frame %d. Adjusting frame count to be (%d) based on the last transient signal.\n", nFramesFinished, iLastBefore );
244
            nFrames = iLastBefore;
245 246
        }
    }
247
    Vec_IntFreeP( &vTransSigs );
248 249 250 251 252 253 254 255 256
    return Saig_ManTemporDecompose( pAig, nFrames );
}

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

ABC_NAMESPACE_IMPL_END