Skip to content

A
abc
Commit fcbd6f83 by Jiang Long
Options

the latest version

parent 574af212
Showing with 120 additions and 117 deletions
src/aig/saig/saigUnfold2.c
......@@ -292,9 +292,10 @@ Vec_Vec_t * Ssw_ManFindDirectImplications2( Aig_Man_t * p, int nFrames, int nCon
Aig_Man_t * Saig_ManDupUnfoldConstrsFunc2( Aig_Man_t * pAig, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose , int * typeII_cnt){
Aig_Man_t * pNew;
Vec_Vec_t * vCands;
Vec_Ptr_t * vNodes, * vNewFlops;
Vec_Ptr_t * vNewFlops;
Aig_Obj_t * pObj;
int i, j, k, nNewFlops;
int i, k, nNewFlops;
const int fCompl = 0 ;
if ( fOldAlgo )
vCands = Saig_ManDetectConstrFunc( pAig, nFrames, nConfs, nProps, fVerbose );
else
......@@ -305,135 +306,57 @@ Aig_Man_t * Saig_ManDupUnfoldConstrsFunc2( Aig_Man_t * pAig, int nFrames, int nC
return Aig_ManDupDfs( pAig );
}
// create new manager
pNew = Aig_ManDupWithoutPos( pAig );
pNew = Aig_ManDupWithoutPos( pAig ); /* good */
pNew->nConstrs = pAig->nConstrs + Vec_VecSizeSize(vCands);
pNew->nConstrs = pAig->nConstrs + Vec_PtrSize(pAig->unfold2_type_II)
+ Vec_PtrSize(pAig->unfold2_type_I);
// pNew->nConstrsTypeII = Vec_PtrSize(pAig->unfold2_type_II);
*typeII_cnt = Vec_PtrSize(pAig->unfold2_type_II);
/* new set of registers */
// add normal POs
Saig_ManForEachPo( pAig, pObj, i )
Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
// create constraint outputs
vNewFlops = Vec_PtrAlloc( 100 );
Vec_PtrForEachEntry(Aig_Obj_t * , pAig->unfold2_type_I, pObj, k){
Aig_Obj_t * x = Aig_ObjRealCopy(pObj);
Aig_ObjCreateCo(pNew, x);
}
Vec_PtrForEachEntry(Aig_Obj_t * , pAig->unfold2_type_II, pObj, k){
Aig_Obj_t * type_II_latch
= Aig_ObjCreateCi(pNew); /* will get connected later; */
Aig_Obj_t * x = Aig_ObjRealCopy(pObj);
Aig_ObjCreateCo(pNew, x);
Aig_Obj_t * n = Aig_And(pNew,
Aig_NotCond(type_II_latch, fCompl),
Aig_NotCond(x, fCompl));
Aig_ObjCreateCo(pNew, n);//Aig_Not(n));
}
if(0) Vec_VecForEachLevel( vCands, vNodes, i )
{
assert(i==0);
Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, k )
{
Vec_PtrPush( vNewFlops, Aig_ObjRealCopy(pObj) );
for ( j = 0; j < i; j++ )
Vec_PtrPush( vNewFlops, Aig_ObjCreateCi(pNew) );
Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Vec_PtrPop(vNewFlops) );
}
}
// add latch outputs
Saig_ManForEachLi( pAig, pObj, i )
Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
// add new latch outputs
nNewFlops = 0;//Vec_VecSizeSize(vCands);
if(0)Vec_VecForEachLevel( vCands, vNodes, i )
{
Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, k )
{
for ( j = 0; j < i; j++ )
Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Vec_PtrEntry(vNewFlops, nNewFlops++) );
}
}
Vec_PtrForEachEntry(Aig_Obj_t * , pAig->unfold2_type_II, pObj, k){
Aig_Obj_t * x = Aig_ObjRealCopy(pObj);
Aig_ObjCreateCo(pNew, x);
}
// add new latch outputs
nNewFlops = Vec_PtrSize(pAig->unfold2_type_II);
//assert( nNewFlops == Vec_PtrSize(vNewFlops) );
Aig_ManSetRegNum( pNew, Aig_ManRegNum(pAig) + nNewFlops );
printf("#reg after unfold2: %d\n", Aig_ManRegNum(pAig) + nNewFlops );
Vec_VecFreeP( &vCands );
Vec_PtrFree( vNewFlops );
return pNew;
}
Aig_Man_t * Saig_ManDupUnfoldConstrsFunc2_( Aig_Man_t * pAig, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose )
{
Aig_Man_t * pNew;
Vec_Vec_t * vCands;
// Vec_Ptr_t * vNodes, * vNewFlops;
Aig_Obj_t * pObj;
int i, k;
Aig_Obj_t * pMiter = NULL;
const int fCompl = 0;
if ( fOldAlgo )
vCands = Saig_ManDetectConstrFunc( pAig, nFrames, nConfs, nProps, fVerbose );
else
vCands = Ssw_ManFindDirectImplications2( pAig, nFrames, nConfs, nProps, fVerbose );
if ( vCands == NULL || Vec_VecSizeSize(vCands) == 0 )
{
Vec_VecFreeP( &vCands );
return Aig_ManDupDfs( pAig );
}
// create new manager
pNew = Aig_ManDupWithoutPos( pAig );
pMiter = Aig_ManConst0( pNew );
Vec_PtrForEachEntry(Aig_Obj_t * , pAig->unfold2_type_I, pObj, k){
pMiter = Aig_Or( pNew, pMiter,
Aig_NotCond( Aig_ObjRealCopy(pObj), fCompl ) );
printf("new id: %d\n", Aig_ObjId(pMiter));
}
Vec_PtrForEachEntry(Aig_Obj_t * , pAig->unfold2_type_II, pObj, k){
Aig_Obj_t * type_II_latch
= Aig_ObjCreateCi(pNew); /* will get connected later; */
Aig_Obj_t *kk = Aig_And(pNew,
Aig_NotCond(type_II_latch, fCompl),
Aig_NotCond(Aig_ObjRealCopy(pObj), fCompl)
);
pMiter = Aig_Or(pNew, pMiter, kk
);
}
{
Aig_Obj_t * pObjLi, *pObjLo;
Aig_Obj_t * pFlopOut = Aig_ObjCreateCi(pNew);
Aig_Obj_t * pFlopIn = Aig_Or(pNew, pMiter, pFlopOut);
Saig_ManForEachPo(pAig, pObj, i){
Aig_Obj_t *p = Aig_And( pNew, Aig_ObjChild0(pObj), Aig_Not(pFlopIn) );
printf("new id: %d\n", Aig_ObjId(p));
Aig_ObjCreateCo(pNew, p);
}
// add latch outputs
Saig_ManForEachLiLo(pAig, pObjLi, pObjLo, i){
Aig_Obj_t *c = Aig_Mux(pNew, Aig_Not(pFlopIn),
Aig_ObjChild0Copy(pObjLi) ,
Aig_ObjRealCopy(pObjLo));//->pData);
Aig_ObjCreateCo(pNew, c);
printf("new id: %d\n", Aig_ObjId(c));
}
Vec_PtrForEachEntry(Aig_Obj_t * , pAig->unfold2_type_II, pObj, k){
Aig_ObjCreateCo( pNew, Aig_ObjRealCopy(pObj));
}
Aig_ObjCreateCo(pNew, pFlopIn);
}
Aig_ManSetRegNum( pNew, Aig_ManRegNum(pAig) + Vec_PtrSize(pAig->unfold2_type_II) + 1);
Vec_VecFreeP( &vCands );
return pNew;
}
/**Function*************************************************************
......@@ -470,7 +393,9 @@ Aig_Man_t * Saig_ManDupFoldConstrsFunc2( Aig_Man_t * pAig, int fCompl, int fVerb
// OR the constraint outputs
pMiter = Aig_ManConst0( pAigNew );
int typeII_cc = 0;//typeII_cnt;
typeII_cnt = 0;
int type_II = 0;
Saig_ManForEachPo( pAig, pObj, i )
......@@ -483,7 +408,7 @@ Aig_Man_t * Saig_ManDupFoldConstrsFunc2( Aig_Man_t * pAig, int fCompl, int fVerb
}
/* now we got the constraint */
if (type_II) {
printf("modeling typeII \n");
Aig_Obj_t * type_II_latch
= Aig_ObjCreateCi(pAigNew); /* will get connected later; */
pMiter = Aig_Or(pAigNew, pMiter,
......@@ -491,6 +416,7 @@ Aig_Man_t * Saig_ManDupFoldConstrsFunc2( Aig_Man_t * pAig, int fCompl, int fVerb
Aig_NotCond(type_II_latch, fCompl),
Aig_NotCond( Aig_ObjChild0Copy(pObj), fCompl ) )
);
printf( "modeling typeII : %d:%s%d \n", i, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
} else
pMiter = Aig_Or( pAigNew, pMiter, Aig_NotCond( Aig_ObjChild0Copy(pObj), fCompl ) );
}
......@@ -517,11 +443,17 @@ Aig_Man_t * Saig_ManDupFoldConstrsFunc2( Aig_Man_t * pAig, int fCompl, int fVerb
{
/* the same for type I and type II */
Aig_Obj_t * pObjLi, *pObjLo;
Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i ) {
Aig_Obj_t *c = Aig_Mux(pAigNew, Aig_Not(pFlopIn),
Aig_ObjChild0Copy(pObjLi) ,
pObjLo->pData);
Aig_ObjCreateCo( pAigNew, c);
if( i + typeII_cc < Aig_ManRegNum(pAig)) {
Aig_Obj_t *c = Aig_Mux(pAigNew, Aig_Not(pFlopIn),
Aig_ObjChild0Copy(pObjLi) ,
pObjLo->pData);
Aig_ObjCreateCo( pAigNew, c);
} else {
printf ( "skipping: reg%d\n", i);
Aig_ObjCreateCo( pAigNew,Aig_ObjChild0Copy(pObjLi));
}
}
}
......@@ -530,19 +462,24 @@ Aig_Man_t * Saig_ManDupFoldConstrsFunc2( Aig_Man_t * pAig, int fCompl, int fVerb
}
Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) );
type_II = 0;
Saig_ManForEachPo( pAig, pObj, i )
{
if ( i < Saig_ManPoNum(pAig)-Aig_ManConstrNum(pAig) )
continue;
if (i + typeII_cnt >= Saig_ManPoNum(pAig) ) {
type_II = 1;
}
/* now we got the constraint */
if (type_II) {
Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj));
Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAigNew)+1 );
printf( "Latch for typeII : %d:%s%d \n", i, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
}
}
// create additional flop
if ( Saig_ManRegNum(pAig) > 0 )
......@@ -550,7 +487,7 @@ Aig_Man_t * Saig_ManDupFoldConstrsFunc2( Aig_Man_t * pAig, int fCompl, int fVerb
Aig_ObjCreateCo( pAigNew, pFlopIn );
Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAigNew)+1 );
}
printf("#reg after fold2: %d\n", Aig_ManRegNum(pAigNew));
// perform cleanup
Aig_ManCleanup( pAigNew );
Aig_ManSeqCleanup( pAigNew );
......
src/base/abci/abc.c
......@@ -294,8 +294,9 @@ static int Abc_CommandTempor ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandInduction ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandConstr ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandUnfold ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandUnfold2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandFold ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandUnfold2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandFold2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandBm ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandBm2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandSaucy ( Abc_Frame_t * pAbc, int argc, char ** argv );
......@@ -871,9 +872,9 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Verification", "ind", Abc_CommandInduction, 0 );
Cmd_CommandAdd( pAbc, "Verification", "constr", Abc_CommandConstr, 0 );
Cmd_CommandAdd( pAbc, "Verification", "unfold", Abc_CommandUnfold, 1 );
Cmd_CommandAdd( pAbc, "Verification", "unfold2", Abc_CommandUnfold2, 1 ); // jlong
Cmd_CommandAdd( pAbc, "Verification", "fold", Abc_CommandFold, 1 );
Cmd_CommandAdd( pAbc, "Verification", "unfold2", Abc_CommandUnfold2, 1 ); // jlong
Cmd_CommandAdd( pAbc, "Verification", "fold2", Abc_CommandFold2, 1 ); // jlong
Cmd_CommandAdd( pAbc, "Verification", "bm", Abc_CommandBm, 1 );
Cmd_CommandAdd( pAbc, "Verification", "bm2", Abc_CommandBm2, 1 );
Cmd_CommandAdd( pAbc, "Verification", "saucy3", Abc_CommandSaucy, 1 );
......@@ -35350,5 +35351,5 @@ usage:
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
#include "abciUnfold2.c"
ABC_NAMESPACE_IMPL_END
src/base/abci/abcDarUnfold2.c
......@@ -32,7 +32,7 @@ Abc_Ntk_t * Abc_NtkDarUnfold2( Abc_Ntk_t * pNtk, int nFrames, int nConfs, int nP
pNtkAig->pSpec = Extra_UtilStrsav(pMan->pSpec);
Aig_ManStop( pMan );
return Abc_NtkDarFold2(pNtkAig, 0, fVerbose, typeII_cnt);
return pNtkAig;//Abc_NtkDarFold2(pNtkAig, 0, fVerbose, typeII_cnt);
//return pNtkAig;
}
......
src/base/abci/abciUnfold2.c
......@@ -110,7 +110,7 @@ int Abc_CommandUnfold2( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
return 0;
usage:
Abc_Print( -2, "usage: unfold [-FCP num] [-savh]\n" );
Abc_Print( -2, "usage: unfold2 [-FCP num] [-savh]\n" );
Abc_Print( -2, "\t unfold hidden constraints as separate outputs\n" );
Abc_Print( -2, "\t-C num : the max number of conflicts in SAT solving [default = %d]\n", nConfs );
Abc_Print( -2, "\t-P num : the max number of constraint propagations [default = %d]\n", nProps );
......@@ -119,3 +119,68 @@ usage:
return 1;
}
int Abc_CommandFold2( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk, * pNtkRes;
int fCompl;
int fVerbose;
int c;
extern Abc_Ntk_t * Abc_NtkDarFold2( Abc_Ntk_t * pNtk, int fCompl, int fVerbose , int);
pNtk = Abc_FrameReadNtk(pAbc);
// set defaults
fCompl = 0;
fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "cvh" ) ) != EOF )
{
switch ( c )
{
/* case 'c': */
/* fCompl ^= 1; */
/* 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, "Currently only works for structurally hashed circuits.\n" );
return 0;
}
if ( Abc_NtkConstrNum(pNtk) == 0 )
{
Abc_Print( 0, "The network has no constraints.\n" );
return 0;
}
if ( Abc_NtkIsComb(pNtk) )
Abc_Print( 0, "The network is combinational.\n" );
// modify the current network
pNtkRes = Abc_NtkDarFold2( pNtk, fCompl, fVerbose ,0);
if ( pNtkRes == NULL )
{
Abc_Print( 1,"Transformation has failed.\n" );
return 0;
}
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
return 0;
usage:
Abc_Print( -2, "usage: fold [-cvh]\n" );
Abc_Print( -2, "\t folds constraints represented as separate outputs\n" );
// Abc_Print( -2, "\t-c : toggle complementing constraints while folding [default = %s]\n", fCompl? "yes": "no" );
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;
}
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