summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/aig/gia/gia.h2
-rw-r--r--src/aig/gia/giaDup.c90
-rw-r--r--src/base/abci/abc.c1
-rw-r--r--src/base/abci/abcDar.c27
-rw-r--r--src/base/wln/wlnCom.c4
-rw-r--r--src/base/wln/wlnRead.c150
6 files changed, 241 insertions, 33 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index d871905c..488f12cf 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -1312,6 +1312,8 @@ extern Gia_Man_t * Gia_ManDupLastPis( Gia_Man_t * p, int nLastPis );
extern Gia_Man_t * Gia_ManDupFlip( Gia_Man_t * p, int * pInitState );
extern Gia_Man_t * Gia_ManDupCycled( Gia_Man_t * pAig, Abc_Cex_t * pCex, int nFrames );
extern Gia_Man_t * Gia_ManDup( Gia_Man_t * p );
+extern Gia_Man_t * Gia_ManDupNoBuf( Gia_Man_t * p );
+extern Gia_Man_t * Gia_ManDupMap( Gia_Man_t * p, Vec_Int_t * vMap );
extern Gia_Man_t * Gia_ManDup2( Gia_Man_t * p1, Gia_Man_t * p2 );
extern Gia_Man_t * Gia_ManDupWithAttributes( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupRemovePis( Gia_Man_t * p, int nRemPis );
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 55f8901f..4f094b48 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -811,6 +811,55 @@ Gia_Man_t * Gia_ManDupRemovePis( Gia_Man_t * p, int nRemPis )
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
return pNew;
}
+Gia_Man_t * Gia_ManDupNoBuf( Gia_Man_t * p )
+{
+ Gia_Man_t * pNew;
+ Gia_Obj_t * pObj;
+ int i;
+ pNew = Gia_ManStart( Gia_ManObjNum(p) );
+ pNew->pName = Abc_UtilStrsav( p->pName );
+ pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+ Gia_ManConst0(p)->Value = 0;
+ Gia_ManForEachObj1( p, pObj, i )
+ {
+ if ( Gia_ObjIsBuf(pObj) )
+ pObj->Value = Gia_ObjFanin0Copy(pObj);
+ else if ( Gia_ObjIsAnd(pObj) )
+ pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+ else if ( Gia_ObjIsCi(pObj) )
+ pObj->Value = Gia_ManAppendCi( pNew );
+ else if ( Gia_ObjIsCo(pObj) )
+ pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+ }
+ Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+ return pNew;
+}
+Gia_Man_t * Gia_ManDupMap( Gia_Man_t * p, Vec_Int_t * vMap )
+{
+ Gia_Man_t * pNew, * pTemp;
+ Gia_Obj_t * pObj;
+ int i;
+ pNew = Gia_ManStart( Gia_ManObjNum(p) );
+ pNew->pName = Abc_UtilStrsav( p->pName );
+ pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+ Gia_ManConst0(p)->Value = 0;
+ Gia_ManHashAlloc( pNew );
+ Gia_ManForEachObj1( p, pObj, i )
+ {
+ if ( Vec_IntEntry(vMap, i) >= 0 )
+ pObj->Value = Gia_ManObj( p, Vec_IntEntry(vMap, i) )->Value;
+ else if ( Gia_ObjIsAnd(pObj) )
+ pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+ else if ( Gia_ObjIsCi(pObj) )
+ pObj->Value = Gia_ManAppendCi( pNew );
+ else if ( Gia_ObjIsCo(pObj) )
+ pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+ }
+ pNew = Gia_ManCleanup( pTemp = pNew );
+ Gia_ManStop( pTemp );
+ Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+ return pNew;
+}
/**Function*************************************************************
@@ -865,7 +914,9 @@ Gia_Man_t * Gia_ManDupPerm( Gia_Man_t * p, Vec_Int_t * vPiPerm )
// Vec_IntFree( vPiPermInv );
Gia_ManForEachObj1( p, pObj, i )
{
- if ( Gia_ObjIsAnd(pObj) )
+ if ( Gia_ObjIsBuf(pObj) )
+ pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
+ else if ( Gia_ObjIsAnd(pObj) )
pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
else if ( Gia_ObjIsCi(pObj) )
{
@@ -1086,7 +1137,7 @@ Gia_Man_t * Gia_ManDupAppendNew( Gia_Man_t * pOne, Gia_Man_t * pTwo )
Gia_ManSetRegNum( pNew, Gia_ManRegNum(pOne) + Gia_ManRegNum(pTwo) );
return pNew;
}
-void Gia_ManDupRebuild( Gia_Man_t * pNew, Gia_Man_t * p, Vec_Int_t * vLits )
+void Gia_ManDupRebuild( Gia_Man_t * pNew, Gia_Man_t * p, Vec_Int_t * vLits, int fBufs )
{
Gia_Obj_t * pObj; int i;
assert( Vec_IntSize(vLits) == Gia_ManCiNum(p) );
@@ -1094,7 +1145,10 @@ void Gia_ManDupRebuild( Gia_Man_t * pNew, Gia_Man_t * p, Vec_Int_t * vLits )
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Vec_IntEntry(vLits, i);
Gia_ManForEachAnd( p, pObj, i )
- pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+ if ( fBufs && Gia_ObjIsBuf(pObj) )
+ pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
+ else
+ pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
Vec_IntClear( vLits );
Gia_ManForEachCo( p, pObj, i )
Vec_IntPush( vLits, Gia_ObjFanin0Copy(pObj) );
@@ -2980,8 +3034,15 @@ Gia_Man_t * Gia_ManMiterInverse( Gia_Man_t * pBot, Gia_Man_t * pTop, int fDualOu
Gia_ManHashAlloc( pNew );
Gia_ManForEachCi( pBot, pObj, i )
pObj->Value = Gia_ManAppendCi( pNew );
- Gia_ManForEachCo( pBot, pObj, i )
- Gia_ManMiter_rec( pNew, pBot, Gia_ObjFanin0(pObj) );
+// Gia_ManForEachCo( pBot, pObj, i )
+// Gia_ManMiter_rec( pNew, pBot, Gia_ObjFanin0(pObj) );
+ Gia_ManForEachAnd( pBot, pObj, i )
+ {
+ if ( Gia_ObjIsBuf(pObj) )
+ pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
+ else if ( Gia_ObjIsAnd(pObj) )
+ pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+ }
Gia_ManForEachCo( pBot, pObj, i )
pObj->Value = Gia_ObjFanin0Copy(pObj);
Gia_ManForEachCi( pTop, pObj, i )
@@ -2989,8 +3050,15 @@ Gia_Man_t * Gia_ManMiterInverse( Gia_Man_t * pBot, Gia_Man_t * pTop, int fDualOu
pObj->Value = Gia_ManCi(pBot, i)->Value;
else
pObj->Value = Gia_ManCo(pBot, i-nInputs1)->Value;
- Gia_ManForEachCo( pTop, pObj, i )
- Gia_ManMiter_rec( pNew, pTop, Gia_ObjFanin0(pObj) );
+// Gia_ManForEachCo( pTop, pObj, i )
+// Gia_ManMiter_rec( pNew, pTop, Gia_ObjFanin0(pObj) );
+ Gia_ManForEachAnd( pTop, pObj, i )
+ {
+ if ( Gia_ObjIsBuf(pObj) )
+ pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
+ else if ( Gia_ObjIsAnd(pObj) )
+ pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+ }
Gia_ManForEachCo( pTop, pObj, i )
{
if ( fDualOut )
@@ -3007,6 +3075,14 @@ Gia_Man_t * Gia_ManMiterInverse( Gia_Man_t * pBot, Gia_Man_t * pTop, int fDualOu
Gia_ManHashStop( pNew );
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
+ assert( (pBot->vBarBufs == NULL) == (pTop->vBarBufs == NULL) );
+ if ( pBot->vBarBufs )
+ {
+ pNew->vBarBufs = Vec_IntAlloc( 1000 );
+ Vec_IntAppend( pNew->vBarBufs, pBot->vBarBufs );
+ Vec_IntAppend( pNew->vBarBufs, pTop->vBarBufs );
+ //printf( "Miter has %d buffers (%d groups).\n", pNew->nBufs, Vec_IntSize(pNew->vBarBufs) );
+ }
return pNew;
}
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 06d7cb08..db0446c9 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -13996,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" );
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/wln/wlnCom.c b/src/base/wln/wlnCom.c
index 90ac4faa..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, Vec_Int_t * vRoots );
+ 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, NULL );
+ Rtl_LibBlast2( pLib, NULL, 0 );
if ( fPrepro )
Rtl_LibPreprocess( pLib );
Rtl_LibSolve( pLib, NULL );
diff --git a/src/base/wln/wlnRead.c b/src/base/wln/wlnRead.c
index 95d2dd31..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); }
@@ -155,6 +156,7 @@ static inline int Rtl_SigIsConcat( int s ) { ret
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 ///
@@ -1750,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) );
@@ -1821,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 );
@@ -2068,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++ )
@@ -2081,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 );
@@ -2103,7 +2137,7 @@ void Rtl_LibMark_rec( Rtl_Ntk_t * pNtk )
assert( pNtk->iCopy == -2 );
pNtk->iCopy = -1;
}
-void Rtl_LibBlast2( Rtl_Lib_t * pLib, Vec_Int_t * vRoots )
+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 )
@@ -2111,9 +2145,13 @@ void Rtl_LibBlast2( Rtl_Lib_t * pLib, Vec_Int_t * vRoots )
if ( vRoots )
{
Vec_PtrForEachEntry( Rtl_Ntk_t *, pLib->vNtks, pNtk, i )
- pNtk->iCopy = -2;
+ pNtk->iCopy = -2, pNtk->fRoot = 0;
Vec_IntForEachEntry( vRoots, iNtk, i )
- Rtl_LibMark_rec( Rtl_LibNtk(pLib, iNtk) );
+ {
+ 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 )
@@ -2211,15 +2249,18 @@ finish:
if ( p != p1 && p != p2 )
Gia_ManStopP( &p->pGia );
//Rtl_LibBlast( pLib );
- Rtl_LibBlast2( pLib, NULL );
+ Rtl_LibBlast2( pLib, NULL, 0 );
}
void Rtl_LibSolve( Rtl_Lib_t * pLib, void * pNtk )
{
+ 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 );
+ 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 );
+ Gia_ManStop( pGia2 );
if ( RetValue == 0 )
printf( "Verification problem solved after SAT sweeping! " );
else
@@ -2263,14 +2304,19 @@ void Wln_SolveEqual( Rtl_Lib_t * p, int iNtk1, int iNtk2 )
else if ( 1 )
{
Gia_Man_t * pGia = Gia_ManMiter( pNtk1->pGia, pNtk2->pGia, 0, 0, 0, 0, 0 );
- 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. " );
+ if ( Abc_NtkFromGiaCollapse( pGia ) )
+ Abc_Print( 1, "Networks are equivalent after collapsing. " );
else
- Abc_Print( 1, "Networks are UNDECIDED. " );
- Gia_ManStopP( &pNew );
- Gia_ManStopP( &pGia );
+ {
+ 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
{
@@ -2284,7 +2330,7 @@ void Wln_SolveEqual( Rtl_Lib_t * p, int iNtk1, int iNtk2 )
}
int Gia_ManFindFirst( Rtl_Ntk_t * p, int * pnOuts )
{
- int i, * pWire, iFirst = -1, Counts[4] = {0}, nBits = 0;
+ int i, * pWire, Counts[4] = {0}, nBits = 0;
assert( p->nOutputs == 1 );
Rtl_NtkForEachWire( p, pWire, i )
{
@@ -2316,9 +2362,49 @@ Gia_Man_t * Gia_ManMoveSharedFirst( Gia_Man_t * pGia, int iFirst, int nBits )
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();
@@ -2331,14 +2417,26 @@ void Wln_SolveInverse( Rtl_Lib_t * p, int iNtk1, int iNtk2 )
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 * 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. " );
+ //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
- Abc_Print( 1, "Networks are UNDECIDED. " );
- Gia_ManStopP( &pNew );
+ {
+ 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
@@ -2358,6 +2456,7 @@ void Wln_SolveProperty( Rtl_Lib_t * p, int iNtk )
{
Rtl_Ntk_t * pNtk = Rtl_LibNtk( p, iNtk );
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 )
@@ -2390,13 +2489,16 @@ void Wln_SolveWithGuidance( char * pFileName, Rtl_Lib_t * p )
{
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_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_LibSetReplace( p, vGuide );
Rtl_LibUpdateBoxes( p );
Rtl_LibReorderModules( p );
vRoots = Wln_ReadNtkRoots( p, vGuide );
- Rtl_LibBlast2( p, vRoots );
+ Rtl_LibBlast2( p, vRoots, fInv );
Vec_WecForEachLevel( vGuide, vLevel, i )
{
int Prove = Vec_IntEntry( vLevel, 0 );
generated by cgit v1.2.3 (git 2.25.1) at 2025-11-04 05:15:23 +0000