summaryrefslogtreecommitdiffstats
path: root/src/base/abci
diff options
context:
space:
mode:
Diffstat (limited to 'src/base/abci')
-rw-r--r--src/base/abci/abc.c132
-rw-r--r--src/base/abci/abcDar.c97
2 files changed, 152 insertions, 77 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 789d2714..f7caad5d 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -40,6 +40,7 @@
#include "cgt.h"
#include "amap.h"
#include "cec.h"
+#include "giaAbs.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@@ -322,6 +323,8 @@ extern int Abc_CommandAbcLivenessToSafetySim ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbcTestNew ( Abc_Frame_t * pAbc, int argc, char ** argv );
+extern Aig_Man_t * Ntl_ManExtract( void * p );
+
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -18807,40 +18810,18 @@ usage:
***********************************************************************/
int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv )
{
+ Gia_ParAbs_t Pars, * pPars = &Pars;
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk, * pNtkRes;
- int nFramesMax;
- int nConfMax;
- int fDynamic;
- int fExtend;
- int fSkipProof;
- int nFramesBmc;
- int nConfMaxBmc;
- int nRatio;
- int fUseBdds;
- int fUseDprove;
- int fUseStart;
- int fVerbose;
int c;
- extern Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int nRatio, int fUseBdds, int fUseDprove, int fUseStart, int fVerbose );
+ extern Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, Gia_ParAbs_t * pPars );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
- nFramesMax = 10;
- nConfMax = 10000;
- fDynamic = 1;
- fExtend = 0;
- fSkipProof = 0;
- nFramesBmc = 2000;
- nConfMaxBmc = 5000;
- nRatio = 10;
- fUseBdds = 0;
- fUseDprove = 0;
- fUseStart = 1;
- fVerbose = 0;
+ Gia_ManAbsSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FCGDRdesrpfvh" ) ) != EOF )
{
@@ -18852,9 +18833,9 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
goto usage;
}
- nFramesMax = atoi(argv[globalUtilOptind]);
+ pPars->nFramesMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
- if ( nFramesMax < 0 )
+ if ( pPars->nFramesMax < 0 )
goto usage;
break;
case 'C':
@@ -18863,9 +18844,9 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
goto usage;
}
- nConfMax = atoi(argv[globalUtilOptind]);
+ pPars->nConfMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
- if ( nConfMax < 0 )
+ if ( pPars->nConfMax < 0 )
goto usage;
break;
case 'G':
@@ -18874,9 +18855,9 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Command line switch \"-G\" should be followed by an integer.\n" );
goto usage;
}
- nFramesBmc = atoi(argv[globalUtilOptind]);
+ pPars->nFramesBmc = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
- if ( nFramesBmc < 0 )
+ if ( pPars->nFramesBmc < 0 )
goto usage;
break;
case 'D':
@@ -18885,9 +18866,9 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Command line switch \"-D\" should be followed by an integer.\n" );
goto usage;
}
- nConfMaxBmc = atoi(argv[globalUtilOptind]);
+ pPars->nConfMaxBmc = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
- if ( nConfMaxBmc < 0 )
+ if ( pPars->nConfMaxBmc < 0 )
goto usage;
break;
case 'R':
@@ -18896,31 +18877,31 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Command line switch \"-R\" should be followed by an integer.\n" );
goto usage;
}
- nRatio = atoi(argv[globalUtilOptind]);
+ pPars->nRatio = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
- if ( nRatio < 0 )
+ if ( pPars->nRatio < 0 )
goto usage;
break;
case 'd':
- fDynamic ^= 1;
+ pPars->fDynamic ^= 1;
break;
case 'e':
- fExtend ^= 1;
+ pPars->fExtend ^= 1;
break;
case 's':
- fSkipProof ^= 1;
+ pPars->fSkipProof ^= 1;
break;
case 'r':
- fUseBdds ^= 1;
+ pPars->fUseBdds ^= 1;
break;
case 'p':
- fUseDprove ^= 1;
+ pPars->fUseDprove ^= 1;
break;
case 'f':
- fUseStart ^= 1;
+ pPars->fUseStart ^= 1;
break;
case 'v':
- fVerbose ^= 1;
+ pPars->fVerbose ^= 1;
break;
case 'h':
goto usage;
@@ -18943,18 +18924,18 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( stdout, "Currently only works for structurally hashed circuits.\n" );
return 0;
}
- if ( !(0 <= nRatio && nRatio <= 100) )
+ if ( !(0 <= pPars->nRatio && pPars->nRatio <= 100) )
{
fprintf( stdout, "Wrong value of parameter \"-R <num>\".\n" );
return 0;
}
// modify the current network
- pNtkRes = Abc_NtkDarPBAbstraction( pNtk, nFramesMax, nConfMax, fDynamic, fExtend, fSkipProof, nFramesBmc, nConfMaxBmc, nRatio, fUseBdds, fUseDprove, fUseStart, fVerbose );
+ pNtkRes = Abc_NtkDarPBAbstraction( pNtk, pPars );
if ( pNtkRes == NULL )
{
if ( pNtk->pSeqModel == NULL )
- printf( "Proof-based abstraction has failed.\n" );
+ printf( "Abstraction has failed.\n" );
return 0;
}
// replace the current network
@@ -18964,18 +18945,18 @@ usage:
fprintf( pErr, "usage: abs [-FCGDR num] [-desrpfvh]\n" );
fprintf( pErr, "\t proof-based abstraction (PBA) using UNSAT core of BMC\n" );
fprintf( pErr, "\t followed by counter-example-based abstraction\n" );
- fprintf( pErr, "\t-F num : the max number of timeframes for PBA [default = %d]\n", nFramesMax );
- fprintf( pErr, "\t-C num : the max number of conflicts by SAT solver for PBA [default = %d]\n", nConfMax );
- fprintf( pErr, "\t-G num : the max number of timeframes for BMC [default = %d]\n", nFramesBmc );
- fprintf( pErr, "\t-D num : the max number of conflicts by SAT solver for BMC [default = %d]\n", nConfMaxBmc );
- fprintf( pErr, "\t-R num : the %% of abstracted flops when refinement stops (0<=num<=100) [default = %d]\n", nRatio );
- fprintf( pErr, "\t-d : toggle dynamic unrolling of timeframes [default = %s]\n", fDynamic? "yes": "no" );
- fprintf( pErr, "\t-e : toggle extending abstraction using COI of flops [default = %s]\n", fExtend? "yes": "no" );
- fprintf( pErr, "\t-s : toggle skipping proof-based abstraction [default = %s]\n", fSkipProof? "yes": "no" );
- fprintf( pErr, "\t-r : toggle using BDD-based reachability for filtering [default = %s]\n", fUseBdds? "yes": "no" );
- fprintf( pErr, "\t-p : toggle using \"dprove\" for filtering [default = %s]\n", fUseDprove? "yes": "no" );
- fprintf( pErr, "\t-f : toggle starting BMC from a later frame [default = %s]\n", fUseStart? "yes": "no" );
- fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+ fprintf( pErr, "\t-F num : the max number of timeframes for PBA [default = %d]\n", pPars->nFramesMax );
+ fprintf( pErr, "\t-C num : the max number of conflicts by SAT solver for PBA [default = %d]\n", pPars->nConfMax );
+ fprintf( pErr, "\t-G num : the max number of timeframes for BMC [default = %d]\n", pPars->nFramesBmc );
+ fprintf( pErr, "\t-D num : the max number of conflicts by SAT solver for BMC [default = %d]\n", pPars->nConfMaxBmc );
+ fprintf( pErr, "\t-R num : the %% of abstracted flops when refinement stops (0<=num<=100) [default = %d]\n", pPars->nRatio );
+ fprintf( pErr, "\t-d : toggle dynamic unrolling of timeframes [default = %s]\n", pPars->fDynamic? "yes": "no" );
+ fprintf( pErr, "\t-e : toggle extending abstraction using COI of flops [default = %s]\n", pPars->fExtend? "yes": "no" );
+ fprintf( pErr, "\t-s : toggle skipping proof-based abstraction [default = %s]\n", pPars->fSkipProof? "yes": "no" );
+ fprintf( pErr, "\t-r : toggle using BDD-based reachability for filtering [default = %s]\n", pPars->fUseBdds? "yes": "no" );
+ fprintf( pErr, "\t-p : toggle using \"dprove\" for filtering [default = %s]\n", pPars->fUseDprove? "yes": "no" );
+ fprintf( pErr, "\t-f : toggle starting BMC from a later frame [default = %s]\n", pPars->fUseStart? "yes": "no" );
+ fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
@@ -19129,7 +19110,6 @@ int Abc_CommandAbc8Read( Abc_Frame_t * pAbc, int argc, char ** argv )
int fAlter;
extern void * Ioa_ReadBlif( char * pFileName, int fCheck );
extern void Ioa_WriteBlif( void * p, char * pFileName );
- extern Aig_Man_t * Ntl_ManExtract( void * p );
extern void * Ntl_ManExtractNwk( void * p, Aig_Man_t * pAig, Tim_Man_t * pManTime );
extern void Ntl_ManPrintStats( void * p );
@@ -21083,7 +21063,6 @@ int Abc_CommandAbc8Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
int nConfLimit;
int nLevelMax;
int fUseCSat;
- extern Aig_Man_t * Ntl_ManExtract( void * p );
extern void * Ntl_ManFraig( void * p, int nPartSize, int nConfLimit, int nLevelMax, int fUseCSat, int fVerbose );
extern void Ntl_ManFree( void * p );
@@ -21204,7 +21183,6 @@ int Abc_CommandAbc8Scl( Abc_Frame_t * pAbc, int argc, char ** argv )
int fLatchConst;
int fLatchEqual;
int fVerbose;
- extern Aig_Man_t * Ntl_ManExtract( void * p );
extern void * Ntl_ManScl( void * p, int fLatchConst, int fLatchEqual, int fVerbose );
extern int Ntl_ManIsComb( void * p );
@@ -21300,7 +21278,6 @@ int Abc_CommandAbc8Lcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
int nFramesP;
int nConfMax;
int fVerbose;
- extern Aig_Man_t * Ntl_ManExtract( void * p );
extern void * Ntl_ManLcorr( void * p, int nConfMax, int fScorrGia, int fUseCSat, int fVerbose );
extern int Ntl_ManIsComb( void * p );
@@ -21417,7 +21394,6 @@ int Abc_CommandAbc8Ssw( Abc_Frame_t * pAbc, int argc, char ** argv )
void * pNtlNew, * pNtlOld;
Fra_Ssw_t Pars, * pPars = &Pars;
int c;
- extern Aig_Man_t * Ntl_ManExtract( void * p );
extern void * Ntl_ManSsw( void * p, Fra_Ssw_t * pPars );
extern int Ntl_ManIsComb( void * p );
@@ -21632,7 +21608,6 @@ int Abc_CommandAbc8Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
void * pNtlNew, * pNtlOld;
Ssw_Pars_t Pars, * pPars = &Pars;
int c;
- extern Aig_Man_t * Ntl_ManExtract( void * p );
extern void * Ntl_ManScorr( void * p, Ssw_Pars_t * pPars );
extern int Ntl_ManIsComb( void * p );
@@ -25186,11 +25161,14 @@ int Abc_CommandAbc9Era( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Gia_Man_t * pTemp = NULL;
int c, fVerbose = 0;
+ int fUseCubes = 1;
int fMiter = 0;
- int nStatesMax = 10000000;
+ int nStatesMax = 1000000000;
extern void Gia_ManCollectReachable( Gia_Man_t * pAig, int nStatesMax, int fMiter, int fVerbose );
+ extern void Gia_ManArePerform( Gia_Man_t * pAig, int nStatesMax, int fMiter, int fVerbose );
+
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "Smvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Smcvh" ) ) != EOF )
{
switch ( c )
{
@@ -25208,6 +25186,9 @@ int Abc_CommandAbc9Era( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'm':
fMiter ^= 1;
break;
+ case 'c':
+ fUseCubes ^= 1;
+ break;
case 'v':
fVerbose ^= 1;
break;
@@ -25222,24 +25203,31 @@ int Abc_CommandAbc9Era( Abc_Frame_t * pAbc, int argc, char ** argv )
printf( "Abc_CommandAbc9Era(): There is no AIG.\n" );
return 1;
}
- if ( Gia_ManPiNum(pAbc->pAig) > 12 )
+ if ( Gia_ManRegNum(pAbc->pAig) == 0 )
{
- printf( "Abc_CommandAbc9Era(): The number of PIs (%d) should be no more than 12.\n", Gia_ManPiNum(pAbc->pAig) );
+ printf( "Abc_CommandAbc9Era(): The network is combinational.\n" );
return 1;
}
- if ( Gia_ManRegNum(pAbc->pAig) == 0 )
+ if ( !fUseCubes && Gia_ManPiNum(pAbc->pAig) > 12 )
{
- printf( "Abc_CommandAbc9Era(): The network is combinational.\n" );
+ printf( "Abc_CommandAbc9Era(): The number of PIs (%d) should be no more than 12 when cubes are not used.\n", Gia_ManPiNum(pAbc->pAig) );
return 1;
}
- Gia_ManCollectReachable( pAbc->pAig, nStatesMax, fMiter, fVerbose );
+ if ( fUseCubes )
+ Gia_ManArePerform( pAbc->pAig, nStatesMax, fMiter, fVerbose );
+ else
+ Gia_ManCollectReachable( pAbc->pAig, nStatesMax, fMiter, fVerbose );
+ pAbc->pCex = ((Gia_Man_t *)pAbc->pAig)->pCexSeq; // temporary ???
+ ((Gia_Man_t *)pAbc->pAig)->pCexSeq = NULL;
return 0;
usage:
- fprintf( stdout, "usage: &era [-S num] [-mvh]\n" );
+ fprintf( stdout, "usage: &era [-S num] [-mcvh]\n" );
+// fprintf( stdout, "usage: &era [-S num] [-mvh]\n" );
fprintf( stdout, "\t explicit reachability analysis for small sequential AIGs\n" );
- fprintf( stdout, "\t-S num : the max number of states to traverse (num > 0) [default = %d]\n", nStatesMax );
+ fprintf( stdout, "\t-S num : the max number of states (num > 0) [default = %d]\n", nStatesMax );
fprintf( stdout, "\t-m : stop when the miter output is 1 [default = %s]\n", fMiter? "yes": "no" );
+ fprintf( stdout, "\t-c : use state cubes instead of state minterms [default = %s]\n", fUseCubes? "yes": "no" );
fprintf( stdout, "\t-v : print verbose information [default = %s]\n", fVerbose? "yes": "no" );
fprintf( stdout, "\t-h : print the command usage\n");
return 1;
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 790a9028..dbe98631 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -32,6 +32,7 @@
//#include "fsim.h"
#include "gia.h"
#include "cec.h"
+#include "giaAbs.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@@ -467,6 +468,92 @@ Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan )
Synopsis [Converts the network from the AIG manager into ABC.]
+ Description [This procedure should be called after seq sweeping,
+ which changes the number of registers.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkAfterTrim( Aig_Man_t * pMan, Abc_Ntk_t * pNtkOld )
+{
+ Vec_Ptr_t * vNodes;
+ Abc_Ntk_t * pNtkNew;
+ Abc_Obj_t * pObjNew, * pObjOld;
+ Aig_Obj_t * pObj, * pObjLo, * pObjLi;
+ int i;
+ assert( pMan->nAsserts == 0 );
+ assert( Aig_ManRegNum(pMan) <= Abc_NtkLatchNum(pNtkOld) );
+ assert( Saig_ManPiNum(pMan) <= Abc_NtkCiNum(pNtkOld) );
+ assert( Saig_ManPoNum(pMan) == Abc_NtkPoNum(pNtkOld) );
+ assert( pMan->vCiNumsOrig != NULL );
+ // perform strashing
+ pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
+ // duplicate the name and the spec
+// pNtkNew->pName = Extra_UtilStrsav(pMan->pName);
+// pNtkNew->pSpec = Extra_UtilStrsav(pMan->pSpec);
+ Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
+ // create PIs
+ Aig_ManForEachPiSeq( pMan, pObj, i )
+ {
+ pObjNew = Abc_NtkCreatePi( pNtkNew );
+ pObj->pData = pObjNew;
+ // find the name
+ pObjOld = Abc_NtkCi( pNtkOld, Vec_IntEntry(pMan->vCiNumsOrig, i) );
+ Abc_ObjAssignName( pObjNew, Abc_ObjName(pObjOld), NULL );
+ }
+ // create POs
+ Aig_ManForEachPoSeq( pMan, pObj, i )
+ {
+ pObjNew = Abc_NtkCreatePo( pNtkNew );
+ pObj->pData = pObjNew;
+ // find the name
+ pObjOld = Abc_NtkCo( pNtkOld, i );
+ Abc_ObjAssignName( pObjNew, Abc_ObjName(pObjOld), NULL );
+ }
+ assert( Abc_NtkCiNum(pNtkNew) == Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan) );
+ assert( Abc_NtkCoNum(pNtkNew) == Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan) );
+ // create as many latches as there are registers in the manager
+ Aig_ManForEachLiLoSeq( pMan, pObjLi, pObjLo, i )
+ {
+ pObjNew = Abc_NtkCreateLatch( pNtkNew );
+ pObjLi->pData = Abc_NtkCreateBi( pNtkNew );
+ pObjLo->pData = Abc_NtkCreateBo( pNtkNew );
+ Abc_ObjAddFanin( pObjNew, pObjLi->pData );
+ Abc_ObjAddFanin( pObjLo->pData, pObjNew );
+ Abc_LatchSetInit0( pObjNew );
+ // find the name
+ pObjOld = Abc_NtkCi( pNtkOld, Vec_IntEntry(pMan->vCiNumsOrig, Saig_ManPiNum(pMan)+i) );
+ Abc_ObjAssignName( pObjLo->pData, Abc_ObjName(pObjOld), NULL );
+ // find the name
+ pObjOld = Abc_NtkCo( pNtkOld, Saig_ManPoNum(pMan)+i );
+ Abc_ObjAssignName( pObjLi->pData, Abc_ObjName(pObjOld), NULL );
+ }
+ // rebuild the AIG
+ vNodes = Aig_ManDfs( pMan, 1 );
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ if ( Aig_ObjIsBuf(pObj) )
+ pObj->pData = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
+ else
+ pObj->pData = Abc_AigAnd( pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
+ Vec_PtrFree( vNodes );
+ // connect the PO nodes
+ Aig_ManForEachPo( pMan, pObj, i )
+ {
+ pObjNew = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
+ Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), pObjNew );
+ }
+ // check the resulting AIG
+ if ( !Abc_NtkCheck( pNtkNew ) )
+ fprintf( stdout, "Abc_NtkFromAigPhase(): Network check has failed.\n" );
+ return pNtkNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Converts the network from the AIG manager into ABC.]
+
Description []
SideEffects []
@@ -1633,12 +1720,12 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nStart, int nFrames, int nSizeMax, int
printf( "No output was asserted in %d frames. Reached conflict limit (%d). ", iFrame, nBTLimit );
else // if ( RetValue == 0 )
{
- extern void Aig_ManCounterExampleValueTest( Aig_Man_t * pAig, Fra_Cex_t * pCex );
+// extern void Aig_ManCounterExampleValueTest( Aig_Man_t * pAig, Fra_Cex_t * pCex );
Fra_Cex_t * pCex = pNtk->pSeqModel;
printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", pCex->iPo, pCex->iFrame );
- Aig_ManCounterExampleValueTest( pMan, pCex );
+// Aig_ManCounterExampleValueTest( pMan, pCex );
}
}
else
@@ -2714,7 +2801,7 @@ ABC_PRT( "Time", clock() - clkTotal );
SeeAlso []
***********************************************************************/
-Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int nRatio, int fUseBdds, int fUseDprove, int fUseStart, int fVerbose )
+Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, Gia_ParAbs_t * pPars )
{
Abc_Ntk_t * pNtkAig;
Aig_Man_t * pMan, * pTemp;
@@ -2724,7 +2811,7 @@ Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConf
return NULL;
Aig_ManSetRegNum( pMan, pMan->nRegs );
- pMan = Saig_ManProofAbstraction( pTemp = pMan, nFramesMax, nConfMax, fDynamic, fExtend, fSkipProof, nFramesBmc, nConfMaxBmc, nRatio, fUseBdds, fUseDprove, fUseStart, fVerbose );
+ pMan = Saig_ManProofAbstraction( pTemp = pMan, pPars );
if ( pTemp->pSeqModel )
{
ABC_FREE( pNtk->pModel );
@@ -2735,7 +2822,7 @@ Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConf
if ( pMan == NULL )
return NULL;
- pNtkAig = Abc_NtkFromAigPhase( pMan );
+ pNtkAig = Abc_NtkAfterTrim( pMan, pNtk );
// pNtkAig->pName = Extra_UtilStrsav(pNtk->pName);
// pNtkAig->pSpec = Extra_UtilStrsav(pNtk->pSpec);
Aig_ManStop( pMan );
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 18:27:06 +0000