summaryrefslogtreecommitdiffstats
path: root/src/base/abci/abcProve.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/base/abci/abcProve.c')
-rw-r--r--src/base/abci/abcProve.c232
1 files changed, 232 insertions, 0 deletions
diff --git a/src/base/abci/abcProve.c b/src/base/abci/abcProve.c
new file mode 100644
index 00000000..18ee9a3f
--- /dev/null
+++ b/src/base/abci/abcProve.c
@@ -0,0 +1,232 @@
+/**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 $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "fraig.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+extern int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerbose );
+extern int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool fUpdateLevel, bool fUseZeros, bool fUseDcs, bool fVerbose );
+extern 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, int * pRetValue );
+static void Abc_NtkMiterPrint( Abc_Ntk_t * pNtk, char * pString, int clk, int fVerbose );
+
+////////////////////////////////////////////////////////////////////////
+/// 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 []
+
+***********************************************************************/
+int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, int nConfLimit, int nImpLimit, int fUseRewrite, int fUseFraig, int fVerbose )
+{
+ Abc_Ntk_t * pNtk, * pNtkTemp;
+ int nConfsStart = 1000, nImpsStart = 0, nBTLimitStart = 2;
+ int nConfs, nImps, nBTLimit, RetValue;
+ int nIter = 0, clk, timeStart = clock();
+
+ // get the starting network
+ pNtk = *ppNtk;
+ assert( Abc_NtkIsStrash(pNtk) );
+ assert( Abc_NtkPoNum(pNtk) == 1 );
+
+ // set the initial limits
+ nConfs = !nConfLimit? nConfsStart : ABC_MIN( nConfsStart, nConfLimit );
+ nImps = !nImpLimit ? nImpsStart : ABC_MIN( nImpsStart , nImpLimit );
+ nBTLimit = nBTLimitStart;
+
+ if ( fVerbose )
+ printf( "Global resource limits: ConfsLim = %6d. ImpsLim = %d.\n", nConfLimit, nImpLimit );
+
+ // if SAT only, solve without iteration
+ if ( !fUseRewrite && !fUseFraig )
+ {
+ clk = clock();
+ RetValue = Abc_NtkMiterSat( pNtk, nConfLimit, nImpLimit, 0 );
+ Abc_NtkMiterPrint( pNtk, "SAT solving", clk, fVerbose );
+ *ppNtk = pNtk;
+ return RetValue;
+ }
+
+ // check the current resource limits
+ do {
+ nIter++;
+
+ if ( fVerbose )
+ printf( "ITERATION %2d : Confs = %6d. FraigBTL = %3d. \n", nIter, nConfs, nBTLimit );
+
+ // try brute-force SAT
+ clk = clock();
+ RetValue = Abc_NtkMiterSat( pNtk, nConfs, nImps, 0 );
+ Abc_NtkMiterPrint( pNtk, "SAT solving", clk, fVerbose );
+ if ( RetValue >= 0 )
+ break;
+
+ if ( fUseRewrite )
+ {
+ clk = clock();
+
+ // try rewriting
+ Abc_NtkRewrite( pNtk, 0, 0, 0 );
+ if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 )
+ break;
+ Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 );
+ if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 )
+ break;
+ pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 ); Abc_NtkDelete( pNtkTemp );
+ if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 )
+ break;
+
+ Abc_NtkMiterPrint( pNtk, "Rewriting ", clk, fVerbose );
+ }
+
+ if ( fUseFraig )
+ {
+ // try FRAIGing
+ clk = clock();
+ pNtk = Abc_NtkMiterFraig( pNtkTemp = pNtk, nBTLimit, &RetValue ); Abc_NtkDelete( pNtkTemp );
+ Abc_NtkMiterPrint( pNtk, "FRAIGing ", clk, fVerbose );
+ if ( RetValue >= 0 )
+ break;
+ }
+
+ // increase resource limits
+ nConfs = ABC_MIN( nConfs * 3 / 2, 1000000000 );
+ nImps = ABC_MIN( nImps * 3 / 2, 1000000000 );
+ nBTLimit = ABC_MIN( nBTLimit * 8, 1000000000 );
+
+ // timeout at 5 minutes
+ if ( clock() - timeStart >= 300 * CLOCKS_PER_SEC )
+ break;
+ if ( nIter == 4 )
+ break;
+ }
+ while ( (nConfLimit == 0 || nConfs <= nConfLimit) &&
+ (nImpLimit == 0 || nImps <= nImpLimit ) );
+
+ // try to prove it using brute force SAT
+ if ( RetValue < 0 )
+ {
+ clk = clock();
+ RetValue = Abc_NtkMiterSat( pNtk, nConfLimit, nImpLimit, 0 );
+ Abc_NtkMiterPrint( pNtk, "SAT solving", clk, fVerbose );
+ }
+
+ *ppNtk = pNtk;
+ return RetValue;
+}
+
+/**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 []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkMiterFraig( Abc_Ntk_t * pNtk, int nBTLimit, int * pRetValue )
+{
+ Abc_Ntk_t * pNtkNew;
+ Fraig_Params_t Params, * pParams = &Params;
+ Fraig_Man_t * pMan;
+ int nWords1, nWords2, nWordsMin, RetValue;
+ int * pModel;
+
+ // to determine the number of simulation patterns
+ // use the following strategy
+ // at least 64 words (32 words random and 32 words dynamic)
+ // no more than 256M for one circuit (128M + 128M)
+ nWords1 = 32;
+ nWords2 = (1<<27) / (Abc_NtkNodeNum(pNtk) + Abc_NtkCiNum(pNtk));
+ nWordsMin = ABC_MIN( nWords1, nWords2 );
+
+ // set the FRAIGing parameters
+ Fraig_ParamsSetDefault( pParams );
+ pParams->nPatsRand = nWordsMin * 32; // the number of words of random simulation info
+ pParams->nPatsDyna = nWordsMin * 32; // the number of words of dynamic simulation info
+ pParams->nBTLimit = nBTLimit; // the max number of backtracks
+ pParams->nSeconds = -1; // the runtime limit
+ pParams->fTryProve = 0; // do not try to prove the final miter
+ pParams->fDoSparse = 1; // try proving sparse functions
+ pParams->fVerbose = 0;
+
+ // transform the target into a fraig
+ pMan = Abc_NtkToFraig( pNtk, pParams, 0, 0 );
+ Fraig_ManProveMiter( pMan );
+ RetValue = Fraig_ManCheckMiter( pMan );
+
+ // save model
+ if ( RetValue == 0 )
+ {
+ pModel = Fraig_ManReadModel( pMan );
+ FREE( pNtk->pModel );
+ pNtk->pModel = ALLOC( int, Abc_NtkCiNum(pNtk) );
+ memcpy( pNtk->pModel, pModel, sizeof(int) * Abc_NtkCiNum(pNtk) );
+ }
+ // create the network
+ pNtkNew = Abc_NtkFromFraig( pMan, pNtk );
+ // delete the fraig manager
+ Fraig_ManFree( pMan );
+ *pRetValue = RetValue;
+ return pNtkNew;
+}
+
+/**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 []
+
+***********************************************************************/
+void Abc_NtkMiterPrint( Abc_Ntk_t * pNtk, char * pString, int clk, int fVerbose )
+{
+ if ( !fVerbose )
+ return;
+ printf( "Nodes = %7d. Levels = %4d. ", Abc_NtkNodeNum(pNtk), Abc_AigGetLevelNum(pNtk) );
+ PRT( pString, clock() - clk );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-06-30 18:52:12 +0000