Skip to content

A
abc
Commit 574af212 by Jiang Long
Options

merge unfold2

parent b1e35da6
Showing with 772 additions and 4 deletions
Makefile
......@@ -131,7 +131,7 @@ tags:
$(PROG): $(OBJ)
@echo "$(MSG_PREFIX)\`\` Building binary:" $(notdir $@)
@$(LD) -o $@ $^ $(LIBS)
$(LD) -o $@ $^ $(LIBS)
lib$(PROG).a: $(OBJ)
@echo "$(MSG_PREFIX)\`\` Linking:" $(notdir $@)
......
src/aig/aig/aig.h
......@@ -165,6 +165,10 @@ struct Aig_Man_t_
// timing statistics
abctime time1;
abctime time2;
//-- jlong -- begin
Vec_Ptr_t * unfold2_type_I;
Vec_Ptr_t * unfold2_type_II;
//-- jlong -- end
};
// cut computation
......
src/aig/aig/aigMan.c
......@@ -60,6 +60,10 @@ Aig_Man_t * Aig_ManStart( int nNodesMax )
p->vCos = Vec_PtrAlloc( 100 );
p->vObjs = Vec_PtrAlloc( 1000 );
p->vBufs = Vec_PtrAlloc( 100 );
//--jlong -- begin
p->unfold2_type_I = Vec_PtrAlloc( 4);
p->unfold2_type_II = Vec_PtrAlloc( 4);
//--jlong -- end
// prepare the internal memory manager
p->pMemObjs = Aig_MmFixedStart( sizeof(Aig_Obj_t), nNodesMax );
// create the constant node
......@@ -200,6 +204,10 @@ void Aig_ManStop( Aig_Man_t * p )
Vec_PtrFreeP( &p->vCos );
Vec_PtrFreeP( &p->vObjs );
Vec_PtrFreeP( &p->vBufs );
//--jlong -- begin
Vec_PtrFreeP( &p->unfold2_type_I );
Vec_PtrFreeP( &p->unfold2_type_II );
//--jlong -- end
Vec_IntFreeP( &p->vLevelR );
Vec_VecFreeP( &p->vLevels );
Vec_IntFreeP( &p->vFlopNums );
......
src/aig/saig/saig.h
......@@ -116,6 +116,11 @@ extern void Saig_ManDetectConstrFuncTest( Aig_Man_t * p, int nFrame
/*=== saigConstr2.c ==========================================================*/
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 );
// -- jlong -- begin
extern Aig_Man_t * Saig_ManDupFoldConstrsFunc2( Aig_Man_t * pAig, int fCompl, int fVerbose, int typeII_cnt );
extern Aig_Man_t * Saig_ManDupUnfoldConstrsFunc2( Aig_Man_t * pAig, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose , int * typeII_cnt);
// --jlong -- end
/*=== saigDual.c ==========================================================*/
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 );
......
src/aig/saig/saigConstr2.c
......@@ -1008,6 +1008,6 @@ Aig_Man_t * Saig_ManDupFoldConstrsFunc( Aig_Man_t * pAig, int fCompl, int fVerbo
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
#include "saigUnfold2.c"
ABC_NAMESPACE_IMPL_END
src/aig/saig/saigUnfold2.c 0 → 100644
int Saig_ManFilterUsingIndOne2( Aig_Man_t * p, Aig_Man_t * pFrame, sat_solver * pSat, Cnf_Dat_t * pCnf, int nConfs, int nProps, int Counter
, int type_ /* jlong -- */
)
{
Aig_Obj_t * pObj;
int Lit, status;
pObj = Aig_ManCo( pFrame, Counter*3+type_ ); /* which co */
Lit = toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], 0 );
status = sat_solver_solve( pSat, &Lit, &Lit + 1, (ABC_INT64_T)nConfs, 0, 0, 0 );
if ( status == l_False ) /* unsat */
return status;
if ( status == l_Undef )
{
printf( "Solver returned undecided.\n" );
return status;
}
assert( status == l_True );
return status;
}
Aig_Man_t * Saig_ManCreateIndMiter2( Aig_Man_t * pAig, Vec_Vec_t * vCands )
{
int nFrames = 3;
Vec_Ptr_t * vNodes;
Aig_Man_t * pFrames;
Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew;
Aig_Obj_t ** pObjMap;
int i, f, k;
// create mapping for the frames nodes
pObjMap = ABC_CALLOC( Aig_Obj_t *, nFrames * Aig_ManObjNumMax(pAig) );
// start the fraig package
pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) * nFrames );
pFrames->pName = Abc_UtilStrsav( pAig->pName );
pFrames->pSpec = Abc_UtilStrsav( pAig->pSpec );
// map constant nodes
for ( f = 0; f < nFrames; f++ )
Aig_ObjSetFrames( pObjMap, nFrames, Aig_ManConst1(pAig), f, Aig_ManConst1(pFrames) );
// create PI nodes for the frames
for ( f = 0; f < nFrames; f++ )
Aig_ManForEachPiSeq( pAig, pObj, i )
Aig_ObjSetFrames( pObjMap, nFrames, pObj, f, Aig_ObjCreateCi(pFrames) );
// set initial state for the latches
Aig_ManForEachLoSeq( pAig, pObj, i )
Aig_ObjSetFrames( pObjMap, nFrames, pObj, 0, Aig_ObjCreateCi(pFrames) );
// add timeframes
for ( f = 0; f < nFrames; f++ )
{
// add internal nodes of this frame
Aig_ManForEachNode( pAig, pObj, i )
{
pObjNew = Aig_And( pFrames, Aig_ObjChild0Frames(pObjMap,nFrames,pObj,f), Aig_ObjChild1Frames(pObjMap,nFrames,pObj,f) );
Aig_ObjSetFrames( pObjMap, nFrames, pObj, f, pObjNew );
}
// set the latch inputs and copy them into the latch outputs of the next frame
Aig_ManForEachLiLoSeq( pAig, pObjLi, pObjLo, i )
{
pObjNew = Aig_ObjChild0Frames(pObjMap,nFrames,pObjLi,f);
if ( f < nFrames - 1 )
Aig_ObjSetFrames( pObjMap, nFrames, pObjLo, f+1, pObjNew );
}
}
// go through the candidates
Vec_VecForEachLevel( vCands, vNodes, i )
{
Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, k )
{
Aig_Obj_t * pObjR = Aig_Regular(pObj);
Aig_Obj_t * pNode0 = pObjMap[nFrames*Aig_ObjId(pObjR)+0];
Aig_Obj_t * pNode1 = pObjMap[nFrames*Aig_ObjId(pObjR)+1];
{
Aig_Obj_t * pFan0 = Aig_NotCond( pNode0, Aig_IsComplement(pObj) );
Aig_Obj_t * pFan1 = Aig_NotCond( pNode1, !Aig_IsComplement(pObj) );
Aig_Obj_t * pMiter = Aig_And( pFrames, pFan0, pFan1 );
Aig_ObjCreateCo( pFrames, pMiter );
/* need to check p & Xp is satisfiable */
/* jlong -- begin */
Aig_Obj_t * pMiter2 = Aig_And( pFrames, pFan0, Aig_Not(pFan1));
Aig_ObjCreateCo( pFrames, pMiter2 ); /* jlong -- end */
}
{ /* jlong -- begin */
Aig_Obj_t * pNode2 = pObjMap[nFrames*Aig_ObjId(pObjR)+2];
Aig_Obj_t * pFan0 = Aig_NotCond( pNode0, Aig_IsComplement(pObj) );
Aig_Obj_t * pFan1 = Aig_NotCond( pNode1, Aig_IsComplement(pObj) );
Aig_Obj_t * pFan2 = Aig_NotCond( pNode2, !Aig_IsComplement(pObj) );
Aig_Obj_t * pMiter = Aig_And( pFrames, Aig_And(pFrames, pFan0, pFan1 ), pFan2);
Aig_ObjCreateCo( pFrames, pMiter ); /* jlong -- end */
}
}
}
Aig_ManCleanup( pFrames );
ABC_FREE( pObjMap );
//Aig_ManShow( pAig, 0, NULL );
//Aig_ManShow( pFrames, 0, NULL );
return pFrames;
}
/**Function*************************************************************
Synopsis [Detects constraints functionally.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Saig_ManFilterUsingInd2( Aig_Man_t * p, Vec_Vec_t * vCands, int nConfs, int nProps, int fVerbose )
{
Vec_Ptr_t * vNodes;
Aig_Man_t * pFrames;
sat_solver * pSat;
Cnf_Dat_t * pCnf;
Aig_Obj_t * pObj;
int i, k, k2, Counter;
/*
Vec_VecForEachLevel( vCands, vNodes, i )
Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, k )
printf( "%d ", Aig_ObjId(Aig_Regular(pObj)) );
printf( "\n" );
*/
// create timeframes
// pFrames = Saig_ManUnrollInd( p );
pFrames = Saig_ManCreateIndMiter2( p, vCands );
assert( Aig_ManCoNum(pFrames) == Vec_VecSizeSize(vCands)*3 );
// start the SAT solver
pCnf = Cnf_DeriveSimple( pFrames, Aig_ManCoNum(pFrames) );
pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
// check candidates
if ( fVerbose )
printf( "Filtered cands: \n" );
Counter = 0;
Vec_VecForEachLevel( vCands, vNodes, i )
{
assert(i==0); /* only one item */
k2 = 0;
Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, k )
{
if ( Saig_ManFilterUsingIndOne2( p, pFrames, pSat, pCnf, nConfs, nProps, Counter++ , 0) == l_False)
// if ( Saig_ManFilterUsingIndOne_old( p, pSat, pCnf, nConfs, pObj ) )
{
Vec_PtrWriteEntry( vNodes, k2++, pObj );
if ( fVerbose )
printf( "%d:%s%d \n", i, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
printf( " type I : %d:%s%d \n", i, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
Vec_PtrPush(p->unfold2_type_I, pObj);
}
/* jlong -- begin */
else if ( Saig_ManFilterUsingIndOne2( p, pFrames, pSat, pCnf, nConfs, nProps, Counter-1 , 1) == l_True ) /* can be self-conflicting */
{
if ( Saig_ManFilterUsingIndOne2( p, pFrames, pSat, pCnf, nConfs, nProps, Counter-1 , 2) == l_False ){
//Vec_PtrWriteEntry( vNodes, k2++, pObj );
if ( fVerbose )
printf( "%d:%s%d \n", i, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
printf( " type II: %d:%s%d \n", i, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
Vec_PtrWriteEntry( vNodes, k2++, pObj ); /* add type II constraints */
Vec_PtrPush(p->unfold2_type_II, pObj);
}
}
/* jlong -- end */
}
Vec_PtrShrink( vNodes, k2 );
}
// clean up
Cnf_DataFree( pCnf );
sat_solver_delete( pSat );
if ( fVerbose )
Aig_ManPrintStats( pFrames );
Aig_ManStop( pFrames );
}
/**Function*************************************************************
Synopsis [Returns the number of variables implied by the output.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Vec_t * Ssw_ManFindDirectImplications2( Aig_Man_t * p, int nFrames, int nConfs, int nProps, int fVerbose )
{
Vec_Vec_t * vCands = NULL;
Vec_Ptr_t * vNodes;
Cnf_Dat_t * pCnf;
sat_solver * pSat;
Aig_Man_t * pFrames;
Aig_Obj_t * pObj, * pRepr, * pReprR;
int i, f, k, value;
assert(nFrames == 1);
vCands = Vec_VecAlloc( nFrames );
assert(nFrames == 1);
// perform unrolling
pFrames = Saig_ManUnrollCOI( p, nFrames );
assert( Aig_ManCoNum(pFrames) == 1 );
// start the SAT solver
pCnf = Cnf_DeriveSimple( pFrames, 0 );
pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
if ( pSat != NULL )
{
Aig_ManIncrementTravId( p );
for ( f = 0; f < nFrames; f++ )
{
Aig_ManForEachObj( p, pObj, i )
{
if ( !Aig_ObjIsCand(pObj) )
continue;
//--jlong : also use internal nodes as well
/* if ( !Aig_ObjIsCi(pObj) ) */
/* continue; */
if ( Aig_ObjIsTravIdCurrent(p, pObj) )
continue;
// get the node from timeframes
pRepr = p->pObjCopies[nFrames*i + nFrames-1-f];
pReprR = Aig_Regular(pRepr);
if ( pCnf->pVarNums[Aig_ObjId(pReprR)] < 0 )
continue;
// value = pSat->assigns[ pCnf->pVarNums[Aig_ObjId(pReprR)] ];
value = sat_solver_get_var_value( pSat, pCnf->pVarNums[Aig_ObjId(pReprR)] );
if ( value == l_Undef )
continue;
// label this node as taken
Aig_ObjSetTravIdCurrent(p, pObj);
if ( Saig_ObjIsLo(p, pObj) )
Aig_ObjSetTravIdCurrent( p, Aig_ObjFanin0(Saig_ObjLoToLi(p, pObj)) );
// remember the node
Vec_VecPush( vCands, f, Aig_NotCond( pObj, (value == l_True) ^ Aig_IsComplement(pRepr) ) );
// printf( "%s%d ", (value == l_False)? "":"!", i );
}
}
// printf( "\n" );
sat_solver_delete( pSat );
}
Aig_ManStop( pFrames );
Cnf_DataFree( pCnf );
if ( fVerbose )
{
printf( "Found %3d candidates.\n", Vec_VecSizeSize(vCands) );
Vec_VecForEachLevel( vCands, vNodes, k )
{
printf( "Level %d. Cands =%d ", k, Vec_PtrSize(vNodes) );
// Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
// printf( "%d:%s%d ", k, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
printf( "\n" );
}
}
ABC_FREE( p->pObjCopies );
/* -- jlong -- this does the SAT proof of the constraints */
Saig_ManFilterUsingInd2( p, vCands, nConfs, nProps, fVerbose );
if ( Vec_VecSizeSize(vCands) )
printf( "Found %3d constraints after filtering.\n", Vec_VecSizeSize(vCands) );
if ( fVerbose )
{
Vec_VecForEachLevel( vCands, vNodes, k )
{
printf( "Level %d. Constr =%d ", k, Vec_PtrSize(vNodes) );
// Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
// printf( "%d:%s%d ", k, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
printf( "\n" );
}
}
return vCands;
}
/**Function*************************************************************
Synopsis [Duplicates the AIG while unfolding constraints.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
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;
Aig_Obj_t * pObj;
int i, j, k, nNewFlops;
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 );
pNew->nConstrs = pAig->nConstrs + Vec_VecSizeSize(vCands);
// pNew->nConstrsTypeII = Vec_PtrSize(pAig->unfold2_type_II);
*typeII_cnt = Vec_PtrSize(pAig->unfold2_type_II);
// 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 * x = Aig_ObjRealCopy(pObj);
Aig_ObjCreateCo(pNew, x);
}
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++) );
}
}
//assert( nNewFlops == Vec_PtrSize(vNewFlops) );
Aig_ManSetRegNum( pNew, 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*************************************************************
Synopsis [Duplicates the AIG while unfolding constraints.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Saig_ManDupFoldConstrsFunc2( Aig_Man_t * pAig, int fCompl, int fVerbose ,
int typeII_cnt)
{
Aig_Man_t * pAigNew;
Aig_Obj_t * pMiter, * pFlopOut, * pFlopIn, * pObj;
int i;
if ( Aig_ManConstrNum(pAig) == 0 )
return Aig_ManDupDfs( pAig );
assert( Aig_ManConstrNum(pAig) < Saig_ManPoNum(pAig) );
// start the new manager
pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
pAigNew->pName = Abc_UtilStrsav( pAig->pName );
pAigNew->pSpec = Abc_UtilStrsav( pAig->pSpec );
// map the constant node
Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
// create variables for PIs
Aig_ManForEachCi( pAig, pObj, i )
pObj->pData = Aig_ObjCreateCi( pAigNew );
// add internal nodes of this frame
Aig_ManForEachNode( pAig, pObj, i )
pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
// OR the constraint outputs
pMiter = Aig_ManConst0( pAigNew );
int 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) {
printf("modeling typeII \n");
Aig_Obj_t * type_II_latch
= Aig_ObjCreateCi(pAigNew); /* will get connected later; */
pMiter = Aig_Or(pAigNew, pMiter,
Aig_And(pAigNew,
Aig_NotCond(type_II_latch, fCompl),
Aig_NotCond( Aig_ObjChild0Copy(pObj), fCompl ) )
);
} else
pMiter = Aig_Or( pAigNew, pMiter, Aig_NotCond( Aig_ObjChild0Copy(pObj), fCompl ) );
}
// create additional flop
if ( Saig_ManRegNum(pAig) > 0 )
{
pFlopOut = Aig_ObjCreateCi( pAigNew );
pFlopIn = Aig_Or( pAigNew, pMiter, pFlopOut );
}
else
pFlopIn = pMiter;
// create primary output
Saig_ManForEachPo( pAig, pObj, i )
{
if ( i >= Saig_ManPoNum(pAig)-Aig_ManConstrNum(pAig) )
continue;
pMiter = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_Not(pFlopIn) );
Aig_ObjCreateCo( pAigNew, pMiter );
}
// transfer to register outputs
{
/* 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(0)Saig_ManForEachLi( pAig, pObj, i ) {
Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
}
Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) );
Saig_ManForEachPo( pAig, pObj, i )
{
if ( i < Saig_ManPoNum(pAig)-Aig_ManConstrNum(pAig) )
continue;
/* now we got the constraint */
if (type_II) {
Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj));
Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAigNew)+1 );
}
}
// create additional flop
if ( Saig_ManRegNum(pAig) > 0 )
{
Aig_ObjCreateCo( pAigNew, pFlopIn );
Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAigNew)+1 );
}
// perform cleanup
Aig_ManCleanup( pAigNew );
Aig_ManSeqCleanup( pAigNew );
return pAigNew;
}
src/base/abci/abc.c
......@@ -294,6 +294,7 @@ 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_CommandBm ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandBm2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
......@@ -870,6 +871,8 @@ 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", "bm", Abc_CommandBm, 1 );
Cmd_CommandAdd( pAbc, "Verification", "bm2", Abc_CommandBm2, 1 );
......@@ -35347,5 +35350,5 @@ usage:
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
#include "abciUnfold2.c"
ABC_NAMESPACE_IMPL_END
src/base/abci/abcDar.c
......@@ -4560,6 +4560,6 @@ Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk )
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
#include "abcDarUnfold2.c"
ABC_NAMESPACE_IMPL_END
src/base/abci/abcDarUnfold2.c 0 → 100644
/**Function*************************************************************
Synopsis [Performs BDD-based reachability analysis.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkDarFold2( Abc_Ntk_t * pNtk, int fCompl, int fVerbose , int);
Abc_Ntk_t * Abc_NtkDarUnfold2( Abc_Ntk_t * pNtk, int nFrames, int nConfs, int nProps, int fStruct, int fOldAlgo, int fVerbose )
{
Abc_Ntk_t * pNtkAig;
Aig_Man_t * pMan, * pTemp;
int typeII_cnt = 0;
assert( Abc_NtkIsStrash(pNtk) );
pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( pMan == NULL )
return NULL;
if ( fStruct ){
assert(0);//pMan = Saig_ManDupUnfoldConstrs( pTemp = pMan );
}else
pMan = Saig_ManDupUnfoldConstrsFunc2( pTemp = pMan, nFrames, nConfs, nProps, fOldAlgo, fVerbose , &typeII_cnt);
Aig_ManStop( pTemp );
if ( pMan == NULL )
return NULL;
// typeII_cnt = pMan->nConstrsTypeII;
pNtkAig = Abc_NtkFromAigPhase( pMan );
pNtkAig->pName = Extra_UtilStrsav(pMan->pName);
pNtkAig->pSpec = Extra_UtilStrsav(pMan->pSpec);
Aig_ManStop( pMan );
return Abc_NtkDarFold2(pNtkAig, 0, fVerbose, typeII_cnt);
//return pNtkAig;
}
/**Function*************************************************************
Synopsis [Performs BDD-based reachability analysis.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkDarFold2( Abc_Ntk_t * pNtk, int fCompl, int fVerbose
, int typeII_cnt
)
{
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_ManDupFoldConstrsFunc2( pTemp = pMan, fCompl, fVerbose, typeII_cnt );
Aig_ManStop( pTemp );
pNtkAig = Abc_NtkFromAigPhase( pMan );
pNtkAig->pName = Extra_UtilStrsav(pMan->pName);
pNtkAig->pSpec = Extra_UtilStrsav(pMan->pSpec);
Aig_ManStop( pMan );
return pNtkAig;
}
src/base/abci/abciUnfold2.c 0 → 100644
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandUnfold2( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk, * pNtkRes;
int nFrames;
int nConfs;
int nProps;
int fStruct = 0;
int fOldAlgo = 0;
int fVerbose;
int c;
extern Abc_Ntk_t * Abc_NtkDarUnfold2( Abc_Ntk_t * pNtk, int nFrames, int nConfs, int nProps, int fStruct, int fOldAlgo, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
// set defaults
nFrames = 1;
nConfs = 1000;
nProps = 1000;
fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "CPvh" ) ) != EOF )
{
switch ( c )
{
/* case 'F': */
/* if ( globalUtilOptind >= argc ) */
/* { */
/* Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" ); */
/* goto usage; */
/* } */
/* nFrames = atoi(argv[globalUtilOptind]); */
/* globalUtilOptind++; */
/* if ( nFrames < 0 ) */
/* goto usage; */
/* break; */
case 'C':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
goto usage;
}
nConfs = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nConfs < 0 )
goto usage;
break;
case 'P':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" );
goto usage;
}
nProps = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nProps < 0 )
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_NtkIsComb(pNtk) )
{
Abc_Print( -1, "The network is combinational.\n" );
return 0;
}
if ( !Abc_NtkIsStrash(pNtk) )
{
Abc_Print( -1, "Currently only works for structurally hashed circuits.\n" );
return 0;
}
if ( Abc_NtkConstrNum(pNtk) > 0 )
{
Abc_Print( -1, "Constraints are already extracted.\n" );
return 0;
}
if ( Abc_NtkPoNum(pNtk) > 1 && !fStruct )
{
Abc_Print( -1, "Functional constraint extraction works for single-output miters (use \"orpos\").\n" );
return 0;
}
// modify the current network
pNtkRes = Abc_NtkDarUnfold2( pNtk, nFrames, nConfs, nProps, fStruct, fOldAlgo, fVerbose );
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: unfold [-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 );
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