diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-05-07 18:21:50 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-05-07 18:21:50 -0700 |
commit | b8b75cf14fd361c02c00ae3792537a0dab7a243f (patch) | |
tree | 6f11cefbc5e38af0682a981db67878d6a3e26adb | |
parent | 4b21edde650c8098e4b1b62042bb3096577d39dd (diff) | |
download | abc-b8b75cf14fd361c02c00ae3792537a0dab7a243f.tar.gz abc-b8b75cf14fd361c02c00ae3792537a0dab7a243f.tar.bz2 abc-b8b75cf14fd361c02c00ae3792537a0dab7a243f.zip |
Improvements in sequential verification.
-rw-r--r-- | .hgignore | 2 | ||||
-rw-r--r-- | src/aig/saig/saigMiter.c | 169 | ||||
-rw-r--r-- | src/base/abci/abc.c | 30 |
3 files changed, 181 insertions, 20 deletions
@@ -18,6 +18,8 @@ src/aig/au/ src/aig/ssm/ src/aig/ddb/ +src/map/if/ifDec.c + *~ *.orig diff --git a/src/aig/saig/saigMiter.c b/src/aig/saig/saigMiter.c index 12a1486d..0fdac6cc 100644 --- a/src/aig/saig/saigMiter.c +++ b/src/aig/saig/saigMiter.c @@ -23,7 +23,7 @@ ABC_NAMESPACE_IMPL_START - + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -347,11 +347,16 @@ Aig_Man_t * Saig_ManUnrollTwo( Aig_Man_t * pBot, Aig_Man_t * pTop, int nFrames ) // add internal nodes of this frame Aig_ManForEachNode( pAig, pObj, i ) pObj->pData = Aig_And( p, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); - // create POs for this frame - Aig_ManForEachPo( pAig, pObj, i ) - Aig_ObjCreatePo( p, Aig_ObjChild0Copy(pObj) ); if ( f == nFrames - 1 ) + { + // create POs for this frame + Aig_ManForEachPo( pAig, pObj, i ) + Aig_ObjCreatePo( p, Aig_ObjChild0Copy(pObj) ); break; + } + // create POs for this frame + Saig_ManForEachPo( pAig, pObj, i ) + Aig_ObjCreatePo( p, Aig_ObjChild0Copy(pObj) ); // save register inputs Saig_ManForEachLi( pAig, pObj, i ) pObj->pData = Aig_ObjChild0Copy(pObj); @@ -447,7 +452,10 @@ Aig_Man_t * Aig_ManDupNodesHalf( Aig_Man_t * p, Vec_Ptr_t * vSet, int iPart ) // Saig_ManForEachPo( p, pObj, i ) // pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); Vec_PtrForEachEntry( Aig_Obj_t *, vSet, pObj, i ) + { + assert( Aig_Regular(pObj)->pData != NULL ); Aig_ObjCreatePo( pNew, Aig_NotCond((Aig_Obj_t *)Aig_Regular(pObj)->pData, Aig_IsComplement(pObj)) ); + } if ( iPart == 0 ) { Saig_ManForEachLi( p, pObj, i ) @@ -541,7 +549,106 @@ int Saig_ManDemiterSimple( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAi /**Function************************************************************* - Synopsis [Duplicates the AIG to have constant-0 initial state.] + Synopsis [Returns 1 if PO can be demitered.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Saig_ManDemiterMarkPos( Aig_Man_t * p ) +{ + Aig_Obj_t * pObj; + int i; + Aig_ManCleanMarkAB( p ); + Saig_ManForEachLo( p, pObj, i ) + if ( i < Saig_ManRegNum(p)/2 ) + pObj->fMarkA = 1; + else + pObj->fMarkB = 1; + Aig_ManForEachNode( p, pObj, i ) + { + pObj->fMarkA = Aig_ObjFanin0(pObj)->fMarkA | Aig_ObjFanin1(pObj)->fMarkA; + pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB | Aig_ObjFanin1(pObj)->fMarkB; + } +} + +/**Function************************************************************* + + Synopsis [Returns 1 if PO can be demitered.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_ManDemiterCheckPo( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t ** ppPo0, Aig_Obj_t ** ppPo1 ) +{ + Aig_Obj_t * pFanin, * pObj0, * pObj1, * pObjR0, * pObjR1; + assert( Saig_ObjIsPo(p, pObj) ); + pFanin = Aig_ObjFanin0( pObj ); + if ( Aig_ObjIsConst1(pFanin) ) + { + if ( !Aig_ObjFaninC0(pObj) ) + return 0; + *ppPo0 = Aig_ManConst0(p); + *ppPo1 = Aig_ManConst0(p); + return 1; + } + if ( !Aig_ObjIsNode(pFanin) ) + return 0; + if ( !Aig_ObjRecognizeExor( pFanin, &pObj0, &pObj1 ) ) + return 0; + if ( Aig_ObjFaninC0(pObj) ) + pObj0 = Aig_Not(pObj0); + // make sure they can reach only one + pObjR0 = Aig_Regular(pObj0); + pObjR1 = Aig_Regular(pObj1); + if ( pObjR0->fMarkA && pObjR0->fMarkB || pObjR1->fMarkA && pObjR1->fMarkB || + pObjR0->fMarkA && pObjR1->fMarkA || pObjR0->fMarkB && pObjR1->fMarkB ) + return 0; + + if ( pObjR1->fMarkA && !pObjR0->fMarkA ) + { + *ppPo0 = pObj1; + *ppPo1 = pObj0; + } + else if ( pObjR0->fMarkA && !pObjR1->fMarkA ) + { + *ppPo0 = pObj0; + *ppPo1 = pObj1; + } + else + { +/* +printf( "%d", pObjR0->fMarkA ); +printf( "%d", pObjR0->fMarkB ); +printf( ":" ); +printf( "%d", pObjR1->fMarkA ); +printf( "%d", pObjR1->fMarkB ); +printf( " " ); +*/ + if ( Aig_Regular(pObj0)->Id < Aig_Regular(pObj1)->Id ) + { + *ppPo0 = pObj0; + *ppPo1 = pObj1; + } + else + { + *ppPo0 = pObj1; + *ppPo1 = pObj0; + } + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if AIG can be demitered.] Description [] @@ -553,6 +660,54 @@ int Saig_ManDemiterSimple( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAi int Saig_ManDemiterSimpleDiff( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 ) { Vec_Ptr_t * vSet0, * vSet1; + Aig_Obj_t * pObj, * pObj0, * pObj1; + int i; + if ( Aig_ManRegNum(p) == 0 || (Aig_ManRegNum(p) & 1) ) + return 0; + Saig_ManDemiterMarkPos( p ); + vSet0 = Vec_PtrAlloc( Saig_ManPoNum(p) ); + vSet1 = Vec_PtrAlloc( Saig_ManPoNum(p) ); + Saig_ManForEachPo( p, pObj, i ) + { + if ( !Saig_ManDemiterCheckPo( p, pObj, &pObj0, &pObj1 ) ) + { + Vec_PtrFree( vSet0 ); + Vec_PtrFree( vSet1 ); + Aig_ManCleanMarkAB( p ); + return 0; + } + Vec_PtrPush( vSet0, pObj0 ); + Vec_PtrPush( vSet1, pObj1 ); + } + // create new AIG + *ppAig0 = Aig_ManDupNodesHalf( p, vSet0, 0 ); + ABC_FREE( (*ppAig0)->pName ); + (*ppAig0)->pName = Aig_UtilStrsav( "part0" ); + // create new AIGs + *ppAig1 = Aig_ManDupNodesHalf( p, vSet1, 1 ); + ABC_FREE( (*ppAig1)->pName ); + (*ppAig1)->pName = Aig_UtilStrsav( "part1" ); + // cleanup + Vec_PtrFree( vSet0 ); + Vec_PtrFree( vSet1 ); + Aig_ManCleanMarkAB( p ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Duplicates the AIG to have constant-0 initial state.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_ManDemiterSimpleDiff_old( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 ) +{ + Vec_Ptr_t * vSet0, * vSet1; Aig_Obj_t * pObj, * pFanin, * pObj0, * pObj1; int i, Counter = 0; // assert( Saig_ManRegNum(p) % 2 == 0 ); @@ -873,6 +1028,7 @@ int Ssw_SecSpecial( Aig_Man_t * pPart0, Aig_Man_t * pPart1, int nFrames, int fVe // Aig_ManDumpBlif( pPart0, "file0.blif", NULL, NULL ); // Aig_ManDumpBlif( pPart1, "file1.blif", NULL, NULL ); // assert( Aig_ManNodeNum(pPart0) <= Aig_ManNodeNum(pPart1) ); +/* if ( Aig_ManNodeNum(pPart0) >= Aig_ManNodeNum(pPart1) ) { printf( "Warning: The design after synthesis is smaller!\n" ); @@ -880,6 +1036,7 @@ int Ssw_SecSpecial( Aig_Man_t * pPart0, Aig_Man_t * pPart1, int nFrames, int fVe printf( "The solver expects the original design as first argument and\n" ); printf( "the modified design as the second argument in \"absec\".\n" ); } +*/ // create two-level miter pMiterCec = Saig_ManCreateMiterTwo( pPart0, pPart1, nFrames ); if ( fVerbose ) @@ -992,6 +1149,8 @@ int Ssw_SecSpecialMiter( Aig_Man_t * p0, Aig_Man_t * p1, int nFrames, int fVerbo assert( Saig_ManPoNum(pPart0) == Saig_ManPoNum(pPart1) ); assert( Aig_ManRegNum(pPart0) == Aig_ManRegNum(pPart1) ); RetValue = Ssw_SecSpecial( pPart0, pPart1, nFrames, fVerbose ); + if ( RetValue != 1 && Aig_ManNodeNum(pPart0) >= Aig_ManNodeNum(pPart1) ) + RetValue = Ssw_SecSpecial( pPart1, pPart0, nFrames, fVerbose ); Aig_ManStop( pPart0 ); Aig_ManStop( pPart1 ); return RetValue; diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index e1398722..cea4d0f7 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -17046,26 +17046,23 @@ int Abc_CommandAbSec( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( fMiter ) { - if ( argc == globalUtilOptind + 1 ) +// pNtk = Io_Read( argv[globalUtilOptind], Io_ReadFileType(argv[globalUtilOptind]), 1 ); + if ( argc == globalUtilOptind + 1 ) { - pNtk = Io_Read( argv[globalUtilOptind], Io_ReadFileType(argv[globalUtilOptind]), 1 ); - if ( pNtk == NULL ) - { - Abc_Print( -1, "Cannot read network from file \"%s\".\n", argv[globalUtilOptind] ); - return 0; - } + Abc_Print( -1, "The miter cannot be given on the command line. Use \"read\".\n" ); + return 0; } - else - pNtk = Abc_NtkDup( pNtk ); if ( !Abc_NtkIsStrash(pNtk) ) { - pNtk = Abc_NtkStrash( pNtk2 = pNtk, 0, 1, 0 ); - Abc_NtkDelete( pNtk2 ); + Abc_Print( -1, "The miter should be structurally hashed. Use \"st\"\n" ); + return 0; } - Abc_NtkDarAbSec( pNtk, NULL, nFrames, fVerbose ); - Abc_NtkDelete( pNtk ); + if ( Abc_NtkDarAbSec( pNtk, NULL, nFrames, fVerbose ) == 1 ) + pAbc->Status = 1; + else + pAbc->Status = -1; } - else + else { pArgvNew = argv + globalUtilOptind; nArgcNew = argc - globalUtilOptind; @@ -17079,7 +17076,10 @@ int Abc_CommandAbSec( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; } // perform verification - Abc_NtkDarAbSec( pNtk1, pNtk2, nFrames, fVerbose ); + if ( Abc_NtkDarAbSec( pNtk1, pNtk2, nFrames, fVerbose ) == 1 ) + pAbc->Status = 1; + else + pAbc->Status = -1; if ( fDelete1 ) Abc_NtkDelete( pNtk1 ); if ( fDelete2 ) Abc_NtkDelete( pNtk2 ); } |