cecSeq.c 15 KB
Newer Older
Alan Mishchenko committed
1 2 3 4 5 6
/**CFile****************************************************************

  FileName    [cecSeq.c]

  SystemName  [ABC: Logic synthesis and verification system.]

Alan Mishchenko committed
7
  PackageName [Combinational equivalence checking.]
Alan Mishchenko committed
8 9 10 11 12 13 14 15 16 17 18 19 20 21 22

  Synopsis    [Refinement of sequential equivalence classes.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

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

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

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

#include "cecInt.h"

23 24 25
ABC_NAMESPACE_IMPL_START


Alan Mishchenko committed
26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44
////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

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

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

  Synopsis    [Sets register values from the counter-example.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
45
void Cec_ManSeqDeriveInfoFromCex( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Abc_Cex_t * pCex )
Alan Mishchenko committed
46 47
{
    unsigned * pInfo;
Alan Mishchenko committed
48
    int k, i, w, nWords;
Alan Mishchenko committed
49
    assert( pCex->nBits == pCex->nRegs + pCex->nPis * (pCex->iFrame + 1) );
Alan Mishchenko committed
50
    assert( pCex->nBits - pCex->nRegs + Gia_ManRegNum(pAig) <= Vec_PtrSize(vInfo) );
Alan Mishchenko committed
51
    nWords = Vec_PtrReadWordsSimInfo( vInfo );
52 53 54
/*
    // user register values
    assert( pCex->nRegs == Gia_ManRegNum(pAig) );
Alan Mishchenko committed
55 56
    for ( k = 0; k < pCex->nRegs; k++ )
    {
57
        pInfo = (unsigned *)Vec_PtrEntry( vInfo, k );
Alan Mishchenko committed
58
        for ( w = 0; w < nWords; w++ )
59
            pInfo[w] = Abc_InfoHasBit( pCex->pData, k )? ~0 : 0;
Alan Mishchenko committed
60
    }
61 62 63
*/
    // print warning about register values
    for ( k = 0; k < pCex->nRegs; k++ )
64
        if ( Abc_InfoHasBit( pCex->pData, k ) )
65 66 67 68 69
            break;
    if ( k < pCex->nRegs )
        Abc_Print( 0, "The CEX has flop values different from 0, but they are currently not used by \"resim\".\n" );

    // assign zero register values
Alan Mishchenko committed
70
    for ( k = 0; k < Gia_ManRegNum(pAig); k++ )
Alan Mishchenko committed
71
    {
72
        pInfo = (unsigned *)Vec_PtrEntry( vInfo, k );
Alan Mishchenko committed
73
        for ( w = 0; w < nWords; w++ )
Alan Mishchenko committed
74 75 76 77
            pInfo[w] = 0;
    }
    for ( i = pCex->nRegs; i < pCex->nBits; i++ )
    {
78
        pInfo = (unsigned *)Vec_PtrEntry( vInfo, k++ );
Alan Mishchenko committed
79
        for ( w = 0; w < nWords; w++ )
Alan Mishchenko committed
80
            pInfo[w] = Gia_ManRandom(0);
Alan Mishchenko committed
81
        // set simulation pattern and make sure it is second (first will be erased during simulation)
82
        pInfo[0] = (pInfo[0] << 1) | Abc_InfoHasBit( pCex->pData, i ); 
Alan Mishchenko committed
83 84 85 86
        pInfo[0] <<= 1;
    }
    for ( ; k < Vec_PtrSize(vInfo); k++ )
    {
87
        pInfo = (unsigned *)Vec_PtrEntry( vInfo, k );
Alan Mishchenko committed
88
        for ( w = 0; w < nWords; w++ )
Alan Mishchenko committed
89
            pInfo[w] = Gia_ManRandom(0);
Alan Mishchenko committed
90 91 92 93 94 95 96 97 98 99 100 101 102 103
    }
}

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

  Synopsis    [Sets register values from the counter-example.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
104
void Cec_ManSeqDeriveInfoInitRandom( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Abc_Cex_t * pCex )
Alan Mishchenko committed
105 106 107 108
{
    unsigned * pInfo;
    int k, w, nWords;
    nWords = Vec_PtrReadWordsSimInfo( vInfo );
Alan Mishchenko committed
109
    assert( pCex == NULL || Gia_ManRegNum(pAig) == pCex->nRegs );
Alan Mishchenko committed
110 111 112
    assert( Gia_ManRegNum(pAig) <= Vec_PtrSize(vInfo) );
    for ( k = 0; k < Gia_ManRegNum(pAig); k++ )
    {
113
        pInfo = (unsigned *)Vec_PtrEntry( vInfo, k );
Alan Mishchenko committed
114
        for ( w = 0; w < nWords; w++ )
115
            pInfo[w] = (pCex && Abc_InfoHasBit(pCex->pData, k))? ~0 : 0;
Alan Mishchenko committed
116 117 118 119
    }

    for ( ; k < Vec_PtrSize(vInfo); k++ )
    {
120
        pInfo = (unsigned *)Vec_PtrEntry( vInfo, k );
Alan Mishchenko committed
121
        for ( w = 0; w < nWords; w++ )
Alan Mishchenko committed
122
            pInfo[w] = Gia_ManRandom( 0 );
Alan Mishchenko committed
123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139
    }
}

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

  Synopsis    [Resimulates the classes using sequential simulation info.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Cec_ManSeqResimulate( Cec_ManSim_t * p, Vec_Ptr_t * vInfo )
{
    unsigned * pInfo0, * pInfo1;
Alan Mishchenko committed
140
    int f, i, k, w;
Alan Mishchenko committed
141
//    assert( Gia_ManRegNum(p->pAig) > 0 );
Alan Mishchenko committed
142
    assert( Vec_PtrSize(vInfo) == Gia_ManRegNum(p->pAig) + Gia_ManPiNum(p->pAig) * p->pPars->nFrames );
Alan Mishchenko committed
143 144
    for ( k = 0; k < Gia_ManRegNum(p->pAig); k++ )
    {
145 146
        pInfo0 = (unsigned *)Vec_PtrEntry( vInfo, k );
        pInfo1 = (unsigned *)Vec_PtrEntry( p->vCoSimInfo, Gia_ManPoNum(p->pAig) + k );
Alan Mishchenko committed
147 148 149
        for ( w = 0; w < p->nWords; w++ )
            pInfo1[w] = pInfo0[w];
    }
Alan Mishchenko committed
150
    for ( f = 0; f < p->pPars->nFrames; f++ )
Alan Mishchenko committed
151 152 153
    {
        for ( i = 0; i < Gia_ManPiNum(p->pAig); i++ )
        {
154 155
            pInfo0 = (unsigned *)Vec_PtrEntry( vInfo, k++ );
            pInfo1 = (unsigned *)Vec_PtrEntry( p->vCiSimInfo, i );
Alan Mishchenko committed
156 157 158 159 160
            for ( w = 0; w < p->nWords; w++ )
                pInfo1[w] = pInfo0[w];
        }
        for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ )
        {
161 162
            pInfo0 = (unsigned *)Vec_PtrEntry( p->vCoSimInfo, Gia_ManPoNum(p->pAig) + i );
            pInfo1 = (unsigned *)Vec_PtrEntry( p->vCiSimInfo, Gia_ManPiNum(p->pAig) + i );
Alan Mishchenko committed
163 164 165 166
            for ( w = 0; w < p->nWords; w++ )
                pInfo1[w] = pInfo0[w];
        }
        if ( Cec_ManSimSimulateRound( p, p->vCiSimInfo, p->vCoSimInfo ) )
Alan Mishchenko committed
167
            return 1;
Alan Mishchenko committed
168 169
    }
    assert( k == Vec_PtrSize(vInfo) );
Alan Mishchenko committed
170
    return 0;
Alan Mishchenko committed
171 172 173 174 175 176 177 178 179 180 181 182 183
}

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

  Synopsis    [Resimulates information to refine equivalence classes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
184
int Cec_ManSeqResimulateInfo( Gia_Man_t * pAig, Vec_Ptr_t * vSimInfo, Abc_Cex_t * pBestState, int fCheckMiter )
Alan Mishchenko committed
185 186 187
{
    Cec_ParSim_t ParsSim, * pParsSim = &ParsSim;
    Cec_ManSim_t * pSim;
188
    int RetValue;//, clkTotal = Abc_Clock();
Alan Mishchenko committed
189 190
    assert( (Vec_PtrSize(vSimInfo) - Gia_ManRegNum(pAig)) % Gia_ManPiNum(pAig) == 0 );
    Cec_ManSimSetDefaultParams( pParsSim );
Alan Mishchenko committed
191
    pParsSim->nFrames = (Vec_PtrSize(vSimInfo) - Gia_ManRegNum(pAig)) / Gia_ManPiNum(pAig);
Alan Mishchenko committed
192
    pParsSim->nWords  = Vec_PtrReadWordsSimInfo( vSimInfo );
Alan Mishchenko committed
193
    pParsSim->fCheckMiter = fCheckMiter;
194
    Gia_ManCreateValueRefs( pAig );
Alan Mishchenko committed
195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214
    pSim = Cec_ManSimStart( pAig, pParsSim );
    if ( pBestState )
        pSim->pBestState = pBestState;
    RetValue = Cec_ManSeqResimulate( pSim, vSimInfo );
    pSim->pBestState = NULL;
    Cec_ManSimStop( pSim );
    return RetValue;
}

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

  Synopsis    [Resimuates one counter-example to refine equivalence classes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
215
int Cec_ManSeqResimulateCounter( Gia_Man_t * pAig, Cec_ParSim_t * pPars, Abc_Cex_t * pCex )
Alan Mishchenko committed
216 217
{
    Vec_Ptr_t * vSimInfo;
218
    int RetValue;
219
    abctime clkTotal = Abc_Clock();
Alan Mishchenko committed
220 221
    if ( pCex == NULL )
    {
222
        Abc_Print( 1, "Cec_ManSeqResimulateCounter(): Counter-example is not available.\n" );
Alan Mishchenko committed
223 224 225 226
        return -1;
    }
    if ( pAig->pReprs == NULL )
    {
227
        Abc_Print( 1, "Cec_ManSeqResimulateCounter(): Equivalence classes are not available.\n" );
Alan Mishchenko committed
228 229 230 231
        return -1;
    }
    if ( Gia_ManRegNum(pAig) == 0 )
    {
232
        Abc_Print( 1, "Cec_ManSeqResimulateCounter(): Not a sequential AIG.\n" );
Alan Mishchenko committed
233 234
        return -1;
    }
Alan Mishchenko committed
235 236
//    if ( Gia_ManRegNum(pAig) != pCex->nRegs || Gia_ManPiNum(pAig) != pCex->nPis )
    if ( Gia_ManPiNum(pAig) != pCex->nPis )
Alan Mishchenko committed
237
    {
238
        Abc_Print( 1, "Cec_ManSeqResimulateCounter(): The number of PIs in the AIG and the counter-example differ.\n" );
Alan Mishchenko committed
239 240 241
        return -1;
    }
    if ( pPars->fVerbose )
242
        Abc_Print( 1, "Resimulating %d timeframes.\n", pPars->nFrames + pCex->iFrame + 1 );
Alan Mishchenko committed
243
    Gia_ManRandom( 1 );
Alan Mishchenko committed
244
    vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pAig) + 
Alan Mishchenko committed
245
        Gia_ManPiNum(pAig) * (pPars->nFrames + pCex->iFrame + 1), 1 );
Alan Mishchenko committed
246 247 248
    Cec_ManSeqDeriveInfoFromCex( vSimInfo, pAig, pCex );
    if ( pPars->fVerbose )
        Gia_ManEquivPrintClasses( pAig, 0, 0 );
Alan Mishchenko committed
249
    RetValue = Cec_ManSeqResimulateInfo( pAig, vSimInfo, NULL, pPars->fCheckMiter );
Alan Mishchenko committed
250 251 252 253
    if ( pPars->fVerbose )
        Gia_ManEquivPrintClasses( pAig, 0, 0 );
    Vec_PtrFree( vSimInfo );
    if ( pPars->fVerbose )
254
        ABC_PRT( "Time", Abc_Clock() - clkTotal );
255 256
//    if ( RetValue && pPars->fCheckMiter )
//        Abc_Print( 1, "Cec_ManSeqResimulateCounter(): An output of the miter is asserted!\n" );
Alan Mishchenko committed
257 258 259 260 261 262
    return RetValue;
}


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

Alan Mishchenko committed
263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318
  Synopsis    [Returns the number of POs that are not const0 cands.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Cec_ManCountNonConstOutputs( Gia_Man_t * pAig )
{
    Gia_Obj_t * pObj;
    int i, Counter = 0;
    if ( pAig->pReprs == NULL )
        return -1;
    Gia_ManForEachPo( pAig, pObj, i )
        if ( !Gia_ObjIsConst( pAig, Gia_ObjFaninId0p(pAig, pObj) ) )
            Counter++;
    return Counter;
}

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

  Synopsis    [Returns the number of POs that are not const0 cands.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Cec_ManCheckNonTrivialCands( Gia_Man_t * pAig )
{
    Gia_Obj_t * pObj;
    int i, RetValue = 0;
    if ( pAig->pReprs == NULL )
        return 0;
    // label internal nodes driving POs
    Gia_ManForEachPo( pAig, pObj, i )
        Gia_ObjFanin0(pObj)->fMark0 = 1;
    // check if there are non-labled equivs
    Gia_ManForEachObj( pAig, pObj, i )
        if ( Gia_ObjIsCand(pObj) && !pObj->fMark0 && Gia_ObjRepr(pAig, i) != GIA_VOID )
        {
            RetValue = 1;
            break;
        }
    // clean internal nodes driving POs
    Gia_ManForEachPo( pAig, pObj, i )
        Gia_ObjFanin0(pObj)->fMark0 = 0;
    return RetValue;
}

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

Alan Mishchenko committed
319 320 321 322 323 324 325 326 327 328 329
  Synopsis    [Performs semiformal refinement of equivalence classes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars )
{ 
Alan Mishchenko committed
330 331 332
    int nAddFrames = 16; // additional timeframes to simulate
    int nCountNoRef = 0;
    int nFramesReal;
Alan Mishchenko committed
333 334
    Cec_ParSat_t ParsSat, * pParsSat = &ParsSat;
    Vec_Ptr_t * vSimInfo; 
Alan Mishchenko committed
335
    Vec_Str_t * vStatus;
336
    Abc_Cex_t * pState;
Alan Mishchenko committed
337 338
    Gia_Man_t * pSrm, * pReduce, * pAux;
    int r, nPats, RetValue = 0;
Alan Mishchenko committed
339
    if ( pAig->pReprs == NULL )
Alan Mishchenko committed
340
    { 
341
        Abc_Print( 1, "Cec_ManSeqSemiformal(): Equivalence classes are not available.\n" );
Alan Mishchenko committed
342 343 344 345
        return -1;
    }
    if ( Gia_ManRegNum(pAig) == 0 )
    {
346
        Abc_Print( 1, "Cec_ManSeqSemiformal(): Not a sequential AIG.\n" );
Alan Mishchenko committed
347 348
        return -1;
    }
Alan Mishchenko committed
349
    Gia_ManRandom( 1 );
Alan Mishchenko committed
350
    // prepare starting pattern
351
    pState = Abc_CexAlloc( Gia_ManRegNum(pAig), 0, 0 );
Alan Mishchenko committed
352 353 354 355 356 357 358 359
    pState->iFrame = -1;
    pState->iPo = -1;
    // prepare SAT solving
    Cec_ManSatSetDefaultParams( pParsSat );
    pParsSat->nBTLimit = pPars->nBTLimit;
    pParsSat->fVerbose = pPars->fVerbose;
    if ( pParsSat->fVerbose )
    {
360
        Abc_Print( 1, "Starting: " );
Alan Mishchenko committed
361 362 363
        Gia_ManEquivPrintClasses( pAig, 0, 0 );
    }
    // perform the given number of BMC rounds
Alan Mishchenko committed
364
    Gia_ManCleanMark0( pAig );
Alan Mishchenko committed
365 366
    for ( r = 0; r < pPars->nRounds; r++ )
    {
Alan Mishchenko committed
367 368
        if ( !Cec_ManCheckNonTrivialCands(pAig) )
        {
369
            Abc_Print( 1, "Cec_ManSeqSemiformal: There are only trivial equiv candidates left (PO drivers). Quitting.\n" );
Alan Mishchenko committed
370 371
            break;
        }
372
//        Abc_CexPrint( pState );
Alan Mishchenko committed
373
        // derive speculatively reduced model
Alan Mishchenko committed
374 375 376 377
//        pSrm = Gia_ManSpecReduceInit( pAig, pState, pPars->nFrames, pPars->fDualOut );
        pSrm = Gia_ManSpecReduceInitFrames( pAig, pState, pPars->nFrames, &nFramesReal, pPars->fDualOut, pPars->nMinOutputs );
        if ( pSrm == NULL )
        {
378
            Abc_Print( 1, "Quitting refinement because miter could not be unrolled.\n" );
Alan Mishchenko committed
379 380 381 382
            break;
        }
        assert( Gia_ManRegNum(pSrm) == 0 && Gia_ManPiNum(pSrm) == (Gia_ManPiNum(pAig) * nFramesReal) );
        if ( pPars->fVerbose )
383
            Abc_Print( 1, "Unrolled for %d frames.\n", nFramesReal );
Alan Mishchenko committed
384 385
        // allocate room for simulation info
        vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pAig) + 
Alan Mishchenko committed
386
            Gia_ManPiNum(pAig) * (nFramesReal + nAddFrames), pPars->nWords );
Alan Mishchenko committed
387 388
        Cec_ManSeqDeriveInfoInitRandom( vSimInfo, pAig, pState );
        // fill in simulation info with counter-examples
Alan Mishchenko committed
389 390
        vStatus = Cec_ManSatSolveSeq( vSimInfo, pSrm, pParsSat, Gia_ManRegNum(pAig), &nPats );
        Vec_StrFree( vStatus );
Alan Mishchenko committed
391 392
        Gia_ManStop( pSrm );
        // resimulate and refine the classes
Alan Mishchenko committed
393
        RetValue = Cec_ManSeqResimulateInfo( pAig, vSimInfo, pState, pPars->fCheckMiter );
Alan Mishchenko committed
394 395 396 397 398
        Vec_PtrFree( vSimInfo );
        assert( pState->iPo >= 0 ); // hit counter
        pState->iPo = -1;
        if ( pPars->fVerbose )
        {
399
            Abc_Print( 1, "BMC = %3d ", nPats );
Alan Mishchenko committed
400 401
            Gia_ManEquivPrintClasses( pAig, 0, 0 );
        }
Alan Mishchenko committed
402 403

        // write equivalence classes
404
        Gia_AigerWrite( pAig, "gore.aig", 0, 0 );
Alan Mishchenko committed
405
        // reduce the model
406
        pReduce = Gia_ManSpecReduce( pAig, 0, 0, 1, 0, 0 );
Alan Mishchenko committed
407 408 409 410
        if ( pReduce )
        {
            pReduce = Gia_ManSeqStructSweep( pAux = pReduce, 1, 1, 0 );
            Gia_ManStop( pAux );
411
            Gia_AigerWrite( pReduce, "gsrm.aig", 0, 0 );
412
//            Abc_Print( 1, "Speculatively reduced model was written into file \"%s\".\n", "gsrm.aig" );
Alan Mishchenko committed
413 414 415 416 417 418
//          Gia_ManPrintStatsShort( pReduce );
            Gia_ManStop( pReduce );
        }

        if ( RetValue )
        {
419
            Abc_Print( 1, "Cec_ManSeqSemiformal(): An output of the miter is asserted. Refinement stopped.\n" );
Alan Mishchenko committed
420 421 422 423 424 425 426
            break;
        }
        // decide when to stop
        if ( nPats > 0 )
            nCountNoRef = 0;
        else if ( ++nCountNoRef == pPars->nNonRefines )
            break;
Alan Mishchenko committed
427 428
    }
    ABC_FREE( pState );
Alan Mishchenko committed
429 430 431 432
    if ( pPars->fCheckMiter )
    {
        int nNonConsts = Cec_ManCountNonConstOutputs( pAig );
        if ( nNonConsts )
433
            Abc_Print( 1, "The number of POs that are not const-0 candidates = %d.\n", nNonConsts );
Alan Mishchenko committed
434
    }
Alan Mishchenko committed
435 436 437
    return RetValue;
}

Alan Mishchenko committed
438 439 440 441 442
//&r s13207.aig; &ps; &equiv; &ps; &semi -R 2 -vm
//&r bug/50/temp.aig; &ps; &equiv -smv; &semi -v
//r mentor/1_05c.blif; st; &get; &ps; &equiv -smv; &semi -mv
//&r bug/50/hdl1.aig; &ps; &equiv -smv; &semi -mv; &srm; &r gsrm.aig; &ps

Alan Mishchenko committed
443 444 445 446 447
////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////


448 449
ABC_NAMESPACE_IMPL_END