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

Making &gla iterate over property outputs.

This commit is contained in:
Alan Mishchenko 2019-12-11 21:13:00 -08:00
parent 4f4b207f2f
commit 6fb8b17c2d
3 changed files with 61 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -1293,6 +1293,7 @@ extern Gia_Man_t * Gia_ManDupFlopClass( Gia_Man_t * p, int iClass );
extern Gia_Man_t * Gia_ManDupMarked( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupTimes( Gia_Man_t * p, int nTimes );
extern Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupDfsOnePo( Gia_Man_t * p, int iPo );
extern Gia_Man_t * Gia_ManDupCofactorVar( Gia_Man_t * p, int iVar, int Value );
extern Gia_Man_t * Gia_ManDupCofactorObj( Gia_Man_t * p, int iObj, int Value );
extern Gia_Man_t * Gia_ManDupMux( int iVar, Gia_Man_t * pCof1, Gia_Man_t * pCof0 );

24
src/aig/gia/giaDup.c
View File

@ -1556,6 +1556,30 @@ Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p )
pNew->pCexSeq = Abc_CexDup( p->pCexSeq, Gia_ManRegNum(p) );
return pNew;
}
Gia_Man_t * Gia_ManDupDfsOnePo( Gia_Man_t * p, int iPo )
{
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj;
int i;
assert( iPo >= 0 && iPo < Gia_ManPoNum(p) );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
Gia_ManFillValue( p );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
Gia_ManForEachCo( p, pObj, i )
if ( !Gia_ObjIsPo(p, pObj) || i == iPo )
Gia_ManDupDfs_rec( pNew, p, Gia_ObjFanin0(pObj) );
Gia_ManForEachCo( p, pObj, i )
if ( !Gia_ObjIsPo(p, pObj) || i == iPo )
pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
return pNew;
}
/**Function*************************************************************

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

@ -45764,11 +45764,6 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
}
*/
if ( Gia_ManPoNum(pAbc->pGia) > 1 )
{
Abc_Print( 1, "The network is more than one PO (run \"orpos\").\n" );
return 0;
}
if ( pPars->nFramesMax < 0 )
{
Abc_Print( 1, "The number of starting frames should be a positive integer.\n" );
@ -45779,14 +45774,42 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( 1, "The starting frame is larger than the max number of frames.\n" );
return 0;
}
if ( fNewAlgo )
pAbc->Status = Gia_ManPerformGla( pAbc->pGia, pPars );
else
pAbc->Status = Gia_ManPerformGlaOld( pAbc->pGia, pPars, 0 );
pAbc->nFrames = pPars->iFrame;
Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
if ( pLogFileName )
Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "&gla" );
if ( Gia_ManPoNum(pAbc->pGia) == 1 )
{
if ( fNewAlgo )
pAbc->Status = Gia_ManPerformGla( pAbc->pGia, pPars );
else
pAbc->Status = Gia_ManPerformGlaOld( pAbc->pGia, pPars, 0 );
pAbc->nFrames = pPars->iFrame;
Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
if ( pLogFileName )
Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "&gla" );
}
else // iterate over outputs
{
Gia_Obj_t * pObj; int o, Status;
Vec_Ptr_t * vSeqModelVec = Vec_PtrStart( Gia_ManPoNum(pAbc->pGia) );
Vec_Int_t * vStatuses = Vec_IntAlloc( Gia_ManPoNum(pAbc->pGia) );
Gia_ManForEachPo( pAbc->pGia, pObj, o )
{
Gia_Man_t * pOne = Gia_ManDupDfsOnePo( pAbc->pGia, o );
if ( fNewAlgo )
Status = Gia_ManPerformGla( pOne, pPars );
else
Status = Gia_ManPerformGlaOld( pOne, pPars, 0 );
Vec_IntPush( vStatuses, Status );
if ( pLogFileName )
Abc_NtkWriteLogFile( pLogFileName, pOne->pCexSeq, Status, pPars->iFrame, "&gla" );
if ( pOne->pCexSeq )
Vec_PtrWriteEntry( vSeqModelVec, o, pOne->pCexSeq );
pOne->pCexSeq = NULL;
Gia_ManStop( pOne );
}
assert( Vec_IntSize(vStatuses) == Gia_ManPoNum(pAbc->pGia) );
Abc_FrameReplaceCexVec( pAbc, &vSeqModelVec );
Abc_FrameReplacePoStatuses( pAbc, &vStatuses );
pAbc->nFrames = -1;
}
return 0;
usage: