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

Added deriving abstraction in GIA from the precomputed flop map.

This commit is contained in:
Alan Mishchenko 2011-07-29 16:21:25 +07:00
parent ce38474c74
commit dac71e9b33
7 changed files with 115 additions and 62 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -656,6 +656,7 @@ extern Gia_Man_t * Gia_ManMiter( Gia_Man_t * pAig0, Gia_Man_t * pAig1, i
extern Gia_Man_t * Gia_ManTransformMiter( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManChoiceMiter( Vec_Ptr_t * vGias );
extern Gia_Man_t * Gia_ManDupWithConstraints( Gia_Man_t * p, Vec_Int_t * vPoTypes );
extern Gia_Man_t * Gia_ManDupAbstraction( Gia_Man_t * p, Vec_Int_t * vFlopClasses );
/*=== giaEnable.c ==========================================================*/
extern void Gia_ManDetectSeqSignals( Gia_Man_t * p, int fSetReset, int fVerbose );
extern Gia_Man_t * Gia_ManUnrollAndCofactor( Gia_Man_t * p, int nFrames, int nFanMax, int fVerbose );

40
src/aig/gia/giaAbs.c
View File

@ -120,12 +120,12 @@ Vec_Int_t * Gia_ManClasses2Flops( Vec_Int_t * vFlopClasses )
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManCexAbstraction( Gia_Man_t * p, Vec_Int_t * vFlops )
Gia_Man_t * Gia_ManDupAbstractionAig( Gia_Man_t * p, Vec_Int_t * vFlops )
{
Gia_Man_t * pGia;
Aig_Man_t * pNew, * pTemp;
pNew = Gia_ManToAig( p, 0 );
pNew = Saig_ManDeriveAbstraction( pTemp = pNew, vFlops );
pNew = Saig_ManDupAbstraction( pTemp = pNew, vFlops );
Aig_ManStop( pTemp );
pGia = Gia_ManFromAig( pNew );
// pGia->vCiNumsOrig = pNew->vCiNumsOrig;
@ -166,32 +166,6 @@ void Gia_ManCexAbstractionStart( Gia_Man_t * pGia, Gia_ParAbs_t * pPars )
}
}
/**Function*************************************************************
Synopsis [Derives abstraction using the latch map.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManCexAbstractionDerive( Gia_Man_t * pGia )
{
Vec_Int_t * vFlops;
Gia_Man_t * pAbs = NULL;
if ( pGia->vFlopClasses == NULL )
{
printf( "Gia_ManCexAbstractionDerive(): Abstraction latch map is missing.\n" );
return NULL;
}
vFlops = Gia_ManClasses2Flops( pGia->vFlopClasses );
pAbs = Gia_ManCexAbstraction( pGia, vFlops );
Vec_IntFree( vFlops );
return pAbs;
}
/**Function*************************************************************
Synopsis [Refines abstraction using the latch map.]
@ -273,8 +247,7 @@ int Gia_ManPbaPerform( Gia_Man_t * pGia, int nFrames, int nConfLimit, int fVerbo
return 0;
}
// derive abstraction
vFlops = Saig_ManClasses2Flops( pGia->vFlopClasses );
pAbs = Gia_ManCexAbstraction( pGia, vFlops );
pAbs = Gia_ManDupAbstraction( pGia, pGia->vFlopClasses );
// refine abstraction using PBA
pAig = Gia_ManToAigSimple( pAbs );
Gia_ManStop( pAbs );
@ -283,6 +256,7 @@ int Gia_ManPbaPerform( Gia_Man_t * pGia, int nFrames, int nConfLimit, int fVerbo
// derive new classes
if ( vFlopsNew != NULL )
{
vFlops = Gia_ManClasses2Flops( pGia->vFlopClasses );
vSelected = Gia_ManFlopsSelect( vFlops, vFlopsNew );
Vec_IntFree( pGia->vFlopClasses );
pGia->vFlopClasses = Saig_ManFlops2Classes( Gia_ManRegNum(pGia), vSelected );
@ -292,7 +266,6 @@ int Gia_ManPbaPerform( Gia_Man_t * pGia, int nFrames, int nConfLimit, int fVerbo
Vec_IntFree( vFlops );
return 1;
}
Vec_IntFree( vFlops );
// found counter-eample for the abstracted model
// or exceeded conflict limit
return 0;
@ -321,8 +294,7 @@ int Gia_ManCbaPerform( Gia_Man_t * pGia, void * p )
pGia->vFlopClasses = Vec_IntStart( Gia_ManRegNum(pGia) );
}
// derive abstraction
vFlops = Saig_ManClasses2Flops( pGia->vFlopClasses );
pAbs = Gia_ManCexAbstraction( pGia, vFlops );
pAbs = Gia_ManDupAbstraction( pGia, pGia->vFlopClasses );
// refine abstraction using PBA
pAig = Gia_ManToAigSimple( pAbs );
Gia_ManStop( pAbs );
@ -331,6 +303,7 @@ int Gia_ManCbaPerform( Gia_Man_t * pGia, void * p )
// derive new classes
if ( vFlopsNew != NULL )
{
vFlops = Gia_ManClasses2Flops( pGia->vFlopClasses );
// vSelected = Saig_ManFlopsSelect( vFlops, vFlopsNew );
vSelected = NULL;
Vec_IntFree( pGia->vFlopClasses );
@ -341,7 +314,6 @@ int Gia_ManCbaPerform( Gia_Man_t * pGia, void * p )
Vec_IntFree( vFlops );
return 1;
}
Vec_IntFree( vFlops );
// found counter-eample for the abstracted model
// or exceeded conflict limit
return 0;

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

@ -1506,6 +1506,81 @@ Gia_Man_t * Gia_ManDupWithConstraints( Gia_Man_t * p, Vec_Int_t * vPoTypes )
return pNew;
}
/**Function*************************************************************
Synopsis [Duplicates the AIG manager recursively.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManDupAbstraction_rec( Gia_Man_t * pNew, Gia_Obj_t * pObj )
{
if ( ~pObj->Value )
return;
Gia_ManDupAbstraction_rec( pNew, Gia_ObjFanin0(pObj) );
Gia_ManDupAbstraction_rec( pNew, Gia_ObjFanin1(pObj) );
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
}
/**Function*************************************************************
Synopsis [Performs abstraction of the AIG to preserve the included flops.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManDupAbstraction( Gia_Man_t * p, Vec_Int_t * vFlopClasses )
{
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj;
int i, nFlops = 0;
Gia_ManFillValue( p );
// start the new manager
pNew = Gia_ManStart( 5000 );
pNew->pName = Gia_UtilStrsav( p->pName );
// create PIs
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachPi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
// create additional PIs
Gia_ManForEachRo( p, pObj, i )
if ( !Vec_IntEntry(vFlopClasses, i) )
pObj->Value = Gia_ManAppendCi(pNew);
// create ROs
Gia_ManForEachRo( p, pObj, i )
if ( Vec_IntEntry(vFlopClasses, i) )
pObj->Value = Gia_ManAppendCi(pNew);
// create POs
Gia_ManHashAlloc( pNew );
Gia_ManForEachPo( p, pObj, i )
{
Gia_ManDupAbstraction_rec( pNew, Gia_ObjFanin0(pObj) );
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
}
// create RIs
Gia_ManForEachRi( p, pObj, i )
if ( Vec_IntEntry(vFlopClasses, i) )
{
Gia_ManDupAbstraction_rec( pNew, Gia_ObjFanin0(pObj) );
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
nFlops++;
}
Gia_ManHashStop( pNew );
Gia_ManSetRegNum( pNew, nFlops );
// clean up
pNew = Gia_ManSeqCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
return pNew;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

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

@ -154,7 +154,7 @@ extern Aig_Man_t * Saig_ManDupUnfoldConstrsFunc( Aig_Man_t * pAig, int nFr
/*=== saigDup.c ==========================================================*/
extern Aig_Man_t * Saig_ManDupOrpos( Aig_Man_t * p );
extern Aig_Man_t * Saig_ManCreateEquivMiter( Aig_Man_t * pAig, Vec_Int_t * vPairs );
extern Aig_Man_t * Saig_ManDeriveAbstraction( Aig_Man_t * pAig, Vec_Int_t * vFlops );
extern Aig_Man_t * Saig_ManDupAbstraction( Aig_Man_t * pAig, Vec_Int_t * vFlops );
extern int Saig_ManVerifyCex( Aig_Man_t * pAig, Abc_Cex_t * p );
extern int Saig_ManFindFailedPoCex( Aig_Man_t * pAig, Abc_Cex_t * p );
/*=== saigHaig.c ==========================================================*/

6
src/aig/saig/saigAbsStart.c
View File

@ -204,7 +204,7 @@ Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlo
Vec_IntForEachEntryStart( vFlops, Entry, i, 1 )
assert( Vec_IntEntry(vFlops, i-1) != Entry );
return Saig_ManDeriveAbstraction( p, vFlops );
return Saig_ManDupAbstraction( p, vFlops );
}
/**Function*************************************************************
@ -223,7 +223,7 @@ int Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlops, Abc_Cex_t * pCex,
Aig_Man_t * pAbs;
Vec_Int_t * vFlopsNew;
int i, Entry, clk = clock();
pAbs = Saig_ManDeriveAbstraction( p, vFlops );
pAbs = Saig_ManDupAbstraction( p, vFlops );
if ( fSensePath )
vFlopsNew = Saig_ManExtendCounterExampleTest2( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pCex, fVerbose );
else
@ -291,7 +291,7 @@ Vec_Int_t * Saig_ManCexAbstractionFlops( Aig_Man_t * p, Gia_ParAbs_t * pPars )
Vec_IntPush( vFlops, iFlop );
*/
// create the resulting AIG
pAbs = Saig_ManDeriveAbstraction( p, vFlops );
pAbs = Saig_ManDupAbstraction( p, vFlops );
if ( !pPars->fVerbose )
{
printf( "Init : " );

44
src/aig/saig/saigDup.c
View File

@ -127,26 +127,6 @@ Aig_Man_t * Saig_ManCreateEquivMiter( Aig_Man_t * pAig, Vec_Int_t * vPairs )
return pAigNew;
}
/**Function*************************************************************
Synopsis [Duplicates the AIG manager recursively.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Obj_t * Saig_ManAbstractionDfs_rec( Aig_Man_t * pNew, Aig_Obj_t * pObj )
{
if ( pObj->pData )
return (Aig_Obj_t *)pObj->pData;
Saig_ManAbstractionDfs_rec( pNew, Aig_ObjFanin0(pObj) );
Saig_ManAbstractionDfs_rec( pNew, Aig_ObjFanin1(pObj) );
return (Aig_Obj_t *)(pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ));
}
/**Function*************************************************************
Synopsis [Trims the model by removing PIs without fanout.]
@ -191,6 +171,26 @@ Aig_Man_t * Saig_ManTrimPis( Aig_Man_t * p )
return pNew;
}
/**Function*************************************************************
Synopsis [Duplicates the AIG manager recursively.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Obj_t * Saig_ManAbstractionDfs_rec( Aig_Man_t * pNew, Aig_Obj_t * pObj )
{
if ( pObj->pData )
return (Aig_Obj_t *)pObj->pData;
Saig_ManAbstractionDfs_rec( pNew, Aig_ObjFanin0(pObj) );
Saig_ManAbstractionDfs_rec( pNew, Aig_ObjFanin1(pObj) );
return (Aig_Obj_t *)(pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ));
}
/**Function*************************************************************
Synopsis [Performs abstraction of the AIG to preserve the included flops.]
@ -202,14 +202,14 @@ Aig_Man_t * Saig_ManTrimPis( Aig_Man_t * p )
SeeAlso []
***********************************************************************/
Aig_Man_t * Saig_ManDeriveAbstraction( Aig_Man_t * p, Vec_Int_t * vFlops )
Aig_Man_t * Saig_ManDupAbstraction( Aig_Man_t * p, Vec_Int_t * vFlops )
{
Aig_Man_t * pNew;//, * pTemp;
Aig_Obj_t * pObj, * pObjLi, * pObjLo;
int i, Entry;
Aig_ManCleanData( p );
// start the new manager
pNew = Aig_ManStart( Aig_ManNodeNum(p) );
pNew = Aig_ManStart( 5000 );
pNew->pName = Aig_UtilStrsav( p->pName );
// map the constant node
Aig_ManConst1(p)->pData = Aig_ManConst1( pNew );

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

@ -27955,13 +27955,18 @@ int Abc_CommandAbc9AbsDerive( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "The network is combinational.\n" );
return 0;
}
pTemp = Gia_ManCexAbstractionDerive( pAbc->pGia );
if ( pAbc->pGia->vFlopClasses == NULL )
{
Abc_Print( -1, "Abstraction flop map is missing.\n" );
return 0;
}
pTemp = Gia_ManDupAbstraction( pAbc->pGia, pAbc->pGia->vFlopClasses );
Abc_CommandUpdate9( pAbc, pTemp );
return 0;
usage:
Abc_Print( -2, "usage: &abs_derive [-vh]\n" );
Abc_Print( -2, "\t performs abstraction using the pre-computed flop map\n" );
Abc_Print( -2, "\t derives abstracted model using the pre-computed flop map\n" );
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");
return 1;