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

Extending &verify to handle combinational designs.

This commit is contained in:
Alan Mishchenko 2026-01-27 21:52:26 +07:00
parent d1157cae39
commit dd21791031
3 changed files with 147 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -5816,10 +5816,12 @@ void Gia_ManProdAdderGen( int nArgA, int nArgB, int Seed, int fSigned, int fCla
/**Function*************************************************************
Synopsis []
Synopsis [Adds a dummy flop to the design.]
Description [Duplicates the AIG while adding one flop with constant 0 input
and no fanout. Handles designs with boxes by also duplicating
the timing manager with an additional CI/CO pair.]
Description []
SideEffects []
SeeAlso []
@ -5827,11 +5829,13 @@ void Gia_ManProdAdderGen( int nArgA, int nArgB, int Seed, int fSigned, int fCla
***********************************************************************/
Gia_Man_t * Gia_ManDupAddFlop( Gia_Man_t * p )
{
extern Tim_Man_t * Tim_ManDupAddFlop( Tim_Man_t * p, int fUnitDelay );
Gia_Man_t * pNew;
Gia_Obj_t * pObj;
int i;
pNew = Gia_ManStart( Gia_ManObjNum(p) + 2 );
pNew->pName = Abc_UtilStrsav(p->pName);
pNew->pSpec = Abc_UtilStrsav(p->pSpec);
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi( pNew );
@ -5840,8 +5844,40 @@ Gia_Man_t * Gia_ManDupAddFlop( Gia_Man_t * p )
pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
Gia_ManForEachCo( p, pObj, i )
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Gia_ManAppendCo( pNew, 0 );
Gia_ManAppendCo( pNew, 0 );
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p)+1 );
if ( p->pManTime )
pNew->pManTime = Tim_ManDupAddFlop( (Tim_Man_t *)p->pManTime, 0 );
if ( p->pAigExtra )
pNew->pAigExtra = Gia_ManDup( p->pAigExtra );
if ( p->vCiArrs )
{
pNew->vCiArrs = Vec_IntDup( p->vCiArrs );
Vec_IntPush( pNew->vCiArrs, 0.0 ); // default arrival for new flop output
}
if ( p->vCoReqs )
{
pNew->vCoReqs = Vec_IntDup( p->vCoReqs );
Vec_IntPush( pNew->vCoReqs, ABC_INFINITY ); // default required for new flop input
}
if ( p->vCoArrs )
{
pNew->vCoArrs = Vec_IntDup( p->vCoArrs );
Vec_IntPush( pNew->vCoArrs, 0.0 ); // default arrival for new flop input
}
if ( p->vCoAttrs )
{
pNew->vCoAttrs = Vec_IntDup( p->vCoAttrs );
Vec_IntPush( pNew->vCoAttrs, 0 ); // default attribute for new flop input
}
// copy other timing-related fields
pNew->And2Delay = p->And2Delay;
if ( p->vInArrs )
pNew->vInArrs = Vec_FltDup( p->vInArrs );
if ( p->vOutReqs )
pNew->vOutReqs = Vec_FltDup( p->vOutReqs );
pNew->DefInArrs = p->DefInArrs;
pNew->DefOutReqs = p->DefOutReqs;
return pNew;
}

10
src/aig/gia/giaTim.c
View File

@ -1128,6 +1128,16 @@ int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, int nBTLimit, int nTimeLim, int fS
// compute the miter
if ( fSeq )
{
extern Gia_Man_t * Gia_ManDupAddFlop( Gia_Man_t * p );
if ( Gia_ManRegNum(pGia0) == 0 ) {
pGia0 = Gia_ManDupAddFlop( pMiter = pGia0 );
Gia_ManStop( pMiter );
}
if ( Gia_ManRegNum(pGia1) == 0 ) {
pGia1 = Gia_ManDupAddFlop( pMiter = pGia1 );
Gia_ManStop( pMiter );
}
pMiter = Gia_ManMiter( pGia0, pGia1, 0, 0, 1, 0, fVerbose );
if ( pMiter )
{

97
src/misc/tim/timMan.c
View File

@ -152,6 +152,103 @@ Tim_Man_t * Tim_ManDup( Tim_Man_t * p, int fUnitDelay )
return pNew;
}
/**Function*************************************************************
Synopsis [Duplicates the timing manager while adding one flop.]
Description [Creates a new timing manager with one additional CI/CO pair
for a new flop. The new CI and CO are added at the end,
after all box inputs/outputs.]
SideEffects []
SeeAlso []
***********************************************************************/
Tim_Man_t * Tim_ManDupAddFlop( Tim_Man_t * p, int fUnitDelay )
{
Tim_Man_t * pNew;
Tim_Box_t * pBox;
Tim_Obj_t * pObj;
float * pDelayTable, * pDelayTableNew;
int i, k, nInputs, nOutputs;
// clear traversal IDs
Tim_ManForEachCi( p, pObj, i )
pObj->TravId = 0;
Tim_ManForEachCo( p, pObj, i )
pObj->TravId = 0;
// create new manager with one additional CI and CO
pNew = Tim_ManStart( p->nCis + 1, p->nCos + 1 );
// copy existing CI connectivity information
memcpy( pNew->pCis, p->pCis, sizeof(Tim_Obj_t) * p->nCis );
// Initialize the new CI (flop output)
pNew->pCis[p->nCis].Id = p->nCis;
pNew->pCis[p->nCis].iObj2Box = -1;
pNew->pCis[p->nCis].iObj2Num = -1;
pNew->pCis[p->nCis].timeArr = 0.0;
pNew->pCis[p->nCis].timeReq = TIM_ETERNITY;
// copy existing CO connectivity information
memcpy( pNew->pCos, p->pCos, sizeof(Tim_Obj_t) * p->nCos );
// Initialize the new CO (flop input)
pNew->pCos[p->nCos].Id = p->nCos;
pNew->pCos[p->nCos].iObj2Box = -1;
pNew->pCos[p->nCos].iObj2Num = -1;
pNew->pCos[p->nCos].timeArr = 0.0;
pNew->pCos[p->nCos].timeReq = TIM_ETERNITY;
if ( fUnitDelay )
{
// clear PI arrival and PO required
Tim_ManInitPiArrivalAll( pNew, 0.0 );
Tim_ManInitPoRequiredAll( pNew, (float)TIM_ETERNITY );
}
// duplicate delay tables
if ( Tim_ManDelayTableNum(p) > 0 )
{
pNew->vDelayTables = Vec_PtrStart( Vec_PtrSize(p->vDelayTables) );
Tim_ManForEachTable( p, pDelayTable, i )
{
if ( pDelayTable == NULL )
continue;
assert( i == (int)pDelayTable[0] );
nInputs = (int)pDelayTable[1];
nOutputs = (int)pDelayTable[2];
pDelayTableNew = ABC_ALLOC( float, 3 + nInputs * nOutputs );
pDelayTableNew[0] = (int)pDelayTable[0];
pDelayTableNew[1] = (int)pDelayTable[1];
pDelayTableNew[2] = (int)pDelayTable[2];
for ( k = 0; k < nInputs * nOutputs; k++ )
if ( pDelayTable[3+k] == -ABC_INFINITY )
pDelayTableNew[3+k] = -ABC_INFINITY;
else
pDelayTableNew[3+k] = fUnitDelay ? (float)fUnitDelay : pDelayTable[3+k];
assert( Vec_PtrEntry(pNew->vDelayTables, i) == NULL );
Vec_PtrWriteEntry( pNew->vDelayTables, i, pDelayTableNew );
}
}
// duplicate boxes
if ( Tim_ManBoxNum(p) > 0 )
{
pNew->vBoxes = Vec_PtrAlloc( Tim_ManBoxNum(p) );
Tim_ManForEachBox( p, pBox, i )
{
Tim_ManCreateBox( pNew, pBox->Inouts[0], pBox->nInputs,
pBox->Inouts[pBox->nInputs], pBox->nOutputs, pBox->iDelayTable, pBox->fBlack );
Tim_ManBoxSetCopy( pNew, i, pBox->iCopy );
}
}
return pNew;
}
/**Function*************************************************************
Synopsis [Trims the timing manager.]