luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Version abc80527

This commit is contained in:
Alan Mishchenko 2008-05-27 08:01:00 -07:00
parent 5b79c78983
commit 9604ecb174
11 changed files with 408 additions and 106 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
src/aig/fra/fra.h
View File

@ -370,8 +370,9 @@ extern Fra_Sml_t * Fra_SmlSimulateComb( Aig_Man_t * pAig, int nWords );
extern Fra_Cex_t * Fra_SmlGetCounterExample( Fra_Sml_t * p ); extern Fra_Cex_t * Fra_SmlGetCounterExample( Fra_Sml_t * p );
extern Fra_Cex_t * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel ); extern Fra_Cex_t * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel );
extern void Fra_SmlFreeCounterExample( Fra_Cex_t * p ); extern void Fra_SmlFreeCounterExample( Fra_Cex_t * p );
extern int Fra_SmlRunCounterExample( Aig_Man_t * pAig, Fra_Cex_t * p );
extern Fra_Cex_t * Fra_SmlTrivCounterExample( Aig_Man_t * pAig, int iFrameOut ); extern Fra_Cex_t * Fra_SmlTrivCounterExample( Aig_Man_t * pAig, int iFrameOut );
extern int Fra_SmlRunCounterExample( Aig_Man_t * pAig, Fra_Cex_t * p );
extern int Fra_SmlWriteCounterExample( FILE * pFile, Aig_Man_t * pAig, Fra_Cex_t * p );
#ifdef __cplusplus #ifdef __cplusplus
} }

147
src/aig/fra/fraSim.c
View File

@ -844,44 +844,6 @@ Fra_Sml_t * Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nW
return p; return p;
} }
/**Function*************************************************************
Synopsis [Resimulates the counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_SmlRunCounterExample( Aig_Man_t * pAig, Fra_Cex_t * p )
{
Fra_Sml_t * pSml;
Aig_Obj_t * pObj;
int RetValue, i, k, iBit;
assert( Aig_ManRegNum(pAig) > 0 );
assert( Aig_ManRegNum(pAig) < Aig_ManPiNum(pAig) );
// start a new sequential simulator
pSml = Fra_SmlStart( pAig, 0, p->iFrame+1, 1 );
// assign simulation info for the registers
iBit = 0;
Aig_ManForEachLoSeq( pAig, pObj, i )
Fra_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), 0 );
// assign simulation info for the primary inputs
for ( i = 0; i <= p->iFrame; i++ )
Aig_ManForEachPiSeq( pAig, pObj, k )
Fra_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), i );
assert( iBit == p->nBits );
// run random simulation
Fra_SmlSimulateOne( pSml );
// check if the given output has failed
RetValue = !Fra_SmlNodeIsZero( pSml, Aig_ManPo(pAig, p->iPo) );
Fra_SmlStop( pSml );
return RetValue;
}
/**Function************************************************************* /**Function*************************************************************
Synopsis [Allocates a counter-example.] Synopsis [Allocates a counter-example.]
@ -1082,6 +1044,115 @@ Fra_Cex_t * Fra_SmlTrivCounterExample( Aig_Man_t * pAig, int iFrameOut )
return pCex; return pCex;
} }
/**Function*************************************************************
Synopsis [Resimulates the counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_SmlRunCounterExample( Aig_Man_t * pAig, Fra_Cex_t * p )
{
Fra_Sml_t * pSml;
Aig_Obj_t * pObj;
int RetValue, i, k, iBit;
assert( Aig_ManRegNum(pAig) > 0 );
assert( Aig_ManRegNum(pAig) < Aig_ManPiNum(pAig) );
// start a new sequential simulator
pSml = Fra_SmlStart( pAig, 0, p->iFrame+1, 1 );
// assign simulation info for the registers
iBit = 0;
Aig_ManForEachLoSeq( pAig, pObj, i )
Fra_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), 0 );
// assign simulation info for the primary inputs
for ( i = 0; i <= p->iFrame; i++ )
Aig_ManForEachPiSeq( pAig, pObj, k )
Fra_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), i );
assert( iBit == p->nBits );
// run random simulation
Fra_SmlSimulateOne( pSml );
// check if the given output has failed
RetValue = !Fra_SmlNodeIsZero( pSml, Aig_ManPo(pAig, p->iPo) );
Fra_SmlStop( pSml );
return RetValue;
}
/**Function*************************************************************
Synopsis [Resimulates the counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_SmlWriteCounterExample( FILE * pFile, Aig_Man_t * pAig, Fra_Cex_t * p )
{
Fra_Sml_t * pSml;
Aig_Obj_t * pObj;
int RetValue, i, k, iBit;
unsigned * pSims;
assert( Aig_ManRegNum(pAig) > 0 );
assert( Aig_ManRegNum(pAig) < Aig_ManPiNum(pAig) );
// start a new sequential simulator
pSml = Fra_SmlStart( pAig, 0, p->iFrame+1, 1 );
// assign simulation info for the registers
iBit = 0;
Aig_ManForEachLoSeq( pAig, pObj, i )
// Fra_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), 0 );
Fra_SmlAssignConst( pSml, pObj, 0, 0 );
// assign simulation info for the primary inputs
iBit = p->nRegs;
for ( i = 0; i <= p->iFrame; i++ )
Aig_ManForEachPiSeq( pAig, pObj, k )
Fra_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), i );
assert( iBit == p->nBits );
// run random simulation
Fra_SmlSimulateOne( pSml );
// check if the given output has failed
RetValue = !Fra_SmlNodeIsZero( pSml, Aig_ManPo(pAig, p->iPo) );
// write the output file
fprintf( pFile, "1\n" );
for ( i = 0; i <= p->iFrame; i++ )
{
Aig_ManForEachLoSeq( pAig, pObj, k )
{
pSims = Fra_ObjSim(pSml, pObj->Id);
fprintf( pFile, "%d", (int)(pSims[i] != 0) );
}
fprintf( pFile, " " );
Aig_ManForEachPiSeq( pAig, pObj, k )
{
pSims = Fra_ObjSim(pSml, pObj->Id);
fprintf( pFile, "%d", (int)(pSims[i] != 0) );
}
fprintf( pFile, " " );
Aig_ManForEachPoSeq( pAig, pObj, k )
{
pSims = Fra_ObjSim(pSml, pObj->Id);
fprintf( pFile, "%d", (int)(pSims[i] != 0) );
}
fprintf( pFile, " " );
Aig_ManForEachLiSeq( pAig, pObj, k )
{
pSims = Fra_ObjSim(pSml, pObj->Id);
fprintf( pFile, "%d", (int)(pSims[i] != 0) );
}
fprintf( pFile, "\n" );
}
Fra_SmlStop( pSml );
return RetValue;
}
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// END OF FILE /// /// END OF FILE ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////

3
src/aig/ntl/ntlCheck.c
View File

@ -123,8 +123,11 @@ int Ntl_ManCheck( Ntl_Man_t * pMan )
} }
// check models // check models
Ntl_ManForEachModel( pMan, pMod1, i ) Ntl_ManForEachModel( pMan, pMod1, i )
{
if ( !Ntl_ModelCheck( pMod1 ) ) if ( !Ntl_ModelCheck( pMod1 ) )
fStatus = 0; fStatus = 0;
break;
}
return fStatus; return fStatus;
} }

38
src/aig/ntl/ntlReadBlif.c
View File

@ -534,6 +534,18 @@ static void Ioa_ReadReadPreparse( Ioa_ReadMan_t * p )
fprintf( stdout, "Line %d: Skipping EXDC network.\n", Ioa_ReadGetLine(p, pCur) ); fprintf( stdout, "Line %d: Skipping EXDC network.\n", Ioa_ReadGetLine(p, pCur) );
break; break;
} }
else if ( !strncmp(pCur, "no_merge", 8) )
{
}
else if ( !strncmp(pCur, "attribute", 9) )
{
}
else if ( !strncmp(pCur, "input_required", 14) )
{
}
else if ( !strncmp(pCur, "output_arrival", 14) )
{
}
else else
{ {
pCur--; pCur--;
@ -682,7 +694,8 @@ static int Ioa_ReadParseLineAttrib( Ioa_ReadMod_t * p, char * pLine )
char * pToken; char * pToken;
Ioa_ReadSplitIntoTokens( vTokens, pLine, '\0' ); Ioa_ReadSplitIntoTokens( vTokens, pLine, '\0' );
pToken = Vec_PtrEntry( vTokens, 0 ); pToken = Vec_PtrEntry( vTokens, 0 );
assert( !strcmp(pToken, "attrib") ); assert( !strncmp(pToken, "attrib", 6) );
/*
if ( Vec_PtrSize(vTokens) != 2 ) if ( Vec_PtrSize(vTokens) != 2 )
{ {
sprintf( p->pMan->sError, "Line %d: The number of entries (%d) in .attrib line is different from two.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrSize(vTokens) ); sprintf( p->pMan->sError, "Line %d: The number of entries (%d) in .attrib line is different from two.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrSize(vTokens) );
@ -695,6 +708,7 @@ static int Ioa_ReadParseLineAttrib( Ioa_ReadMod_t * p, char * pLine )
sprintf( p->pMan->sError, "Line %d: Unknown attribute (%s) in the .attrib line of model %s.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 1), p->pNtk->pName ); sprintf( p->pMan->sError, "Line %d: Unknown attribute (%s) in the .attrib line of model %s.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 1), p->pNtk->pName );
return 0; return 0;
} }
*/
return 1; return 1;
} }
@ -864,12 +878,28 @@ static int Ioa_ReadParseLineSubckt( Ioa_ReadMod_t * p, char * pLine )
sprintf( p->pMan->sError, "Line %d: Cannot find the model for subcircuit %s.", Ioa_ReadGetLine(p->pMan, pToken), pName ); sprintf( p->pMan->sError, "Line %d: Cannot find the model for subcircuit %s.", Ioa_ReadGetLine(p->pMan, pToken), pName );
return 0; return 0;
} }
/*
// temporary fix for splitting the .subckt line
if ( nEquals < Ntl_ModelPiNum(pModel) + Ntl_ModelPoNum(pModel) )
{
Vec_Ptr_t * vTokens2 = Vec_PtrAlloc( 10 );
// get one additional token
pToken = Vec_PtrEntry( vTokens, Vec_PtrSize(vTokens) - 1 );
for ( ; *pToken; pToken++ );
for ( ; *pToken == 0; pToken++ );
Ioa_ReadSplitIntoTokensAndClear( vTokens2, pToken, '\0', '=' );
// assert( Vec_PtrSize( vTokens2 ) == 2 );
Vec_PtrForEachEntry( vTokens2, pToken, i )
Vec_PtrPush( vTokens, pToken );
nEquals += Vec_PtrSize(vTokens2)/2;
Vec_PtrFree( vTokens2 );
}
*/
// check if the number of tokens is correct // check if the number of tokens is correct
if ( nEquals != Ntl_ModelPiNum(pModel) + Ntl_ModelPoNum(pModel) ) if ( nEquals != Ntl_ModelPiNum(pModel) + Ntl_ModelPoNum(pModel) )
{ {
sprintf( p->pMan->sError, "Line %d: The number of ports (%d) in .subckt differs from the sum of PIs and POs of the model (%d).", sprintf( p->pMan->sError, "Line %d: The number of ports (%d) in .subckt %s differs from the sum of PIs and POs of the model (%d).",
Ioa_ReadGetLine(p->pMan, pToken), nEquals, Ntl_ModelPiNum(pModel) + Ntl_ModelPoNum(pModel) ); Ioa_ReadGetLine(p->pMan, pToken), nEquals, pName, Ntl_ModelPiNum(pModel) + Ntl_ModelPoNum(pModel) );
return 0; return 0;
} }

1
src/aig/saig/saig.h
View File

@ -89,6 +89,7 @@ extern int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int
/*=== saigPhase.c ==========================================================*/ /*=== saigPhase.c ==========================================================*/
extern Aig_Man_t * Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrames, int fIgnore, int fPrint, int fVerbose ); extern Aig_Man_t * Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrames, int fIgnore, int fPrint, int fVerbose );
/*=== saigRetFwd.c ==========================================================*/ /*=== saigRetFwd.c ==========================================================*/
extern void Saig_ManMarkAutonomous( Aig_Man_t * p );
extern Aig_Man_t * Saig_ManRetimeForward( Aig_Man_t * p, int nMaxIters, int fVerbose ); extern Aig_Man_t * Saig_ManRetimeForward( Aig_Man_t * p, int nMaxIters, int fVerbose );
/*=== saigRetMin.c ==========================================================*/ /*=== saigRetMin.c ==========================================================*/
extern Aig_Man_t * Saig_ManRetimeDupForward( Aig_Man_t * p, Vec_Ptr_t * vCut ); extern Aig_Man_t * Saig_ManRetimeDupForward( Aig_Man_t * p, Vec_Ptr_t * vCut );

2
src/aig/saig/saigBmc.c
View File

@ -191,6 +191,7 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
} }
else else
pFrames = Saig_ManFramesBmc( pAig, nFrames ); pFrames = Saig_ManFramesBmc( pAig, nFrames );
if ( piFrame )
*piFrame = nFrames; *piFrame = nFrames;
if ( fVerbose ) if ( fVerbose )
{ {
@ -281,6 +282,7 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
} }
else else
{ {
if ( piFrame )
*piFrame = i / Saig_ManPoNum(pAig); *piFrame = i / Saig_ManPoNum(pAig);
RetValue = -1; RetValue = -1;
break; break;

115
src/aig/saig/saigHaig.c
View File

@ -195,7 +195,7 @@ int Aig_ManMapHaigNodes( Aig_Man_t * pHaig )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Aig_ManHaigVerify( Aig_Man_t * p, Aig_Man_t * pAig, Aig_Man_t * pHaig, int nFrames ) int Aig_ManHaigVerify( Aig_Man_t * p, Aig_Man_t * pAig, Aig_Man_t * pHaig, int nFrames, int clkSynth )
{ {
int nBTLimit = 0; int nBTLimit = 0;
Aig_Man_t * pFrames, * pTemp; Aig_Man_t * pFrames, * pTemp;
@ -203,7 +203,7 @@ int Aig_ManHaigVerify( Aig_Man_t * p, Aig_Man_t * pAig, Aig_Man_t * pHaig, int n
sat_solver * pSat; sat_solver * pSat;
Aig_Obj_t * pObj1, * pObj2; Aig_Obj_t * pObj1, * pObj2;
int i, RetValue1, RetValue2, Counter, Lits[2], nOvers; int i, RetValue1, RetValue2, Counter, Lits[2], nOvers;
int clk = clock(); int clk = clock(), clkVerif;
nOvers = Aig_ManMapHaigNodes( pHaig ); nOvers = Aig_ManMapHaigNodes( pHaig );
@ -226,57 +226,6 @@ clk = clock();
// pCnf = Cnf_DeriveSimple( pFrames, Aig_ManPoNum(pFrames) ); // pCnf = Cnf_DeriveSimple( pFrames, Aig_ManPoNum(pFrames) );
pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) ); pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) );
/*
// print the statistic into a file
{
FILE * pTable;
Aig_Man_t * pTemp, * pHaig2;
pHaig2 = pAig->pManHaig;
pAig->pManHaig = NULL;
pTemp = Aig_ManDupDfs( pAig );
pAig->pManHaig = pHaig2;
Aig_ManSeqCleanup( pTemp );
pTable = fopen( "stats.txt", "a+" );
fprintf( pTable, "%s ", p->pName );
fprintf( pTable, "%d ", Saig_ManPiNum(p) );
fprintf( pTable, "%d ", Saig_ManPoNum(p) );
fprintf( pTable, "%d ", Saig_ManRegNum(p) );
fprintf( pTable, "%d ", Aig_ManNodeNum(p) );
fprintf( pTable, "%d ", Aig_ManLevelNum(p) );
fprintf( pTable, "%d ", Saig_ManRegNum(pTemp) );
fprintf( pTable, "%d ", Aig_ManNodeNum(pTemp) );
fprintf( pTable, "%d ", Aig_ManLevelNum(pTemp) );
fprintf( pTable, "%d ", Saig_ManRegNum(pHaig) );
fprintf( pTable, "%d ", Aig_ManNodeNum(pHaig) );
fprintf( pTable, "%d ", Aig_ManLevelNum(pHaig) );
fprintf( pTable, "\n" );
fclose( pTable );
pTable = fopen( "stats2.txt", "a+" );
fprintf( pTable, "%s ", p->pSpec );
fprintf( pTable, "%d ", Aig_ManNodeNum(pFrames) );
fprintf( pTable, "%d ", Aig_ManLevelNum(pFrames) );
fprintf( pTable, "%d ", pCnf->nVars );
fprintf( pTable, "%d ", pCnf->nClauses );
fprintf( pTable, "%d ", pCnf->nLiterals );
fprintf( pTable, "%d ", Aig_ManPoNum(pFrames)/2 - pFrames->nAsserts/2 );
fprintf( pTable, "%d ", pFrames->nAsserts/2 );
fprintf( pTable, "%d ", Vec_IntSize(pHaig->vEquPairs)/2 );
fprintf( pTable, "\n" );
fclose( pTable );
Aig_ManStop( pTemp );
}
*/
// pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) - pFrames->nAsserts ); // pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) - pFrames->nAsserts );
@ -375,11 +324,66 @@ clk = clock();
} }
printf( " \r" ); printf( " \r" );
PRT( "Solving ", clock() - clk ); PRT( "Solving ", clock() - clk );
clkVerif = clock() - clk;
if ( Counter ) if ( Counter )
printf( "Verification failed for %d out of %d assertions.\n", Counter, pFrames->nAsserts/2 ); printf( "Verification failed for %d out of %d assertions.\n", Counter, pFrames->nAsserts/2 );
else else
printf( "Verification is successful for all %d assertions.\n", pFrames->nAsserts/2 ); printf( "Verification is successful for all %d assertions.\n", pFrames->nAsserts/2 );
// print the statistic into a file
{
FILE * pTable;
Aig_Man_t * pTemp, * pHaig2;
pHaig2 = pAig->pManHaig;
pAig->pManHaig = NULL;
pTemp = Aig_ManDupDfs( pAig );
pAig->pManHaig = pHaig2;
Aig_ManSeqCleanup( pTemp );
pTable = fopen( "stats.txt", "a+" );
fprintf( pTable, "%s ", p->pName );
fprintf( pTable, "%d ", Saig_ManPiNum(p) );
fprintf( pTable, "%d ", Saig_ManPoNum(p) );
fprintf( pTable, "%d ", Saig_ManRegNum(p) );
fprintf( pTable, "%d ", Aig_ManNodeNum(p) );
fprintf( pTable, "%d ", Aig_ManLevelNum(p) );
fprintf( pTable, "%d ", Saig_ManRegNum(pTemp) );
fprintf( pTable, "%d ", Aig_ManNodeNum(pTemp) );
fprintf( pTable, "%d ", Aig_ManLevelNum(pTemp) );
fprintf( pTable, "%d ", Saig_ManRegNum(pHaig) );
fprintf( pTable, "%d ", Aig_ManNodeNum(pHaig) );
fprintf( pTable, "%d ", Aig_ManLevelNum(pHaig) );
fprintf( pTable, "%.2f", (float)(clkSynth)/(float)(CLOCKS_PER_SEC) );
fprintf( pTable, "\n" );
fclose( pTable );
pTable = fopen( "stats2.txt", "a+" );
fprintf( pTable, "%s ", p->pName );
fprintf( pTable, "%d ", Aig_ManNodeNum(pFrames) );
fprintf( pTable, "%d ", Aig_ManLevelNum(pFrames) );
fprintf( pTable, "%d ", pCnf->nVars );
fprintf( pTable, "%d ", pCnf->nClauses );
fprintf( pTable, "%d ", pCnf->nLiterals );
fprintf( pTable, "%d ", Aig_ManPoNum(pFrames)/2 - pFrames->nAsserts/2 );
fprintf( pTable, "%d ", pFrames->nAsserts/2 );
fprintf( pTable, "%d ", Vec_IntSize(pHaig->vEquPairs)/2 );
fprintf( pTable, "%.2f", (float)(clkVerif)/(float)(CLOCKS_PER_SEC) );
fprintf( pTable, "\n" );
fclose( pTable );
Aig_ManStop( pTemp );
}
// clean up // clean up
Aig_ManStop( pFrames ); Aig_ManStop( pFrames );
Cnf_DataFree( pCnf ); Cnf_DataFree( pCnf );
@ -617,7 +621,7 @@ Aig_Man_t * Saig_ManHaigRecord( Aig_Man_t * p, int nIters, int nSteps, int fReti
Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr; Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
Aig_Man_t * pNew, * pTemp; Aig_Man_t * pNew, * pTemp;
Aig_Obj_t * pObj; Aig_Obj_t * pObj;
int i, k, nStepsReal, clk = clock(); int i, k, nStepsReal, clk = clock(), clkSynth;
Dar_ManDefaultRwrParams( pParsRwr ); Dar_ManDefaultRwrParams( pParsRwr );
clk = clock(); clk = clock();
@ -679,6 +683,7 @@ clk = clock();
} }
} }
PRT( "Synthesis time ", clock() - clk ); PRT( "Synthesis time ", clock() - clk );
clkSynth = clock() - clk;
// use the haig for verification // use the haig for verification
// Aig_ManAntiCleanup( pNew->pManHaig ); // Aig_ManAntiCleanup( pNew->pManHaig );
@ -699,7 +704,7 @@ PRT( "Synthesis time ", clock() - clk );
} }
else else
{ {
if ( !Aig_ManHaigVerify( p, pNew, pNew->pManHaig, 1+fSeqHaig ) ) if ( !Aig_ManHaigVerify( p, pNew, pNew->pManHaig, 1+fSeqHaig, clkSynth ) )
printf( "Constructing SAT solver has failed.\n" ); printf( "Constructing SAT solver has failed.\n" );
} }

8
src/aig/saig/saigRetStep.c
View File

@ -62,6 +62,10 @@ Aig_Obj_t * Saig_ManRetimeNodeFwd( Aig_Man_t * p, Aig_Obj_t * pObj, int fMakeBug
assert( Aig_ObjPioNum(pFanin0) > 0 ); assert( Aig_ObjPioNum(pFanin0) > 0 );
assert( Aig_ObjPioNum(pFanin1) > 0 ); assert( Aig_ObjPioNum(pFanin1) > 0 );
// skip latch guns
if ( !Aig_ObjIsTravIdCurrent(p, pFanin0) && !Aig_ObjIsTravIdCurrent(p, pFanin1) )
return NULL;
// get the inputs of these registers // get the inputs of these registers
pInput0 = Saig_ManLi( p, Aig_ObjPioNum(pFanin0) - Saig_ManPiNum(p) ); pInput0 = Saig_ManLi( p, Aig_ObjPioNum(pFanin0) - Saig_ManPiNum(p) );
pInput1 = Saig_ManLi( p, Aig_ObjPioNum(pFanin1) - Saig_ManPiNum(p) ); pInput1 = Saig_ManLi( p, Aig_ObjPioNum(pFanin1) - Saig_ManPiNum(p) );
@ -90,6 +94,9 @@ Aig_Obj_t * Saig_ManRetimeNodeFwd( Aig_Man_t * p, Aig_Obj_t * pObj, int fMakeBug
pObjLo->PioNum = Aig_ManPiNum(p) - 1; pObjLo->PioNum = Aig_ManPiNum(p) - 1;
p->nRegs++; p->nRegs++;
// make sure the register is retimable.
Aig_ObjSetTravIdCurrent(p, pObjLo);
//printf( "Reg = %4d. Reg = %4d. Compl = %d. Phase = %d.\n", //printf( "Reg = %4d. Reg = %4d. Compl = %d. Phase = %d.\n",
// pFanin0->PioNum, pFanin1->PioNum, Aig_IsComplement(pObjNew), fCompl ); // pFanin0->PioNum, pFanin1->PioNum, Aig_IsComplement(pObjNew), fCompl );
@ -177,6 +184,7 @@ int Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward, int fAddBugs )
p->fCreatePios = 1; p->fCreatePios = 1;
if ( fForward ) if ( fForward )
{ {
Saig_ManMarkAutonomous( p );
for ( s = 0; s < nSteps; s++ ) for ( s = 0; s < nSteps; s++ )
{ {
Aig_ManForEachNode( p, pObj, i ) Aig_ManForEachNode( p, pObj, i )

2
src/base/abc/abcNtk.c
View File

@ -522,7 +522,7 @@ Abc_Ntk_t * Abc_NtkCreateCone( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, char * pNode
int i, k; int i, k;
assert( Abc_NtkIsLogic(pNtk) || Abc_NtkIsStrash(pNtk) ); assert( Abc_NtkIsLogic(pNtk) || Abc_NtkIsStrash(pNtk) );
assert( Abc_ObjIsNode(pNode) || (Abc_NtkIsStrash(pNtk) && Abc_AigNodeIsConst(pNode)) ); assert( Abc_ObjIsNode(pNode) || (Abc_NtkIsStrash(pNtk) && (Abc_AigNodeIsConst(pNode) || Abc_ObjIsCi(pNode))) );
// start the network // start the network
pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 ); pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 );

44
src/base/abci/abc.c
View File

@ -14291,9 +14291,9 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults // set defaults
Fra_SecSetDefaultParams( pSecPar ); Fra_SecSetDefaultParams( pSecPar );
pSecPar->TimeLimit = 600; pSecPar->TimeLimit = 0;
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Farmfwvh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "FTarmfwvh" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
@ -14308,6 +14308,17 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pSecPar->nFramesMax < 0 ) if ( pSecPar->nFramesMax < 0 )
goto usage; goto usage;
break; break;
case 'T':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-T\" should be followed by an integer.\n" );
goto usage;
}
pSecPar->TimeLimit = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pSecPar->TimeLimit < 0 )
goto usage;
break;
case 'a': case 'a':
pSecPar->fPhaseAbstract ^= 1; pSecPar->fPhaseAbstract ^= 1;
break; break;
@ -14350,9 +14361,10 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0; return 0;
usage: usage:
fprintf( pErr, "usage: dsec [-F num] [-armfwvh] <file1> <file2>\n" ); fprintf( pErr, "usage: dsec [-F num] [-T num] [-armfwvh] <file1> <file2>\n" );
fprintf( pErr, "\t performs inductive sequential equivalence checking\n" ); fprintf( pErr, "\t performs inductive sequential equivalence checking\n" );
fprintf( pErr, "\t-F num : the limit on the depth of induction [default = %d]\n", pSecPar->nFramesMax ); fprintf( pErr, "\t-F num : the limit on the depth of induction [default = %d]\n", pSecPar->nFramesMax );
fprintf( pErr, "\t-T num : the approximate runtime limit (in seconds) [default = %d]\n", pSecPar->TimeLimit );
fprintf( pErr, "\t-a : toggles the use of phase abstraction [default = %s]\n", pSecPar->fPhaseAbstract? "yes": "no" ); fprintf( pErr, "\t-a : toggles the use of phase abstraction [default = %s]\n", pSecPar->fPhaseAbstract? "yes": "no" );
fprintf( pErr, "\t-r : toggles forward retiming at the beginning [default = %s]\n", pSecPar->fRetimeFirst? "yes": "no" ); fprintf( pErr, "\t-r : toggles forward retiming at the beginning [default = %s]\n", pSecPar->fRetimeFirst? "yes": "no" );
fprintf( pErr, "\t-m : toggles min-register retiming [default = %s]\n", pSecPar->fRetimeRegs? "yes": "no" ); fprintf( pErr, "\t-m : toggles min-register retiming [default = %s]\n", pSecPar->fRetimeRegs? "yes": "no" );
@ -14459,6 +14471,9 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
// perform verification // perform verification
Abc_NtkDarProve( pNtk, pSecPar ); Abc_NtkDarProve( pNtk, pSecPar );
// Fra_SmlWriteCounterExample( stdout, Aig_Man_t * pAig, Fra_Cex_t * p )
return 0; return 0;
usage: usage:
@ -15617,20 +15632,25 @@ int Abc_CommandAbc8Read( Abc_Frame_t * pAbc, int argc, char ** argv )
char * pFileName; char * pFileName;
int c; int c;
int fMapped; int fMapped;
int fTest;
extern void * Ioa_ReadBlif( char * pFileName, int fCheck ); extern void * Ioa_ReadBlif( char * pFileName, int fCheck );
extern Aig_Man_t * Ntl_ManExtract( void * p ); 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_ManExtractNwk( void * p, Aig_Man_t * pAig, Tim_Man_t * pManTime );
// set defaults // set defaults
fMapped = 0; fMapped = 0;
fTest = 0;
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "mh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "mth" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
case 'm': case 'm':
fMapped ^= 1; fMapped ^= 1;
break; break;
case 't':
fTest ^= 1;
break;
case 'h': case 'h':
goto usage; goto usage;
default: default:
@ -15650,6 +15670,19 @@ int Abc_CommandAbc8Read( Abc_Frame_t * pAbc, int argc, char ** argv )
} }
fclose( pFile ); fclose( pFile );
if ( fTest )
{
extern void Ntl_ManFree( void * p );
extern void Ntl_ManPrintStats( void * p );
void * pTemp = Ioa_ReadBlif( pFileName, 1 );
if ( pTemp )
{
Ntl_ManPrintStats( pTemp );
Ntl_ManFree( pTemp );
}
return 0;
}
Abc_FrameClearDesign(); Abc_FrameClearDesign();
pAbc->pAbc8Ntl = Ioa_ReadBlif( pFileName, 1 ); pAbc->pAbc8Ntl = Ioa_ReadBlif( pFileName, 1 );
if ( pAbc->pAbc8Ntl == NULL ) if ( pAbc->pAbc8Ntl == NULL )
@ -15672,9 +15705,10 @@ int Abc_CommandAbc8Read( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0; return 0;
usage: usage:
fprintf( stdout, "usage: *r [-mh]\n" ); fprintf( stdout, "usage: *r [-mth]\n" );
fprintf( stdout, "\t reads the design with whiteboxes\n" ); fprintf( stdout, "\t reads the design with whiteboxes\n" );
fprintf( stdout, "\t-m : toggle extracting mapped network [default = %s]\n", fMapped? "yes": "no" ); fprintf( stdout, "\t-m : toggle extracting mapped network [default = %s]\n", fMapped? "yes": "no" );
fprintf( stdout, "\t-t : toggle reading in the test mode [default = %s]\n", fTest? "yes": "no" );
fprintf( stdout, "\t-h : print the command usage\n"); fprintf( stdout, "\t-h : print the command usage\n");
return 1; return 1;
} }

147
src/base/main/mainMC.c Normal file
View File

@ -0,0 +1,147 @@
/**CFile****************************************************************
FileName [mainMC.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [The main package.]
Synopsis [The main file for the model checker.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: main.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "mainInt.h"
#include "aig.h"
#include "saig.h"
#include "fra.h"
#include "ioa.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [The main() procedure.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int main( int argc, char * argv[] )
{
Fra_Sec_t SecPar, * pSecPar = &SecPar;
FILE * pFile;
Aig_Man_t * pAig;
int RetValue;
// BMC parameters
int nFrames = 30;
int nSizeMax = 200000;
int nBTLimit = 10000;
int fRewrite = 0;
int fNewAlgo = 1;
int fVerbose = 0;
if ( argc != 2 )
{
printf( " Expecting one command-line argument (an input file in AIGER format).\n" );
printf( " usage: %s <file.aig>", argv[0] );
return 0;
}
pFile = fopen( argv[1], "r" );
if ( pFile == NULL )
{
printf( " Cannot open input AIGER file \"%s\".\n", argv[1] );
printf( " usage: %s <file.aig>", argv[0] );
return 0;
}
fclose( pFile );
pAig = Ioa_ReadAiger( argv[1], 1 );
if ( pAig == NULL )
{
printf( " Parsing the AIGER file \"%s\" has failed.\n", argv[1] );
printf( " usage: %s <file.aig>", argv[0] );
return 0;
}
// perform BMC
Aig_ManSetRegNum( pAig, pAig->nRegs );
RetValue = Saig_ManBmcSimple( pAig, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, NULL );
// perform full-blown SEC
if ( RetValue != 0 )
{
extern void Dar_LibStart();
extern void Dar_LibStop();
extern void Cnf_ClearMemory();
Fra_SecSetDefaultParams( pSecPar );
pSecPar->nFramesMax = 2; // the max number of frames used for induction
Dar_LibStart();
RetValue = Fra_FraigSec( pAig, pSecPar );
Dar_LibStop();
Cnf_ClearMemory();
}
// perform BMC again
if ( RetValue == -1 )
{
}
// decide how to report the output
pFile = stdout;
// report the result
if ( RetValue == 0 )
{
// fprintf(stdout, "s SATIFIABLE\n");
Fra_SmlWriteCounterExample( pFile, pAig, pAig->pSeqModel );
if ( pFile != stdout )
fclose(pFile);
Aig_ManStop( pAig );
exit(10);
}
else if ( RetValue == 1 )
{
// fprintf(stdout, "s UNSATISFIABLE\n");
fprintf( pFile, "0\n" );
if ( pFile != stdout )
fclose(pFile);
Aig_ManStop( pAig );
exit(20);
}
else // if ( RetValue == -1 )
{
// fprintf(stdout, "s UNKNOWN\n");
if ( pFile != stdout )
fclose(pFile);
Aig_ManStop( pAig );
exit(0);
}
return 0;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////