summaryrefslogtreecommitdiffstats
path: root/src/base
diff options
context:
space:
mode:
Diffstat (limited to 'src/base')
-rw-r--r--src/base/abc/abc.h2
-rw-r--r--src/base/abc/abcAig.c5
-rw-r--r--src/base/abc/abcMinBase.c21
-rw-r--r--src/base/abci/abc.c62
-rw-r--r--src/base/abci/abcDar.c27
-rw-r--r--src/base/abci/abcRefactor.c34
-rw-r--r--src/base/abci/abcRestruct.c2
-rw-r--r--src/base/abci/abcResub.c2
-rw-r--r--src/base/abci/abcRewrite.c31
-rw-r--r--src/base/abci/abcRr.c5
-rw-r--r--src/base/cmd/cmd.c8
-rw-r--r--src/base/cmd/cmdLoad.c3
-rw-r--r--src/base/wlc/wlcBlast.c44
-rw-r--r--src/base/wlc/wlcCom.c21
-rw-r--r--src/base/wln/wlnCom.c4
-rw-r--r--src/base/wln/wlnGuide.c52
-rw-r--r--src/base/wln/wlnRead.c392
17 files changed, 597 insertions, 118 deletions
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index eea66f29..b4e22a38 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -559,7 +559,7 @@ extern ABC_DLL Abc_Obj_t * Abc_AigOr( Abc_Aig_t * pMan, Abc_Obj_t * p0, A
extern ABC_DLL Abc_Obj_t * Abc_AigXor( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 );
extern ABC_DLL Abc_Obj_t * Abc_AigMux( Abc_Aig_t * pMan, Abc_Obj_t * pC, Abc_Obj_t * p1, Abc_Obj_t * p0 );
extern ABC_DLL Abc_Obj_t * Abc_AigMiter( Abc_Aig_t * pMan, Vec_Ptr_t * vPairs, int fImplic );
-extern ABC_DLL void Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, int fUpdateLevel );
+extern ABC_DLL int Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, int fUpdateLevel );
extern ABC_DLL void Abc_AigDeleteNode( Abc_Aig_t * pMan, Abc_Obj_t * pOld );
extern ABC_DLL void Abc_AigRehash( Abc_Aig_t * pMan );
extern ABC_DLL int Abc_AigNodeHasComplFanoutEdge( Abc_Obj_t * pNode );
diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c
index d3347a13..636fe30a 100644
--- a/src/base/abc/abcAig.c
+++ b/src/base/abc/abcAig.c
@@ -847,7 +847,7 @@ Abc_Obj_t * Abc_AigMiter2( Abc_Aig_t * pMan, Vec_Ptr_t * vPairs )
SeeAlso []
***********************************************************************/
-void Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, int fUpdateLevel )
+int Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, int fUpdateLevel )
{
assert( Vec_PtrSize(pMan->vStackReplaceOld) == 0 );
assert( Vec_PtrSize(pMan->vStackReplaceNew) == 0 );
@@ -859,6 +859,8 @@ void Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, int f
{
pOld = (Abc_Obj_t *)Vec_PtrPop( pMan->vStackReplaceOld );
pNew = (Abc_Obj_t *)Vec_PtrPop( pMan->vStackReplaceNew );
+ if ( Abc_ObjFanoutNum(pOld) == 0 )
+ return 0;
Abc_AigReplace_int( pMan, pOld, pNew, fUpdateLevel );
}
if ( fUpdateLevel )
@@ -867,6 +869,7 @@ void Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, int f
if ( pMan->pNtkAig->vLevelsR )
Abc_AigUpdateLevelR_int( pMan );
}
+ return 1;
}
/**Function*************************************************************
diff --git a/src/base/abc/abcMinBase.c b/src/base/abc/abcMinBase.c
index 991f65a4..92dbd0c9 100644
--- a/src/base/abc/abcMinBase.c
+++ b/src/base/abc/abcMinBase.c
@@ -113,7 +113,7 @@ int Abc_NodeMinimumBase( Abc_Obj_t * pNode )
DdNode * bTemp, ** pbVars;
Vec_Str_t * vSupport;
int i, nVars, j, iFanin, iFanin2, k = 0;
- int fDupFanins = 0;
+ int ddSize, fDupFanins = 0;
assert( Abc_NtkIsBddLogic(pNode->pNtk) );
assert( Abc_ObjIsNode(pNode) );
@@ -127,8 +127,14 @@ int Abc_NodeMinimumBase( Abc_Obj_t * pNode )
return 0;
}
- // remove unused fanins
- pbVars = ABC_CALLOC( DdNode *, Abc_ObjFaninNum(pNode) );
+ // remove unused fanins.
+
+ // By default, every BDD variable stays equivalent to itself.
+ ddSize = Cudd_ReadSize( dd );
+ pbVars = ABC_CALLOC( DdNode *, ddSize );
+ for (i = 0; i < ddSize; i += 1 ) {
+ pbVars[i] = Cudd_bddIthVar( dd, i );
+ }
Vec_IntForEachEntry( &pNode->vFanins, iFanin, i )
{
Abc_Obj_t * pFanin = Abc_NtkObj( pNode->pNtk, iFanin );
@@ -146,13 +152,18 @@ int Abc_NodeMinimumBase( Abc_Obj_t * pNode )
Vec_IntWriteEntry( &pNode->vFanins, k++, iFanin );
else if ( !Vec_IntRemove( &pFanin->vFanouts, pNode->Id ) )
printf( "The obj %d is not found among the fanouts of obj %d ...\n", pNode->Id, iFanin );
+
+ // i-th variable becomes equivalent to j-th variable (can be itself)
pbVars[i] = Cudd_bddIthVar( dd, j );
}
Vec_IntShrink( &pNode->vFanins, k );
// update the function of the node
- pNode->pData = Cudd_bddVectorCompose( dd, bTemp = (DdNode *)pNode->pData, pbVars ); Cudd_Ref( (DdNode *)pNode->pData );
- Cudd_RecursiveDeref( dd, bTemp );
+ if ( ! Cudd_IsConstant((DdNode *) pNode->pData ) ) {
+ pNode->pData = Cudd_bddVectorCompose( dd, bTemp = (DdNode *)pNode->pData, pbVars );
+ Cudd_Ref( (DdNode *)pNode->pData );
+ Cudd_RecursiveDeref( dd, bTemp );
+ }
Vec_StrFree( vSupport );
ABC_FREE( pbVars );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index c92917ac..34f15cf2 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -7312,8 +7312,8 @@ usage:
***********************************************************************/
int Abc_CommandRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
{
- Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
- int c;
+ Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc), * pDup;
+ int c, RetValue;
int fUpdateLevel;
int fPrecompute;
int fUseZeros;
@@ -7383,10 +7383,21 @@ int Abc_CommandRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// modify the current network
- if ( !Abc_NtkRewrite( pNtk, fUpdateLevel, fUseZeros, fVerbose, fVeryVerbose, fPlaceEnable ) )
+ pDup = Abc_NtkDup( pNtk );
+ RetValue = Abc_NtkRewrite( pNtk, fUpdateLevel, fUseZeros, fVerbose, fVeryVerbose, fPlaceEnable );
+ if ( RetValue == -1 )
{
- Abc_Print( -1, "Rewriting has failed.\n" );
- return 1;
+ Abc_FrameReplaceCurrentNetwork( pAbc, pDup );
+ printf( "An error occurred during computation. The original network is restored.\n" );
+ }
+ else
+ {
+ Abc_NtkDelete( pDup );
+ if ( RetValue == 0 )
+ {
+ Abc_Print( 0, "Rewriting has failed.\n" );
+ return 1;
+ }
}
return 0;
@@ -7415,8 +7426,8 @@ usage:
***********************************************************************/
int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv )
{
- Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
- int c;
+ Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc), * pDup;
+ int c, RetValue;
int nNodeSizeMax;
int nConeSizeMax;
int fUpdateLevel;
@@ -7506,10 +7517,21 @@ int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// modify the current network
- if ( !Abc_NtkRefactor( pNtk, nNodeSizeMax, nConeSizeMax, fUpdateLevel, fUseZeros, fUseDcs, fVerbose ) )
+ pDup = Abc_NtkDup( pNtk );
+ RetValue = Abc_NtkRefactor( pNtk, nNodeSizeMax, nConeSizeMax, fUpdateLevel, fUseZeros, fUseDcs, fVerbose );
+ if ( RetValue == -1 )
{
- Abc_Print( -1, "Refactoring has failed.\n" );
- return 1;
+ Abc_FrameReplaceCurrentNetwork( pAbc, pDup );
+ printf( "An error occurred during computation. The original network is restored.\n" );
+ }
+ else
+ {
+ Abc_NtkDelete( pDup );
+ if ( RetValue == 0 )
+ {
+ Abc_Print( 0, "Refactoring has failed.\n" );
+ return 1;
+ }
}
return 0;
@@ -13974,6 +13996,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
//Dau_NetworkEnumTest();
//Extra_SimulationTest( nDivMax, nNumOnes, fNewOrder );
//Mnist_ExperimentWithScaling( nDecMax );
+ //Gyx_ProblemSolveTest();
return 0;
usage:
Abc_Print( -2, "usage: test [-CKDNM] [-aovwh] <file_name>\n" );
@@ -32601,9 +32624,10 @@ int Abc_CommandAbc9Dfs( Abc_Frame_t * pAbc, int argc, char ** argv )
int fNormal = 0;
int fRevFans = 0;
int fRevOuts = 0;
+ int fLeveled = 0;
int fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "nfovh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "nfolvh" ) ) != EOF )
{
switch ( c )
{
@@ -32616,6 +32640,9 @@ int Abc_CommandAbc9Dfs( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'o':
fRevOuts ^= 1;
break;
+ case 'l':
+ fLeveled ^= 1;
+ break;
case 'v':
fVerbose ^= 1;
break;
@@ -32630,7 +32657,9 @@ int Abc_CommandAbc9Dfs( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Abc_CommandAbc9Dfs(): There is no AIG.\n" );
return 1;
}
- if ( fNormal )
+ if ( fLeveled )
+ pTemp = Gia_ManDupLevelized( pAbc->pGia );
+ else if ( fNormal )
pTemp = Gia_ManDupOrderAiger( pAbc->pGia );
else
pTemp = Gia_ManDupOrderDfsReverse( pAbc->pGia, fRevFans, fRevOuts );
@@ -32638,12 +32667,13 @@ int Abc_CommandAbc9Dfs( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- Abc_Print( -2, "usage: &dfs [-nfovh]\n" );
+ Abc_Print( -2, "usage: &dfs [-nfolvh]\n" );
Abc_Print( -2, "\t orders objects in the DFS order\n" );
- Abc_Print( -2, "\t-n : toggle using normalized ordering [default = %s]\n", fNormal? "yes": "no" );
- Abc_Print( -2, "\t-f : toggle using reverse fanin traversal order [default = %s]\n", fRevFans? "yes": "no" );
+ Abc_Print( -2, "\t-n : toggle using normalized ordering [default = %s]\n", fNormal? "yes": "no" );
+ Abc_Print( -2, "\t-f : toggle using reverse fanin traversal order [default = %s]\n", fRevFans? "yes": "no" );
Abc_Print( -2, "\t-o : toggle using reverse output traversal order [default = %s]\n", fRevOuts? "yes": "no" );
- Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-l : toggle using levelized order [default = %s]\n", fLeveled? "yes": "no" );
+ Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index f6818010..677cb7d0 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -658,6 +658,33 @@ Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan )
}
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_NtkFromGiaCollapse( Gia_Man_t * pGia )
+{
+ Aig_Man_t * pMan = Gia_ManToAig( pGia, 0 ); int Res;
+ Abc_Ntk_t * pNtk = Abc_NtkFromAigPhase( pMan ), * pTemp;
+ //pNtk->pName = Extra_UtilStrsav(pGia->pName);
+ Aig_ManStop( pMan );
+ // collapse the network
+ pNtk = Abc_NtkCollapse( pTemp = pNtk, 10000, 0, 1, 0, 0, 0 );
+ Abc_NtkDelete( pTemp );
+ if ( pNtk == NULL )
+ return 0;
+ Res = Abc_NtkGetBddNodeNum( pNtk );
+ Abc_NtkDelete( pNtk );
+ return Res == 0;
+}
+
/**Function*************************************************************
diff --git a/src/base/abci/abcRefactor.c b/src/base/abci/abcRefactor.c
index 3cc6d793..8ec5944f 100644
--- a/src/base/abci/abcRefactor.c
+++ b/src/base/abci/abcRefactor.c
@@ -325,7 +325,7 @@ void Abc_NtkManRefPrintStats( Abc_ManRef_t * p )
***********************************************************************/
int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, int fUpdateLevel, int fUseZeros, int fUseDcs, int fVerbose )
{
- extern void Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int fUpdateLevel, int nGain );
+ extern int Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int fUpdateLevel, int nGain );
ProgressBar * pProgress;
Abc_ManRef_t * pManRef;
Abc_ManCut_t * pManCut;
@@ -333,7 +333,7 @@ int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, int f
Vec_Ptr_t * vFanins;
Abc_Obj_t * pNode;
abctime clk, clkStart = Abc_Clock();
- int i, nNodes;
+ int i, nNodes, RetValue = 1;
assert( Abc_NtkIsStrash(pNtk) );
// cleanup the AIG
@@ -377,7 +377,12 @@ pManRef->timeRes += Abc_Clock() - clk;
continue;
// acceptable replacement found, update the graph
clk = Abc_Clock();
- Dec_GraphUpdateNetwork( pNode, pFForm, fUpdateLevel, pManRef->nLastGain );
+ if ( !Dec_GraphUpdateNetwork( pNode, pFForm, fUpdateLevel, pManRef->nLastGain ) )
+ {
+ Dec_GraphFree( pFForm );
+ RetValue = -1;
+ break;
+ }
pManRef->timeNtk += Abc_Clock() - clk;
Dec_GraphFree( pFForm );
}
@@ -394,18 +399,21 @@ pManRef->timeTotal = Abc_Clock() - clkStart;
// put the nodes into the DFS order and reassign their IDs
Abc_NtkReassignIds( pNtk );
// Abc_AigCheckFaninOrder( pNtk->pManFunc );
- // fix the levels
- if ( fUpdateLevel )
- Abc_NtkStopReverseLevels( pNtk );
- else
- Abc_NtkLevel( pNtk );
- // check
- if ( !Abc_NtkCheck( pNtk ) )
+ if ( RetValue != -1 )
{
- printf( "Abc_NtkRefactor: The network check has failed.\n" );
- return 0;
+ // fix the levels
+ if ( fUpdateLevel )
+ Abc_NtkStopReverseLevels( pNtk );
+ else
+ Abc_NtkLevel( pNtk );
+ // check
+ if ( !Abc_NtkCheck( pNtk ) )
+ {
+ printf( "Abc_NtkRefactor: The network check has failed.\n" );
+ return 0;
+ }
}
- return 1;
+ return RetValue;
}
diff --git a/src/base/abci/abcRestruct.c b/src/base/abci/abcRestruct.c
index ef5dd451..87f15238 100644
--- a/src/base/abci/abcRestruct.c
+++ b/src/base/abci/abcRestruct.c
@@ -105,7 +105,7 @@ static void Abc_NtkManRstPrintStats( Abc_ManRst_t * p );
***********************************************************************/
int Abc_NtkRestructure( Abc_Ntk_t * pNtk, int nCutMax, int fUpdateLevel, int fUseZeros, int fVerbose )
{
- extern void Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int fUpdateLevel, int nGain );
+ extern int Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int fUpdateLevel, int nGain );
ProgressBar * pProgress;
Abc_ManRst_t * pManRst;
Cut_Man_t * pManCut;
diff --git a/src/base/abci/abcResub.c b/src/base/abci/abcResub.c
index b8934e23..dc1b6036 100644
--- a/src/base/abci/abcResub.c
+++ b/src/base/abci/abcResub.c
@@ -136,7 +136,7 @@ extern abctime s_ResubTime;
***********************************************************************/
int Abc_NtkResubstitute( Abc_Ntk_t * pNtk, int nCutMax, int nStepsMax, int nLevelsOdc, int fUpdateLevel, int fVerbose, int fVeryVerbose )
{
- extern void Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int fUpdateLevel, int nGain );
+ extern int Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int fUpdateLevel, int nGain );
ProgressBar * pProgress;
Abc_ManRes_t * pManRes;
Abc_ManCut_t * pManCut;
diff --git a/src/base/abci/abcRewrite.c b/src/base/abci/abcRewrite.c
index 0b0881a6..1da7e4e8 100644
--- a/src/base/abci/abcRewrite.c
+++ b/src/base/abci/abcRewrite.c
@@ -60,14 +60,14 @@ extern void Abc_PlaceUpdate( Vec_Ptr_t * vAddedCells, Vec_Ptr_t * vUpdatedNets
***********************************************************************/
int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerbose, int fVeryVerbose, int fPlaceEnable )
{
- extern void Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int fUpdateLevel, int nGain );
+ extern int Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int fUpdateLevel, int nGain );
ProgressBar * pProgress;
Cut_Man_t * pManCut;
Rwr_Man_t * pManRwr;
Abc_Obj_t * pNode;
// Vec_Ptr_t * vAddedCells = NULL, * vUpdatedNets = NULL;
Dec_Graph_t * pGraph;
- int i, nNodes, nGain, fCompl;
+ int i, nNodes, nGain, fCompl, RetValue = 1;
abctime clk, clkStart = Abc_Clock();
assert( Abc_NtkIsStrash(pNtk) );
@@ -138,7 +138,11 @@ Rwr_ManAddTimeCuts( pManRwr, Abc_Clock() - clk );
// complement the FF if needed
if ( fCompl ) Dec_GraphComplement( pGraph );
clk = Abc_Clock();
- Dec_GraphUpdateNetwork( pNode, pGraph, fUpdateLevel, nGain );
+ if ( !Dec_GraphUpdateNetwork( pNode, pGraph, fUpdateLevel, nGain ) )
+ {
+ RetValue = -1;
+ break;
+ }
Rwr_ManAddTimeUpdate( pManRwr, Abc_Clock() - clk );
if ( fCompl ) Dec_GraphComplement( pGraph );
@@ -175,17 +179,20 @@ Rwr_ManAddTimeTotal( pManRwr, Abc_Clock() - clkStart );
}
// Abc_AigCheckFaninOrder( pNtk->pManFunc );
// fix the levels
- if ( fUpdateLevel )
- Abc_NtkStopReverseLevels( pNtk );
- else
- Abc_NtkLevel( pNtk );
- // check
- if ( !Abc_NtkCheck( pNtk ) )
+ if ( RetValue >= 0 )
{
- printf( "Abc_NtkRewrite: The network check has failed.\n" );
- return 0;
+ if ( fUpdateLevel )
+ Abc_NtkStopReverseLevels( pNtk );
+ else
+ Abc_NtkLevel( pNtk );
+ // check
+ if ( !Abc_NtkCheck( pNtk ) )
+ {
+ printf( "Abc_NtkRewrite: The network check has failed.\n" );
+ return 0;
+ }
}
- return 1;
+ return RetValue;
}
diff --git a/src/base/abci/abcRr.c b/src/base/abci/abcRr.c
index 52d1fd32..86c5f13e 100644
--- a/src/base/abci/abcRr.c
+++ b/src/base/abci/abcRr.c
@@ -397,10 +397,7 @@ int Abc_NtkRRUpdate( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, Abc_Obj_t * pFanin, Ab
else assert( 0 );
// replace
if ( pFanout == NULL )
- {
- Abc_AigReplace( (Abc_Aig_t *)pNtk->pManFunc, pNode, pNodeNew, 1 );
- return 1;
- }
+ return Abc_AigReplace( (Abc_Aig_t *)pNtk->pManFunc, pNode, pNodeNew, 1 );
// find the fanout after redundancy removal
if ( pNode == Abc_ObjFanin0(pFanout) )
pFanoutNew = Abc_AigAnd( (Abc_Aig_t *)pNtk->pManFunc, Abc_ObjNotCond(pNodeNew,Abc_ObjFaninC0(pFanout)), Abc_ObjChild1(pFanout) );
diff --git a/src/base/cmd/cmd.c b/src/base/cmd/cmd.c
index a0042443..fe7286b7 100644
--- a/src/base/cmd/cmd.c
+++ b/src/base/cmd/cmd.c
@@ -1161,7 +1161,7 @@ int CmdCommandScanDir( Abc_Frame_t * pAbc, int argc, char **argv )
struct _finddata_t c_file;
char * pDirStr = NULL;
char* pDirCur = NULL;
- long hFile;
+ ABC_PTRINT_T hFile;
char c;
Extra_UtilGetoptReset();
@@ -1354,7 +1354,7 @@ void CnfDupFileUnzip( char * pOldName )
int CmdCommandRenameFiles( Abc_Frame_t * pAbc, int argc, char **argv )
{
struct _finddata_t c_file;
- long hFile;
+ ABC_PTRINT_T hFile;
char pNewName[1000];
char * pDirStr = NULL;
char * pDirCur = NULL;
@@ -1515,7 +1515,7 @@ usage:
int CmdCommandLs( Abc_Frame_t * pAbc, int argc, char **argv )
{
struct _finddata_t c_file;
- long hFile;
+ ABC_PTRINT_T hFile;
int fLong = 0;
int fOnlyBLIF = 0;
char Buffer[25];
@@ -1618,7 +1618,7 @@ usage:
int CmdCommandScrGen( Abc_Frame_t * pAbc, int argc, char **argv )
{
struct _finddata_t c_file;
- long hFile;
+ ABC_PTRINT_T hFile;
FILE * pFile = NULL;
char * pFileStr = "test.s";
char * pDirStr = NULL;
diff --git a/src/base/cmd/cmdLoad.c b/src/base/cmd/cmdLoad.c
index accd9440..bd511fec 100644
--- a/src/base/cmd/cmdLoad.c
+++ b/src/base/cmd/cmdLoad.c
@@ -114,7 +114,8 @@ Vec_Ptr_t * CmdCollectFileNames()
{
Vec_Ptr_t * vFileNames;
struct _finddata_t c_file;
- long hFile;
+ //long hFile;
+ ABC_PTRINT_T hFile;
if( (hFile = _findfirst( "*.exe", &c_file )) == -1L )
{
// Abc_Print( 0, "No files with extention \"%s\" in the current directory.\n", "exe" );
diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c
index c6edb3ab..cf7ae5df 100644
--- a/src/base/wlc/wlcBlast.c
+++ b/src/base/wlc/wlcBlast.c
@@ -2588,6 +2588,50 @@ Gia_Man_t * Wlc_BlastArray( char * pFileName )
return pNew;
}
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Wlc_ComputePerm( Wlc_Ntk_t * pNtk, int nPis )
+{
+ Vec_Int_t * vPerm = Vec_IntAlloc( 100 );
+ Vec_Int_t * vSizes = Vec_IntAlloc( 100 );
+ Vec_Int_t * vOffs = Vec_IntAlloc( 100 );
+ Wlc_Obj_t * pObj;
+ int i, k, First, Size, nBitCis = 0, fChange = 1;
+ Wlc_NtkForEachPi( pNtk, pObj, i )
+ {
+ Vec_IntPush( vOffs, nBitCis );
+ Vec_IntPush( vSizes, Wlc_ObjRange(pObj) );
+ nBitCis += Wlc_ObjRange(pObj);
+ }
+ for ( k = 0; fChange; k++ )
+ {
+ fChange = 0;
+ Vec_IntForEachEntryTwo( vOffs, vSizes, First, Size, i )
+ if ( k < Size )
+ {
+ Vec_IntPush( vPerm, First+k );
+ fChange = 1;
+ }
+ }
+ assert( Vec_IntSize(vPerm) == nBitCis );
+ Vec_IntFree( vOffs );
+ Vec_IntFree( vSizes );
+ Vec_IntReverseOrder( vPerm );
+ for ( i = Vec_IntSize(vPerm); i < nPis; i++ )
+ Vec_IntPush( vPerm, i );
+ //Vec_IntPrint( vPerm );
+ return vPerm;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index dd7a3e32..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
@@ -1031,12 +1031,12 @@ int Abc_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Wlc_NtkPrintInputInfo( Wlc_Ntk_t * pNtk );
Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
- Gia_Man_t * pNew = NULL; int c, fMiter = 0, fDumpNames = 0, fPrintInputInfo = 0;
+ Gia_Man_t * pNew = NULL; int c, fMiter = 0, fDumpNames = 0, fPrintInputInfo = 0, fReorder = 0;
Wlc_BstPar_t Par, * pPar = &Par;
Wlc_BstParDefault( pPar );
pPar->nOutputRange = 2;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "ORAMcombqaydestnizvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "ORAMcombqaydestrnizvh" ) ) != EOF )
{
switch ( c )
{
@@ -1118,6 +1118,9 @@ int Abc_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv )
pPar->fCreateMiter ^= 1;
fMiter ^= 1;
break;
+ case 'r':
+ fReorder ^= 1;
+ break;
case 'n':
fDumpNames ^= 1;
break;
@@ -1197,10 +1200,19 @@ int Abc_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( 1, "Finished dumping file \"pio_name_map.txt\" containing PI/PO name mapping.\n" );
}
}
+ if ( fReorder )
+ {
+ extern Vec_Int_t * Wlc_ComputePerm( Wlc_Ntk_t * pNtk, int nPis );
+ Vec_Int_t * vPiPerm = Wlc_ComputePerm( pNtk, Gia_ManPiNum(pNew) );
+ Gia_Man_t * pTemp = Gia_ManDupPerm( pNew, vPiPerm );
+ Vec_IntFree( vPiPerm );
+ Gia_ManStop( pNew );
+ pNew = pTemp;
+ }
Abc_FrameUpdateGia( pAbc, pNew );
return 0;
usage:
- Abc_Print( -2, "usage: %%blast [-ORAM num] [-combqaydestnizvh]\n" );
+ Abc_Print( -2, "usage: %%blast [-ORAM num] [-combqaydestrnizvh]\n" );
Abc_Print( -2, "\t performs bit-blasting of the word-level design\n" );
Abc_Print( -2, "\t-O num : zero-based index of the first word-level PO to bit-blast [default = %d]\n", pPar->iOutput );
Abc_Print( -2, "\t-R num : the total number of word-level POs to bit-blast [default = %d]\n", pPar->nOutputRange );
@@ -1217,6 +1229,7 @@ usage:
Abc_Print( -2, "\t-e : toggle creating miter with output word bits combined [default = %s]\n", pPar->fCreateWordMiter? "yes": "no" );
Abc_Print( -2, "\t-s : toggle creating decoded MUXes [default = %s]\n", pPar->fDecMuxes? "yes": "no" );
Abc_Print( -2, "\t-t : toggle creating regular multi-output miter [default = %s]\n", fMiter? "yes": "no" );
+ Abc_Print( -2, "\t-r : toggle using interleaved variable ordering [default = %s]\n", fReorder? "yes": "no" );
Abc_Print( -2, "\t-n : toggle dumping signal names into a text file [default = %s]\n", fDumpNames? "yes": "no" );
Abc_Print( -2, "\t-i : toggle to print input names after blasting [default = %s]\n", fPrintInputInfo ? "yes": "no" );
Abc_Print( -2, "\t-z : toggle saving flop names after blasting [default = %s]\n", pPar->fSaveFfNames ? "yes": "no" );
diff --git a/src/base/wln/wlnCom.c b/src/base/wln/wlnCom.c
index 3db27785..a010c7c2 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, int fInv );
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, 0 );
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..43003075 100644
--- a/src/base/wln/wlnRead.c
+++ b/src/base/wln/wlnRead.c
@@ -73,6 +73,7 @@ struct Rtl_Ntk_t_
int Slice0; // first slice
int Slice1; // last slice
int iCopy; // place in array
+ int fRoot; // denote root network
};
static inline int Rtl_LibNtkNum( Rtl_Lib_t * pLib ) { return Vec_PtrSize(pLib->vNtks); }
@@ -154,11 +155,13 @@ static inline int Rtl_SigIsConcat( int s ) { ret
#define Rtl_CellForEachOutput( p, pCell, Par, Val, i ) \
Rtl_CellForEachConnect( p, pCell, Par, Val, i ) if ( i < Rtl_CellInputNum(pCell) ) continue; else
+extern Gia_Man_t * Cec4_ManSimulateTest3( Gia_Man_t * p, int nBTLimit, int fVerbose );
+extern int Abc_NtkFromGiaCollapse( Gia_Man_t * pGia );
+
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
-
/**Function*************************************************************
Synopsis []
@@ -335,6 +338,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 +1440,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;
}
}
@@ -1716,16 +1752,34 @@ void Rtl_NtkBlastConnect( Gia_Man_t * pNew, Rtl_Ntk_t * p, int * pCon )
void Rtl_NtkBlastHierarchy( Gia_Man_t * pNew, Rtl_Ntk_t * p, int * pCell )
{
extern Gia_Man_t * Rtl_NtkBlast( Rtl_Ntk_t * p );
- extern void Gia_ManDupRebuild( Gia_Man_t * pNew, Gia_Man_t * p, Vec_Int_t * vLits );
+ extern void Gia_ManDupRebuild( Gia_Man_t * pNew, Gia_Man_t * p, Vec_Int_t * vLits, int fBufs );
+ extern int Gia_ManFindFirst( Rtl_Ntk_t * p, int * pnOuts );
Rtl_Ntk_t * pModel = Rtl_NtkModule( p, Rtl_CellModule(pCell)-ABC_INFINITY );
+ int nOuts1, iFirst1 = Gia_ManFindFirst( pModel, &nOuts1 );
int k, Par, Val, nBits = 0;
+ //printf( "Blasting %s -> %s...\n", Rtl_NtkName(p), Rtl_NtkName(pModel) );
Vec_IntClear( &p->vBitTemp );
Rtl_CellForEachInput( p, pCell, Par, Val, k )
Rtl_NtkCollectSignalRange( p, Val );
// if ( pModel->pGia == NULL )
// pModel->pGia = Rtl_NtkBlast( pModel );
assert( pModel->pGia );
- Gia_ManDupRebuild( pNew, pModel->pGia, &p->vBitTemp );
+ if ( pModel->fRoot )
+ {
+ Vec_IntForEachEntry( &p->vBitTemp, Val, k )
+ Vec_IntWriteEntry( &p->vBitTemp, k, (k >= iFirst1 && k < iFirst1 + nOuts1) ? Gia_ManAppendBuf(pNew, Val) : Val );
+ Vec_IntPush( pNew->vBarBufs, Abc_Var2Lit(pModel->NameId, 0) );
+ }
+ Gia_ManDupRebuild( pNew, pModel->pGia, &p->vBitTemp, !pModel->fRoot );
+ if ( !pModel->fRoot )
+ Vec_IntAppend( pNew->vBarBufs, pModel->pGia->vBarBufs );
+ if ( pModel->fRoot )
+ {
+ Vec_IntForEachEntry( &p->vBitTemp, Val, k )
+ Vec_IntWriteEntry( &p->vBitTemp, k, Gia_ManAppendBuf(pNew, Val) );
+ Vec_IntPush( pNew->vBarBufs, Abc_Var2Lit(pModel->NameId, 1) );
+ printf( "Added %d and %d output buffers for module %s.\n", nOuts1, Vec_IntSize(&p->vBitTemp), Rtl_NtkName(pModel) );
+ }
Rtl_CellForEachOutput( p, pCell, Par, Val, k )
nBits += Rtl_NtkInsertSignalRange( p, Val, Vec_IntArray(&p->vBitTemp)+nBits, Vec_IntSize(&p->vBitTemp)-nBits );
assert( nBits == Vec_IntSize(&p->vBitTemp) );
@@ -1787,6 +1841,16 @@ char * Rtl_ShortenName( char * pName, int nSize )
Buffer[nSize-0] = 0;
return Buffer;
}
+void Rtl_NtkPrintBufs( Rtl_Ntk_t * p, Vec_Int_t * vBufs )
+{
+ int i, Lit;
+ if ( Vec_IntSize(vBufs) )
+ printf( "Found %d buffers: ", p->pGia->nBufs );
+ Vec_IntForEachEntry( vBufs, Lit, i )
+ printf( "%s (%c) ", Rtl_LibStr(p->pLib, Abc_Lit2Var(Lit)), Abc_LitIsCompl(Lit)? 'o' : 'i' );
+ if ( Vec_IntSize(vBufs) )
+ printf( "\n" );
+}
Gia_Man_t * Rtl_NtkBlast( Rtl_Ntk_t * p )
{
Gia_Man_t * pTemp, * pNew = Gia_ManStart( 1000 );
@@ -2034,6 +2098,7 @@ printf( "Blasting %s...\r", Rtl_NtkName(p) );
Rtl_NtkBlastMap( p, nBits );
assert( p->pGia == NULL );
p->pGia = Gia_ManStart( 1000 );
+ p->pGia->vBarBufs = Vec_IntAlloc( 1000 );
Rtl_NtkBlastInputs( p->pGia, p );
Gia_ManHashAlloc( p->pGia );
for ( i = 0; i < p->nOutputs; i++ )
@@ -2047,7 +2112,10 @@ printf( "Blasting %s...\r", Rtl_NtkName(p) );
Rtl_NtkBlastOutputs( p->pGia, p );
Rtl_NtkMapWires( p, 1 );
p->pGia = Gia_ManCleanup( pTemp = p->pGia );
+ ABC_SWAP( Vec_Int_t *, p->pGia->vBarBufs, pTemp->vBarBufs );
Gia_ManStop( pTemp );
+// if ( p->fRoot )
+// Rtl_NtkPrintBufs( p, p->pGia->vBarBufs );
sprintf( Buffer, "new%02d.aig", counter++ );
Gia_AigerWrite( p->pGia, Buffer, 0, 0, 0 );
@@ -2055,12 +2123,80 @@ 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, int fInv )
+{
+ 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, pNtk->fRoot = 0;
+ Vec_IntForEachEntry( vRoots, iNtk, i )
+ {
+ Rtl_Ntk_t * pNtk = Rtl_LibNtk(pLib, iNtk);
+ pNtk->fRoot = fInv;
+ Rtl_LibMark_rec( pNtk );
+ }
+ }
+ 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 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;
+ }
+ if ( Type != Rtl_LibStrId(p, "equal") )
+ continue;
+ 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,17 +2249,19 @@ finish:
if ( p != p1 && p != p2 )
Gia_ManStopP( &p->pGia );
//Rtl_LibBlast( pLib );
- Rtl_LibBlast2( pLib );
+ Rtl_LibBlast2( pLib, NULL, 0 );
}
void Rtl_LibSolve( Rtl_Lib_t * pLib, void * pNtk )
{
- extern Gia_Man_t * Cec4_ManSimulateTest3( Gia_Man_t * p, int nBTLimit, int fVerbose );
+ extern Gia_Man_t * Gia_ManReduceBuffers( Rtl_Lib_t * pLib, Gia_Man_t * p );
abctime clk = Abc_Clock(); int Status;
- Rtl_Ntk_t * pTop = pNtk ? (Rtl_Ntk_t *)pNtk : Rtl_LibTop( pLib );
- Gia_Man_t * pSwp = Cec4_ManSimulateTest3( pTop->pGia, 1000000, 0 );
- int RetValue = Gia_ManAndNum(pSwp) == 0;
+ Rtl_Ntk_t * pTop = pNtk ? (Rtl_Ntk_t *)pNtk : Rtl_LibTop( pLib );
+ Gia_Man_t * pGia2 = Gia_ManReduceBuffers( pLib, pTop->pGia );
+ Gia_Man_t * pSwp = Cec4_ManSimulateTest3( pGia2, 1000000, 0 );
+ int RetValue = Gia_ManAndNum(pSwp);
Gia_ManStop( pSwp );
- if ( RetValue )
+ Gia_ManStop( pGia2 );
+ if ( RetValue == 0 )
printf( "Verification problem solved after SAT sweeping! " );
else
{
@@ -2135,7 +2273,7 @@ void Rtl_LibSolve( Rtl_Lib_t * pLib, void * pNtk )
if ( Status == 1 )
printf( "Verification problem solved after CEC! " );
else
- printf( "Verification problem is NOT solved! " );
+ printf( "Verification problem is NOT solved (miter has %d nodes)! ", RetValue );
}
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
@@ -2154,55 +2292,231 @@ void Rtl_LibSolve( Rtl_Lib_t * pLib, void * pNtk )
***********************************************************************/
void Wln_SolveEqual( Rtl_Lib_t * p, int iNtk1, int iNtk2 )
{
+ abctime clk = Abc_Clock();
Rtl_Ntk_t * pNtk1 = Rtl_LibNtk( p, iNtk1 );
Rtl_Ntk_t * pNtk2 = Rtl_LibNtk( p, iNtk2 );
- printf( "Proving equivalence of \"%s\" and \"%s\".\n", Rtl_NtkName(pNtk1), Rtl_NtkName(pNtk2) );
-/*
+ printf( "\nProving equivalence of \"%s\" and \"%s\"...\n", Rtl_NtkName(pNtk1), Rtl_NtkName(pNtk2) );
if ( Gia_ManCiNum(pNtk1->pGia) != Gia_ManCiNum(pNtk2->pGia) ||
Gia_ManCoNum(pNtk1->pGia) != Gia_ManCoNum(pNtk2->pGia) )
{
printf( "The number of inputs/outputs does not match.\n" );
}
+ else if ( 1 )
+ {
+ Gia_Man_t * pGia = Gia_ManMiter( pNtk1->pGia, pNtk2->pGia, 0, 0, 0, 0, 0 );
+ if ( Abc_NtkFromGiaCollapse( pGia ) )
+ Abc_Print( 1, "Networks are equivalent after collapsing. " );
+ else
+ {
+ Gia_Man_t * pNew = Cec4_ManSimulateTest3( pGia, 10000000, 0 );
+ //printf( "Miter %d -> %d\n", Gia_ManAndNum(pGia), Gia_ManAndNum(pNew) );
+ if ( Gia_ManAndNum(pNew) == 0 )
+ Abc_Print( 1, "Networks are equivalent. " );
+ else
+ Abc_Print( 1, "Networks are UNDECIDED. " );
+ Gia_ManStopP( &pNew );
+ Gia_ManStopP( &pGia );
+ }
+ }
else
{
int Status = Cec_ManVerifyTwo( pNtk1->pGia, pNtk2->pGia, 0 );
if ( Status == 1 )
- printf( "The networks are equivalence.\n" );
+ printf( "The networks are equivalent. " );
else
- printf( "The networks are NOT equivalent.\n" );
+ printf( "The networks are NOT equivalent. " );
}
-*/
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+}
+int Gia_ManFindFirst( Rtl_Ntk_t * p, int * pnOuts )
+{
+ int i, * pWire, Counts[4] = {0}, nBits = 0;
+ assert( p->nOutputs == 1 );
+ Rtl_NtkForEachWire( p, pWire, i )
+ {
+ if ( pWire[0] & 1 ) // PI
+ Counts[0]++, Counts[1] += pWire[1];
+ if ( pWire[0] & 2 ) // PO
+ Counts[2]++, Counts[3] += pWire[1];
+ }
+ assert( p->nInputs == Counts[0] );
+ assert( p->nOutputs == Counts[2] );
+ *pnOuts = Counts[3];
+ Rtl_NtkForEachWire( p, pWire, i )
+ {
+ if ( pWire[0] & 1 ) // PI
+ {
+ if ( pWire[1] == Counts[3] )
+ return nBits;
+ nBits += pWire[1];
+ }
+ }
+ return -1;
+}
+Gia_Man_t * Gia_ManMoveSharedFirst( Gia_Man_t * pGia, int iFirst, int nBits )
+{
+ Vec_Int_t * vPiPerm = Vec_IntAlloc( Gia_ManPiNum(pGia) );
+ Gia_Man_t * pTemp; int i, n;
+ for ( n = 0; n < 2; n++ )
+ for ( i = 0; i < Gia_ManPiNum(pGia); i++ )
+ if ( n == (i >= iFirst && i < iFirst + nBits) )
+ Vec_IntPush( vPiPerm, i );
+ pTemp = Gia_ManDupPerm( pGia, vPiPerm );
+ if ( pGia->vBarBufs )
+ pTemp->vBarBufs = Vec_IntDup( pGia->vBarBufs );
+ Vec_IntFree( vPiPerm );
+ return pTemp;
+}
+Vec_Int_t * Gia_ManCollectBufs( Gia_Man_t * p, int iFirst, int nBufs )
+{
+ Vec_Int_t * vRes = Vec_IntAlloc( 100 );
+ Gia_Obj_t * pObj; int i, iBuf = 0;
+ assert( iFirst >= 0 && iFirst + nBufs < p->nBufs );
+ Gia_ManForEachAnd( p, pObj, i )
+ {
+ if ( Gia_ObjIsBuf(pObj) && iBuf >= iFirst && iBuf < iFirst + nBufs )
+ Vec_IntPush( vRes, i );
+ iBuf += Gia_ObjIsBuf(pObj);
+ }
+ assert( iBuf == p->nBufs );
+ return vRes;
+}
+Gia_Man_t * Gia_ManReduceBuffers( Rtl_Lib_t * pLib, Gia_Man_t * p )
+{
+ Gia_Man_t * pNew;
+ Vec_Int_t * vMap = Vec_IntStartFull( Gia_ManObjNum(p) );
+ Vec_Int_t * vOne = Gia_ManCollectBufs( p, 0, 64 );
+ Vec_Int_t * vTwo = Gia_ManCollectBufs( p, 1280-64, 64 );
+ //Vec_Int_t * vOne = Gia_ManCollectBufs( p, 0, 1280/2 );
+ //Vec_Int_t * vTwo = Gia_ManCollectBufs( p, 1280/2, 1280/2 );
+ int i, One, Two;
+ printf( "Reducing %d buffers... Size(vOne) = %d. Size(vTwo) = %d. \n", p->nBufs, Vec_IntSize(vOne), Vec_IntSize(vTwo) );
+ assert( p->nBufs == 1280 );
+ Vec_IntForEachEntryTwo( vOne, vTwo, One, Two, i )
+ Vec_IntWriteEntry( vMap, Two, One );
+ Vec_IntFree( vOne );
+ Vec_IntFree( vTwo );
+Gia_ManPrintStats( p, NULL );
+ //pNew = Gia_ManDupNoBuf( p );
+ pNew = Gia_ManDupMap( p, vMap );
+Gia_ManPrintStats( pNew, NULL );
+ Vec_IntFree( vMap );
+ //Rtl_NtkPrintBufs( pNtk1, pGia->vBarBufs );
+ //printf( "Found %d buffers.\n", p->nBufs );
+ return pNew;
}
void Wln_SolveInverse( Rtl_Lib_t * p, int iNtk1, int iNtk2 )
{
+ abctime clk = Abc_Clock();
Rtl_Ntk_t * pNtk1 = Rtl_LibNtk( p, iNtk1 );
Rtl_Ntk_t * pNtk2 = Rtl_LibNtk( p, iNtk2 );
- printf( "Proving inverse equivalence of \"%s\" and \"%s\".\n", Rtl_NtkName(pNtk1), Rtl_NtkName(pNtk2) );
+ int Res = printf( "\nProving inverse equivalence of \"%s\" and \"%s\".\n", Rtl_NtkName(pNtk1), Rtl_NtkName(pNtk2) );
+ int nOuts1, iFirst1 = Gia_ManFindFirst( pNtk1, &nOuts1 );
+ int nOuts2, iFirst2 = Gia_ManFindFirst( pNtk2, &nOuts2 );
+ Gia_Man_t * pGia1 = Gia_ManMoveSharedFirst( pNtk1->pGia, iFirst1, nOuts1 );
+ Gia_Man_t * pGia2 = Gia_ManMoveSharedFirst( pNtk2->pGia, iFirst2, nOuts2 );
+ if ( 1 )
+ {
+ char * pFileName = "inv_miter.aig";
+ Gia_Man_t * pGia = Gia_ManMiterInverse( pGia1, pGia2, 0, 0 );
+ //Gia_Man_t * pGia2 = Gia_ManReduceBuffers( p, pGia );
+ Gia_Man_t * pGia2 = Gia_ManDupNoBuf( pGia );
+ printf( "Dumping inverse miter into file \"%s\".\n", pFileName );
+ Gia_AigerWrite( pGia2, pFileName, 0, 0, 0 );
+ if ( Abc_NtkFromGiaCollapse( pGia2 ) )
+ Abc_Print( 1, "Networks are equivalent after collapsing. " );
+ else
+ {
+ Gia_Man_t * pNew = Cec4_ManSimulateTest3( pGia2, 10000000, 0 );
+ Rtl_NtkPrintBufs( pNtk1, pGia->vBarBufs );
+ //printf( "Miter %d -> %d\n", Gia_ManAndNum(pGia), Gia_ManAndNum(pNew) );
+ if ( Gia_ManAndNum(pNew) == 0 )
+ Abc_Print( 1, "Networks are equivalent. " );
+ else
+ Abc_Print( 1, "Networks are UNDECIDED. " );
+ Gia_ManStopP( &pNew );
+ }
+ Gia_ManStopP( &pGia2 );
+ Gia_ManStopP( &pGia );
+ }
+ else
+ {
+ int Status = Cec_ManVerifyTwoInv( pGia1, pGia2, 0 );
+ if ( Status == 1 )
+ printf( "The networks are equivalent. " );
+ else
+ printf( "The networks are NOT equivalent. " );
+ }
+ Res = 0;
+ Gia_ManStopP( &pGia1 );
+ Gia_ManStopP( &pGia2 );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
void Wln_SolveProperty( Rtl_Lib_t * p, int iNtk )
{
Rtl_Ntk_t * pNtk = Rtl_LibNtk( p, iNtk );
- printf( "Proving property \"%s\".\n", Rtl_NtkName(pNtk) );
+ printf( "\nProving property \"%s\".\n", Rtl_NtkName(pNtk) );
+ Rtl_NtkPrintBufs( pNtk, pNtk->pGia->vBarBufs );
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, fInv = 0;
+ Vec_WecForEachLevel( vGuide, vLevel, i )
+ if ( Vec_IntEntry( vLevel, 1 ) == Rtl_LibStrId(p, "inverse") )
+ fInv = 1;
Vec_IntFillExtra( p->vMap, Abc_NamObjNumMax(p->pManName), -1 );
- Rtl_LibBlast2( p );
- for ( i = 0; i < Vec_IntSize(vGuide); i += 4 )
- {
- 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 );
+ Rtl_LibSetReplace( p, vGuide );
+ Rtl_LibUpdateBoxes( p );
+ Rtl_LibReorderModules( p );
+ vRoots = Wln_ReadNtkRoots( p, vGuide );
+ Rtl_LibBlast2( p, vRoots, fInv );
+ Vec_WecForEachLevel( vGuide, vLevel, i )
+ {
+ 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 +2529,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 2025-02-05 15:15:42 +0000