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

Added backward flop order to &icheck (switch -b).

This commit is contained in:
Alan Mishchenko 2015-04-01 15:36:23 +07:00
parent 0c47d04c0b
commit 9cee436686
4 changed files with 94 additions and 17 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -36176,9 +36176,9 @@ usage:
***********************************************************************/
int Abc_CommandAbc9ICheck( Abc_Frame_t * pAbc, int argc, char ** argv )
{
int c, nFramesMax = 1, nTimeOut = 0, fEmpty = 0, fSearch = 1, fReverse = 0, fDump = 0, fVerbose = 0;
int c, nFramesMax = 1, nTimeOut = 0, fEmpty = 0, fSearch = 1, fReverse = 0, fBackTopo = 0, fDump = 0, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "MTesrdvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "MTesrbdvh" ) ) != EOF )
{
switch ( c )
{
@ -36213,6 +36213,9 @@ int Abc_CommandAbc9ICheck( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'r':
fReverse ^= 1;
break;
case 'b':
fBackTopo ^= 1;
break;
case 'd':
fDump ^= 1;
break;
@ -36237,20 +36240,21 @@ int Abc_CommandAbc9ICheck( Abc_Frame_t * pAbc, int argc, char ** argv )
}
Vec_IntFreeP( &pAbc->vIndFlops );
if ( fSearch )
pAbc->vIndFlops = Bmc_PerformISearch( pAbc->pGia, nFramesMax, nTimeOut, fReverse, fDump, fVerbose );
pAbc->vIndFlops = Bmc_PerformISearch( pAbc->pGia, nFramesMax, nTimeOut, fReverse, fBackTopo, fDump, fVerbose );
else
Bmc_PerformICheck( pAbc->pGia, nFramesMax, nTimeOut, fEmpty, fVerbose );
pAbc->nIndFrames = pAbc->vIndFlops ? nFramesMax : 0;
return 0;
usage:
Abc_Print( -2, "usage: &icheck [-MT num] [-esrdvh]\n" );
Abc_Print( -2, "usage: &icheck [-MT num] [-esrbdvh]\n" );
Abc_Print( -2, "\t performs specialized induction check\n" );
Abc_Print( -2, "\t-M num : the number of timeframes used for induction [default = %d]\n", nFramesMax );
Abc_Print( -2, "\t-T num : approximate global runtime limit in seconds [default = %d]\n", nTimeOut );
Abc_Print( -2, "\t-e : toggle using empty set of next-state functions [default = %s]\n", fEmpty? "yes": "no" );
Abc_Print( -2, "\t-s : toggle searching for a minimal subset [default = %s]\n", fSearch? "yes": "no" );
Abc_Print( -2, "\t-r : toggle searching in the reverse order [default = %s]\n", fReverse? "yes": "no" );
Abc_Print( -2, "\t-b : toggle searching in backward order from POs [default = %s]\n", fBackTopo? "yes": "no" );
Abc_Print( -2, "\t-d : toggle printing out the resulting set [default = %s]\n", fDump? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");

4
src/base/abci/abcMfs.c
View File

@ -397,7 +397,7 @@ void Abc_NtkReinsertNodes( Abc_Ntk_t * p, Abc_Ntk_t * pNtk, int iPivot )
assert( Vec_PtrSize(vNodes) + Abc_NtkCiNum(p) + Abc_NtkPoNum(p) == iPivot );
Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
{
pNodeNew = Abc_NtkObj( pNtk, Abc_NtkCiNum(p) + i );
pNodeNew = Abc_NtkObj( pNtk, Abc_NtkCiNum(p) + i + 1 );
if ( pNodeNew == NULL )
continue;
pNodeNew->pCopy = pNode;
@ -405,7 +405,7 @@ void Abc_NtkReinsertNodes( Abc_Ntk_t * p, Abc_Ntk_t * pNtk, int iPivot )
// connect internal nodes
Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
{
pNodeNew = Abc_NtkObj( pNtk, Abc_NtkCiNum(p) + i );
pNodeNew = Abc_NtkObj( pNtk, Abc_NtkCiNum(p) + i + 1 );
if ( pNodeNew == NULL )
continue;
assert( pNodeNew->pCopy == pNode );

2
src/sat/bmc/bmc.h
View File

@ -169,7 +169,7 @@ extern void Bmc_CexPrint( Abc_Cex_t * pCex, int nInputs, int fVerbo
extern int Bmc_CexVerify( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare );
/*=== bmcICheck.c ==========================================================*/
extern void Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fEmpty, int fVerbose );
extern Vec_Int_t * Bmc_PerformISearch( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fReverse, int fDump, int fVerbose );
extern Vec_Int_t * Bmc_PerformISearch( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fReverse, int fBackTopo, int fDump, int fVerbose );
/*=== bmcUnroll.c ==========================================================*/
extern Unr_Man_t * Unr_ManUnrollStart( Gia_Man_t * pGia, int fVerbose );
extern Gia_Man_t * Unr_ManUnrollFrame( Unr_Man_t * p, int f );

93
src/sat/bmc/bmcICheck.c
View File

@ -293,6 +293,69 @@ void Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fEmpty,
Vec_IntFree( vUsed );
}
/**Function*************************************************************
Synopsis [Collect flops starting from the POs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Bmc_PerformFindFlopOrder_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vRegs )
{
if ( Gia_ObjIsTravIdCurrent(p, pObj) )
return;
Gia_ObjSetTravIdCurrent(p, pObj);
if ( Gia_ObjIsCi(pObj) )
{
if ( Gia_ObjIsRo(p, pObj) )
Vec_IntPush( vRegs, Gia_ObjId(p, pObj) );
return;
}
assert( Gia_ObjIsAnd(pObj) );
Bmc_PerformFindFlopOrder_rec( p, Gia_ObjFanin0(pObj), vRegs );
Bmc_PerformFindFlopOrder_rec( p, Gia_ObjFanin1(pObj), vRegs );
}
void Bmc_PerformFindFlopOrder( Gia_Man_t * p, Vec_Int_t * vRegs )
{
Gia_Obj_t * pObj;
int i, iReg, k = 0;
// start with POs
Vec_IntClear( vRegs );
Gia_ManForEachPo( p, pObj, i )
Vec_IntPush( vRegs, Gia_ObjId(p, pObj) );
// add flop outputs in the B
Gia_ManIncrementTravId( p );
Gia_ObjSetTravIdCurrent( p, Gia_ManConst0(p) );
Gia_ManForEachObjVec( vRegs, p, pObj, i )
{
assert( Gia_ObjIsPo(p, pObj) || Gia_ObjIsRo(p, pObj) );
if ( Gia_ObjIsRo(p, pObj) )
pObj = Gia_ObjRoToRi( p, pObj );
Bmc_PerformFindFlopOrder_rec( p, Gia_ObjFanin0(pObj), vRegs );
}
// add dangling flops
Gia_ManForEachRo( p, pObj, i )
if ( !Gia_ObjIsTravIdCurrent(p, pObj) )
Vec_IntPush( vRegs, Gia_ObjId(p, pObj) );
// remove POs; keep flop outputs only; remap ObjId into CiId
assert( Vec_IntSize(vRegs) == Gia_ManCoNum(p) );
Gia_ManForEachObjVec( vRegs, p, pObj, i )
{
if ( i < Gia_ManPoNum(p) )
continue;
iReg = Gia_ObjCioId(pObj) - Gia_ManPiNum(p);
assert( iReg >= 0 && iReg < Gia_ManRegNum(p) );
Vec_IntWriteEntry( vRegs, k++, iReg );
}
Vec_IntShrink( vRegs, k );
assert( Vec_IntSize(vRegs) == Gia_ManRegNum(p) );
}
/**Function*************************************************************
Synopsis []
@ -304,12 +367,13 @@ void Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fEmpty,
SeeAlso []
***********************************************************************/
int Bmc_PerformISearchOne( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fReverse, int fVerbose, Vec_Int_t * vLits )
int Bmc_PerformISearchOne( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fReverse, int fBackTopo, int fVerbose, Vec_Int_t * vLits )
{
int fUseOldCnf = 0;
Gia_Man_t * pMiter, * pTemp;
Cnf_Dat_t * pCnf;
sat_solver * pSat;
Vec_Int_t * vRegs;
// Vec_Int_t * vLits;
int i, Iter, status;
int nLitsUsed, RetValue = 0;
@ -328,9 +392,11 @@ int Bmc_PerformISearchOne( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fRev
pCnf = Cnf_DeriveGiaRemapped( pMiter );
else
{
pMiter = Jf_ManDeriveCnf( pTemp = pMiter, 0 );
Gia_ManStop( pTemp );
pCnf = (Cnf_Dat_t *)pMiter->pData; pMiter->pData = NULL;
extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose );
//pMiter = Jf_ManDeriveCnf( pTemp = pMiter, 0 );
//Gia_ManStop( pTemp );
//pCnf = (Cnf_Dat_t *)pMiter->pData; pMiter->pData = NULL;
pCnf = Mf_ManGenerateCnf( pMiter, 8, 0, 0, 0 );
}
/*
// collect positive literals
@ -365,9 +431,15 @@ int Bmc_PerformISearchOne( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fRev
nLitsUsed++;
// try removing variables
for ( Iter = 0; Iter < Gia_ManRegNum(p); Iter++ )
vRegs = Vec_IntStartNatural( Gia_ManRegNum(p) );
if ( fBackTopo )
Bmc_PerformFindFlopOrder( p, vRegs );
if ( fReverse )
Vec_IntReverseOrder( vRegs );
// for ( Iter = 0; Iter < Gia_ManRegNum(p); Iter++ )
Vec_IntForEachEntry( vRegs, i, Iter )
{
i = fReverse ? Gia_ManRegNum(p) - 1 - Iter : Iter;
// i = fReverse ? Gia_ManRegNum(p) - 1 - Iter : Iter;
if ( Abc_LitIsCompl(Vec_IntEntry(vLits, i)) )
continue;
Vec_IntWriteEntry( vLits, i, Abc_LitNot(Vec_IntEntry(vLits, i)) );
@ -411,16 +483,17 @@ cleanup:
sat_solver_delete( pSat );
Cnf_DataFree( pCnf );
Gia_ManStop( pMiter );
Vec_IntFree( vRegs );
// Vec_IntFree( vLits );
return RetValue;
}
Vec_Int_t * Bmc_PerformISearch( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fReverse, int fDump, int fVerbose )
Vec_Int_t * Bmc_PerformISearch( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fReverse, int fBackTopo, int fDump, int fVerbose )
{
Vec_Int_t * vLits, * vFlops;
int i, f;
if ( fVerbose )
printf( "Solving M-inductiveness for design %s with %d AND nodes and %d flip-flops:\n",
Gia_ManName(p), Gia_ManAndNum(p), Gia_ManRegNum(p) );
printf( "Solving M-inductiveness for design %s with %d AND nodes and %d flip-flops with %s %s flop order:\n",
Gia_ManName(p), Gia_ManAndNum(p), Gia_ManRegNum(p), fReverse ? "reverse":"direct", fBackTopo ? "backward":"natural" );
fflush( stdout );
// collect positive literals
@ -429,7 +502,7 @@ Vec_Int_t * Bmc_PerformISearch( Gia_Man_t * p, int nFramesMax, int nTimeOut, int
Vec_IntPush( vLits, Abc_Var2Lit(i, 0) );
for ( f = 1; f <= nFramesMax; f++ )
if ( Bmc_PerformISearchOne( p, f, nTimeOut, fReverse, fVerbose, vLits ) )
if ( Bmc_PerformISearchOne( p, f, nTimeOut, fReverse, fBackTopo, fVerbose, vLits ) )
{
Vec_IntFree( vLits );
return NULL;