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

Changes to enable CEX minimization.

This commit is contained in:
Alan Mishchenko 2011-08-01 12:13:49 +07:00
parent 02b04efe9c
commit 81620f2e92
4 changed files with 538 additions and 83 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
abclib.dsp
View File

@ -2421,6 +2421,10 @@ SOURCE=.\src\misc\util\utilMem.h
SOURCE=.\src\misc\util\utilSignal.c
# End Source File
# Begin Source File
SOURCE=.\src\misc\util\utilSort.c
# End Source File
# End Group
# Begin Group "nm"
@ -3511,6 +3515,10 @@ SOURCE=.\src\aig\saig\saigBmc3.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\saig\saigCexMin.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\saig\saigCone.c
# End Source File
# Begin Source File

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

@ -144,6 +144,8 @@ extern int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFra
/*=== saigBmc3.c ==========================================================*/
extern void Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p );
extern int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars );
/*=== saigCexMin.c ==========================================================*/
extern Abc_Cex_t * Saig_ManCexMinPerform( Aig_Man_t * pAig, Abc_Cex_t * pCex );
/*=== saigCone.c ==========================================================*/
extern void Saig_ManPrintCones( Aig_Man_t * p );
/*=== saigConstr.c ==========================================================*/

330
src/aig/saig/saigCexMin.c Normal file
View File

@ -0,0 +1,330 @@
/**CFile****************************************************************
FileName [saigCexMin.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Sequential AIG package.]
Synopsis [CEX minimization.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: saigCexMin.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "saig.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Returns reasons for the property to fail.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Saig_ManCexMinFindReason_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t * vPrios, Vec_Int_t * vReasonPis, Vec_Int_t * vReasonLis )
{
if ( Aig_ObjIsTravIdCurrent(p, pObj) )
return;
Aig_ObjSetTravIdCurrent(p, pObj);
if ( Saig_ObjIsPi(p, pObj) )
{
Vec_IntPush( vReasonPis, Aig_ObjPioNum(pObj) );
return;
}
if ( Saig_ObjIsLo(p, pObj) )
{
Vec_IntPush( vReasonLis, Aig_ObjPioNum(pObj) - Aig_ManRegNum(p) );
return;
}
assert( Aig_ObjIsNode(pObj) );
if ( pObj->fPhase )
{
Saig_ManCexMinFindReason_rec( p, Aig_ObjFanin0(pObj), vPrios, vReasonPis, vReasonLis );
Saig_ManCexMinFindReason_rec( p, Aig_ObjFanin1(pObj), vPrios, vReasonPis, vReasonLis );
}
else
{
int fPhase0 = Aig_ObjFaninC0(pObj) ^ Aig_ObjFanin0(pObj)->fPhase;
int fPhase1 = Aig_ObjFaninC1(pObj) ^ Aig_ObjFanin1(pObj)->fPhase;
assert( !fPhase0 || !fPhase1 );
if ( !fPhase0 && fPhase1 )
Saig_ManCexMinFindReason_rec( p, Aig_ObjFanin0(pObj), vPrios, vReasonPis, vReasonLis );
else if ( fPhase0 && !fPhase1 )
Saig_ManCexMinFindReason_rec( p, Aig_ObjFanin1(pObj), vPrios, vReasonPis, vReasonLis );
else
{
int iPrio0 = Vec_IntEntry( vPrios, Aig_ObjFaninId0(pObj) );
int iPrio1 = Vec_IntEntry( vPrios, Aig_ObjFaninId1(pObj) );
if ( iPrio0 >= iPrio1 )
Saig_ManCexMinFindReason_rec( p, Aig_ObjFanin0(pObj), vPrios, vReasonPis, vReasonLis );
else
Saig_ManCexMinFindReason_rec( p, Aig_ObjFanin1(pObj), vPrios, vReasonPis, vReasonLis );
}
}
}
/**Function*************************************************************
Synopsis [Recursively sets phase and priority.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Saig_ManCexMinComputePrio_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vPrios )
{
if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
return;
Aig_ObjSetTravIdCurrent(pAig, pObj);
if ( Aig_ObjIsPo(pObj) )
{
Saig_ManCexMinComputePrio_rec( pAig, Aig_ObjFanin0(pObj), vPrios );
pObj->fPhase = Aig_ObjFaninC0(pObj) ^ Aig_ObjFanin0(pObj)->fPhase;
Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), Vec_IntEntry( vPrios, Aig_ObjFaninId0(pObj) ) );
}
else if ( Aig_ObjIsNode(pObj) )
{
int fPhase0, fPhase1, iPrio0, iPrio1;
Saig_ManCexMinComputePrio_rec( pAig, Aig_ObjFanin0(pObj), vPrios );
Saig_ManCexMinComputePrio_rec( pAig, Aig_ObjFanin1(pObj), vPrios );
fPhase0 = Aig_ObjFaninC0(pObj) ^ Aig_ObjFanin0(pObj)->fPhase;
fPhase1 = Aig_ObjFaninC1(pObj) ^ Aig_ObjFanin1(pObj)->fPhase;
iPrio0 = Vec_IntEntry( vPrios, Aig_ObjFaninId0(pObj) );
iPrio1 = Vec_IntEntry( vPrios, Aig_ObjFaninId1(pObj) );
pObj->fPhase = fPhase0 && fPhase1;
if ( fPhase0 && fPhase1 ) // both are one
Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), Abc_MinInt(iPrio0, iPrio1) );
else if ( !fPhase0 && fPhase1 )
Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), iPrio0 );
else if ( fPhase0 && !fPhase1 )
Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), iPrio1 );
else // both are zero
Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), Abc_MaxInt(iPrio0, iPrio1) );
}
}
/**Function*************************************************************
Synopsis [Collect nodes in the unrolled timeframes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Saig_ManCollectFrameTerms_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vFramePis, Vec_Int_t * vFrameLis )
{
if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
return;
Aig_ObjSetTravIdCurrent(pAig, pObj);
if ( Aig_ObjIsPo(pObj) )
Saig_ManCollectFrameTerms_rec( pAig, Aig_ObjFanin0(pObj), vFramePis, vFrameLis );
else if ( Aig_ObjIsNode(pObj) )
{
Saig_ManCollectFrameTerms_rec( pAig, Aig_ObjFanin0(pObj), vFramePis, vFrameLis );
Saig_ManCollectFrameTerms_rec( pAig, Aig_ObjFanin1(pObj), vFramePis, vFrameLis );
}
if ( Saig_ObjIsPi( pAig, pObj ) )
Vec_IntPush( vFramePis, Aig_ObjId(pObj) );
if ( vFrameLis && Saig_ObjIsLo( pAig, pObj ) )
Vec_IntPush( vFrameLis, Aig_ObjId( Saig_ObjLoToLi(pAig, pObj) ) );
}
/**Function*************************************************************
Synopsis [Derive unrolled timeframes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Saig_ManCollectFrameTerms( Aig_Man_t * pAig, Abc_Cex_t * pCex, Vec_Vec_t * vFramePis, Vec_Vec_t * vFrameLis )
{
Aig_Obj_t * pObj;
int i, f, Entry;
// sanity checks
assert( Saig_ManPiNum(pAig) == pCex->nPis );
assert( Saig_ManRegNum(pAig) == pCex->nRegs );
assert( pCex->iPo >= 0 && pCex->iPo < Saig_ManPoNum(pAig) );
// initialized the topmost frame
pObj = Aig_ManPo( pAig, pCex->iPo );
Vec_VecPushInt( vFrameLis, pCex->iFrame, Aig_ObjId(pObj) );
for ( f = pCex->iFrame; f >= 0; f-- )
{
// collect nodes starting from the roots
Aig_ManIncrementTravId( pAig );
Vec_VecForEachEntryIntLevel( vFrameLis, Entry, i, f )
Saig_ManCollectFrameTerms_rec( pAig, Aig_ManObj(pAig, Entry),
(Vec_Int_t *)Vec_VecEntry( vFramePis, f ),
(Vec_Int_t *)(f ? Vec_VecEntry( vFrameLis, f-1 ) : NULL) );
}
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Saig_ManCexMinPhasePriority( Aig_Man_t * pAig, Abc_Cex_t * pCex, int f,
Vec_Vec_t * vFramePis, Vec_Vec_t * vFrameLis, Vec_Vec_t * vPrioPis, Vec_Vec_t * vPrioLis, Vec_Vec_t * vPhaseLis, Vec_Int_t * vPrios )
{
Aig_Obj_t * pObj;
int i, Entry;
// set PI priority for this frame
Vec_VecForEachEntryIntLevel( vFramePis, Entry, i, f )
{
pObj = Aig_ManObj( pAig, Entry );
pObj->fPhase = Aig_InfoHasBit( pCex->pData, pCex->nRegs + pCex->nPis * f + i );
Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), Vec_VecEntryEntryInt(vPrioPis, f, i) );
}
// set LO priority for this frame
if ( f == 0 )
{
int nPiPrioStart = Vec_VecSizeSize(vFramePis);
Saig_ManForEachLo( pAig, pObj, i )
Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), nPiPrioStart + i );
}
else
{
Vec_Int_t * vPrioLiOne = Vec_VecEntryInt( vPrioLis, f-1 );
Vec_Int_t * vPhaseLiOne = Vec_VecEntryInt( vPhaseLis, f-1 );
Vec_VecForEachEntryIntLevel( vFrameLis, Entry, i, f-1 )
{
pObj = Saig_ObjLiToLo( pAig, Aig_ManObj(pAig, Entry) );
pObj->fPhase = Vec_IntEntry( vPhaseLiOne, i );
Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), Vec_IntEntry(vPrioLiOne, i) );
}
}
// traverse, set phase and priority for internal nodes
Aig_ManIncrementTravId( pAig );
Vec_VecForEachEntryIntLevel( vFrameLis, Entry, i, f )
Saig_ManCexMinComputePrio_rec( pAig, Aig_ManObj(pAig, Entry), vPrios );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Cex_t * Saig_ManCexMinPerform( Aig_Man_t * pAig, Abc_Cex_t * pCex )
{
Abc_Cex_t * pCexMin = NULL;
Aig_Obj_t * pObj;
Vec_Vec_t * vFramePis, * vFrameLis, * vPrioPis, * vPrioLis, * vPhaseLis, * vReasonPis, * vReasonLis;
Vec_Int_t * vPrios;
int f, i, Entry, nPiPrioStart;
// collect PIs and LOs visited in each frame
vFramePis = Vec_VecStart( pCex->iFrame+1 );
vFrameLis = Vec_VecStart( pCex->iFrame+1 );
Saig_ManCollectFrameTerms( pAig, pCex, vFramePis, vFrameLis );
// set priority for the PIs
nPiPrioStart = 0;
vPrioPis = Vec_VecStart( pCex->iFrame+1 );
Vec_VecForEachEntryInt( vFramePis, Entry, f, i )
Vec_VecPushInt( vPrioPis, f, nPiPrioStart++ );
assert( nPiPrioStart == Vec_VecSizeSize(vFramePis) );
// storage for priorities
vPrios = Vec_IntStartFull( Aig_ManObjNumMax(pAig) );
Vec_IntWriteEntry( vPrios, Aig_ObjId(Aig_ManConst1(pAig)), Vec_VecSizeSize(vFramePis) + Aig_ManRegNum(pAig) );
// compute LO priority and phase
vPrioLis = Vec_VecStart( pCex->iFrame+1 );
vPhaseLis = Vec_VecStart( pCex->iFrame+1 );
for ( f = 0; f <= pCex->iFrame; f++ )
{
// set phase and polarity
Saig_ManCexMinPhasePriority( pAig, pCex, f, vFramePis, vFrameLis, vPrioPis, vPrioLis, vPhaseLis, vPrios );
// save phase and priority
Vec_VecForEachEntryIntLevel( vFrameLis, Entry, i, f )
{
pObj = Aig_ManObj( pAig, Entry );
Vec_VecPushInt( vPrioLis, f, Vec_IntEntry(vPrios, Aig_ObjId(pObj)) );
Vec_VecPushInt( vPhaseLis, f, pObj->fPhase );
}
}
// check the property output
pObj = Aig_ManPo( pAig, pCex->iPo );
assert( pObj->fPhase );
// select reason for the property to fail
vReasonPis = Vec_VecStart( pCex->iFrame+1 );
vReasonLis = Vec_VecStart( pCex->iFrame+1 );
for ( f = pCex->iFrame; f >= 0; f-- )
{
// set phase and polarity
Saig_ManCexMinPhasePriority( pAig, pCex, f, vFramePis, vFrameLis, vPrioPis, vPrioLis, vPhaseLis, vPrios );
// select reasons
Aig_ManIncrementTravId( pAig );
Vec_VecForEachEntryIntLevel( vFrameLis, Entry, i, f )
Saig_ManCexMinFindReason_rec( pAig, Aig_ManObj(pAig, Entry), vPrios,
(Vec_Int_t *)Vec_VecEntry( vReasonPis, f ),
(Vec_Int_t *)(f ? Vec_VecEntry( vReasonLis, f-1 ) : NULL) );
}
// here are computes the reasons
printf( "Total number of reason PIs = %d.\n", Vec_VecSizeSize(vReasonPis) );
// clean up
Vec_VecFree( vFramePis );
Vec_VecFree( vFrameLis );
Vec_VecFree( vPrioPis );
Vec_VecFree( vPrioLis );
Vec_VecFree( vPhaseLis );
Vec_VecFree( vReasonPis );
Vec_VecFree( vReasonLis );
Vec_IntFree( vPrios );
return pCexMin;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

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

@ -252,6 +252,8 @@ static int Abc_CommandSynch ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandClockGate ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandExtWin ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandInsWin ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandPermute ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandUnpermute ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandCec ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDCec ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -278,8 +280,7 @@ static int Abc_CommandBm ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandTestCex ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandPdr ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandReconcile ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandPermute ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandUnpermute ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandCexMin ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTraceStart ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTraceCheck ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -674,6 +675,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Sequential", "clockgate", Abc_CommandClockGate, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "extwin", Abc_CommandExtWin, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "inswin", Abc_CommandInsWin, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "permute", Abc_CommandPermute, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "unpermute", Abc_CommandUnpermute, 1 );
Cmd_CommandAdd( pAbc, "Verification", "cec", Abc_CommandCec, 0 );
Cmd_CommandAdd( pAbc, "Verification", "dcec", Abc_CommandDCec, 0 );
@ -705,8 +708,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Verification", "testcex", Abc_CommandTestCex, 0 );
Cmd_CommandAdd( pAbc, "Verification", "pdr", Abc_CommandPdr, 0 );
Cmd_CommandAdd( pAbc, "Verification", "reconcile", Abc_CommandReconcile, 1 );
Cmd_CommandAdd( pAbc, "Verification", "permute", Abc_CommandPermute, 1 );
Cmd_CommandAdd( pAbc, "Verification", "unpermute", Abc_CommandUnpermute, 1 );
Cmd_CommandAdd( pAbc, "Verification", "cexmin", Abc_CommandCexMin, 0 );
Cmd_CommandAdd( pAbc, "ABC8", "*r", Abc_CommandAbc8Read, 0 );
@ -16520,6 +16522,120 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandPermute( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk = pAbc->pNtkCur, * pNtkRes = NULL;
int fInputs = 1;
int fOutputs = 1;
int c, fFlops = 1;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "iofh" ) ) != EOF )
{
switch ( c )
{
case 'i':
fInputs ^= 1;
break;
case 'o':
fOutputs ^= 1;
break;
case 'f':
fFlops ^= 1;
break;
case 'h':
goto usage;
default:
Abc_Print( -2, "Unknown switch.\n");
goto usage;
}
}
if ( pNtk == NULL )
{
Abc_Print( -1, "Empty network.\n" );
return 1;
}
pNtkRes = Abc_NtkDup( pNtk );
if ( pNtkRes == NULL )
{
Abc_Print( -1, "Command \"permute\" has failed.\n" );
return 1;
}
Abc_NtkPermute( pNtkRes, fInputs, fOutputs, fFlops );
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
return 0;
usage:
Abc_Print( -2, "usage: permute [-iofh]\n" );
Abc_Print( -2, "\t performs random permutation of inputs/outputs/flops\n" );
Abc_Print( -2, "\t-i : toggle permuting primary inputs [default = %s]\n", fInputs? "yes": "no" );
Abc_Print( -2, "\t-o : toggle permuting primary outputs [default = %s]\n", fOutputs? "yes": "no" );
Abc_Print( -2, "\t-f : toggle permuting flip-flops [default = %s]\n", fFlops? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandUnpermute( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk = pAbc->pNtkCur, * pNtkRes = NULL;
int c;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
{
switch ( c )
{
case 'h':
goto usage;
default:
Abc_Print( -2, "Unknown switch.\n");
goto usage;
}
}
if ( pNtk == NULL )
{
Abc_Print( -1, "Empty network.\n" );
return 1;
}
pNtkRes = Abc_NtkDup( pNtk );
if ( pNtkRes == NULL )
{
Abc_Print( -1, "Command \"unpermute\" has failed.\n" );
return 1;
}
Abc_NtkUnpermute( pNtkRes );
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
return 0;
usage:
Abc_Print( -2, "usage: unpermute [-h]\n" );
Abc_Print( -2, "\t restores inputs/outputs/flops before the last permutation\n" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []
@ -20503,78 +20619,44 @@ usage:
SeeAlso []
***********************************************************************/
int Abc_CommandPermute( Abc_Frame_t * pAbc, int argc, char ** argv )
int Abc_CommandCexMin( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk = pAbc->pNtkCur, * pNtkRes = NULL;
int fInputs = 1;
int fOutputs = 1;
int c, fFlops = 1;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "iofh" ) ) != EOF )
{
switch ( c )
{
case 'i':
fInputs ^= 1;
break;
case 'o':
fOutputs ^= 1;
break;
case 'f':
fFlops ^= 1;
break;
case 'h':
goto usage;
default:
Abc_Print( -2, "Unknown switch.\n");
goto usage;
}
}
if ( pNtk == NULL )
{
Abc_Print( -1, "Empty network.\n" );
return 1;
}
pNtkRes = Abc_NtkDup( pNtk );
if ( pNtkRes == NULL )
{
Abc_Print( -1, "Command \"permute\" has failed.\n" );
return 1;
}
Abc_NtkPermute( pNtkRes, fInputs, fOutputs, fFlops );
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
return 0;
usage:
Abc_Print( -2, "usage: permute [-iofh]\n" );
Abc_Print( -2, "\t performs random permutation of inputs/outputs/flops\n" );
Abc_Print( -2, "\t-i : toggle permuting primary inputs [default = %s]\n", fInputs? "yes": "no" );
Abc_Print( -2, "\t-o : toggle permuting primary outputs [default = %s]\n", fOutputs? "yes": "no" );
Abc_Print( -2, "\t-f : toggle permuting flip-flops [default = %s]\n", fFlops? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandUnpermute( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk = pAbc->pNtkCur, * pNtkRes = NULL;
Abc_Ntk_t * pNtk;
Abc_Cex_t * vCexNew = NULL;
int c;
int nConfLimit = 1000;
int nRounds = 1;
int fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "CRvh" ) ) != EOF )
{
switch ( c )
{
case 'C':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
goto usage;
}
nConfLimit = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nConfLimit < 0 )
goto usage;
break;
case 'R':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" );
goto usage;
}
nRounds = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nRounds < 0 )
goto usage;
break;
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
@ -20582,25 +20664,58 @@ int Abc_CommandUnpermute( Abc_Frame_t * pAbc, int argc, char ** argv )
goto usage;
}
}
if ( pAbc->pCex == NULL )
{
Abc_Print( 1, "There is no current cex.\n");
return 0;
}
// check the main AIG
pNtk = Abc_FrameReadNtk(pAbc);
if ( pNtk == NULL )
Abc_Print( 1, "Main AIG: There is no current network.\n");
else if ( !Abc_NtkIsStrash(pNtk) )
Abc_Print( 1, "Main AIG: The current network is not an AIG.\n");
else if ( Abc_NtkPiNum(pNtk) != pAbc->pCex->nPis )
Abc_Print( 1, "Main AIG: The number of PIs (%d) is different from cex (%d).\n", Abc_NtkPiNum(pNtk), pAbc->pCex->nPis );
// else if ( Abc_NtkLatchNum(pNtk) != pAbc->pCex->nRegs )
// Abc_Print( 1, "Main AIG: The number of registers (%d) is different from cex (%d).\n", Abc_NtkLatchNum(pNtk), pAbc->pCex->nRegs );
// else if ( Abc_NtkPoNum(pNtk) <= pAbc->pCex->iPo )
// Abc_Print( 1, "Main AIG: The number of POs (%d) is less than the PO index in cex (%d).\n", Abc_NtkPoNum(pNtk), pAbc->pCex->iPo );
else
{
Abc_Print( -1, "Empty network.\n" );
return 1;
extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
Gia_Man_t * pGia = Gia_ManFromAigSimple( pAig );
// if ( !Gia_ManVerifyCex( pGia, pAbc->pCex, 0 ) )
int iPoOld = pAbc->pCex->iPo;
pAbc->pCex->iPo = Gia_ManFindFailedPoCex( pGia, pAbc->pCex, 0 );
Gia_ManStop( pGia );
if ( pAbc->pCex->iPo == -1 )
{
pAbc->pCex->iPo = iPoOld;
Abc_Print( -1, "Main AIG: The cex does not fail any outputs.\n" );
return 0;
}
else if ( iPoOld != pAbc->pCex->iPo )
Abc_Print( 0, "Main AIG: The cex refined PO %d instead of PO %d.\n", pAbc->pCex->iPo, iPoOld );
// perform minimization
// vCexNew = Saig_ManCexMinPerform( pAig, pAbc->pCex );
Aig_ManStop( pAig );
// Abc_FrameReplaceCex( pAbc, &vCexNew );
printf( "Implementation of this command is not finished.\n" );
}
pNtkRes = Abc_NtkDup( pNtk );
if ( pNtkRes == NULL )
{
Abc_Print( -1, "Command \"unpermute\" has failed.\n" );
return 1;
}
Abc_NtkUnpermute( pNtkRes );
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
return 0;
usage:
Abc_Print( -2, "usage: unpermute [-h]\n" );
Abc_Print( -2, "\t restores inputs/outputs/flops before the last permutation\n" );
Abc_Print( -2, "\t-h : print the command usage\n");
Abc_Print( -2, "usage: cexmin [-CR num] [-vh]\n" );
Abc_Print( -2, "\t reduces the length of the counter-example\n" );
Abc_Print( -2, "\t-C num : the maximum number of conflicts [default = %d]\n", nConfLimit );
Abc_Print( -2, "\t-R num : the number of minimization rounds [default = %d]\n", nRounds );
Abc_Print( -2, "\t-v : toggle printing optimization summary [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}