summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/aig/cec/cecClass.c2
-rw-r--r--src/aig/cec/cecMan.c3
-rw-r--r--src/aig/gia/giaCSat.c10
-rw-r--r--src/aig/gia/giaCSatOld.c5
-rw-r--r--src/aig/gia/giaDfs.c30
-rw-r--r--src/aig/gia/giaEquiv.c2
-rw-r--r--src/base/abci/abc.c39
-rw-r--r--src/base/abci/abcXsim.c9
-rw-r--r--src/base/io/ioReadBlifMv.c3
-rw-r--r--src/opt/mfs/mfsInter.c3
10 files changed, 86 insertions, 20 deletions
diff --git a/src/aig/cec/cecClass.c b/src/aig/cec/cecClass.c
index 5a52e913..cd3ce7b9 100644
--- a/src/aig/cec/cecClass.c
+++ b/src/aig/cec/cecClass.c
@@ -711,6 +711,7 @@ int Cec_ManSimSimulateRound( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t *
pRes = Cec_ManSimSimRef( p, i );
pRes0 = Cec_ManSimSimDeref( p, Gia_ObjFaninId0(pObj,i) );
pRes1 = Cec_ManSimSimDeref( p, Gia_ObjFaninId1(pObj,i) );
+
if ( Gia_ObjFaninC0(pObj) )
{
if ( Gia_ObjFaninC1(pObj) )
@@ -729,6 +730,7 @@ int Cec_ManSimSimulateRound( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t *
for ( w = 1; w <= p->nWords; w++ )
pRes[w] = pRes0[w] & pRes1[w];
}
+
references:
// if this node is candidate constant, collect it
if ( Gia_ObjIsConst(p->pAig, i) && !Cec_ManSimCompareConst(pRes + 1, p->nWords) )
diff --git a/src/aig/cec/cecMan.c b/src/aig/cec/cecMan.c
index eb582e4c..de71ecc9 100644
--- a/src/aig/cec/cecMan.c
+++ b/src/aig/cec/cecMan.c
@@ -70,7 +70,8 @@ Cec_ManSat_t * Cec_ManSatCreate( Gia_Man_t * pAig, Cec_ParSat_t * pPars )
***********************************************************************/
void Cec_ManSatPrintStats( Cec_ManSat_t * p )
{
- printf( "CO = %6d ", Gia_ManCoNum(p->pAig) );
+ printf( "CO = %8d ", Gia_ManCoNum(p->pAig) );
+ printf( "AND = %8d ", Gia_ManAndNum(p->pAig) );
printf( "Conf = %5d ", p->pPars->nBTLimit );
printf( "MinVar = %5d ", p->pPars->nSatVarMax );
printf( "MinCalls = %5d\n", p->pPars->nCallsRecycle );
diff --git a/src/aig/gia/giaCSat.c b/src/aig/gia/giaCSat.c
index 832eff26..f53a3d33 100644
--- a/src/aig/gia/giaCSat.c
+++ b/src/aig/gia/giaCSat.c
@@ -885,6 +885,8 @@ int Cbs_ManSolve_rec( Cbs_Man_t * p, int Level )
pDecVar = Gia_Not(Gia_ObjChild0(pVar));
else
pDecVar = Gia_Not(Gia_ObjChild1(pVar));
+// pDecVar = Gia_NotCond( Gia_Regular(pDecVar), Gia_Regular(pDecVar)->fPhase );
+// pDecVar = Gia_Not(pDecVar);
// decide on first fanin
Cbs_ManAssign( p, pDecVar, Level+1, NULL, NULL );
if ( !(hLearn0 = Cbs_ManSolve_rec( p, Level+1 )) )
@@ -955,8 +957,9 @@ int Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj )
***********************************************************************/
void Cbs_ManSatPrintStats( Cbs_Man_t * p )
{
- printf( "CO = %6d ", Gia_ManCoNum(p->pAig) );
- printf( "Conf = %5d ", p->Pars.nBTLimit );
+ printf( "CO = %8d ", Gia_ManCoNum(p->pAig) );
+ printf( "AND = %8d ", Gia_ManAndNum(p->pAig) );
+ printf( "Conf = %6d ", p->Pars.nBTLimit );
printf( "JustMax = %5d ", p->Pars.nJustLimit );
printf( "\n" );
printf( "Unsat calls %6d (%6.2f %%) Ave conf = %8.1f ",
@@ -984,6 +987,7 @@ void Cbs_ManSatPrintStats( Cbs_Man_t * p )
***********************************************************************/
Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStatus, int fVerbose )
{
+ extern void Gia_ManCollectTest( Gia_Man_t * pAig );
extern void Cec_ManSatAddToStore( Vec_Int_t * vCexStore, Vec_Int_t * vCex, int Out );
Cbs_Man_t * p;
Vec_Int_t * vCex, * vVisit, * vCexStore;
@@ -991,11 +995,13 @@ Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvSt
Gia_Obj_t * pRoot;
int i, status, clk, clkTotal = clock();
assert( Gia_ManRegNum(pAig) == 0 );
+// Gia_ManCollectTest( pAig );
// prepare AIG
Gia_ManCreateRefs( pAig );
Gia_ManCleanMark0( pAig );
Gia_ManCleanMark1( pAig );
Gia_ManFillValue( pAig ); // maps nodes into trail ids
+ Gia_ManSetPhase( pAig ); // maps nodes into trail ids
// create logic network
p = Cbs_ManAlloc();
p->Pars.nBTLimit = nConfs;
diff --git a/src/aig/gia/giaCSatOld.c b/src/aig/gia/giaCSatOld.c
index 409af56c..a0d97693 100644
--- a/src/aig/gia/giaCSatOld.c
+++ b/src/aig/gia/giaCSatOld.c
@@ -674,8 +674,9 @@ int Cbs0_ManSolve( Cbs0_Man_t * p, Gia_Obj_t * pObj )
***********************************************************************/
void Cbs0_ManSatPrintStats( Cbs0_Man_t * p )
{
- printf( "CO = %6d ", Gia_ManCoNum(p->pAig) );
- printf( "Conf = %5d ", p->Pars.nBTLimit );
+ printf( "CO = %8d ", Gia_ManCoNum(p->pAig) );
+ printf( "AND = %8d ", Gia_ManAndNum(p->pAig) );
+ printf( "Conf = %6d ", p->Pars.nBTLimit );
printf( "JustMax = %5d ", p->Pars.nJustLimit );
printf( "\n" );
printf( "Unsat calls %6d (%6.2f %%) Ave conf = %8.1f ",
diff --git a/src/aig/gia/giaDfs.c b/src/aig/gia/giaDfs.c
index a978dcc3..8a3aef92 100644
--- a/src/aig/gia/giaDfs.c
+++ b/src/aig/gia/giaDfs.c
@@ -122,7 +122,7 @@ void Gia_ManCollectAnds( Gia_Man_t * p, int * pNodes, int nNodes, Vec_Int_t * vN
Gia_Obj_t * pObj;
int i;
Vec_IntClear( vNodes );
- Gia_ManIncrementTravId( p );
+// Gia_ManIncrementTravId( p );
Gia_ObjSetTravIdCurrent( p, Gia_ManConst0(p) );
for ( i = 0; i < nNodes; i++ )
{
@@ -145,6 +145,34 @@ void Gia_ManCollectAnds( Gia_Man_t * p, int * pNodes, int nNodes, Vec_Int_t * vN
SeeAlso []
***********************************************************************/
+void Gia_ManCollectTest( Gia_Man_t * p )
+{
+ Vec_Int_t * vNodes;
+ Gia_Obj_t * pObj;
+ int i, iNode, clk = clock();
+ vNodes = Vec_IntAlloc( 100 );
+ Gia_ManResetTravId( p );
+ Gia_ManIncrementTravId( p );
+ Gia_ManForEachCo( p, pObj, i )
+ {
+ iNode = Gia_ObjId(p, pObj);
+ Gia_ManCollectAnds( p, &iNode, 1, vNodes );
+ }
+ Vec_IntFree( vNodes );
+ ABC_PRT( "DFS from each output", clock() - clk );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Collects support nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Gia_ManSuppSize_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
{
if ( Gia_ObjIsTravIdCurrent(p, pObj) )
diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
index cdee73d0..041be0f5 100644
--- a/src/aig/gia/giaEquiv.c
+++ b/src/aig/gia/giaEquiv.c
@@ -1135,6 +1135,8 @@ void Gia_ManEquivToChoices_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pOb
assert( (int)pObj->Value == Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ) );
return;
}
+ if ( pRepr->Value > pObj->Value ) // should never happen with high resource limit
+ return;
assert( pRepr->Value < pObj->Value );
pReprNew = Gia_ManObj( pNew, Gia_Lit2Var(pRepr->Value) );
pObjNew = Gia_ManObj( pNew, Gia_Lit2Var(pObj->Value) );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 8ac8b241..6beaf144 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -2575,7 +2575,7 @@ int Abc_CommandStrash( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
if ( fComplOuts )
- Abc_NtkForEachCo( pNtkRes, pObj, c )
+ Abc_NtkForEachPo( pNtkRes, pObj, c )
Abc_ObjXorFaninC( pObj, 0 );
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
@@ -14914,8 +14914,9 @@ int Abc_CommandCycle( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Ntk_t * pNtk;
int c;
int nFrames;
+ int fUseXval;
int fVerbose;
- extern void Abc_NtkCycleInitState( Abc_Ntk_t * pNtk, int nFrames, int fVerbose );
+ extern void Abc_NtkCycleInitState( Abc_Ntk_t * pNtk, int nFrames, int fUseXval, int fVerbose );
extern void Abc_NtkCycleInitStateSop( Abc_Ntk_t * pNtk, int nFrames, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
@@ -14924,9 +14925,10 @@ int Abc_CommandCycle( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
nFrames = 100;
+ fUseXval = 0;
fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "Fvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Fxvh" ) ) != EOF )
{
switch ( c )
{
@@ -14941,6 +14943,9 @@ int Abc_CommandCycle( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nFrames < 0 )
goto usage;
break;
+ case 'x':
+ fUseXval ^= 1;
+ break;
case 'v':
fVerbose ^= 1;
break;
@@ -14966,18 +14971,25 @@ int Abc_CommandCycle( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "The network is combinational.\n" );
return 0;
}
-
- if ( Abc_NtkIsStrash(pNtk) )
- Abc_NtkCycleInitState( pNtk, nFrames, fVerbose );
+ if ( fUseXval && !Abc_NtkIsStrash(pNtk) )
+ {
+ fprintf( pErr, "X-valued simulation only works for AIGs. Run \"strash\".\n" );
+ return 0;
+ }
+ if ( fUseXval )
+ Abc_NtkCycleInitState( pNtk, nFrames, 1, fVerbose );
+ else if ( Abc_NtkIsStrash(pNtk) )
+ Abc_NtkCycleInitState( pNtk, nFrames, 0, fVerbose );
else
Abc_NtkCycleInitStateSop( pNtk, nFrames, fVerbose );
return 0;
usage:
- fprintf( pErr, "usage: cycle [-F num] [-vh]\n" );
- fprintf( pErr, "\t cycles sequiential circuit for the given number of timeframes\n" );
+ fprintf( pErr, "usage: cycle [-F num] [-xvh]\n" );
+ fprintf( pErr, "\t cycles sequential circuit for the given number of timeframes\n" );
fprintf( pErr, "\t to derive a new initial state (which may be on the envelope)\n" );
fprintf( pErr, "\t-F num : the number of frames to simulate [default = %d]\n", nFrames );
+ fprintf( pErr, "\t-x : use x-valued primary inputs [default = %s]\n", fUseXval? "yes": "no" );
fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
@@ -16090,6 +16102,14 @@ int Abc_CommandDCec( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
+ if ( Abc_NtkLatchNum(pNtk1) || Abc_NtkLatchNum(pNtk2) )
+ {
+ if ( fDelete1 ) Abc_NtkDelete( pNtk1 );
+ if ( fDelete2 ) Abc_NtkDelete( pNtk2 );
+ printf( "Currently this command only works for networks without latches. Run \"comb\".\n" );
+ return 1;
+ }
+
// perform equivalence checking
if ( fSat && fMiter )
Abc_NtkDSat( pNtk1, nConfLimit, nInsLimit, 0, 0, fVerbose );
@@ -21934,6 +21954,7 @@ int Abc_CommandAbc9Put( Abc_Frame_t * pAbc, int argc, char ** argv )
{
pMan = Gia_ManToAig( pAbc->pAig, 0 );
pNtk = Abc_NtkFromAigPhase( pMan );
+ pNtk->pName = Extra_UtilStrsav(pMan->pName);
Aig_ManStop( pMan );
}
else
@@ -23059,7 +23080,7 @@ usage:
fprintf( stdout, "usage: &frames [-FL <num>] [-ivh]\n" );
fprintf( stdout, "\t unrolls the design for several timeframes\n" );
fprintf( stdout, "\t-F num : the number of frames to unroll [default = %d]\n", pPars->nFrames );
- fprintf( stdout, "\t-L num : the limit on fanout count of resets/enables to cofactor [default = %d]\n", nCofFanLit? "yes": "no" );
+ fprintf( stdout, "\t-L num : the limit on fanout count of resets/enables to cofactor [default = %d]\n", nCofFanLit );
fprintf( stdout, "\t-i : toggle initializing registers [default = %s]\n", pPars->fInit? "yes": "no" );
fprintf( stdout, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
fprintf( stdout, "\t-h : print the command usage\n");
diff --git a/src/base/abci/abcXsim.c b/src/base/abci/abcXsim.c
index e63b296a..76a82b51 100644
--- a/src/base/abci/abcXsim.c
+++ b/src/base/abci/abcXsim.c
@@ -181,15 +181,15 @@ void Abc_NtkXValueSimulate( Abc_Ntk_t * pNtk, int nFrames, int fXInputs, int fXS
Synopsis [Cycles the circuit to create a new initial state.]
- Description [Simulates the circuit with random input for the given
- number of timeframes to get a better initial state.]
+ Description [Simulates the circuit with random (or ternary) input
+ for the given number of timeframes to get a better initial state.]
SideEffects []
SeeAlso []
***********************************************************************/
-void Abc_NtkCycleInitState( Abc_Ntk_t * pNtk, int nFrames, int fVerbose )
+void Abc_NtkCycleInitState( Abc_Ntk_t * pNtk, int nFrames, int fUseXval, int fVerbose )
{
Abc_Obj_t * pObj;
int i, f;
@@ -198,13 +198,12 @@ void Abc_NtkCycleInitState( Abc_Ntk_t * pNtk, int nFrames, int fVerbose )
// initialize the values
Abc_ObjSetXsim( Abc_AigConst1(pNtk), XVS1 );
Abc_NtkForEachLatch( pNtk, pObj, i )
-// Abc_ObjSetXsim( Abc_ObjFanout0(pObj), Abc_LatchIsInit1(pObj)? XVS1 : XVS0 );
Abc_ObjSetXsim( Abc_ObjFanout0(pObj), Abc_LatchInit(pObj) );
// simulate for the given number of timeframes
for ( f = 0; f < nFrames; f++ )
{
Abc_NtkForEachPi( pNtk, pObj, i )
- Abc_ObjSetXsim( pObj, Abc_XsimRand2() );
+ Abc_ObjSetXsim( pObj, fUseXval? ABC_INIT_DC : Abc_XsimRand2() );
Abc_AigForEachAnd( pNtk, pObj, i )
Abc_ObjSetXsim( pObj, Abc_XsimAnd(Abc_ObjGetXsimFanin0(pObj), Abc_ObjGetXsimFanin1(pObj)) );
Abc_NtkForEachCo( pNtk, pObj, i )
diff --git a/src/base/io/ioReadBlifMv.c b/src/base/io/ioReadBlifMv.c
index eea601a8..95e7cd1d 100644
--- a/src/base/io/ioReadBlifMv.c
+++ b/src/base/io/ioReadBlifMv.c
@@ -941,6 +941,9 @@ static int Io_MvParseLineLatch( Io_MvMod_t * p, char * pLine )
Abc_LatchSetInit0( pObj );
else
{
+ if ( Vec_PtrSize(vTokens) > 6 )
+ printf( "Warning: Line %d has .latch directive with unrecognized entries (the total of %d entries).\n",
+ Io_MvGetLine(p->pMan, pToken), Vec_PtrSize(vTokens) );
if ( Vec_PtrSize(vTokens) > 3 )
Init = atoi( Vec_PtrEntryLast(vTokens) );
else
diff --git a/src/opt/mfs/mfsInter.c b/src/opt/mfs/mfsInter.c
index 8fc30056..9cacd021 100644
--- a/src/opt/mfs/mfsInter.c
+++ b/src/opt/mfs/mfsInter.c
@@ -332,6 +332,7 @@ Hop_Obj_t * Abc_NtkMfsInterplate( Mfs_Man_t * p, int * pCands, int nCands )
Hop_Obj_t * pFunc;
int nFanins, status;
int c, i, * pGloVars;
+// int clk = clock();
// p->nDcMints += Abc_NtkMfsInterplateEval( p, pCands, nCands );
@@ -345,6 +346,8 @@ Hop_Obj_t * Abc_NtkMfsInterplate( Mfs_Man_t * p, int * pCands, int nCands )
p->nTimeOuts++;
return NULL;
}
+//printf( "%d\n", pSat->stats.conflicts );
+// ABC_PRT( "S", clock() - clk );
// get the learned clauses
pCnf = sat_solver_store_release( pSat );
sat_solver_delete( pSat );
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-15 09:35:36 +0000