abc/src/proof/ssw/sswCore.c

/**CFile****************************************************************

  FileName    [sswCore.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Inductive prover with constraints.]

  Synopsis    [The core procedures.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

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

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

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

#include "sswInt.h"

ABC_NAMESPACE_IMPL_START


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

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

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

  Synopsis    [This procedure sets default parameters.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ssw_ManSetDefaultParams( Ssw_Pars_t * p )
{
    memset( p, 0, sizeof(Ssw_Pars_t) );
    p->nPartSize      =       0;  // size of the partition
    p->nOverSize      =       0;  // size of the overlap between partitions
    p->nFramesK       =       1;  // the induction depth
    p->nFramesAddSim  =       2;  // additional frames to simulate
    p->fConstrs       =       0;  // treat the last nConstrs POs as seq constraints
    p->fMergeFull     =       0;  // enables full merge when constraints are used
    p->nBTLimit       =    1000;  // conflict limit at a node
    p->nBTLimitGlobal = 5000000;  // conflict limit for all runs
    p->nMinDomSize    =     100;  // min clock domain considered for optimization
    p->nItersStop     =      -1;  // stop after the given number of iterations
    p->nResimDelta    =    1000;  // the internal of nodes to resimulate
    p->nStepsMax      =      -1;  // (scorr only) the max number of induction steps
    p->fPolarFlip     =       0;  // uses polarity adjustment
    p->fLatchCorr     =       0;  // performs register correspondence
    p->fConstCorr     =       0;  // performs constant correspondence
    p->fOutputCorr    =       0;  // perform 'PO correspondence'
    p->fSemiFormal    =       0;  // enable semiformal filtering
    p->fDynamic       =       0;  // dynamic partitioning
    p->fLocalSim      =       0;  // local simulation
    p->fVerbose       =       0;  // verbose stats
    p->fEquivDump     =       0;  // enables dumping equivalences
    p->fEquivDump2    =       0;  // enables dumping equivalences

    // latch correspondence
    p->fLatchCorrOpt  =       0;  // performs optimized register correspondence
    p->nSatVarMax     =    1000;  // the max number of SAT variables
    p->nRecycleCalls  =      50;  // calls to perform before recycling SAT solver
    // signal correspondence
    p->nSatVarMax2    =    5000;  // the max number of SAT variables
    p->nRecycleCalls2 =     250;  // calls to perform before recycling SAT solver
    // return values
    p->nIters         =       0;  // the number of iterations performed
}

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

  Synopsis    [This procedure sets default parameters.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ssw_ManSetDefaultParamsLcorr( Ssw_Pars_t * p )
{
    Ssw_ManSetDefaultParams( p );
    p->fLatchCorrOpt = 1;
    p->nBTLimit      = 10000;
}

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

  Synopsis    [Reports improvements for property cones.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ssw_ReportConeReductions( Ssw_Man_t * p, Aig_Man_t * pAigInit, Aig_Man_t * pAigStop )
{
    Aig_Man_t * pAig1, * pAig2, * pAux;
    pAig1 = Aig_ManDupOneOutput( pAigInit, 0, 1 );
    pAig1 = Aig_ManScl( pAux = pAig1, 1, 1, 0, -1, -1, 0, 0 );
    Aig_ManStop( pAux );
    pAig2 = Aig_ManDupOneOutput( pAigStop, 0, 1 );
    pAig2 = Aig_ManScl( pAux = pAig2, 1, 1, 0, -1, -1, 0, 0 );
    Aig_ManStop( pAux );

    p->nNodesBegC = Aig_ManNodeNum(pAig1);
    p->nNodesEndC = Aig_ManNodeNum(pAig2);
    p->nRegsBegC  = Aig_ManRegNum(pAig1);
    p->nRegsEndC  = Aig_ManRegNum(pAig2);

    Aig_ManStop( pAig1 );
    Aig_ManStop( pAig2 );
}

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

  Synopsis    [Reports one node.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ssw_ReportOneOutput( Aig_Man_t * p, Aig_Obj_t * pObj )
{
    if ( pObj == Aig_ManConst1(p) )
        Abc_Print( 1, "1" );
    else if ( pObj == Aig_ManConst0(p) )
        Abc_Print( 1, "0" );
    else
        Abc_Print( 1, "X" );
}

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

  Synopsis    [Reports improvements for property cones.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ssw_ReportOutputs( Aig_Man_t * pAig )
{
    Aig_Obj_t * pObj;
    int i;
    Saig_ManForEachPo( pAig, pObj, i )
    {
        if ( i < Saig_ManPoNum(pAig)-Saig_ManConstrNum(pAig) )
            Abc_Print( 1, "o" );
        else
            Abc_Print( 1, "c" );
        Ssw_ReportOneOutput( pAig, Aig_ObjChild0(pObj) );
    }
    Abc_Print( 1, "\n" );
}

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

  Synopsis    [Remove from-equivs that are in the cone of constraints.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ssw_ManUpdateEquivs( Ssw_Man_t * p, Aig_Man_t * pAig, int fVerbose )
{
    Vec_Ptr_t * vCones;
    Aig_Obj_t ** pArray;
    Aig_Obj_t * pObj;
    int i, nTotal = 0, nRemoved = 0;
    // collect the nodes in the cone of constraints
    pArray  = (Aig_Obj_t **)Vec_PtrArray(pAig->vCos);
    pArray += Saig_ManPoNum(pAig) - Saig_ManConstrNum(pAig);
    vCones  = Aig_ManDfsNodes( pAig, pArray, Saig_ManConstrNum(pAig) );
    // remove all the node that are equiv to something and are in the cones
    Aig_ManForEachObj( pAig, pObj, i )
    {
        if ( !Aig_ObjIsCi(pObj) && !Aig_ObjIsNode(pObj) )
            continue;
        if ( pAig->pReprs[i] != NULL )
            nTotal++;
        if ( !Aig_ObjIsTravIdCurrent(pAig, pObj) )
            continue;
        if ( pAig->pReprs[i] )
        {
            if ( p->pPars->fConstrs && !p->pPars->fMergeFull )
            {
                pAig->pReprs[i] = NULL;
                nRemoved++;
            }
        }
    }
    // collect statistics    
    p->nConesTotal   = Aig_ManCiNum(pAig) + Aig_ManNodeNum(pAig);
    p->nConesConstr  = Vec_PtrSize(vCones);
    p->nEquivsTotal  = nTotal;
    p->nEquivsConstr = nRemoved;
    Vec_PtrFree( vCones );
}

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

  Synopsis    [Performs computation of signal correspondence with constraints.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p )
{
    int nSatProof, nSatCallsSat, nRecycles, nSatFailsReal, nUniques;
    Aig_Man_t * pAigNew;
    int RetValue, nIter = -1;
    abctime clk, clkTotal = Abc_Clock();
    // get the starting stats
    p->nLitsBeg  = Ssw_ClassesLitNum( p->ppClasses );
    p->nNodesBeg = Aig_ManNodeNum(p->pAig);
    p->nRegsBeg  = Aig_ManRegNum(p->pAig);
    // refine classes using BMC
    if ( p->pPars->fVerbose )
    {
        Abc_Print( 1, "Before BMC: " );
        Ssw_ClassesPrint( p->ppClasses, 0 );
    }
    if ( !p->pPars->fLatchCorr || p->pPars->nFramesK > 1 )
    {
        p->pMSat = Ssw_SatStart( 0 );
        if ( p->pPars->fConstrs )
            Ssw_ManSweepBmcConstr( p );
        else
            Ssw_ManSweepBmc( p );
        Ssw_SatStop( p->pMSat );
        p->pMSat = NULL;
        Ssw_ManCleanup( p );
    }
    if ( p->pPars->fVerbose )
    {
        Abc_Print( 1, "After  BMC: " );
        Ssw_ClassesPrint( p->ppClasses, 0 );
    }
    // apply semi-formal filtering
/*
    if ( p->pPars->fSemiFormal )
    {
        Aig_Man_t * pSRed;
        Ssw_FilterUsingSemi( p, 0, 2000, p->pPars->fVerbose );
//        Ssw_FilterUsingSemi( p, 1, 100000, p->pPars->fVerbose );
        pSRed = Ssw_SpeculativeReduction( p );
        Aig_ManDumpBlif( pSRed, "srm.blif", NULL, NULL );
        Aig_ManStop( pSRed );
    }
*/
    if ( p->pPars->pFunc )
    {
        ((int (*)(void *))p->pPars->pFunc)( p->pPars->pData );
        ((int (*)(void *))p->pPars->pFunc)( p->pPars->pData );
    }
    if ( p->pPars->nStepsMax == 0 )
    {
        Abc_Print( 1, "Stopped signal correspondence after BMC.\n" );
        goto finalize;
    }
    // refine classes using induction
    nSatProof = nSatCallsSat = nRecycles = nSatFailsReal = nUniques = 0;
    for ( nIter = 0; ; nIter++ )
    {
        if ( p->pPars->nStepsMax == nIter )
        {
            Abc_Print( 1, "Stopped signal correspondence after %d refiment iterations.\n", nIter );
            goto finalize;
        }
        if ( p->pPars->nItersStop >= 0 && p->pPars->nItersStop == nIter )
        {
            Aig_Man_t * pSRed = Ssw_SpeculativeReduction( p );
            Aig_ManDumpBlif( pSRed, "srm.blif", NULL, NULL );
            Aig_ManStop( pSRed );
            Abc_Print( 1, "Iterative refinement is stopped before iteration %d.\n", nIter );
            Abc_Print( 1, "The network is reduced using candidate equivalences.\n" );
            Abc_Print( 1, "Speculatively reduced miter is saved in file \"%s\".\n", "srm.blif" );
            Abc_Print( 1, "If the miter is SAT, the reduced result is incorrect.\n" );
            break;
        }

clk = Abc_Clock();
        p->pMSat = Ssw_SatStart( 0 );
        if ( p->pPars->fLatchCorrOpt )
        {
            RetValue = Ssw_ManSweepLatch( p );
            if ( p->pPars->fVerbose )
            {
                Abc_Print( 1, "%3d : C =%7d. Cl =%7d. Pr =%6d. Cex =%5d. R =%4d. F =%4d. ",
                    nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses),
                    p->nSatProof-nSatProof, p->nSatCallsSat-nSatCallsSat,
                    p->nRecycles-nRecycles, p->nSatFailsReal-nSatFailsReal );
                ABC_PRT( "T", Abc_Clock() - clk );
            }
        }
        else
        {
            if ( p->pPars->fConstrs )
                RetValue = Ssw_ManSweepConstr( p );
            else if ( p->pPars->fDynamic )
                RetValue = Ssw_ManSweepDyn( p );
            else
                RetValue = Ssw_ManSweep( p );

            p->pPars->nConflicts += p->pMSat->pSat->stats.conflicts;
            if ( p->pPars->fVerbose )
            {
                Abc_Print( 1, "%3d : C =%7d. Cl =%7d. LR =%6d. NR =%6d. ",
                    nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses),
                    p->nConstrReduced, Aig_ManNodeNum(p->pFrames) );
                if ( p->pPars->fDynamic )
                {
                    Abc_Print( 1, "Cex =%5d. ", p->nSatCallsSat-nSatCallsSat );
                    Abc_Print( 1, "R =%4d. ",   p->nRecycles-nRecycles );
                }
                Abc_Print( 1, "F =%5d. %s ", p->nSatFailsReal-nSatFailsReal,
                    (Saig_ManPoNum(p->pAig)==1 && Ssw_ObjIsConst1Cand(p->pAig,Aig_ObjFanin0(Aig_ManCo(p->pAig,0))))? "+" : "-" );
                ABC_PRT( "T", Abc_Clock() - clk );
            }
//            if ( p->pPars->fDynamic && p->nSatCallsSat-nSatCallsSat < 100 )
//                p->pPars->nBTLimit = 10000;

            if ( p->pPars->fStopWhenGone && Saig_ManPoNum(p->pAig) == 1 && !Ssw_ObjIsConst1Cand(p->pAig,Aig_ObjFanin0(Aig_ManCo(p->pAig,0))) )
            {
                printf( "Iterative refinement is stopped after iteration %d\n", nIter );
                printf( "because the property output is no longer a candidate constant.\n" );
                // prepare to quite
                p->nLitsEnd  = p->nLitsBeg;
                p->nNodesEnd = p->nNodesBeg;
                p->nRegsEnd  = p->nRegsBeg;
                // cleanup
                Ssw_SatStop( p->pMSat );
                p->pMSat = NULL;
                Ssw_ManCleanup( p );
                // cleanup
                Aig_ManSetPhase( p->pAig );
                Aig_ManCleanMarkB( p->pAig );
                return Aig_ManDupSimple( p->pAig );
            }
        }
        nSatProof     = p->nSatProof;
        nSatCallsSat  = p->nSatCallsSat;
        nRecycles     = p->nRecycles;
        nSatFailsReal = p->nSatFailsReal;
        nUniques      = p->nUniques;

        p->nVarsMax  = Abc_MaxInt( p->nVarsMax,  p->pMSat->nSatVars );
        p->nCallsMax = Abc_MaxInt( p->nCallsMax, p->pMSat->nSolverCalls );
        Ssw_SatStop( p->pMSat );
        p->pMSat = NULL;
        Ssw_ManCleanup( p );
        if ( !RetValue )
            break;
        if ( p->pPars->pFunc )
            ((int (*)(void *))p->pPars->pFunc)( p->pPars->pData );
    }

finalize:
    p->pPars->nIters = nIter + 1;
p->timeTotal = Abc_Clock() - clkTotal;

    Ssw_ManUpdateEquivs( p, p->pAig, p->pPars->fVerbose );
    pAigNew = Aig_ManDupRepr( p->pAig, 0 );
    Aig_ManSeqCleanup( pAigNew );
//Ssw_ClassesPrint( p->ppClasses, 1 );
    // get the final stats
    p->nLitsEnd  = Ssw_ClassesLitNum( p->ppClasses );
    p->nNodesEnd = Aig_ManNodeNum(pAigNew);
    p->nRegsEnd  = Aig_ManRegNum(pAigNew);
    // cleanup
    Aig_ManSetPhase( p->pAig );
    Aig_ManCleanMarkB( p->pAig );
    return pAigNew;
}

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

  Synopsis    [Performs computation of signal correspondence with constraints.]

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
{
    Ssw_Pars_t Pars;
    Aig_Man_t * pAigNew;
    Ssw_Man_t * p;
    assert( Aig_ManRegNum(pAig) > 0 );
    // reset random numbers
    Aig_ManRandom( 1 );
    // if parameters are not given, create them
    if ( pPars == NULL )
        Ssw_ManSetDefaultParams( pPars = &Pars );
    // consider the case of empty AIG
    if ( Aig_ManNodeNum(pAig) == 0 )
    {
        pPars->nIters = 0;
        // Ntl_ManFinalize() needs the following to satisfy an assertion
        Aig_ManReprStart( pAig,Aig_ManObjNumMax(pAig) );
        return Aig_ManDupOrdered(pAig);
    }
    // check and update parameters
    if ( pPars->fLatchCorrOpt )
    {
        pPars->fLatchCorr = 1;
        pPars->nFramesAddSim = 0;
        if ( (pAig->vClockDoms && Vec_VecSize(pAig->vClockDoms) > 0) )
           return Ssw_SignalCorrespondencePart( pAig, pPars );
    }
    else
    {
        assert( pPars->nFramesK > 0 );
        // perform partitioning
        if ( (pPars->nPartSize > 0 && pPars->nPartSize < Aig_ManRegNum(pAig))
             || (pAig->vClockDoms && Vec_VecSize(pAig->vClockDoms) > 0)  )
            return Ssw_SignalCorrespondencePart( pAig, pPars );
    }

    if ( pPars->fScorrGia )
    {
        if ( pPars->fLatchCorrOpt )
        {
            extern Aig_Man_t * Cec_LatchCorrespondence( Aig_Man_t * pAig, int nConfs, int fUseCSat );
            return Cec_LatchCorrespondence( pAig, pPars->nBTLimit, pPars->fUseCSat );
        }
        else
        {
            extern Aig_Man_t * Cec_SignalCorrespondence( Aig_Man_t * pAig, int nConfs, int fUseCSat );
            return Cec_SignalCorrespondence( pAig, pPars->nBTLimit, pPars->fUseCSat );
        }
    }

    // start the induction manager
    p = Ssw_ManCreate( pAig, pPars );
    // compute candidate equivalence classes
//    p->pPars->nConstrs = 1;
    if ( p->pPars->fConstrs )
    {
        // create trivial equivalence classes with all nodes being candidates for constant 1
        p->ppClasses = Ssw_ClassesPrepareSimple( pAig, pPars->fLatchCorr, pPars->nMaxLevs );
        Ssw_ClassesSetData( p->ppClasses, NULL, NULL, Ssw_SmlObjIsConstBit, Ssw_SmlObjsAreEqualBit );
        // derive phase bits to satisfy the constraints
        if ( Ssw_ManSetConstrPhases( pAig, p->pPars->nFramesK + 1, &p->vInits ) != 0 )
        {
            Abc_Print( 1, "Ssw_SignalCorrespondence(): The init state does not satisfy the constraints!\n" );
            p->pPars->fVerbose = 0;
            Ssw_ManStop( p );
            return NULL;
        }
        // perform simulation of the first timeframes
        Ssw_ManRefineByConstrSim( p );
    }
    else
    {
        // perform one round of seq simulation and generate candidate equivalence classes
        p->ppClasses = Ssw_ClassesPrepare( pAig, pPars->nFramesK, pPars->fLatchCorr, pPars->fConstCorr, pPars->fOutputCorr, pPars->nMaxLevs, pPars->fVerbose );
//        p->ppClasses = Ssw_ClassesPrepareTargets( pAig );
        if ( pPars->fLatchCorrOpt )
            p->pSml = Ssw_SmlStart( pAig, 0, 2, 1 );
        else if ( pPars->fDynamic )
            p->pSml = Ssw_SmlStart( pAig, 0, p->nFrames + p->pPars->nFramesAddSim, 1 );
        else
            p->pSml = Ssw_SmlStart( pAig, 0, 1 + p->pPars->nFramesAddSim, 1 );
        Ssw_ClassesSetData( p->ppClasses, p->pSml, (unsigned(*)(void *,Aig_Obj_t *))Ssw_SmlObjHashWord, (int(*)(void *,Aig_Obj_t *))Ssw_SmlObjIsConstWord, (int(*)(void *,Aig_Obj_t *,Aig_Obj_t *))Ssw_SmlObjsAreEqualWord );
    }
    // allocate storage
    if ( p->pPars->fLocalSim )
        p->pVisited = ABC_CALLOC( int, Ssw_SmlNumFrames( p->pSml ) * Aig_ManObjNumMax(p->pAig) );
    // perform refinement of classes
    pAigNew = Ssw_SignalCorrespondenceRefine( p );
//    Ssw_ReportOutputs( pAigNew );
    if ( pPars->fConstrs && pPars->fVerbose )
        Ssw_ReportConeReductions( p, pAig, pAigNew );
    // cleanup
    Ssw_ManStop( p );
    return pAigNew;
}

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

  Synopsis    [Performs computation of latch correspondence.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Aig_Man_t * Ssw_LatchCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
{
    Aig_Man_t * pRes;
    Ssw_Pars_t Pars;
    if ( pPars == NULL )
        Ssw_ManSetDefaultParamsLcorr( pPars = &Pars );
    pRes = Ssw_SignalCorrespondence( pAig, pPars );
//    if ( pPars->fConstrs && pPars->fVerbose )
//        Ssw_ReportConeReductions( pAig, pRes );
    return pRes;
}


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


ABC_NAMESPACE_IMPL_END