diff options
Diffstat (limited to 'src/base/wln/wlnRead.c')
-rw-r--r-- | src/base/wln/wlnRead.c | 175 |
1 files changed, 154 insertions, 21 deletions
diff --git a/src/base/wln/wlnRead.c b/src/base/wln/wlnRead.c index bc4211ac..b4e5f009 100644 --- a/src/base/wln/wlnRead.c +++ b/src/base/wln/wlnRead.c @@ -335,6 +335,39 @@ int Rtl_LibFindModule( Rtl_Lib_t * p, int NameId ) return i; return -1; } +int Rtl_LibFindModule2( Rtl_Lib_t * p, int NameId, int iNtk0 ) +{ + char * pName = Rtl_LibStr( p, NameId ); + Rtl_Ntk_t * pNtk0 = Rtl_LibNtk( p, iNtk0 ); + Rtl_Ntk_t * pNtk; int i; + int Counts0[4] = {0}; Rtl_NtkCountPio( pNtk0, Counts0 ); + Vec_PtrForEachEntry( Rtl_Ntk_t *, p->vNtks, pNtk, i ) + if ( strstr(Rtl_NtkName(pNtk), pName+1) ) + { + int Counts[4] = {0}; Rtl_NtkCountPio( pNtk, Counts ); + if ( Counts[1] == Counts0[1] && Counts[3] == Counts0[3] ) + return i; + } + return -1; +} +int Rtl_LibFindTwoModules( Rtl_Lib_t * p, int Name1, int Name2 ) +{ + int iNtk1 = Rtl_LibFindModule( p, Name1 ); + if ( Name2 == -1 ) + return (iNtk1 << 16) | iNtk1; + else + { + int Counts1[4] = {0}, Counts2[4] = {0}; + int iNtk2 = Rtl_LibFindModule( p, Name2 ); + Rtl_Ntk_t * pNtk1 = Rtl_LibNtk( p, iNtk1 ); + Rtl_Ntk_t * pNtk2 = Rtl_LibNtk( p, iNtk2 ); + Rtl_NtkCountPio( pNtk1, Counts1 ); + Rtl_NtkCountPio( pNtk2, Counts2 ); + if ( Counts1[1] != Counts2[1] || Counts1[3] != Counts2[3] ) + iNtk1 = Rtl_LibFindModule2( p, Name1, iNtk2 ); + return (iNtk1 << 16) | iNtk2; + } +} void Rtl_LibPrintStats( Rtl_Lib_t * p ) { Rtl_Ntk_t * pNtk; int i, nSymbs = 0; @@ -1404,7 +1437,7 @@ void Rtl_NtkUpdateBoxes( Rtl_Ntk_t * p ) Rtl_NtkForEachCell( p, pCell, i ) { Rtl_Ntk_t * pMod = Rtl_CellNtk( p, pCell ); - if ( pMod ) + if ( pMod && pMod->iCopy >= 0 ) pCell[2] = ABC_INFINITY + pMod->iCopy; } } @@ -2055,12 +2088,73 @@ printf( "Dumped \"%s\" with AIG for module %-20s : ", Buffer, Rtl_ShortenName(Rt Gia_ManPrintStats( p->pGia, NULL ); return p->pGia; } -void Rtl_LibBlast2( Rtl_Lib_t * pLib ) +void Rtl_LibMark_rec( Rtl_Ntk_t * pNtk ) { - Rtl_Ntk_t * p; int i; - Vec_PtrForEachEntry( Rtl_Ntk_t *, pLib->vNtks, p, i ) - if ( p->pGia == NULL ) - p->pGia = Rtl_NtkBlast2( p ); + int i, * pCell; + if ( pNtk->iCopy == -1 ) + return; + Rtl_NtkForEachCell( pNtk, pCell, i ) + { + Rtl_Ntk_t * pMod = Rtl_CellNtk( pNtk, pCell ); + if ( pMod ) + Rtl_LibMark_rec( pMod ); + } + assert( pNtk->iCopy == -2 ); + pNtk->iCopy = -1; +} +void Rtl_LibBlast2( Rtl_Lib_t * pLib, Vec_Int_t * vRoots ) +{ + Rtl_Ntk_t * pNtk; int i, iNtk; + Vec_PtrForEachEntry( Rtl_Ntk_t *, pLib->vNtks, pNtk, i ) + pNtk->iCopy = -1; + if ( vRoots ) + { + Vec_PtrForEachEntry( Rtl_Ntk_t *, pLib->vNtks, pNtk, i ) + pNtk->iCopy = -2; + Vec_IntForEachEntry( vRoots, iNtk, i ) + Rtl_LibMark_rec( Rtl_LibNtk(pLib, iNtk) ); + } + Vec_PtrForEachEntry( Rtl_Ntk_t *, pLib->vNtks, pNtk, i ) + if ( pNtk->iCopy == -1 && pNtk->pGia == NULL ) + pNtk->pGia = Rtl_NtkBlast2( pNtk ); +// Vec_PtrForEachEntry( Rtl_Ntk_t *, pLib->vNtks, pNtk, i ) +// if ( pNtk->iCopy == -2 ) +// printf( "Skipping network \"%s\" during bit-blasting.\n", Rtl_NtkName(pNtk) ); + Vec_PtrForEachEntry( Rtl_Ntk_t *, pLib->vNtks, pNtk, i ) + pNtk->iCopy = -1; +} +void Rtl_LibBlastClean( Rtl_Lib_t * p ) +{ + Rtl_Ntk_t * pNtk; int i; + Vec_PtrForEachEntry( Rtl_Ntk_t *, p->vNtks, pNtk, i ) + Gia_ManStopP( &pNtk->pGia ); +} +void Rtl_LibSetReplace( Rtl_Lib_t * p, Vec_Wec_t * vGuide ) +{ + Vec_Int_t * vLevel; int i, iNtk1, iNtk2; + Rtl_Ntk_t * pNtk, * pNtk1, * pNtk2; + Vec_PtrForEachEntry( Rtl_Ntk_t *, p->vNtks, pNtk, i ) + pNtk->iCopy = -1; + Vec_WecForEachLevel( vGuide, vLevel, i ) + { + int Name1 = Vec_IntEntry( vLevel, 2 ); + int Name2 = Vec_IntEntry( vLevel, 3 ); + int iNtk = Rtl_LibFindTwoModules( p, Name1, Name2 ); + if ( iNtk == -1 ) + { + printf( "Cannot find networks \"%s\" and \"%s\" in the design.\n", Rtl_LibStr(p, Name1), Rtl_LibStr(p, Name2) ); + break; + } + iNtk1 = iNtk >> 16; + iNtk2 = iNtk & 0xFFFF; + pNtk1 = Rtl_LibNtk(p, iNtk1); + pNtk2 = Rtl_LibNtk(p, iNtk2); + pNtk1->iCopy = iNtk2; + if ( iNtk1 == iNtk2 ) + printf( "Preparing to prove \"%s\".\n", Rtl_NtkName(pNtk1) ); + else + printf( "Preparing to replace \"%s\" by \"%s\".\n", Rtl_NtkName(pNtk1), Rtl_NtkName(pNtk2) ); + } } @@ -2113,7 +2207,7 @@ finish: if ( p != p1 && p != p2 ) Gia_ManStopP( &p->pGia ); //Rtl_LibBlast( pLib ); - Rtl_LibBlast2( pLib ); + Rtl_LibBlast2( pLib, NULL ); } void Rtl_LibSolve( Rtl_Lib_t * pLib, void * pNtk ) { @@ -2185,24 +2279,61 @@ void Wln_SolveProperty( Rtl_Lib_t * p, int iNtk ) printf( "Proving property \"%s\".\n", Rtl_NtkName(pNtk) ); Rtl_LibSolve( p, pNtk ); } +Vec_Int_t * Wln_ReadNtkRoots( Rtl_Lib_t * p, Vec_Wec_t * vGuide ) +{ + Vec_Int_t * vLevel; int i; + Vec_Int_t * vRoots = Vec_IntAlloc( 100 ); + Vec_WecForEachLevel( vGuide, vLevel, i ) + { + int Name1 = Vec_IntEntry( vLevel, 2 ); + int Name2 = Vec_IntEntry( vLevel, 3 ); + int iNtk = Rtl_LibFindTwoModules( p, Name1, Name2 ); + if ( iNtk == -1 ) + { + printf( "Cannot find networks \"%s\" and \"%s\" in the design.\n", Rtl_LibStr(p, Name1), Rtl_LibStr(p, Name2) ); + break; + } +/* + else + { + Rtl_Ntk_t * pNtk1 = Rtl_LibNtk( p, iNtk >> 16 ); + Rtl_Ntk_t * pNtk2 = Rtl_LibNtk( p, iNtk & 0xFFFF ); + printf( "Matching \"%s\" and \"%s\".\n", Rtl_NtkName(pNtk1), Rtl_NtkName(pNtk2) ); + } +*/ + Vec_IntPushTwo( vRoots, iNtk >> 16, iNtk & 0xFFFF ); + } + return vRoots; +} void Wln_SolveWithGuidance( char * pFileName, Rtl_Lib_t * p ) { - extern Vec_Int_t * Wln_ReadGuidance( char * pFileName, Abc_Nam_t * p ); - Vec_Int_t * vGuide = Wln_ReadGuidance( pFileName, p->pManName ); int i; + extern Vec_Wec_t * Wln_ReadGuidance( char * pFileName, Abc_Nam_t * p ); + Vec_Wec_t * vGuide = Wln_ReadGuidance( pFileName, p->pManName ); + Vec_Int_t * vRoots, * vLevel; int i, iNtk1, iNtk2; Vec_IntFillExtra( p->vMap, Abc_NamObjNumMax(p->pManName), -1 ); - Rtl_LibBlast2( p ); - for ( i = 0; i < Vec_IntSize(vGuide); i += 4 ) + Rtl_LibSetReplace( p, vGuide ); + Rtl_LibUpdateBoxes( p ); + Rtl_LibReorderModules( p ); + vRoots = Wln_ReadNtkRoots( p, vGuide ); + Rtl_LibBlast2( p, vRoots ); + Vec_WecForEachLevel( vGuide, vLevel, i ) { - int Prove = Vec_IntEntry( vGuide, i+0 ); - int Type = Vec_IntEntry( vGuide, i+1 ); - int Name1 = Vec_IntEntry( vGuide, i+2 ); - int Name2 = Vec_IntEntry( vGuide, i+3 ); - int iNtk1 = Rtl_LibFindModule( p, Name1 ); - int iNtk2 = Name2 == -1 ? -1 : Rtl_LibFindModule( p, Name2 ); + int Prove = Vec_IntEntry( vLevel, 0 ); + int Type = Vec_IntEntry( vLevel, 1 ); + int Name1 = Vec_IntEntry( vLevel, 2 ); + int Name2 = Vec_IntEntry( vLevel, 3 ); + int iNtk = Rtl_LibFindTwoModules( p, Name1, Name2 ); + if ( iNtk == -1 ) + { + printf( "Cannot find networks \"%s\" and \"%s\" in the design.\n", Rtl_LibStr(p, Name1), Rtl_LibStr(p, Name2) ); + break; + } + iNtk1 = iNtk >> 16; + iNtk2 = iNtk & 0xFFFF; if ( Prove != Rtl_LibStrId(p, "prove") ) - printf( "Unknown task in line %d.\n", i/4 ); - else if ( iNtk1 == -1 ) - printf( "Network %s cannot be found in this design.\n", Rtl_LibStr(p, Name1) ); + printf( "Unknown task in line %d.\n", i ); + //else if ( iNtk1 == -1 ) + // printf( "Network %s cannot be found in this design.\n", Rtl_LibStr(p, Name1) ); else { if ( Type == Rtl_LibStrId(p, "equal") ) @@ -2215,7 +2346,9 @@ void Wln_SolveWithGuidance( char * pFileName, Rtl_Lib_t * p ) } break; } - Vec_IntFree( vGuide ); + Rtl_LibBlastClean( p ); + Vec_WecFree( vGuide ); + Vec_IntFree( vRoots ); } //////////////////////////////////////////////////////////////////////// |