diff options
Diffstat (limited to 'src/proof/fra/fra.h')
| -rw-r--r-- | src/proof/fra/fra.h | 389 |
1 files changed, 389 insertions, 0 deletions
diff --git a/src/proof/fra/fra.h b/src/proof/fra/fra.h new file mode 100644 index 00000000..3e50ff57 --- /dev/null +++ b/src/proof/fra/fra.h @@ -0,0 +1,389 @@ +/**CFile**************************************************************** + + FileName [fra.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [[New FRAIG package.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 30, 2007.] + + Revision [$Id: fra.h,v 1.00 2007/06/30 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef ABC__aig__fra__fra_h +#define ABC__aig__fra__fra_h + + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +#include <stdio.h> +#include <stdlib.h> +#include <string.h> +#include <assert.h> +#include <time.h> + +#include "src/misc/vec/vec.h" +#include "src/aig/aig/aig.h" +#include "src/opt/dar/dar.h" +#include "src/sat/bsat/satSolver.h" +#include "src/aig/ioa/ioa.h" + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + + + +ABC_NAMESPACE_HEADER_START + + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Fra_Par_t_ Fra_Par_t; +typedef struct Fra_Ssw_t_ Fra_Ssw_t; +typedef struct Fra_Sec_t_ Fra_Sec_t; +typedef struct Fra_Man_t_ Fra_Man_t; +typedef struct Fra_Cla_t_ Fra_Cla_t; +typedef struct Fra_Sml_t_ Fra_Sml_t; +typedef struct Fra_Bmc_t_ Fra_Bmc_t; + +// FRAIG parameters +struct Fra_Par_t_ +{ + int nSimWords; // the number of words in the simulation info + double dSimSatur; // the ratio of refined classes when saturation is reached + int fPatScores; // enables simulation pattern scoring + int MaxScore; // max score after which resimulation is used + double dActConeRatio; // the ratio of cone to be bumped + double dActConeBumpMax; // the largest bump in activity + int fChoicing; // enables choicing + int fSpeculate; // use speculative reduction + int fProve; // prove the miter outputs + int fVerbose; // verbose output + int fDoSparse; // skip sparse functions + int fConeBias; // bias variables in the cone (good for unsat runs) + int nBTLimitNode; // conflict limit at a node + int nBTLimitMiter; // conflict limit at an output + int nLevelMax; // the max level to consider seriously + int nFramesP; // the number of timeframes to in the prefix + int nFramesK; // the number of timeframes to unroll + int nMaxImps; // the maximum number of implications to consider + int nMaxLevs; // the maximum number of levels to consider + int fRewrite; // use rewriting for constraint reduction + int fLatchCorr; // computes latch correspondence only + int fUseImps; // use implications + int fUse1Hot; // use one-hotness conditions + int fWriteImps; // record implications + int fDontShowBar; // does not show progressbar during fraiging +}; + +// seq SAT sweeping parameters +struct Fra_Ssw_t_ +{ + int nPartSize; // size of the partition + int nOverSize; // size of the overlap between partitions + int nFramesP; // number of frames in the prefix + int nFramesK; // number of frames for induction (1=simple) + int nMaxImps; // max implications to consider + int nMaxLevs; // max levels to consider + int nMinDomSize; // min clock domain considered for optimization + int fUseImps; // use implications + int fRewrite; // enable rewriting of the specualatively reduced model + int fFraiging; // enable comb SAT sweeping as preprocessing + int fLatchCorr; // perform register correspondence + int fWriteImps; // write implications into a file + int fUse1Hot; // use one-hotness constraints + int fVerbose; // enable verbose output + int fSilent; // disable any output + int nIters; // the number of iterations performed + float TimeLimit; // the runtime budget for this call +}; + +// SEC parametesr +struct Fra_Sec_t_ +{ + int fTryComb; // try CEC call as a preprocessing step + int fTryBmc; // try BMC call as a preprocessing step + int nFramesMax; // the max number of frames used for induction + int nBTLimit; // the conflict limit at a node + int nBTLimitGlobal; // the global conflict limit + int nBTLimitInter; // the conflict limit for interpolation + int nBddVarsMax; // the state space limit for BDD reachability + int nBddMax; // the max number of BDD nodes + int nBddIterMax; // the limit on the number of BDD iterations + int nPdrTimeout; // the timeout for PDR in the end + int fPhaseAbstract; // enables phase abstraction + int fRetimeFirst; // enables most-forward retiming at the beginning + int fRetimeRegs; // enables min-register retiming at the beginning + int fFraiging; // enables fraiging at the beginning + int fInduction; // enable the use of induction + int fInterpolation; // enables interpolation + int fInterSeparate; // enables interpolation for each outputs separately + int fReachability; // enables BDD based reachability + int fReorderImage; // enables BDD reordering during image computation + int fStopOnFirstFail; // enables stopping after first output of a miter has failed to prove + int fUseNewProver; // the new prover + int fUsePdr; // the PDR + int fSilent; // disables all output + int fVerbose; // enables verbose reporting of statistics + int fVeryVerbose; // enables very verbose reporting + int TimeLimit; // enables the timeout + int fReadUnsolved; // inserts the unsolved model back + int nSMnumber; // the number of model written + // internal parameters + int fRecursive; // set to 1 when SEC is called recursively + int fReportSolution; // enables report solution in a special form +}; + +// FRAIG equivalence classes +struct Fra_Cla_t_ +{ + Aig_Man_t * pAig; // the original AIG manager + Aig_Obj_t ** pMemRepr; // pointers to representatives of each node + Vec_Ptr_t * vClasses; // equivalence classes + Vec_Ptr_t * vClasses1; // equivalence class of Const1 node + Vec_Ptr_t * vClassesTemp; // temporary storage for new classes + Aig_Obj_t ** pMemClasses; // memory allocated for equivalence classes + Aig_Obj_t ** pMemClassesFree; // memory allocated for equivalence classes to be used + Vec_Ptr_t * vClassOld; // old equivalence class after splitting + Vec_Ptr_t * vClassNew; // new equivalence class(es) after splitting + int nPairs; // the number of pairs of nodes + int fRefinement; // set to 1 when refinement has happened + Vec_Int_t * vImps; // implications + // procedures used for class refinement + int (*pFuncNodeHash) (Aig_Obj_t *, int); // returns has key of the node + int (*pFuncNodeIsConst) (Aig_Obj_t *); // returns 1 if the node is a constant + int (*pFuncNodesAreEqual)(Aig_Obj_t *, Aig_Obj_t *); // returns 1 if nodes are equal up to a complement +}; + +// simulation manager +struct Fra_Sml_t_ +{ + Aig_Man_t * pAig; // the original AIG manager + int nPref; // the number of times frames in the prefix + int nFrames; // the number of times frames + int nWordsFrame; // the number of words in each time frame + int nWordsTotal; // the total number of words at a node + int nWordsPref; // the number of word in the prefix + int fNonConstOut; // have seen a non-const-0 output during simulation + int nSimRounds; // statistics + int timeSim; // statistics + unsigned pData[0]; // simulation data for the nodes +}; + +// FRAIG manager +struct Fra_Man_t_ +{ + // high-level data + Fra_Par_t * pPars; // parameters governing fraiging + // AIG managers + Aig_Man_t * pManAig; // the starting AIG manager + Aig_Man_t * pManFraig; // the final AIG manager + // mapping AIG into FRAIG + int nFramesAll; // the number of timeframes used + Aig_Obj_t ** pMemFraig; // memory allocated for points to the fraig nodes + int nSizeAlloc; // allocated size of the arrays for timeframe nodes + // equivalence classes + Fra_Cla_t * pCla; // representation of (candidate) equivalent nodes + // simulation info + Fra_Sml_t * pSml; // simulation manager + // bounded model checking manager + Fra_Bmc_t * pBmc; + // counter example storage + int nPatWords; // the number of words in the counter example + unsigned * pPatWords; // the counter example + Vec_Int_t * vCex; + // one-hotness conditions + Vec_Int_t * vOneHots; + // satisfiability solving + sat_solver * pSat; // SAT solver + int nSatVars; // the number of variables currently used + Vec_Ptr_t * vPiVars; // the PIs of the cone used + ABC_INT64_T nBTLimitGlobal; // resource limit + ABC_INT64_T nInsLimitGlobal; // resource limit + Vec_Ptr_t ** pMemFanins; // the arrays of fanins for some FRAIG nodes + int * pMemSatNums; // the array of SAT numbers for some FRAIG nodes + int nMemAlloc; // allocated size of the arrays for FRAIG varnums and fanins + Vec_Ptr_t * vTimeouts; // the nodes, for which equivalence checking timed out + // statistics + int nSimRounds; + int nNodesMiter; + int nLitsBeg; + int nLitsEnd; + int nNodesBeg; + int nNodesEnd; + int nRegsBeg; + int nRegsEnd; + int nSatCalls; + int nSatCallsSat; + int nSatCallsUnsat; + int nSatProof; + int nSatFails; + int nSatFailsReal; + int nSpeculs; + int nChoices; + int nChoicesFake; + int nSatCallsRecent; + int nSatCallsSkipped; + // runtime + int timeSim; + int timeTrav; + int timeRwr; + int timeSat; + int timeSatUnsat; + int timeSatSat; + int timeSatFail; + int timeRef; + int timeTotal; + int time1; + int time2; +}; + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +static inline unsigned * Fra_ObjSim( Fra_Sml_t * p, int Id ) { return p->pData + p->nWordsTotal * Id; } +static inline unsigned Fra_ObjRandomSim() { return Aig_ManRandom(0); } + +static inline Aig_Obj_t * Fra_ObjFraig( Aig_Obj_t * pObj, int i ) { return ((Fra_Man_t *)pObj->pData)->pMemFraig[((Fra_Man_t *)pObj->pData)->nFramesAll*pObj->Id + i]; } +static inline void Fra_ObjSetFraig( Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pMemFraig[((Fra_Man_t *)pObj->pData)->nFramesAll*pObj->Id + i] = pNode; } + +static inline Vec_Ptr_t * Fra_ObjFaninVec( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id]; } +static inline void Fra_ObjSetFaninVec( Aig_Obj_t * pObj, Vec_Ptr_t * vFanins ) { ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id] = vFanins; } + +static inline int Fra_ObjSatNum( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id]; } +static inline void Fra_ObjSetSatNum( Aig_Obj_t * pObj, int Num ) { ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id] = Num; } + +static inline Aig_Obj_t * Fra_ClassObjRepr( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pCla->pMemRepr[pObj->Id]; } +static inline void Fra_ClassObjSetRepr( Aig_Obj_t * pObj, Aig_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pCla->pMemRepr[pObj->Id] = pNode; } + +static inline Aig_Obj_t * Fra_ObjChild0Fra( Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Fra_ObjFraig(Aig_ObjFanin0(pObj),i), Aig_ObjFaninC0(pObj)) : NULL; } +static inline Aig_Obj_t * Fra_ObjChild1Fra( Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Fra_ObjFraig(Aig_ObjFanin1(pObj),i), Aig_ObjFaninC1(pObj)) : NULL; } + +static inline int Fra_ImpLeft( int Imp ) { return Imp & 0xFFFF; } +static inline int Fra_ImpRight( int Imp ) { return Imp >> 16; } +static inline int Fra_ImpCreate( int Left, int Right ) { return (Right << 16) | Left; } + +//////////////////////////////////////////////////////////////////////// +/// ITERATORS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== fraCec.c ========================================================*/ +extern int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose ); +extern int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose ); +extern int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int nPartSize, int fSmart, int fVerbose ); +/*=== fraClass.c ========================================================*/ +extern int Fra_BmcNodeIsConst( Aig_Obj_t * pObj ); +extern int Fra_BmcNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ); +extern void Fra_BmcStop( Fra_Bmc_t * p ); +extern void Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth ); +extern void Fra_BmcPerformSimple( Aig_Man_t * pAig, int nFrames, int nBTLimit, int fRewrite, int fVerbose ); +/*=== fraClass.c ========================================================*/ +extern Fra_Cla_t * Fra_ClassesStart( Aig_Man_t * pAig ); +extern void Fra_ClassesStop( Fra_Cla_t * p ); +extern void Fra_ClassesCopyReprs( Fra_Cla_t * p, Vec_Ptr_t * vFailed ); +extern void Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose ); +extern void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr, int nMaxLevs ); +extern int Fra_ClassesRefine( Fra_Cla_t * p ); +extern int Fra_ClassesRefine1( Fra_Cla_t * p, int fRefineNewClass, int * pSkipped ); +extern int Fra_ClassesCountLits( Fra_Cla_t * p ); +extern int Fra_ClassesCountPairs( Fra_Cla_t * p ); +extern void Fra_ClassesTest( Fra_Cla_t * p, int Id1, int Id2 ); +extern void Fra_ClassesLatchCorr( Fra_Man_t * p ); +extern void Fra_ClassesPostprocess( Fra_Cla_t * p ); +extern void Fra_ClassesSelectRepr( Fra_Cla_t * p ); +extern Aig_Man_t * Fra_ClassesDeriveAig( Fra_Cla_t * p, int nFramesK ); +/*=== fraCnf.c ========================================================*/ +extern void Fra_CnfNodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ); +/*=== fraCore.c ========================================================*/ +extern void Fra_FraigSweep( Fra_Man_t * pManAig ); +extern int Fra_FraigMiterStatus( Aig_Man_t * p ); +extern int Fra_FraigMiterAssertedOutput( Aig_Man_t * p ); +extern Aig_Man_t * Fra_FraigPerform( Aig_Man_t * pManAig, Fra_Par_t * pPars ); +extern Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax, int nLevelMax ); +extern Aig_Man_t * Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax, int fProve ); +/*=== fraHot.c ========================================================*/ +extern Vec_Int_t * Fra_OneHotCompute( Fra_Man_t * p, Fra_Sml_t * pSim ); +extern void Fra_OneHotAssume( Fra_Man_t * p, Vec_Int_t * vOneHots ); +extern void Fra_OneHotCheck( Fra_Man_t * p, Vec_Int_t * vOneHots ); +extern int Fra_OneHotRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vOneHots ); +extern int Fra_OneHotCount( Fra_Man_t * p, Vec_Int_t * vOneHots ); +extern void Fra_OneHotEstimateCoverage( Fra_Man_t * p, Vec_Int_t * vOneHots ); +extern Aig_Man_t * Fra_OneHotCreateExdc( Fra_Man_t * p, Vec_Int_t * vOneHots ); +extern void Fra_OneHotAddKnownConstraint( Fra_Man_t * p, Vec_Ptr_t * vOnehots ); +/*=== fraImp.c ========================================================*/ +extern Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, int fLatchCorr ); +extern void Fra_ImpAddToSolver( Fra_Man_t * p, Vec_Int_t * vImps, int * pSatVarNums ); +extern int Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps, Aig_Obj_t * pNode, int Pos ); +extern int Fra_ImpRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vImps ); +extern void Fra_ImpCompactArray( Vec_Int_t * vImps ); +extern double Fra_ImpComputeStateSpaceRatio( Fra_Man_t * p ); +extern int Fra_ImpVerifyUsingSimulation( Fra_Man_t * p ); +extern void Fra_ImpRecordInManager( Fra_Man_t * p, Aig_Man_t * pNew ); +/*=== fraInd.c ========================================================*/ +extern Aig_Man_t * Fra_FraigInduction( Aig_Man_t * p, Fra_Ssw_t * pPars ); +/*=== fraIndVer.c =====================================================*/ +extern int Fra_InvariantVerify( Aig_Man_t * p, int nFrames, Vec_Int_t * vClauses, Vec_Int_t * vLits ); +/*=== fraLcr.c ========================================================*/ +extern Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fProve, int fVerbose, int * pnIter, float TimeLimit ); +/*=== fraMan.c ========================================================*/ +extern void Fra_ParamsDefault( Fra_Par_t * pParams ); +extern void Fra_ParamsDefaultSeq( Fra_Par_t * pParams ); +extern Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pParams ); +extern void Fra_ManClean( Fra_Man_t * p, int nNodesMax ); +extern Aig_Man_t * Fra_ManPrepareComb( Fra_Man_t * p ); +extern void Fra_ManFinalizeComb( Fra_Man_t * p ); +extern void Fra_ManStop( Fra_Man_t * p ); +extern void Fra_ManPrint( Fra_Man_t * p ); +/*=== fraSat.c ========================================================*/ +extern int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ); +extern int Fra_NodesAreImp( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fComplL, int fComplR ); +extern int Fra_NodesAreClause( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fComplL, int fComplR ); +extern int Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew ); +/*=== fraSec.c ========================================================*/ +extern void Fra_SecSetDefaultParams( Fra_Sec_t * p ); +extern int Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pParSec, Aig_Man_t ** ppResult ); +/*=== fraSim.c ========================================================*/ +extern int Fra_SmlNodeHash( Aig_Obj_t * pObj, int nTableSize ); +extern int Fra_SmlNodeIsConst( Aig_Obj_t * pObj ); +extern int Fra_SmlNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ); +extern int Fra_SmlNodeNotEquWeight( Fra_Sml_t * p, int Left, int Right ); +extern int Fra_SmlNodeCountOnes( Fra_Sml_t * p, Aig_Obj_t * pObj ); +extern int Fra_SmlCheckOutput( Fra_Man_t * p ); +extern void Fra_SmlSavePattern( Fra_Man_t * p ); +extern void Fra_SmlSimulate( Fra_Man_t * p, int fInit ); +extern void Fra_SmlResimulate( Fra_Man_t * p ); +extern Fra_Sml_t * Fra_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFrame ); +extern void Fra_SmlStop( Fra_Sml_t * p ); +extern Fra_Sml_t * Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords, int fCheckMiter ); +extern Fra_Sml_t * Fra_SmlSimulateComb( Aig_Man_t * pAig, int nWords ); +extern Abc_Cex_t * Fra_SmlGetCounterExample( Fra_Sml_t * p ); +extern Abc_Cex_t * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel ); + +ABC_NAMESPACE_HEADER_END + + + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + |