Commit dfe5f511 by Alan Mishchenko

Adding new features to 'dualrail'.

parent f33c3007
...@@ -117,7 +117,7 @@ extern void Saig_ManDetectConstrFuncTest( Aig_Man_t * p, int nFrame ...@@ -117,7 +117,7 @@ extern void Saig_ManDetectConstrFuncTest( Aig_Man_t * p, int nFrame
extern Aig_Man_t * Saig_ManDupFoldConstrsFunc( Aig_Man_t * pAig, int fCompl, int fVerbose ); extern Aig_Man_t * Saig_ManDupFoldConstrsFunc( Aig_Man_t * pAig, int fCompl, int fVerbose );
extern Aig_Man_t * Saig_ManDupUnfoldConstrsFunc( Aig_Man_t * pAig, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose ); extern Aig_Man_t * Saig_ManDupUnfoldConstrsFunc( Aig_Man_t * pAig, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose );
/*=== saigDual.c ==========================================================*/ /*=== saigDual.c ==========================================================*/
extern Aig_Man_t * Saig_ManDupDual( Aig_Man_t * pAig, int nDualPis, int fDualFfs, int fMiterFfs, int fComplPo ); extern Aig_Man_t * Saig_ManDupDual( Aig_Man_t * pAig, Vec_Int_t * vDcFlops, int nDualPis, int fDualFfs, int fMiterFfs, int fComplPo, int fCheckZero, int fCheckOne );
extern void Saig_ManBlockPo( Aig_Man_t * pAig, int nCycles ); extern void Saig_ManBlockPo( Aig_Man_t * pAig, int nCycles );
/*=== saigDup.c ==========================================================*/ /*=== saigDup.c ==========================================================*/
extern Aig_Man_t * Saig_ManDupOrpos( Aig_Man_t * p ); extern Aig_Man_t * Saig_ManDupOrpos( Aig_Man_t * p );
......
...@@ -78,7 +78,7 @@ static inline void Saig_ObjDualFanin( Aig_Man_t * pAigNew, Vec_Ptr_t * vC ...@@ -78,7 +78,7 @@ static inline void Saig_ObjDualFanin( Aig_Man_t * pAigNew, Vec_Ptr_t * vC
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Aig_Man_t * Saig_ManDupDual( Aig_Man_t * pAig, int nDualPis, int fDualFfs, int fMiterFfs, int fComplPo ) Aig_Man_t * Saig_ManDupDual( Aig_Man_t * pAig, Vec_Int_t * vDcFlops, int nDualPis, int fDualFfs, int fMiterFfs, int fComplPo, int fCheckZero, int fCheckOne )
{ {
Vec_Ptr_t * vCopies; Vec_Ptr_t * vCopies;
Aig_Man_t * pAigNew; Aig_Man_t * pAigNew;
...@@ -86,6 +86,7 @@ Aig_Man_t * Saig_ManDupDual( Aig_Man_t * pAig, int nDualPis, int fDualFfs, int f ...@@ -86,6 +86,7 @@ Aig_Man_t * Saig_ManDupDual( Aig_Man_t * pAig, int nDualPis, int fDualFfs, int f
int i; int i;
assert( Saig_ManPoNum(pAig) > 0 ); assert( Saig_ManPoNum(pAig) > 0 );
assert( nDualPis >= 0 && nDualPis <= Saig_ManPiNum(pAig) ); assert( nDualPis >= 0 && nDualPis <= Saig_ManPiNum(pAig) );
assert( vDcFlops == NULL || Vec_IntSize(vDcFlops) == Aig_ManRegNum(pAig) );
vCopies = Vec_PtrStart( 2*Aig_ManObjNum(pAig) ); vCopies = Vec_PtrStart( 2*Aig_ManObjNum(pAig) );
// start the new manager // start the new manager
pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) ); pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
...@@ -110,6 +111,9 @@ Aig_Man_t * Saig_ManDupDual( Aig_Man_t * pAig, int nDualPis, int fDualFfs, int f ...@@ -110,6 +111,9 @@ Aig_Man_t * Saig_ManDupDual( Aig_Man_t * pAig, int nDualPis, int fDualFfs, int f
{ {
pTemp0 = Aig_ObjCreateCi( pAigNew ); pTemp0 = Aig_ObjCreateCi( pAigNew );
pTemp1 = Aig_ObjCreateCi( pAigNew ); pTemp1 = Aig_ObjCreateCi( pAigNew );
if ( vDcFlops )
pTemp0 = Aig_NotCond( pTemp0, !Vec_IntEntry(vDcFlops, i-Saig_ManPiNum(pAig)) );
else
pTemp0 = Aig_NotCond( pTemp0, !fDualFfs ); pTemp0 = Aig_NotCond( pTemp0, !fDualFfs );
} }
Saig_ObjSetDual( vCopies, Aig_ObjId(pObj), 0, Aig_And(pAigNew, pTemp0, Aig_Not(pTemp1)) ); Saig_ObjSetDual( vCopies, Aig_ObjId(pObj), 0, Aig_And(pAigNew, pTemp0, Aig_Not(pTemp1)) );
...@@ -130,8 +134,21 @@ Aig_Man_t * Saig_ManDupDual( Aig_Man_t * pAig, int nDualPis, int fDualFfs, int f ...@@ -130,8 +134,21 @@ Aig_Man_t * Saig_ManDupDual( Aig_Man_t * pAig, int nDualPis, int fDualFfs, int f
Saig_ManForEachLi( pAig, pObj, i ) Saig_ManForEachLi( pAig, pObj, i )
{ {
Saig_ObjDualFanin( pAigNew, vCopies, pObj, 0, &pTemp0, &pTemp1 ); Saig_ObjDualFanin( pAigNew, vCopies, pObj, 0, &pTemp0, &pTemp1 );
pCare = Aig_Or( pAigNew, pTemp0, pTemp1 ); if ( fCheckZero )
pMiter = Aig_Or( pAigNew, pMiter, Aig_Not(pCare) ); {
pCare = Aig_And( pAigNew, pTemp0, Aig_Not(pTemp1) );
pMiter = Aig_Or( pAigNew, pMiter, pCare );
}
else if ( fCheckOne )
{
pCare = Aig_And( pAigNew, Aig_Not(pTemp0), pTemp1 );
pMiter = Aig_Or( pAigNew, pMiter, pCare );
}
else // check X
{
pCare = Aig_And( pAigNew, Aig_Not(pTemp0), Aig_Not(pTemp1) );
pMiter = Aig_Or( pAigNew, pMiter, pCare );
}
} }
} }
else else
...@@ -139,8 +156,21 @@ Aig_Man_t * Saig_ManDupDual( Aig_Man_t * pAig, int nDualPis, int fDualFfs, int f ...@@ -139,8 +156,21 @@ Aig_Man_t * Saig_ManDupDual( Aig_Man_t * pAig, int nDualPis, int fDualFfs, int f
Saig_ManForEachPo( pAig, pObj, i ) Saig_ManForEachPo( pAig, pObj, i )
{ {
Saig_ObjDualFanin( pAigNew, vCopies, pObj, 0, &pTemp0, &pTemp1 ); Saig_ObjDualFanin( pAigNew, vCopies, pObj, 0, &pTemp0, &pTemp1 );
pCare = Aig_Or( pAigNew, pTemp0, pTemp1 ); if ( fCheckZero )
pMiter = Aig_Or( pAigNew, pMiter, Aig_Not(pCare) ); {
pCare = Aig_And( pAigNew, pTemp0, Aig_Not(pTemp1) );
pMiter = Aig_Or( pAigNew, pMiter, pCare );
}
else if ( fCheckOne )
{
pCare = Aig_And( pAigNew, Aig_Not(pTemp0), pTemp1 );
pMiter = Aig_Or( pAigNew, pMiter, pCare );
}
else // check X
{
pCare = Aig_And( pAigNew, Aig_Not(pTemp0), Aig_Not(pTemp1) );
pMiter = Aig_Or( pAigNew, pMiter, pCare );
}
} }
} }
// create PO // create PO
...@@ -150,6 +180,9 @@ Aig_Man_t * Saig_ManDupDual( Aig_Man_t * pAig, int nDualPis, int fDualFfs, int f ...@@ -150,6 +180,9 @@ Aig_Man_t * Saig_ManDupDual( Aig_Man_t * pAig, int nDualPis, int fDualFfs, int f
Saig_ManForEachLi( pAig, pObj, i ) Saig_ManForEachLi( pAig, pObj, i )
{ {
Saig_ObjDualFanin( pAigNew, vCopies, pObj, 0, &pTemp0, &pTemp1 ); Saig_ObjDualFanin( pAigNew, vCopies, pObj, 0, &pTemp0, &pTemp1 );
if ( vDcFlops )
pTemp0 = Aig_NotCond( pTemp0, !Vec_IntEntry(vDcFlops, i) );
else
pTemp0 = Aig_NotCond( pTemp0, !fDualFfs ); pTemp0 = Aig_NotCond( pTemp0, !fDualFfs );
Aig_ObjCreateCo( pAigNew, pTemp0 ); Aig_ObjCreateCo( pAigNew, pTemp0 );
Aig_ObjCreateCo( pAigNew, pTemp1 ); Aig_ObjCreateCo( pAigNew, pTemp1 );
......
...@@ -23110,18 +23110,23 @@ usage: ...@@ -23110,18 +23110,23 @@ usage:
***********************************************************************/ ***********************************************************************/
int Abc_CommandDualRail( Abc_Frame_t * pAbc, int argc, char ** argv ) int Abc_CommandDualRail( Abc_Frame_t * pAbc, int argc, char ** argv )
{ {
extern Vec_Int_t * Abc_NtkFindDcLatches( Abc_Ntk_t * pNtk );
extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters ); extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan ); extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
Abc_Ntk_t * pNtk, * pNtkNew = NULL; Abc_Ntk_t * pNtk, * pNtkNew = NULL;
Aig_Man_t * pAig, * pAigNew; Aig_Man_t * pAig, * pAigNew;
Vec_Int_t * vDcFlops = NULL;
int c; int c;
int nDualPis = 0; int nDualPis = 0;
int fDualFfs = 0; int fDualFfs = 0;
int fDualDcFfs = 0;
int fMiterFfs = 0; int fMiterFfs = 0;
int fComplPo = 0; int fComplPo = 0;
int fCheckZero = 0;
int fCheckOne = 0;
int fVerbose = 0; int fVerbose = 0;
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Itfcvh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "Itxfczovh" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
...@@ -23139,12 +23144,21 @@ int Abc_CommandDualRail( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -23139,12 +23144,21 @@ int Abc_CommandDualRail( Abc_Frame_t * pAbc, int argc, char ** argv )
case 't': case 't':
fDualFfs ^= 1; fDualFfs ^= 1;
break; break;
case 'x':
fDualDcFfs ^= 1;
break;
case 'f': case 'f':
fMiterFfs ^= 1; fMiterFfs ^= 1;
break; break;
case 'c': case 'c':
fComplPo ^= 1; fComplPo ^= 1;
break; break;
case 'z':
fCheckZero ^= 1;
break;
case 'o':
fCheckOne ^= 1;
break;
case 'v': case 'v':
fVerbose ^= 1; fVerbose ^= 1;
break; break;
...@@ -23169,27 +23183,34 @@ int Abc_CommandDualRail( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -23169,27 +23183,34 @@ int Abc_CommandDualRail( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0; return 0;
} }
// tranform if ( fDualDcFfs )
vDcFlops = Abc_NtkFindDcLatches( pNtk );
// transform
pAig = Abc_NtkToDar( pNtk, 0, 1 ); pAig = Abc_NtkToDar( pNtk, 0, 1 );
pAigNew = Saig_ManDupDual( pAig, nDualPis, fDualFfs, fMiterFfs, fComplPo ); pAigNew = Saig_ManDupDual( pAig, vDcFlops, nDualPis, fDualFfs, fMiterFfs, fComplPo, fCheckZero, fCheckOne );
Aig_ManStop( pAig ); Aig_ManStop( pAig );
pNtkNew = Abc_NtkFromAigPhase( pAigNew ); pNtkNew = Abc_NtkFromAigPhase( pAigNew );
pNtkNew->pName = Extra_UtilStrsav(pNtk->pName); pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
Aig_ManStop( pAigNew ); Aig_ManStop( pAigNew );
Vec_IntFreeP( &vDcFlops );
// replace the current network // replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkNew ); Abc_FrameReplaceCurrentNetwork( pAbc, pNtkNew );
return 0; return 0;
usage: usage:
Abc_Print( -2, "usage: dualrail [-I num] [-tfcvh]\n" ); Abc_Print( -2, "usage: dualrail [-I num] [-txfczovh]\n" );
Abc_Print( -2, "\t transforms the current AIG into a dual-rail miter\n" ); Abc_Print( -2, "\t transforms the current AIG into a dual-rail miter\n" );
Abc_Print( -2, "\t expressing the property \"at least one PO has ternary value\"\n" ); Abc_Print( -2, "\t expressing the property \"at least one PO has ternary value\"\n" );
Abc_Print( -2, "\t (to compute an initialization sequence, use switches \"-tfc\")\n" ); Abc_Print( -2, "\t (to compute an initialization sequence, use switches \"-tfc\")\n" );
Abc_Print( -2, "\t-I num : the number of first PIs interpreted as ternary [default = %d]\n", nDualPis ); Abc_Print( -2, "\t-I num : the number of first PIs interpreted as ternary [default = %d]\n", nDualPis );
Abc_Print( -2, "\t-t : toggle ternary flop init values [default = %s]\n", fDualFfs? "yes": "const0 init values" ); Abc_Print( -2, "\t-t : toggle ternary flop init values for all flops [default = %s]\n", fDualFfs? "yes": "const0 init values" );
Abc_Print( -2, "\t-x : toggle ternary flop init values for DC-valued flops [default = %s]\n", fDualDcFfs? "yes": "const0 init values" );
Abc_Print( -2, "\t-f : toggle mitering flops instead of POs [default = %s]\n", fMiterFfs? "flops": "POs" ); Abc_Print( -2, "\t-f : toggle mitering flops instead of POs [default = %s]\n", fMiterFfs? "flops": "POs" );
Abc_Print( -2, "\t-c : toggle complementing the miter output [default = %s]\n", fComplPo? "yes": "no" ); Abc_Print( -2, "\t-c : toggle complementing the miter output [default = %s]\n", fComplPo? "yes": "no" );
Abc_Print( -2, "\t-z : toggle checking PO==0 instead of PO==X [default = %s]\n", fCheckZero? "yes": "no" );
Abc_Print( -2, "\t-o : toggle checking PO==1 instead of PO==X [default = %s]\n", fCheckOne? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing optimization summary [default = %s]\n", fVerbose? "yes": "no" ); 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"); Abc_Print( -2, "\t-h : print the command usage\n");
return 1; return 1;
......
...@@ -193,6 +193,29 @@ Aig_Man_t * Abc_NtkToDarBmc( Abc_Ntk_t * pNtk, Vec_Int_t ** pvMap ) ...@@ -193,6 +193,29 @@ Aig_Man_t * Abc_NtkToDarBmc( Abc_Ntk_t * pNtk, Vec_Int_t ** pvMap )
/**Function************************************************************* /**Function*************************************************************
Synopsis [Collects information about what flops have unknown values.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Abc_NtkFindDcLatches( Abc_Ntk_t * pNtk )
{
Vec_Int_t * vUnknown;
Abc_Obj_t * pObj;
int i;
vUnknown = Vec_IntStart( Abc_NtkLatchNum(pNtk) );
Abc_NtkForEachLatch( pNtk, pObj, i )
if ( Abc_LatchIsInitDc(pObj) )
Vec_IntWriteEntry( vUnknown, i, 1 );
return vUnknown;
}
/**Function*************************************************************
Synopsis [Converts the network from the AIG manager into ABC.] Synopsis [Converts the network from the AIG manager into ABC.]
Description [Assumes that registers are ordered after PIs/POs.] Description [Assumes that registers are ordered after PIs/POs.]
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment