mirror of https://github.com/YosysHQ/abc.git
Added new command 'outdec'.
This commit is contained in:
Alan Mishchenko
parent
27311713c7
commit
31360734b7
|
|
@ -3523,6 +3523,10 @@ SOURCE=.\src\aig\saig\saigMiter.c
|
|||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\aig\saig\saigOutDec.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\aig\saig\saigPba.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
|
|
|||
|
|
@ -11,6 +11,7 @@ SRC += src/aig/saig/saigAbs.c \
|
|||
src/aig/saig/saigInd.c \
|
||||
src/aig/saig/saigIoa.c \
|
||||
src/aig/saig/saigMiter.c \
|
||||
src/aig/saig/saigOutDec.c \
|
||||
src/aig/saig/saigPba.c \
|
||||
src/aig/saig/saigPhase.c \
|
||||
src/aig/saig/saigRetFwd.c \
|
||||
|
|
|
|||
|
|
@ -169,6 +169,8 @@ extern Aig_Man_t * Saig_ManCreateMiterTwo( Aig_Man_t * pOld, Aig_Man_t * p
|
|||
extern int Saig_ManDemiterSimple( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 );
|
||||
extern int Saig_ManDemiterSimpleDiff( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 );
|
||||
extern int Ssw_SecSpecialMiter( Aig_Man_t * p0, Aig_Man_t * p1, int nFrames, int fVerbose );
|
||||
/*=== saigOutdec.c ==========================================================*/
|
||||
extern Aig_Man_t * Saig_ManDecPropertyOutput( Aig_Man_t * pAig, int nLits, int fVerbose );
|
||||
/*=== saigPhase.c ==========================================================*/
|
||||
extern Aig_Man_t * Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrames, int nPref, int fIgnore, int fPrint, int fVerbose );
|
||||
/*=== saigRetFwd.c ==========================================================*/
|
||||
|
|
|
|||
|
|
@ -0,0 +1,205 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [saigOutDec.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Sequential AIG package.]
|
||||
|
||||
Synopsis [Output cone decomposition.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - June 20, 2005.]
|
||||
|
||||
Revision [$Id: saigOutDec.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "saig.h"
|
||||
#include "cnf.h"
|
||||
#include "satSolver.h"
|
||||
|
||||
ABC_NAMESPACE_IMPL_START
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Performs decomposition of the property output.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Vec_Ptr_t * Saig_ManFindPrimes( Aig_Man_t * pAig, int nLits, int fVerbose )
|
||||
{
|
||||
Cnf_Dat_t * pCnf;
|
||||
sat_solver * pSat;
|
||||
Aig_Obj_t * pObj0, * pObj1, * pRoot, * pMiter;
|
||||
Vec_Ptr_t * vPrimes, * vNodes;
|
||||
Vec_Int_t * vCube, * vMarks;
|
||||
int i0, i1, m, RetValue, Lits[10];
|
||||
int fCompl0, fCompl1, nNodes1, nNodes2;
|
||||
assert( nLits == 1 || nLits == 2 );
|
||||
assert( nLits < 10 );
|
||||
|
||||
// create SAT solver
|
||||
pCnf = Cnf_DeriveSimple( pAig, Aig_ManPoNum(pAig) );
|
||||
pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
|
||||
|
||||
// collect nodes in the property output cone
|
||||
pMiter = Aig_ManPo( pAig, 0 );
|
||||
pRoot = Aig_ObjFanin0( pMiter );
|
||||
vNodes = Aig_ManDfsNodes( pAig, &pRoot, 1 );
|
||||
// sort nodes by level and remove the last few
|
||||
|
||||
// try single nodes
|
||||
vPrimes = Vec_PtrAlloc( 100 );
|
||||
// create assumptions
|
||||
vMarks = Vec_IntStart( Vec_PtrSize(vNodes) );
|
||||
Lits[0] = toLitCond( pCnf->pVarNums[Aig_ObjId(pMiter)], 1 );
|
||||
Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj0, i0 )
|
||||
if ( pObj0 != pRoot )
|
||||
{
|
||||
// create assumptions
|
||||
Lits[1] = toLitCond( pCnf->pVarNums[Aig_ObjId(pObj0)], pObj0->fPhase );
|
||||
// solve the problem
|
||||
RetValue = sat_solver_solve( pSat, Lits, Lits+2, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
|
||||
if ( RetValue == l_False )
|
||||
{
|
||||
vCube = Vec_IntAlloc( 1 );
|
||||
Vec_IntPush( vCube, toLitCond(Aig_ObjId(pObj0), pObj0->fPhase) );
|
||||
Vec_PtrPush( vPrimes, vCube );
|
||||
if ( fVerbose )
|
||||
printf( "Adding prime %d%c\n", Aig_ObjId(pObj0), pObj0->fPhase?'-':'+' );
|
||||
Vec_IntWriteEntry( vMarks, i0, 1 );
|
||||
}
|
||||
}
|
||||
nNodes1 = Vec_PtrSize(vPrimes);
|
||||
if ( nLits > 1 )
|
||||
{
|
||||
// try adding second literal
|
||||
Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj0, i0 )
|
||||
if ( pObj0 != pRoot )
|
||||
Vec_PtrForEachEntryStart( Aig_Obj_t *, vNodes, pObj1, i1, i0+1 )
|
||||
if ( pObj1 != pRoot )
|
||||
{
|
||||
if ( Vec_IntEntry(vMarks,i0) || Vec_IntEntry(vMarks,i1) )
|
||||
continue;
|
||||
for ( m = 0; m < 3; m++ )
|
||||
{
|
||||
fCompl0 = m & 1;
|
||||
fCompl1 = (m >> 1) & 1;
|
||||
// create assumptions
|
||||
Lits[1] = toLitCond( pCnf->pVarNums[Aig_ObjId(pObj0)], fCompl0 ^ pObj0->fPhase );
|
||||
Lits[2] = toLitCond( pCnf->pVarNums[Aig_ObjId(pObj1)], fCompl1 ^ pObj1->fPhase );
|
||||
// solve the problem
|
||||
RetValue = sat_solver_solve( pSat, Lits, Lits+3, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
|
||||
if ( RetValue == l_False )
|
||||
{
|
||||
vCube = Vec_IntAlloc( 2 );
|
||||
Vec_IntPush( vCube, toLitCond(Aig_ObjId(pObj0), fCompl0 ^ pObj0->fPhase) );
|
||||
Vec_IntPush( vCube, toLitCond(Aig_ObjId(pObj1), fCompl1 ^ pObj1->fPhase) );
|
||||
Vec_PtrPush( vPrimes, vCube );
|
||||
if ( fVerbose )
|
||||
printf( "Adding prime %d%c %d%c\n",
|
||||
Aig_ObjId(pObj0), (fCompl0 ^ pObj0->fPhase)?'-':'+',
|
||||
Aig_ObjId(pObj1), (fCompl1 ^ pObj1->fPhase)?'-':'+' );
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
nNodes2 = Vec_PtrSize(vPrimes) - nNodes1;
|
||||
|
||||
printf( "Property cone size = %6d 1-lit primes = %5d 2-lit primes = %5d\n",
|
||||
Vec_PtrSize(vNodes), nNodes1, nNodes2 );
|
||||
|
||||
// clean up
|
||||
sat_solver_delete( pSat );
|
||||
Cnf_DataFree( pCnf );
|
||||
Vec_PtrFree( vNodes );
|
||||
Vec_IntFree( vMarks );
|
||||
return vPrimes;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Performs decomposition of the property output.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Aig_Man_t * Saig_ManDecPropertyOutput( Aig_Man_t * pAig, int nLits, int fVerbose )
|
||||
{
|
||||
Aig_Man_t * pAigNew = NULL;
|
||||
Aig_Obj_t * pObj, * pMiter;
|
||||
Vec_Ptr_t * vPrimes;
|
||||
Vec_Int_t * vCube;
|
||||
int i, k, Lit;
|
||||
|
||||
// compute primes of the comb output function
|
||||
vPrimes = Saig_ManFindPrimes( pAig, nLits, fVerbose );
|
||||
|
||||
// start the new manager
|
||||
pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
|
||||
pAigNew->pName = Aig_UtilStrsav( pAig->pName );
|
||||
pAigNew->nConstrs = pAig->nConstrs;
|
||||
// map the constant node
|
||||
Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
|
||||
// create variables for PIs
|
||||
Aig_ManForEachPi( pAig, pObj, i )
|
||||
pObj->pData = Aig_ObjCreatePi( pAigNew );
|
||||
// add internal nodes of this frame
|
||||
Aig_ManForEachNode( pAig, pObj, i )
|
||||
pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
|
||||
// create original POs of the circuit
|
||||
Saig_ManForEachPo( pAig, pObj, i )
|
||||
Aig_ObjCreatePo( pAigNew, Aig_ObjChild0Copy(pObj) );
|
||||
// create prime POs of the circuit
|
||||
if ( vPrimes )
|
||||
Vec_PtrForEachEntry( Vec_Int_t *, vPrimes, vCube, k )
|
||||
{
|
||||
pMiter = Aig_ManConst1( pAigNew );
|
||||
Vec_IntForEachEntry( vCube, Lit, i )
|
||||
{
|
||||
pObj = Aig_NotCond( Aig_ObjCopy(Aig_ManObj(pAig, Aig_Lit2Var(Lit))), Aig_LitIsCompl(Lit) );
|
||||
pMiter = Aig_And( pAigNew, pMiter, pObj );
|
||||
}
|
||||
Aig_ObjCreatePo( pAigNew, pMiter );
|
||||
}
|
||||
// transfer to register outputs
|
||||
Saig_ManForEachLi( pAig, pObj, i )
|
||||
Aig_ObjCreatePo( pAigNew, Aig_ObjChild0Copy(pObj) );
|
||||
Aig_ManCleanup( pAigNew );
|
||||
Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) );
|
||||
|
||||
Vec_VecFreeP( (Vec_Vec_t **)&vPrimes );
|
||||
return pAigNew;
|
||||
}
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
ABC_NAMESPACE_IMPL_END
|
||||
|
||||
|
|
@ -160,6 +160,7 @@ static int Abc_CommandCover ( Abc_Frame_t * pAbc, int argc, cha
|
|||
static int Abc_CommandDouble ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
static int Abc_CommandInter ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
static int Abc_CommandBb2Wb ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
static int Abc_CommandOutdec ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
static int Abc_CommandTest ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
|
||||
static int Abc_CommandQuaVar ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
|
|
@ -579,6 +580,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
|
|||
Cmd_CommandAdd( pAbc, "Various", "double", Abc_CommandDouble, 1 );
|
||||
Cmd_CommandAdd( pAbc, "Various", "inter", Abc_CommandInter, 1 );
|
||||
Cmd_CommandAdd( pAbc, "Various", "bb2wb", Abc_CommandBb2Wb, 0 );
|
||||
Cmd_CommandAdd( pAbc, "Various", "outdec", Abc_CommandOutdec, 1 );
|
||||
Cmd_CommandAdd( pAbc, "Various", "test", Abc_CommandTest, 0 );
|
||||
// Cmd_CommandAdd( pAbc, "Various", "qbf_solve", Abc_CommandTest, 0 );
|
||||
|
||||
|
|
@ -8408,6 +8410,82 @@ usage:
|
|||
return 1;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Abc_CommandOutdec( Abc_Frame_t * pAbc, int argc, char ** argv )
|
||||
{
|
||||
extern Abc_Ntk_t * Abc_NtkDarOutdec( Abc_Ntk_t * pNtk, int nLits, int fVerbose );
|
||||
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
|
||||
Abc_Ntk_t * pNtkRes;
|
||||
int c, nLits = 1;
|
||||
int fVerbose = 0;
|
||||
|
||||
// set defaults
|
||||
Extra_UtilGetoptReset();
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "Lvh" ) ) != EOF )
|
||||
{
|
||||
switch ( c )
|
||||
{
|
||||
case 'L':
|
||||
if ( globalUtilOptind >= argc )
|
||||
{
|
||||
Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" );
|
||||
goto usage;
|
||||
}
|
||||
nLits = atoi(argv[globalUtilOptind]);
|
||||
globalUtilOptind++;
|
||||
if ( nLits < 1 || nLits > 2 )
|
||||
{
|
||||
printf( "Currently, command \"outdec\" works for 1-lit and 2-lit primes only.\n" );
|
||||
goto usage;
|
||||
}
|
||||
break;
|
||||
case 'v':
|
||||
fVerbose ^= 1;
|
||||
break;
|
||||
case 'h':
|
||||
goto usage;
|
||||
default:
|
||||
goto usage;
|
||||
}
|
||||
}
|
||||
if ( pNtk == NULL )
|
||||
{
|
||||
Abc_Print( -1, "Empty network.\n" );
|
||||
return 1;
|
||||
}
|
||||
if ( !Abc_NtkIsStrash(pNtk) )
|
||||
{
|
||||
Abc_Print( -1, "Only works for strashed networks.\n" );
|
||||
return 1;
|
||||
}
|
||||
pNtkRes = Abc_NtkDarOutdec( pNtk, nLits, fVerbose );
|
||||
if ( pNtkRes == NULL )
|
||||
{
|
||||
Abc_Print( -1, "Command has failed.\n" );
|
||||
return 0;
|
||||
}
|
||||
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
|
||||
return 0;
|
||||
|
||||
usage:
|
||||
Abc_Print( -2, "usage: outdec [-Lvh]\n" );
|
||||
Abc_Print( -2, "\t performs prime decomposition of the first output\n" );
|
||||
Abc_Print( -2, "\t-L num : the number of literals in the primes [default = %d]\n", nLits );
|
||||
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;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
|
@ -8577,6 +8655,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
}
|
||||
}
|
||||
*/
|
||||
|
||||
return 0;
|
||||
usage:
|
||||
Abc_Print( -2, "usage: test [-CKDN] [-vwh] <file_name>\n" );
|
||||
|
|
|
|||
|
|
@ -3832,6 +3832,36 @@ void Abc_NtkDarConstr( Abc_Ntk_t * pNtk, int nFrames, int nConfs, int nProps, in
|
|||
Aig_ManStop( pMan );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Performs BDD-based reachability analysis.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Abc_Ntk_t * Abc_NtkDarOutdec( Abc_Ntk_t * pNtk, int nLits, int fVerbose )
|
||||
{
|
||||
Abc_Ntk_t * pNtkAig;
|
||||
Aig_Man_t * pMan, * pTemp;
|
||||
assert( Abc_NtkIsStrash(pNtk) );
|
||||
pMan = Abc_NtkToDar( pNtk, 0, 1 );
|
||||
if ( pMan == NULL )
|
||||
return NULL;
|
||||
pMan = Saig_ManDecPropertyOutput( pTemp = pMan, nLits, fVerbose );
|
||||
Aig_ManStop( pTemp );
|
||||
if ( pMan == NULL )
|
||||
return NULL;
|
||||
pNtkAig = Abc_NtkFromAigPhase( pMan );
|
||||
pNtkAig->pName = Extra_UtilStrsav(pMan->pName);
|
||||
pNtkAig->pSpec = Extra_UtilStrsav(pMan->pSpec);
|
||||
Aig_ManStop( pMan );
|
||||
return pNtkAig;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Performs BDD-based reachability analysis.]
|
||||
|
|
|
|||
Loading…
Reference in New Issue