src/base/abci/abcProve.c File Reference

#include "abc.h"
#include "fraig.h"
#include "math.h"
Include dependency graph for abcProve.c:

Go to the source code of this file.

Functions

int Abc_NtkRefactor (Abc_Ntk_t *pNtk, int nNodeSizeMax, int nConeSizeMax, bool fUpdateLevel, bool fUseZeros, bool fUseDcs, bool fVerbose)
Abc_Ntk_t * Abc_NtkFromFraig (Fraig_Man_t *pMan, Abc_Ntk_t *pNtk)
static Abc_Ntk_t * Abc_NtkMiterFraig (Abc_Ntk_t *pNtk, int nBTLimit, sint64 nInspLimit, int *pRetValue, int *pNumFails, sint64 *pNumConfs, sint64 *pNumInspects)
static void Abc_NtkMiterPrint (Abc_Ntk_t *pNtk, char *pString, int clk, int fVerbose)
int Abc_NtkMiterProve (Abc_Ntk_t **ppNtk, void *pPars)
Abc_Ntk_t * Abc_NtkMiterRwsat (Abc_Ntk_t *pNtk)

Function Documentation

Abc_Ntk_t* Abc_NtkFromFraig ( Fraig_Man_t *  pMan,
Abc_Ntk_t *  pNtk 
)

CFile****************************************************************

FileName [abcFraig.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Network and node package.]

Synopsis [Procedures interfacing with the FRAIG package.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id
abcFraig.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

] DECLARATIONS ///

Function*************************************************************

Synopsis [Transforms FRAIG into strashed network with choices.]

Description []

SideEffects []

SeeAlso []

Definition at line 276 of file abcFraig.c.

00277 {
00278     ProgressBar * pProgress;
00279     Abc_Ntk_t * pNtkNew;
00280     Abc_Obj_t * pNode, * pNodeNew;
00281     int i;
00282     // create the new network
00283     pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
00284     // make the mapper point to the new network
00285     Abc_NtkForEachCi( pNtk, pNode, i )
00286         Fraig_NodeSetData1( Fraig_ManReadIthVar(pMan, i), (Fraig_Node_t *)pNode->pCopy );
00287     // set the constant node
00288     Fraig_NodeSetData1( Fraig_ManReadConst1(pMan), (Fraig_Node_t *)Abc_AigConst1(pNtkNew) );
00289     // process the nodes in topological order
00290     pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) );
00291     Abc_NtkForEachCo( pNtk, pNode, i )
00292     {
00293         Extra_ProgressBarUpdate( pProgress, i, NULL );
00294         pNodeNew = Abc_NodeFromFraig_rec( pNtkNew, Fraig_ManReadOutputs(pMan)[i] );
00295         Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
00296     }
00297     Extra_ProgressBarStop( pProgress );
00298     Abc_NtkReassignIds( pNtkNew );
00299     return pNtkNew;
00300 }

Abc_Ntk_t * Abc_NtkMiterFraig ( Abc_Ntk_t *  pNtk,
int  nBTLimit,
sint64  nInspLimit,
int *  pRetValue,
int *  pNumFails,
sint64 *  pNumConfs,
sint64 *  pNumInspects 
) [static]

Function*************************************************************

Synopsis [Attempts to solve the miter using a number of tricks.]

Description [Returns -1 if timed out; 0 if SAT; 1 if UNSAT.]

SideEffects []

SeeAlso []

Definition at line 241 of file abcProve.c.

00242 {
00243     Abc_Ntk_t * pNtkNew;
00244     Fraig_Params_t Params, * pParams = &Params;
00245     Fraig_Man_t * pMan;
00246     int nWords1, nWords2, nWordsMin, RetValue;
00247     int * pModel;
00248 
00249     // to determine the number of simulation patterns
00250     // use the following strategy
00251     // at least 64 words (32 words random and 32 words dynamic)
00252     // no more than 256M for one circuit (128M + 128M)
00253     nWords1 = 32;
00254     nWords2 = (1<<27) / (Abc_NtkNodeNum(pNtk) + Abc_NtkCiNum(pNtk));
00255     nWordsMin = ABC_MIN( nWords1, nWords2 );
00256 
00257     // set the FRAIGing parameters
00258     Fraig_ParamsSetDefault( pParams );
00259     pParams->nPatsRand  = nWordsMin * 32; // the number of words of random simulation info
00260     pParams->nPatsDyna  = nWordsMin * 32; // the number of words of dynamic simulation info
00261     pParams->nBTLimit   = nBTLimit;       // the max number of backtracks
00262     pParams->nSeconds   = -1;             // the runtime limit
00263     pParams->fTryProve  = 0;              // do not try to prove the final miter
00264     pParams->fDoSparse  = 1;              // try proving sparse functions
00265     pParams->fVerbose   = 0;
00266     pParams->nInspLimit = nInspLimit;
00267 
00268     // transform the target into a fraig
00269     pMan = Abc_NtkToFraig( pNtk, pParams, 0, 0 ); 
00270     Fraig_ManProveMiter( pMan );
00271     RetValue = Fraig_ManCheckMiter( pMan );
00272 
00273     // create the network 
00274     pNtkNew = Abc_NtkFromFraig( pMan, pNtk );
00275 
00276     // save model
00277     if ( RetValue == 0 )
00278     {
00279         pModel = Fraig_ManReadModel( pMan );
00280         FREE( pNtkNew->pModel );
00281         pNtkNew->pModel = ALLOC( int, Abc_NtkCiNum(pNtkNew) );
00282         memcpy( pNtkNew->pModel, pModel, sizeof(int) * Abc_NtkCiNum(pNtkNew) );
00283     }
00284 
00285     // save the return values
00286     *pRetValue = RetValue;
00287     *pNumFails = Fraig_ManReadSatFails( pMan );
00288     *pNumConfs = Fraig_ManReadConflicts( pMan );
00289     *pNumInspects = Fraig_ManReadInspects( pMan );
00290 
00291     // delete the fraig manager
00292     Fraig_ManFree( pMan );
00293     return pNtkNew;
00294 }

void Abc_NtkMiterPrint ( Abc_Ntk_t *  pNtk,
char *  pString,
int  clk,
int  fVerbose 
) [static]

Function*************************************************************

Synopsis [Attempts to solve the miter using a number of tricks.]

Description [Returns -1 if timed out; 0 if SAT; 1 if UNSAT.]

SideEffects []

SeeAlso []

Definition at line 307 of file abcProve.c.

00308 {
00309     if ( !fVerbose )
00310         return;
00311     printf( "Nodes = %7d.  Levels = %4d.  ", Abc_NtkNodeNum(pNtk), 
00312         Abc_NtkIsStrash(pNtk)? Abc_AigLevel(pNtk) : Abc_NtkLevel(pNtk) );
00313     PRT( pString, clock() - clk );
00314 }

int Abc_NtkMiterProve ( Abc_Ntk_t **  ppNtk,
void *  pPars 
)

FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Attempts to solve the miter using a number of tricks.]

Description [Returns -1 if timed out; 0 if SAT; 1 if UNSAT. Returns a simplified version of the original network (or a constant 0 network). In case the network is not a constant zero and a SAT assignment is found, pNtk->pModel contains a satisfying assignment.]

SideEffects []

SeeAlso []

Definition at line 54 of file abcProve.c.

00055 {
00056     Prove_Params_t * pParams = pPars;
00057     Abc_Ntk_t * pNtk, * pNtkTemp;
00058     int RetValue, nIter, nSatFails, Counter, clk, timeStart = clock();
00059     sint64 nSatConfs, nSatInspects, nInspectLimit;
00060 
00061     // get the starting network
00062     pNtk = *ppNtk;
00063     assert( Abc_NtkIsStrash(pNtk) );
00064     assert( Abc_NtkPoNum(pNtk) == 1 );
00065  
00066     if ( pParams->fVerbose )
00067     {
00068         printf( "RESOURCE LIMITS: Iterations = %d. Rewriting = %s. Fraiging = %s.\n",
00069             pParams->nItersMax, pParams->fUseRewriting? "yes":"no", pParams->fUseFraiging? "yes":"no" );
00070         printf( "Mitering = %d (%3.1f).  Rewriting = %d (%3.1f).  Fraiging = %d (%3.1f).\n", 
00071             pParams->nMiteringLimitStart,  pParams->nMiteringLimitMulti, 
00072             pParams->nRewritingLimitStart, pParams->nRewritingLimitMulti,
00073             pParams->nFraigingLimitStart,  pParams->nFraigingLimitMulti );
00074         printf( "Mitering last = %d.\n", 
00075             pParams->nMiteringLimitLast );
00076     }
00077 
00078     // if SAT only, solve without iteration
00079     if ( !pParams->fUseRewriting && !pParams->fUseFraiging )
00080     {
00081         clk = clock();
00082         RetValue = Abc_NtkMiterSat( pNtk, (sint64)pParams->nMiteringLimitLast, (sint64)0, 0, NULL, NULL );
00083         Abc_NtkMiterPrint( pNtk, "SAT solving", clk, pParams->fVerbose );
00084         *ppNtk = pNtk;
00085         return RetValue;
00086     }
00087 
00088     // check the current resource limits
00089     for ( nIter = 0; nIter < pParams->nItersMax; nIter++ )
00090     {
00091         if ( pParams->fVerbose )
00092         {
00093             printf( "ITERATION %2d : Confs = %6d. FraigBTL = %3d. \n", nIter+1, 
00094                  (int)(pParams->nMiteringLimitStart * pow(pParams->nMiteringLimitMulti,nIter)), 
00095                  (int)(pParams->nFraigingLimitStart * pow(pParams->nFraigingLimitMulti,nIter)) );
00096             fflush( stdout );
00097         }
00098 
00099         // try brute-force SAT
00100         clk = clock();
00101         nInspectLimit = pParams->nTotalInspectLimit? pParams->nTotalInspectLimit - pParams->nTotalInspectsMade : 0;
00102         RetValue = Abc_NtkMiterSat( pNtk, (sint64)(pParams->nMiteringLimitStart * pow(pParams->nMiteringLimitMulti,nIter)), (sint64)nInspectLimit, 0, &nSatConfs, &nSatInspects );
00103         Abc_NtkMiterPrint( pNtk, "SAT solving", clk, pParams->fVerbose );
00104         if ( RetValue >= 0 )
00105             break;
00106 
00107         // add to the number of backtracks and inspects
00108         pParams->nTotalBacktracksMade += nSatConfs;
00109         pParams->nTotalInspectsMade   += nSatInspects;
00110         // check if global resource limit is reached
00111         if ( (pParams->nTotalBacktrackLimit && pParams->nTotalBacktracksMade >= pParams->nTotalBacktrackLimit) ||
00112              (pParams->nTotalInspectLimit   && pParams->nTotalInspectsMade   >= pParams->nTotalInspectLimit) )
00113         {
00114             printf( "Reached global limit on conflicts/inspects. Quitting.\n" );
00115             *ppNtk = pNtk;
00116             return -1;
00117         }
00118 
00119         // try rewriting
00120         if ( pParams->fUseRewriting )
00121         {
00122             clk = clock();
00123             Counter = (int)(pParams->nRewritingLimitStart * pow(pParams->nRewritingLimitMulti,nIter));
00124 //            Counter = 1;
00125             while ( 1 )
00126             {
00127 /*
00128                 extern Abc_Ntk_t * Abc_NtkIvyResyn( Abc_Ntk_t * pNtk, int fUpdateLevel, int fVerbose );
00129                 pNtk = Abc_NtkIvyResyn( pNtkTemp = pNtk, 0, 0 );  Abc_NtkDelete( pNtkTemp );
00130                 if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 )
00131                     break;
00132                 if ( --Counter == 0 )
00133                     break;
00134 */
00135 /*
00136                 Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 );
00137                 if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 )
00138                     break;
00139                 if ( --Counter == 0 )
00140                     break;
00141 */
00142                 Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 );
00143                 if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 )
00144                     break;
00145                 if ( --Counter == 0 )
00146                     break;
00147                 Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 );
00148                 if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 )
00149                     break;
00150                 if ( --Counter == 0 )
00151                     break;
00152                 pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 );  Abc_NtkDelete( pNtkTemp );
00153                 if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 )
00154                     break;
00155                 if ( --Counter == 0 )
00156                     break;
00157             }
00158             Abc_NtkMiterPrint( pNtk, "Rewriting  ", clk, pParams->fVerbose );
00159         }
00160  
00161         if ( pParams->fUseFraiging )
00162         {
00163             // try FRAIGing
00164             clk = clock();
00165             nInspectLimit = pParams->nTotalInspectLimit? pParams->nTotalInspectLimit - pParams->nTotalInspectsMade : 0;
00166             pNtk = Abc_NtkMiterFraig( pNtkTemp = pNtk, (int)(pParams->nFraigingLimitStart * pow(pParams->nFraigingLimitMulti,nIter)), nInspectLimit, &RetValue, &nSatFails, &nSatConfs, &nSatInspects );  Abc_NtkDelete( pNtkTemp );
00167             Abc_NtkMiterPrint( pNtk, "FRAIGing   ", clk, pParams->fVerbose );
00168 //            printf( "NumFails = %d\n", nSatFails );
00169             if ( RetValue >= 0 )
00170                 break;
00171 
00172             // add to the number of backtracks and inspects
00173             pParams->nTotalBacktracksMade += nSatConfs;
00174             pParams->nTotalInspectsMade += nSatInspects;
00175             // check if global resource limit is reached
00176             if ( (pParams->nTotalBacktrackLimit && pParams->nTotalBacktracksMade >= pParams->nTotalBacktrackLimit) ||
00177                  (pParams->nTotalInspectLimit   && pParams->nTotalInspectsMade   >= pParams->nTotalInspectLimit) )
00178             {
00179                 printf( "Reached global limit on conflicts/inspects. Quitting.\n" );
00180                 *ppNtk = pNtk;
00181                 return -1;
00182             }
00183         }
00184 
00185     }    
00186 
00187     // try to prove it using brute force SAT
00188     if ( RetValue < 0 && pParams->fUseBdds )
00189     {
00190         if ( pParams->fVerbose )
00191         {
00192             printf( "Attempting BDDs with node limit %d ...\n", pParams->nBddSizeLimit );
00193             fflush( stdout );
00194         }
00195         clk = clock();
00196         pNtk = Abc_NtkCollapse( pNtkTemp = pNtk, pParams->nBddSizeLimit, 0, pParams->fBddReorder, 0 );
00197         if ( pNtk )   
00198         {
00199             Abc_NtkDelete( pNtkTemp );
00200             RetValue = ( (Abc_NtkNodeNum(pNtk) == 1) && (Abc_ObjFanin0(Abc_NtkPo(pNtk,0))->pData == Cudd_ReadLogicZero(pNtk->pManFunc)) );
00201         }
00202         else 
00203             pNtk = pNtkTemp;
00204         Abc_NtkMiterPrint( pNtk, "BDD building", clk, pParams->fVerbose );
00205     }
00206 
00207     if ( RetValue < 0 )
00208     {
00209         if ( pParams->fVerbose )
00210         {
00211             printf( "Attempting SAT with conflict limit %d ...\n", pParams->nMiteringLimitLast );
00212             fflush( stdout );
00213         }
00214         clk = clock();
00215         nInspectLimit = pParams->nTotalInspectLimit? pParams->nTotalInspectLimit - pParams->nTotalInspectsMade : 0;
00216         RetValue = Abc_NtkMiterSat( pNtk, (sint64)pParams->nMiteringLimitLast, (sint64)nInspectLimit, 0, NULL, NULL );
00217         Abc_NtkMiterPrint( pNtk, "SAT solving", clk, pParams->fVerbose );
00218     }
00219 
00220     // assign the model if it was proved by rewriting (const 1 miter)
00221     if ( RetValue == 0 && pNtk->pModel == NULL )
00222     {
00223         pNtk->pModel = ALLOC( int, Abc_NtkCiNum(pNtk) );
00224         memset( pNtk->pModel, 0, sizeof(int) * Abc_NtkCiNum(pNtk) );
00225     }
00226     *ppNtk = pNtk;
00227     return RetValue;
00228 }

Abc_Ntk_t* Abc_NtkMiterRwsat ( Abc_Ntk_t *  pNtk  ) 

Function*************************************************************

Synopsis [Implements resynthesis for CEC.]

Description []

SideEffects []

SeeAlso []

Definition at line 328 of file abcProve.c.

00329 {
00330     Abc_Ntk_t * pNtkTemp;
00331     Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 );
00332     pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 );  Abc_NtkDelete( pNtkTemp );
00333     Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 );
00334     Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 );
00335     return pNtk;
00336 }

int Abc_NtkRefactor ( Abc_Ntk_t *  pNtk,
int  nNodeSizeMax,
int  nConeSizeMax,
bool  fUpdateLevel,
bool  fUseZeros,
bool  fUseDcs,
bool  fVerbose 
)

CFile****************************************************************

FileName [abcProve.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Network and node package.]

Synopsis [Proves the miter using AIG rewriting, FRAIGing, and SAT solving.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id
abcProve.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

] DECLARATIONS ///

FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Performs incremental resynthesis of the AIG.]

Description [Starting from each node, computes a reconvergence-driven cut, derives BDD of the cut function, constructs ISOP, factors the ISOP, and replaces the current implementation of the MFFC of the node by the new factored form, if the number of AIG nodes is reduced and the total number of levels of the AIG network is not increated. Returns the number of AIG nodes saved.]

SideEffects []

SeeAlso []

Definition at line 85 of file abcRefactor.c.

00086 {
00087     ProgressBar * pProgress;
00088     Abc_ManRef_t * pManRef;
00089     Abc_ManCut_t * pManCut;
00090     Dec_Graph_t * pFForm;
00091     Vec_Ptr_t * vFanins;
00092     Abc_Obj_t * pNode;
00093     int clk, clkStart = clock();
00094     int i, nNodes;
00095 
00096     assert( Abc_NtkIsStrash(pNtk) );
00097     // cleanup the AIG
00098     Abc_AigCleanup(pNtk->pManFunc);
00099     // start the managers
00100     pManCut = Abc_NtkManCutStart( nNodeSizeMax, nConeSizeMax, 2, 1000 );
00101     pManRef = Abc_NtkManRefStart( nNodeSizeMax, nConeSizeMax, fUseDcs, fVerbose );
00102     pManRef->vLeaves   = Abc_NtkManCutReadCutLarge( pManCut );
00103     // compute the reverse levels if level update is requested
00104     if ( fUpdateLevel )
00105         Abc_NtkStartReverseLevels( pNtk, 0 );
00106 
00107     // resynthesize each node once
00108     pManRef->nNodesBeg = Abc_NtkNodeNum(pNtk);
00109     nNodes = Abc_NtkObjNumMax(pNtk);
00110     pProgress = Extra_ProgressBarStart( stdout, nNodes );
00111     Abc_NtkForEachNode( pNtk, pNode, i )
00112     {
00113         Extra_ProgressBarUpdate( pProgress, i, NULL );
00114         // skip the constant node
00115 //        if ( Abc_NodeIsConst(pNode) )
00116 //            continue;
00117         // skip persistant nodes
00118         if ( Abc_NodeIsPersistant(pNode) )
00119             continue;
00120         // skip the nodes with many fanouts
00121         if ( Abc_ObjFanoutNum(pNode) > 1000 )
00122             continue;
00123         // stop if all nodes have been tried once
00124         if ( i >= nNodes )
00125             break;
00126         // compute a reconvergence-driven cut
00127 clk = clock();
00128         vFanins = Abc_NodeFindCut( pManCut, pNode, fUseDcs );
00129 pManRef->timeCut += clock() - clk;
00130         // evaluate this cut
00131 clk = clock();
00132         pFForm = Abc_NodeRefactor( pManRef, pNode, vFanins, fUpdateLevel, fUseZeros, fUseDcs, fVerbose );
00133 pManRef->timeRes += clock() - clk;
00134         if ( pFForm == NULL )
00135             continue;
00136         // acceptable replacement found, update the graph
00137 clk = clock();
00138         Dec_GraphUpdateNetwork( pNode, pFForm, fUpdateLevel, pManRef->nLastGain );
00139 pManRef->timeNtk += clock() - clk;
00140         Dec_GraphFree( pFForm );
00141 //    {
00142 //        extern int s_TotalChanges;
00143 //        s_TotalChanges++;
00144 //    }
00145     }
00146     Extra_ProgressBarStop( pProgress );
00147 pManRef->timeTotal = clock() - clkStart;
00148     pManRef->nNodesEnd = Abc_NtkNodeNum(pNtk);
00149 
00150     // print statistics of the manager
00151     if ( fVerbose )
00152         Abc_NtkManRefPrintStats( pManRef );
00153     // delete the managers
00154     Abc_NtkManCutStop( pManCut );
00155     Abc_NtkManRefStop( pManRef );
00156     // put the nodes into the DFS order and reassign their IDs
00157     Abc_NtkReassignIds( pNtk );
00158 //    Abc_AigCheckFaninOrder( pNtk->pManFunc );
00159     // fix the levels
00160     if ( fUpdateLevel )
00161         Abc_NtkStopReverseLevels( pNtk );
00162     else
00163         Abc_NtkLevel( pNtk );
00164     // check
00165     if ( !Abc_NtkCheck( pNtk ) )
00166     {
00167         printf( "Abc_NtkRefactor: The network check has failed.\n" );
00168         return 0;
00169     }
00170     return 1;
00171 }

Generated on Tue Jan 5 12:18:39 2010 for abc70930 by  doxygen 1.6.1