diff options
Diffstat (limited to 'src/aig/saig')
-rw-r--r-- | src/aig/saig/module.make | 3 | ||||
-rw-r--r-- | src/aig/saig/saig.h | 6 | ||||
-rw-r--r-- | src/aig/saig/saigBmc.c | 201 | ||||
-rw-r--r-- | src/aig/saig/saigCone.c | 176 | ||||
-rw-r--r-- | src/aig/saig/saigInter.c | 40 |
5 files changed, 406 insertions, 20 deletions
diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make index 20428b36..68c49133 100644 --- a/src/aig/saig/module.make +++ b/src/aig/saig/module.make @@ -1,4 +1,5 @@ -SRC += src/aig/saig/saig_.c \ +SRC += src/aig/saig/saigBmc.c \ + src/aig/saig/saigCone.c \ src/aig/saig/saigInter.c \ src/aig/saig/saigPhase.c \ src/aig/saig/saigRetFwd.c \ diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index 60db874b..f0eb7099 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -75,8 +75,12 @@ static inline int Saig_ObjIsLi( Aig_Man_t * p, Aig_Obj_t * pObj ) { /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +/*=== saigBmc.c ==========================================================*/ +extern int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nBTLimit, int fRewrite, int fVerbose, int * piFrame ); +/*=== saigCone.c ==========================================================*/ +extern void Saig_ManPrintCones( Aig_Man_t * p ); /*=== saigInter.c ==========================================================*/ -extern int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int fVerbose, int * pDepth ); +extern int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int fRewrite, int fTransLoop, int fVerbose, int * pDepth ); /*=== saigPhase.c ==========================================================*/ extern Aig_Man_t * Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrames, int fIgnore, int fPrint, int fVerbose ); /*=== saigRetFwd.c ==========================================================*/ diff --git a/src/aig/saig/saigBmc.c b/src/aig/saig/saigBmc.c new file mode 100644 index 00000000..3a6aa611 --- /dev/null +++ b/src/aig/saig/saigBmc.c @@ -0,0 +1,201 @@ +/**CFile**************************************************************** + + FileName [saigBmc.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Sequential AIG package.] + + Synopsis [Simple BMC package.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: saigBmc.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "saig.h" +#include "cnf.h" +#include "satStore.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Create timeframes of the manager for BMC.] + + Description [The resulting manager is combinational. The primary inputs + corresponding to register outputs are ordered first. POs correspond to \ + the property outputs in each time-frame.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Saig_ManFramesBmc( Aig_Man_t * pAig, int nFrames ) +{ + Aig_Man_t * pFrames; + Aig_Obj_t * pObj, * pObjLi, * pObjLo; + int i, f; + assert( Saig_ManRegNum(pAig) > 0 ); + pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFrames ); + // map the constant node + Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames ); + // create variables for register outputs + Saig_ManForEachLo( pAig, pObj, i ) + pObj->pData = Aig_ManConst0( pFrames ); + // add timeframes + for ( f = 0; f < nFrames; f++ ) + { + // create PI nodes for this frame + Saig_ManForEachPi( pAig, pObj, i ) + pObj->pData = Aig_ObjCreatePi( pFrames ); + // add internal nodes of this frame + Aig_ManForEachNode( pAig, pObj, i ) + pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + // create POs for this frame + Saig_ManForEachPo( pAig, pObj, i ) + Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) ); + if ( f == nFrames - 1 ) + break; + // save register inputs + Saig_ManForEachLi( pAig, pObj, i ) + pObj->pData = Aig_ObjChild0Copy(pObj); + // transfer to register outputs + Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i ) + pObjLo->pData = pObjLi->pData; + } + Aig_ManCleanup( pFrames ); + return pFrames; +} + +/**Function************************************************************* + + Synopsis [Performs BMC for the given AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nConfLimit, int fRewrite, int fVerbose, int * piFrame ) +{ + sat_solver * pSat; + Cnf_Dat_t * pCnf; + Aig_Man_t * pFrames, * pAigTemp; + Aig_Obj_t * pObj; + int status, clk, Lit, i, RetValue = 1; + *piFrame = -1; + // derive the timeframes + clk = clock(); + pFrames = Saig_ManFramesBmc( pAig, nFrames ); + if ( fVerbose ) + { + printf( "AIG: PI/PO/Reg = %d/%d/%d. Node = %6d. Lev = %5d.\n", + Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), Saig_ManRegNum(pAig), + Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) ); + printf( "Time-frames (%d): PI/PO = %d/%d. Node = %6d. Lev = %5d. ", + nFrames, Aig_ManPiNum(pFrames), Aig_ManPoNum(pFrames), + Aig_ManNodeNum(pFrames), Aig_ManLevelNum(pFrames) ); + PRT( "Time", clock() - clk ); + } + // rewrite the timeframes + if ( fRewrite ) + { + clk = clock(); +// pFrames = Dar_ManBalance( pAigTemp = pFrames, 0 ); + pFrames = Dar_ManRwsat( pAigTemp = pFrames, 1, 0 ); + Aig_ManStop( pAigTemp ); + if ( fVerbose ) + { + printf( "Time-frames after rewriting: Node = %6d. Lev = %5d. ", + Aig_ManNodeNum(pFrames), Aig_ManLevelNum(pFrames) ); + PRT( "Time", clock() - clk ); + } + } + // create the SAT solver + clk = clock(); + pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) ); + pSat = sat_solver_new(); + sat_solver_setnvars( pSat, pCnf->nVars ); + for ( i = 0; i < pCnf->nClauses; i++ ) + { + if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) ) + assert( 0 ); + } + if ( fVerbose ) + { + printf( "CNF: Variables = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals ); + PRT( "Time", clock() - clk ); + } + status = sat_solver_simplify(pSat); + if ( status == 0 ) + { + if ( fVerbose ) + printf( "The BMC problem is trivially UNSAT\n" ); + } + else + { + Aig_ManForEachPo( pFrames, pObj, i ) + { + Lit = toLitCond( pCnf->pVarNums[pObj->Id], 0 ); + if ( fVerbose ) + printf( "Solving output %2d of frame %3d ... \r", + i % Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) ); + clk = clock(); + status = sat_solver_solve( pSat, &Lit, &Lit + 1, (sint64)nConfLimit, (sint64)0, (sint64)0, (sint64)0 ); + if ( fVerbose ) + { + printf( "Solved output %2d of frame %3d. ", + i % Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) ); + printf( "Conf =%8.0f. Imp =%11.0f. ", (double)pSat->stats.conflicts, (double)pSat->stats.propagations ); + PRT( "Time", clock() - clk ); + } + if ( status == l_False ) + { + } + else if ( status == l_True ) + { + extern void * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel ); + Vec_Int_t * vCiIds = Cnf_DataCollectPiSatNums( pCnf, pFrames ); + int * pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize ); + pModel[Aig_ManPiNum(pFrames)] = pObj->Id; + pAig->pSeqModel = Fra_SmlCopyCounterExample( pAig, pFrames, pModel ); + free( pModel ); + Vec_IntFree( vCiIds ); + + RetValue = 0; + break; + } + else + { + *piFrame = i; + RetValue = -1; + break; + } + } + } + sat_solver_delete( pSat ); + Cnf_DataFree( pCnf ); + Aig_ManStop( pFrames ); + return RetValue; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/saig/saigCone.c b/src/aig/saig/saigCone.c new file mode 100644 index 00000000..7ca077c8 --- /dev/null +++ b/src/aig/saig/saigCone.c @@ -0,0 +1,176 @@ +/**CFile**************************************************************** + + FileName [saigCone.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Sequential AIG package.] + + Synopsis [Cone of influence computation.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: saigCone.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "saig.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Counts the support size of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Saig_ManSupport_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vSupp ) +{ + if ( Aig_ObjIsTravIdCurrent(p, pObj) ) + return; + Aig_ObjSetTravIdCurrent(p, pObj); + if ( Aig_ObjIsConst1(pObj) ) + return; + if ( Aig_ObjIsPi(pObj) ) + { + if ( Saig_ObjIsLo(p,pObj) ) + { + pObj = Saig_ManLi( p, Aig_ObjPioNum(pObj)-Saig_ManPiNum(p) ); + Vec_PtrPush( vSupp, pObj ); + } + return; + } + assert( Aig_ObjIsNode(pObj) ); + Saig_ManSupport_rec( p, Aig_ObjFanin0(pObj), vSupp ); + Saig_ManSupport_rec( p, Aig_ObjFanin1(pObj), vSupp ); +} + +/**Function************************************************************* + + Synopsis [Counts the support size of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Saig_ManSupport( Aig_Man_t * p, Vec_Ptr_t * vNodes ) +{ + Vec_Ptr_t * vSupp; + Aig_Obj_t * pObj; + int i; + vSupp = Vec_PtrAlloc( 100 ); + Aig_ManIncrementTravId( p ); + Vec_PtrForEachEntry( vNodes, pObj, i ) + { + assert( Aig_ObjIsPo(pObj) ); + Saig_ManSupport_rec( p, Aig_ObjFanin0(pObj), vSupp ); + } + return vSupp; +} + +/**Function************************************************************* + + Synopsis [Prints information about cones of influence of the POs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Saig_ManPrintConeOne( Aig_Man_t * p, Aig_Obj_t * pObj ) +{ + Vec_Ptr_t * vPrev, * vCur, * vTotal; + int s, i, nCurNew, nCurPrev, nCurOld; + assert( Saig_ObjIsPo(p, pObj) ); + // start the array + vPrev = Vec_PtrAlloc( 100 ); + Vec_PtrPush( vPrev, pObj ); + // get the current support + vCur = Saig_ManSupport( p, vPrev ); + Vec_PtrClear( vPrev ); + printf( " PO %3d ", Aig_ObjPioNum(pObj) ); + // continue computing supports as long as there are now nodes + vTotal = Vec_PtrAlloc( 100 ); + for ( s = 0; ; s++ ) + { + // classify current into those new, prev, and older + nCurNew = nCurPrev = nCurOld = 0; + Vec_PtrForEachEntry( vCur, pObj, i ) + { + if ( Vec_PtrFind(vTotal, pObj) == -1 ) + { + Vec_PtrPush( vTotal, pObj ); + nCurNew++; + } + else if ( Vec_PtrFind(vPrev, pObj) >= 0 ) + nCurPrev++; + else + nCurOld++; + } + assert( nCurNew + nCurPrev + nCurOld == Vec_PtrSize(vCur) ); + // print the result + printf( "%d:%d %d=%d+%d+%d ", s, Vec_PtrSize(vTotal), Vec_PtrSize(vCur), nCurNew, nCurPrev, nCurOld ); + if ( nCurNew == 0 ) + break; + // compute one more step + Vec_PtrFree( vPrev ); + vCur = Saig_ManSupport( p, vPrev = vCur ); + } + printf( "\n" ); + Vec_PtrFree( vPrev ); + Vec_PtrFree( vCur ); + Vec_PtrFree( vTotal ); +} + +/**Function************************************************************* + + Synopsis [Prints information about cones of influence of the POs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Saig_ManPrintCones( Aig_Man_t * p ) +{ + Aig_Obj_t * pObj; + int i; + printf( "The format of this print-out: For each PO, x:a b=c+d+e, where \n" ); + printf( "- x is the time-frame counting back from the PO\n" ); + printf( "- a is the total number of registers in the COI of the PO so far\n" ); + printf( "- b is the number of registers in the COI of the PO in this time-frame\n" ); + printf( "- c is the number of registers in b that are new (appear for the first time)\n" ); + printf( "- d is the number of registers in b in common with the previous time-frame\n" ); + printf( "- e is the number of registers in b in common with other time-frames\n" ); + Aig_ManSetPioNumbers( p ); + Saig_ManForEachPo( p, pObj, i ) + Saig_ManPrintConeOne( p, pObj ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/saig/saigInter.c b/src/aig/saig/saigInter.c index 34069b03..ffd32206 100644 --- a/src/aig/saig/saigInter.c +++ b/src/aig/saig/saigInter.c @@ -23,15 +23,14 @@ #include "cnf.h" #include "satStore.h" -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - /* The interpolation algorithm implemented here was introduced in the paper: K. L. McMillan. Interpolation and SAT-based model checking. CAV’03, pp. 1-13. */ +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// // simulation manager typedef struct Saig_IntMan_t_ Saig_IntMan_t; @@ -203,8 +202,8 @@ Aig_Man_t * Saig_ManFramesInter( Aig_Man_t * pAig, int nFrames ) Aig_Man_t * pFrames; Aig_Obj_t * pObj, * pObjLi, * pObjLo; int i, f; + assert( Saig_ManRegNum(pAig) > 0 ); assert( Saig_ManPoNum(pAig) == 1 ); - // start the fraig package pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFrames ); // map the constant node Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames ); @@ -265,7 +264,7 @@ sat_solver * Saig_DeriveSatSolver( assert( Aig_ManPoNum(pInter) == 1 ); assert( Aig_ManPoNum(pFrames) == 1 ); assert( Aig_ManPiNum(pInter) == Aig_ManRegNum(pAig) ); - assert( (Aig_ManPiNum(pFrames) - Aig_ManRegNum(pAig)) % Saig_ManPiNum(pAig) == 0 ); +// assert( (Aig_ManPiNum(pFrames) - Aig_ManRegNum(pAig)) % Saig_ManPiNum(pAig) == 0 ); // prepare CNFs Cnf_DataLift( pCnfAig, pCnfFrames->nVars ); @@ -354,7 +353,7 @@ int Saig_PerformOneStep( Saig_IntMan_t * p ) // derive the SAT solver pSat = Saig_DeriveSatSolver( p->pInter, p->pCnfInter, p->pAigTrans, p->pCnfAig, p->pFrames, p->pCnfFrames, p->vVarsAB ); -Sat_SolverWriteDimacs( pSat, "test.cnf", NULL, NULL, 1 ); +//Sat_SolverWriteDimacs( pSat, "test.cnf", NULL, NULL, 1 ); // solve the problem clk = clock(); status = sat_solver_solve( pSat, NULL, NULL, (sint64)p->nConfLimit, (sint64)0, (sint64)0, (sint64)0 ); @@ -403,14 +402,15 @@ int Saig_ManCheckContainment( Aig_Man_t * pNew, Aig_Man_t * pOld ) Aig_Man_t * pMiter, * pAigTemp; int RetValue; pMiter = Aig_ManCreateMiter( pNew, pOld, 1 ); - pMiter = Dar_ManRwsat( pAigTemp = pMiter, 1, 0 ); - Aig_ManStop( pAigTemp ); +// pMiter = Dar_ManRwsat( pAigTemp = pMiter, 1, 0 ); +// Aig_ManStop( pAigTemp ); RetValue = Fra_FraigMiterStatus( pMiter ); if ( RetValue == -1 ) { pAigTemp = Fra_FraigEquivence( pMiter, 1000000, 1 ); RetValue = Fra_FraigMiterStatus( pAigTemp ); Aig_ManStop( pAigTemp ); +// RetValue = Fra_FraigSat( pMiter, 1000000, 0, 0 ); } assert( RetValue != -1 ); Aig_ManStop( pMiter ); @@ -495,9 +495,8 @@ void Saig_ManagerFree( Saig_IntMan_t * p ) SeeAlso [] ***********************************************************************/ -int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int fVerbose, int * pDepth ) +int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int fRewrite, int fTransLoop, int fVerbose, int * pDepth ) { - int fUseTransRel = 0; Saig_IntMan_t * p; Aig_Man_t * pAigTemp; int s, i, RetValue, Status, clk, clk2, clkTotal = clock(); @@ -516,18 +515,20 @@ int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int fVerbose, int * pDep p->fVerbose = fVerbose; // can perform SAT sweeping and/or rewriting of this AIG... p->pAig = pAig; - if ( fUseTransRel ) + if ( fTransLoop ) p->pAigTrans = Saig_ManTransformed( pAig ); else p->pAigTrans = Saig_ManDuplicated( pAig ); +// p->pAigTrans = Dar_ManRwsat( pAigTemp = p->pAigTrans, 1, 0 ); +// Aig_ManStop( pAigTemp ); // derive CNF for the transformed AIG clk = clock(); p->pCnfAig = Cnf_Derive( p->pAigTrans, Aig_ManRegNum(p->pAigTrans) ); p->timeCnf += clock() - clk; if ( fVerbose ) - { + { printf( "AIG: PI/PO/Reg = %d/%d/%d. And = %d. Lev = %d. CNF: Var/Cla = %d/%d.\n", - Aig_ManPiNum(pAig), Aig_ManPoNum(pAig), Aig_ManRegNum(pAig), + Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), Saig_ManRegNum(pAig), Aig_ManAndNum(pAig), Aig_ManLevelNum(pAig), p->pCnfAig->nVars, p->pCnfAig->nClauses ); } @@ -545,10 +546,13 @@ p->timeCnf += clock() - clk; // timeframes p->pFrames = Saig_ManFramesInter( pAig, p->nFrames ); clk = clock(); -// p->pFrames = Dar_ManRwsat( pAigTemp = p->pFrames, 1, 0 ); -// Aig_ManStop( pAigTemp ); + if ( fRewrite ) + { + p->pFrames = Dar_ManRwsat( pAigTemp = p->pFrames, 1, 0 ); + Aig_ManStop( pAigTemp ); // p->pFrames = Fra_FraigEquivence( pAigTemp = p->pFrames, 100, 0 ); // Aig_ManStop( pAigTemp ); + } p->timeRwr += clock() - clk; // can also do SAT sweeping on the timeframes... clk = clock(); @@ -569,7 +573,7 @@ p->timeCnf += clock() - clk; RetValue = Saig_PerformOneStep( p ); if ( fVerbose ) { - printf( " I = %2d. Bmc =%3d. IntAnd =%6d. IntLev =%4d. Conf =%6d. ", + printf( " I = %2d. Bmc =%3d. IntAnd =%6d. IntLev =%5d. Conf =%6d. ", i+1, i + 1 + p->nFrames, Aig_ManNodeNum(p->pInter), Aig_ManLevelNum(p->pInter), p->nConfCur ); PRT( "Time", clock() - clk ); if ( Aig_ManNodeNum(p->pInter) == 0 ) @@ -623,7 +627,7 @@ p->timeEqu += clock() - clk; return 1; } // save interpolant and convert it into CNF - if ( fUseTransRel ) + if ( fTransLoop ) { Aig_ManStop( p->pInter ); p->pInter = p->pInterNew; |