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

Making %ufar preserve AIG name.

This commit is contained in:
Alan Mishchenko 2026-02-13 09:52:37 -08:00
parent 2726f0e470
commit 8475386dfa
5 changed files with 84 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/base/wlc/wlcBlast.c
View File

@ -1434,6 +1434,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn )
// create AIG manager
pNew = Gia_ManStart( 5 * Wlc_NtkObjNum(p) + 1000 );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
pNew->fGiaSimple = pPar->fGiaSimple;
if ( !pPar->fGiaSimple )
Gia_ManHashAlloc( pNew );
@ -2730,7 +2731,6 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn )
Abc_FrameSetLibBox( pBoxLib );
}
//pNew->pSpec = Abc_UtilStrsav( p->pSpec ? p->pSpec : p->pName );
// dump the miter parts
if ( 0 )
{

14
src/opt/ufar/UfarMgr.cpp
View File

@ -981,6 +981,10 @@ void UfarManager::Initialize(Wlc_Ntk_t * pNtk, const set<unsigned>& types) {
profile = Profile();
_pOrigNtk = Wlc_NtkDupDfsSimple(pNtk);
if ( _pOrigNtk->pName == NULL )
_pOrigNtk->pName = Abc_UtilStrsav( pNtk->pName ? pNtk->pName : pNtk->pSpec );
if ( _pOrigNtk->pSpec == NULL )
_pOrigNtk->pSpec = Abc_UtilStrsav( pNtk->pName ? pNtk->pName : pNtk->pSpec );
Wlc_Obj_t * pObj;
int i;
@ -1083,6 +1087,16 @@ Wlc_Ntk_t * UfarManager::BuildCurrentAbstraction() {
pNew = RemoveAuxPOs(pTemp = pNew, Wlc_NtkPoNum(_pOrigNtk));
Wlc_NtkFree(pTemp);
// Preserve benchmark identity through abstraction refinements so
// downstream bit-level engines report a meaningful miter name.
if ( _pOrigNtk )
{
ABC_FREE( pNew->pName );
ABC_FREE( pNew->pSpec );
pNew->pName = Abc_UtilStrsav( _pOrigNtk->pName ? _pOrigNtk->pName : _pOrigNtk->pSpec );
pNew->pSpec = Abc_UtilStrsav( _pOrigNtk->pName ? _pOrigNtk->pName : _pOrigNtk->pSpec );
}
// Wlc_WriteVer(pNew, "Abs.v", 0, 0);
return pNew;

26
src/opt/ufar/UfarPth.cpp
View File

@ -33,6 +33,28 @@ using namespace std;
namespace UFAR {
static inline void Ufar_CopyGiaNameToAig( Gia_Man_t * pGia, Aig_Man_t * pAig )
{
char * pName = pGia->pName ? pGia->pName : pGia->pSpec;
if ( pName == NULL )
return;
if ( pAig->pName == NULL )
pAig->pName = Abc_UtilStrsav( pName );
if ( pAig->pSpec == NULL )
pAig->pSpec = Abc_UtilStrsav( pName );
}
static inline void Ufar_CopyAigNameToNtk( Aig_Man_t * pAig, Abc_Ntk_t * pNtk )
{
char * pName = pAig->pName ? pAig->pName : pAig->pSpec;
if ( pName == NULL )
return;
if ( pNtk->pName == NULL )
pNtk->pName = Abc_UtilStrsav( pName );
if ( pNtk->pSpec == NULL )
pNtk->pSpec = Abc_UtilStrsav( pName );
}
// mutext to control access to shared variables
pthread_mutex_t g_mutex;
// cv to control timer
@ -63,6 +85,7 @@ class PDR : public Solver {
Pth_Data_t * pData = (Pth_Data_t *)pArg;
_pAig = Gia_ManToAigSimple( pData->pGia );
Ufar_CopyGiaNameToAig( pData->pGia, _pAig );
Pdr_Par_t * pPdrPars = &_PdrPars;
Pdr_ManSetDefaultParams(pPdrPars);
@ -93,6 +116,7 @@ class PDRA : public Solver {
Pth_Data_t * pData = (Pth_Data_t *)pArg;
_pAig = Gia_ManToAigSimple( pData->pGia );
Ufar_CopyGiaNameToAig( pData->pGia, _pAig );
Pdr_Par_t * pPdrPars = &_PdrPars;
Pdr_ManSetDefaultParams(pPdrPars);
@ -126,7 +150,9 @@ class BMC3 : public Solver {
BMC3 ( void * pArg ) {
Pth_Data_t * pData = (Pth_Data_t *)pArg;
Aig_Man_t * pAig = Gia_ManToAigSimple( pData->pGia );
Ufar_CopyGiaNameToAig( pData->pGia, pAig );
_pNtk = Abc_NtkFromAigPhase( pAig );
Ufar_CopyAigNameToNtk( pAig, _pNtk );
Aig_ManStop( pAig );
Saig_ParBmc_t * pBmcPars = &_Pars;

21
src/opt/untk/NtkNtk.cpp
View File

@ -52,11 +52,14 @@ static inline int create_buffer(Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Int_t * vFa
Gia_Man_t * BitBlast(Wlc_Ntk_t * pNtk) {
Wlc_BstPar_t Par, * pPar = &Par;
Wlc_BstParDefault( pPar );
return Wlc_NtkBitBlast(pNtk, pPar);
//Gia_Man_t * pGia = Wlc_NtkBitBlast2(pNtk, NULL);
//printf( "Usingn old bit-blaster: " );
//Gia_ManPrintStats( pGia, NULL );
//return pGia;
Gia_Man_t * pGia = Wlc_NtkBitBlast(pNtk, pPar);
if ( pGia == NULL )
return NULL;
if ( pGia->pName == NULL )
pGia->pName = Abc_UtilStrsav( pNtk->pName ? pNtk->pName : pNtk->pSpec );
if ( pGia->pSpec == NULL )
pGia->pSpec = Abc_UtilStrsav( pNtk->pName ? pNtk->pName : pNtk->pSpec );
return pGia;
}
template<typename Functor>
@ -1292,7 +1295,15 @@ int bit_level_solve(Wlc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, const string* pFileNam
}
Aig_Man_t * pAig = Gia_ManToAig(pGia, 0);
if ( pAig->pName == NULL )
pAig->pName = Abc_UtilStrsav( pGia->pName ? pGia->pName : pGia->pSpec );
if ( pAig->pSpec == NULL )
pAig->pSpec = Abc_UtilStrsav( pGia->pName ? pGia->pName : pGia->pSpec );
Abc_Ntk_t * pAbcNtk = Abc_NtkFromAigPhase(pAig);
if ( pAbcNtk->pName == NULL )
pAbcNtk->pName = Abc_UtilStrsav( pAig->pName ? pAig->pName : pAig->pSpec );
if ( pAbcNtk->pSpec == NULL )
pAbcNtk->pSpec = Abc_UtilStrsav( pAig->pName ? pAig->pName : pAig->pSpec );
if (pFileName && !pFileName->empty())
Gia_AigerWriteSimple(pGia, &((*pFileName + ".aig")[0u]));

28
src/proof/cec/cecProve.c
View File

@ -83,6 +83,26 @@ typedef struct Par_ThData_t_
Par_Share_t * pShare;
} Par_ThData_t;
static volatile Par_Share_t * g_pUfarShare = NULL;
static inline void Cec_CopyGiaName( Gia_Man_t * pSrc, Gia_Man_t * pDst )
{
char * pName = pSrc->pName ? pSrc->pName : pSrc->pSpec;
if ( pName == NULL )
return;
if ( pDst->pName == NULL )
pDst->pName = Abc_UtilStrsav( pName );
if ( pDst->pSpec == NULL )
pDst->pSpec = Abc_UtilStrsav( pName );
}
static inline void Cec_CopyGiaNameToAig( Gia_Man_t * pGia, Aig_Man_t * pAig )
{
char * pName = pGia->pName ? pGia->pName : pGia->pSpec;
if ( pName == NULL )
return;
if ( pAig->pName == NULL )
pAig->pName = Abc_UtilStrsav( pName );
if ( pAig->pSpec == NULL )
pAig->pSpec = Abc_UtilStrsav( pName );
}
static int Cec_SProveStopUfar( int RunId )
{
(void)RunId;
@ -161,6 +181,7 @@ int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose, Par
pPars->pProgress = (void *)pThData;
}
Aig_Man_t * pAig = Gia_ManToAigSimple( p );
Cec_CopyGiaNameToAig( p, pAig );
RetValue = Saig_ManBmcScalable( pAig, pPars );
p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL;
Aig_ManStop( pAig );
@ -177,6 +198,7 @@ int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose, Par
pPars->pProgress = (void *)pThData;
}
Aig_Man_t * pAig = Gia_ManToAigSimple( p );
Cec_CopyGiaNameToAig( p, pAig );
RetValue = Pdr_ManSolve( pAig, pPars );
p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL;
Aig_ManStop( pAig );
@ -194,6 +216,7 @@ int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose, Par
pPars->pProgress = (void *)pThData;
}
Aig_Man_t * pAig = Gia_ManToAigSimple( p );
Cec_CopyGiaNameToAig( p, pAig );
RetValue = Saig_ManBmcScalable( pAig, pPars );
p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL;
Aig_ManStop( pAig );
@ -211,6 +234,7 @@ int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose, Par
pPars->pProgress = (void *)pThData;
}
Aig_Man_t * pAig = Gia_ManToAigSimple( p );
Cec_CopyGiaNameToAig( p, pAig );
RetValue = Pdr_ManSolve( pAig, pPars );
p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL;
Aig_ManStop( pAig );
@ -313,6 +337,7 @@ void Cec_GiaInitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t * p, int
for ( i = 0; i < nWorkers; i++ )
{
ThData[i].p = Gia_ManDup(p);
Cec_CopyGiaName( p, ThData[i].p );
ThData[i].iEngine = (fUseUif && i == nWorkers - 1) ? PAR_ENGINE_UFAR : i;
ThData[i].nTimeOut = nTimeOut;
ThData[i].fWorking = 0;
@ -414,7 +439,8 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in
}
if ( !fSilent )
{
printf( "Problem \"%s\" is ", p->pSpec );
char * pProbName = p->pSpec ? p->pSpec : Gia_ManName(p);
printf( "Problem \"%s\" is ", pProbName ? pProbName : "(none)" );
if ( RetValue == 0 )
printf( "SATISFIABLE (solved by %d).", RetEngine );
else if ( RetValue == 1 )