Skip to content

A
abc
Commit 77fab468 by Alan Mishchenko
Options

Version abc90413

parent ccd1b572
Showing with 86 additions and 20 deletions
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) )
......
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 );
......
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;
......
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 ",
......
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) )
......
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) );
......
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");
......
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 )
......
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
......
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 );
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment