From 32693e9857c21c03257ec620fb2439ad36d381e3 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 5 Mar 2022 20:58:38 -0800 Subject: Experiments with word-level data structures. --- src/base/wlc/wlcCom.c | 2 +- src/base/wln/wlnCom.c | 4 +- src/base/wln/wlnGuide.c | 52 +++++++++----- src/base/wln/wlnRead.c | 175 ++++++++++++++++++++++++++++++++++++++++++------ 4 files changed, 194 insertions(+), 39 deletions(-) (limited to 'src/base') diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c index 37ecf2c7..dcddd042 100644 --- a/src/base/wlc/wlcCom.c +++ b/src/base/wlc/wlcCom.c @@ -21,7 +21,7 @@ #include "wlc.h" #include "base/wln/wln.h" #include "base/main/mainInt.h" -#include "aig/miniaig/ndr.h" +//#include "aig/miniaig/ndr.h" ABC_NAMESPACE_IMPL_START diff --git a/src/base/wln/wlnCom.c b/src/base/wln/wlnCom.c index 3db27785..90ac4faa 100644 --- a/src/base/wln/wlnCom.c +++ b/src/base/wln/wlnCom.c @@ -276,7 +276,7 @@ usage: int Abc_CommandSolve( Abc_Frame_t * pAbc, int argc, char ** argv ) { extern void Rtl_LibBlast( Rtl_Lib_t * pLib ); - extern void Rtl_LibBlast2( Rtl_Lib_t * pLib ); + extern void Rtl_LibBlast2( Rtl_Lib_t * pLib, Vec_Int_t * vRoots ); extern void Rtl_LibSolve( Rtl_Lib_t * pLib, void * pNtk ); extern void Rtl_LibPreprocess( Rtl_Lib_t * pLib ); extern void Wln_SolveWithGuidance( char * pFileName, Rtl_Lib_t * p ); @@ -327,7 +327,7 @@ int Abc_CommandSolve( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( fOldBlast ) Rtl_LibBlast( pLib ); else - Rtl_LibBlast2( pLib ); + Rtl_LibBlast2( pLib, NULL ); if ( fPrepro ) Rtl_LibPreprocess( pLib ); Rtl_LibSolve( pLib, NULL ); diff --git a/src/base/wln/wlnGuide.c b/src/base/wln/wlnGuide.c index abe9a6d8..b7e656eb 100644 --- a/src/base/wln/wlnGuide.c +++ b/src/base/wln/wlnGuide.c @@ -41,26 +41,48 @@ ABC_NAMESPACE_IMPL_START SeeAlso [] ***********************************************************************/ -Vec_Int_t * Wln_ReadGuidance( char * pFileName, Abc_Nam_t * p ) +int Wln_ReadFindToken( char * pToken, Abc_Nam_t * p ) { - char Buffer[1000] = {'\\'}, * pBuffer = Buffer+1; - Vec_Int_t * vTokens = Vec_IntAlloc( 100 ); + char * pBuffer = Abc_UtilStrsavTwo( "\\", pToken ); + int RetValue = Abc_NamStrFindOrAdd( p, pBuffer, NULL ); + ABC_FREE( pBuffer ); + return RetValue; +} +void Wln_PrintGuidance( Vec_Wec_t * vGuide, Abc_Nam_t * p ) +{ + Vec_Int_t * vLevel; int i, k, Obj; + Vec_WecForEachLevel( vGuide, vLevel, i ) + { + Vec_IntForEachEntry( vLevel, Obj, k ) + printf( "%s ", Obj >= 0 ? Abc_NamStr(p, Obj) : "[unknown]" ); + printf( "\n" ); + } +} +Vec_Wec_t * Wln_ReadGuidance( char * pFileName, Abc_Nam_t * p ) +{ + char * pBuffer = ABC_CALLOC( char, 10000 ), * pToken; + Vec_Wec_t * vTokens = Vec_WecAlloc( 100 ); Vec_Int_t * vLevel; FILE * pFile = fopen( pFileName, "rb" ); - while ( fscanf( pFile, "%s", pBuffer ) == 1 ) + while ( fgets( pBuffer, 10000, pFile ) ) { - if ( pBuffer[(int)strlen(pBuffer)-1] == '\r' ) - pBuffer[(int)strlen(pBuffer)-1] = 0; - if ( !strcmp(pBuffer, "prove") && Vec_IntSize(vTokens) % 4 == 3 ) // account for "property" - Vec_IntPush( vTokens, -1 ); - if ( Vec_IntSize(vTokens) % 4 == 2 || Vec_IntSize(vTokens) % 4 == 3 ) - Vec_IntPush( vTokens, Abc_NamStrFindOrAdd(p, Buffer, NULL) ); - else - Vec_IntPush( vTokens, Abc_NamStrFindOrAdd(p, pBuffer, NULL) ); + if ( pBuffer[0] == '#' ) + continue; + vLevel = Vec_WecPushLevel( vTokens ); + pToken = strtok( pBuffer, " \t\r\n" ); + while ( pToken ) + { + Vec_IntPush( vLevel, Vec_IntSize(vLevel) < 2 ? Abc_NamStrFindOrAdd(p, pToken, NULL) : Wln_ReadFindToken(pToken, p) ); + pToken = strtok( NULL, " \t\r\n" ); + } + if ( Vec_IntSize(vLevel) % 4 == 3 ) // account for "property" + Vec_IntPush( vLevel, -1 ); + assert( Vec_IntSize(vLevel) % 4 == 0 ); } fclose( pFile ); - if ( Vec_IntSize(vTokens) % 4 == 3 ) // account for "property" - Vec_IntPush( vTokens, -1 ); - assert( Vec_IntSize(vTokens) % 4 == 0 ); + if ( Vec_WecSize(vTokens) == 0 ) + printf( "Guidance is empty.\n" ); + //Wln_PrintGuidance( vTokens, p ); + ABC_FREE( pBuffer ); return vTokens; } 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 ); } //////////////////////////////////////////////////////////////////////// -- cgit v1.2.3