summaryrefslogtreecommitdiffstats
path: root/src/base/wln
diff options
context:
space:
mode:
Diffstat (limited to 'src/base/wln')
-rw-r--r--src/base/wln/wlnCom.c4
-rw-r--r--src/base/wln/wlnGuide.c52
-rw-r--r--src/base/wln/wlnRead.c175
3 files changed, 193 insertions, 38 deletions
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 );
}
////////////////////////////////////////////////////////////////////////
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-17 15:01:48 +0000