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

Version abc80301

This commit is contained in:
Alan Mishchenko 2008-03-01 08:01:00 -08:00
parent f65983c2c0
commit 320c429bc4
58 changed files with 993 additions and 175 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

100
regtest_output.txt
View File

@ -93,4 +93,102 @@ s6669 : i/o = 83/ 55 lat = 183 and = 1915 (exor = 371) lev = 97
Networks are equivalent after fraiging.
abc - > time
elapse: 44.07 seconds, total: 44.07 seconds
abc 150>
abc 150>
UC Berkeley, ABC 1.01 (compiled Mar 1 2008 16:23:34)
abc 01> so regtest.script
abc - > r examples/apex4.pla; resyn; if; cec; ps; clp; resyn; map; cec; ps
Networks are equivalent.
examples/apex4: i/o = 9/ 19 lat = 0 nd = 1176 edge = 4298 aig = 4314 lev = 7
Shared BDD size = 917 nodes. BDD construction time = 0.04 sec
A simple supergate library is derived from gate library "mcnc_temp.genlib".
Loaded 20 unique 5-input supergates from "mcnc_temp.super". Time = 0.02 sec
Networks are equivalent.
examples/apex4: i/o = 9/ 19 lat = 0 nd = 1734 edge = 4291 aig = 2576 lev = 12
abc - > r examples/C2670.blif; st; w 1.aig; cec 1.aig
Networks are equivalent after structural hashing.
abc - > r examples/C2670.blif; st; short_names; w 1.bench; cec 1.bench
Networks are equivalent after structural hashing.
abc - > r examples/C2670.blif; st; short_names; ren -s; w 1.eqn; cec 1.eqn
Networks are equivalent.
abc - > r examples/C2670.blif; resyn2; if -K 8; cec; ps; u; map; cec; ps
Networks are equivalent.
C2670.iscas : i/o = 233/ 140 lat = 0 nd = 121 edge = 701 aig = 1088 lev = 4
Networks are equivalent.
C2670.iscas : i/o = 233/ 140 lat = 0 nd = 467 edge = 1029 aig = 651 lev = 14
abc - > r examples/frg2.blif; dsd; muxes; cec; ps; clp; share; resyn; map; cec; ps
Networks are equivalent.
frg2 : i/o = 143/ 139 lat = 0 nd = 1648 edge = 2646 aig = 2268 lev = 18
Shared BDD size = 1505 nodes. BDD construction time = 0.13 sec
Networks are equivalent.
frg2 : i/o = 143/ 139 lat = 0 nd = 557 edge = 1295 aig = 748 lev = 9
abc - > r examples/frg2.blif; bdd; muxes; cec; ps; clp; st; ren -b; muxes; cec; ps
Networks are equivalent.
frg2 : i/o = 143/ 139 lat = 0 nd = 2868 edge = 4855 aig = 4221 lev = 38
Shared BDD size = 1555 nodes. BDD construction time = 0.12 sec
Networks are equivalent.
frg2 : i/o = 143/ 139 lat = 0 nd = 2150 edge = 3465 aig = 3075 lev = 19
abc - > r examples/i10.blif; resyn2; fpga; cec; ps; u; map; cec; ps
Networks are equivalent.
i10 : i/o = 257/ 224 lat = 0 nd = 808 edge = 2767 aig = 2630 lev = 12
Networks are equivalent.
i10 : i/o = 257/ 224 lat = 0 nd = 1555 edge = 3379 aig = 1980 lev = 24
abc - > r examples/i10.blif; choice; fpga; cec; ps; u; map; cec; ps
Performing LUT mapping with 548 choices.
Networks are equivalent.
i10 : i/o = 257/ 224 lat = 0 nd = 788 edge = 2722 aig = 2522 lev = 13
Performing mapping with choices.
Networks are equivalent.
i10 : i/o = 257/ 224 lat = 0 nd = 1462 edge = 3271 aig = 1977 lev = 23
abc - > r examples/pj1.blif; st; if; cec; ps; u; map; cec; ps
Networks are equivalent after structural hashing.
exCombCkt : i/o = 1769/ 1063 lat = 0 nd = 5924 edge = 21224 aig = 22799 lev = 52
Networks are equivalent.
exCombCkt : i/o = 1769/ 1063 lat = 0 nd = 11474 edge = 26350 aig = 16032 lev = 80
abc - > r examples/s38417.blif; comb; w 1.blif; resyn; if; cec 1.blif; ps
Line 14: Skipping line ".wire_load_slope 0.00".
Networks are equivalent.
s38417 : i/o = 1664/ 1742 lat = 0 nd = 3502 edge = 11182 aig = 10001 lev = 9
abc - > r examples/s38417.blif; resyn; if; cec; ps; u; map; cec; ps
Line 14: Skipping line ".wire_load_slope 0.00".
Line 14: Skipping line ".wire_load_slope 0.00".
Networks are equivalent.
s38417 : i/o = 28/ 106 lat = 1636 nd = 3502 edge = 11182 aig = 10001 lev = 9
Line 14: Skipping line ".wire_load_slope 0.00".
Networks are equivalent.
s38417 : i/o = 28/ 106 lat = 1636 nd = 7189 edge = 15262 aig = 8689 lev = 17
abc - > r examples/s38584.bench; resyn; ren -s; fx; if; cec; ps; u; map; cec; ps
The network was strashed and balanced before FPGA mapping.
Networks are equivalent.
examples/s38584: i/o = 12/ 278 lat = 1452 nd = 4452 edge = 14910 aig = 12424 lev = 9
The network was strashed and balanced before mapping.
Networks are equivalent.
examples/s38584: i/o = 12/ 278 lat = 1452 nd = 8339 edge = 18690 aig = 10633 lev = 18
abc - > r examples/s444.blif; b; esd -v; print_exdc; dsd; cec; ps
Shared BDD size = 181 nodes.
BDD nodes in the transition relation before reordering 557.
BDD nodes in the transition relation after reordering 456.
Reachability analysis completed in 151 iterations.
The number of minterms in the reachable state set = 8865. ( 0.42 %)
BDD nodes in the unreachable states before reordering 124.
BDD nodes in the unreachable states after reordering 113.
EXDC network statistics:
exdc : i/o = 21/ 21 lat = 0 nd = 21 edge = 41 cube = 86 lev = 2
Networks are equivalent.
s444 : i/o = 3/ 6 lat = 21 nd = 82 edge = 186 aig = 176 lev = 7
abc - > r examples/s444.blif; double; frames -F 5; w 1.blif; ffpga -K 8; cec 1.blif
Networks are equivalent after structural hashing.
abc - > r examples/s5378.blif; frames -F 5; cycle; w 1.blif; ps; ret; ps; sec 1.blif
s5378_5_frames: i/o = 175/ 245 lat = 164 and = 6629 (exor = 115) lev = 59
s5378_5_frames: i/o = 175/ 245 lat = 182 nd = 6957 edge = 13585 cube = 6956 lev = 50
Networks are equivalent after framing.
abc - > r examples/s6669.blif; cycle; w 1.blif; ps; ret -M 3; resyn; ps; sec 1.blif
s6669 : i/o = 83/ 55 lat = 239 nd = 3148 edge = 5411 cube = 3148 lev = 93
s6669 : i/o = 83/ 55 lat = 183 and = 1915 (exor = 371) lev = 97
Networks are equivalent after fraiging.
abc - > time
elapse: 43.01 seconds, total: 43.01 seconds
abc 159>

38
src/aig/aig/aig.h
View File

@ -143,6 +143,7 @@ struct Aig_Man_t_
void * pSeqModel;
Aig_Man_t * pManHaig;
Aig_Man_t * pManExdc;
Vec_Ptr_t * vOnehots;
// timing statistics
int time1;
int time2;
@ -241,28 +242,28 @@ static inline int Aig_WordFindFirstBit( unsigned uWord )
return -1;
}
static inline Aig_Obj_t * Aig_Regular( Aig_Obj_t * p ) { return (Aig_Obj_t *)((unsigned long)(p) & ~01); }
static inline Aig_Obj_t * Aig_Not( Aig_Obj_t * p ) { return (Aig_Obj_t *)((unsigned long)(p) ^ 01); }
static inline Aig_Obj_t * Aig_NotCond( Aig_Obj_t * p, int c ) { return (Aig_Obj_t *)((unsigned long)(p) ^ (c)); }
static inline int Aig_IsComplement( Aig_Obj_t * p ) { return (int)((unsigned long)(p) & 01); }
static inline Aig_Obj_t * Aig_Regular( Aig_Obj_t * p ) { return (Aig_Obj_t *)((PORT_PTRUINT_T)(p) & ~01); }
static inline Aig_Obj_t * Aig_Not( Aig_Obj_t * p ) { return (Aig_Obj_t *)((PORT_PTRUINT_T)(p) ^ 01); }
static inline Aig_Obj_t * Aig_NotCond( Aig_Obj_t * p, int c ) { return (Aig_Obj_t *)((PORT_PTRUINT_T)(p) ^ (c)); }
static inline int Aig_IsComplement( Aig_Obj_t * p ) { return (int)((PORT_PTRUINT_T)(p) & 01); }
static inline int Aig_ManPiNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_PI]; }
static inline int Aig_ManPoNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_PO]; }
static inline int Aig_ManBufNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_BUF]; }
static inline int Aig_ManAndNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_AND]; }
static inline int Aig_ManExorNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_EXOR]; }
static inline int Aig_ManLatchNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_LATCH]; }
static inline int Aig_ManPiNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_PI]; }
static inline int Aig_ManPoNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_PO]; }
static inline int Aig_ManBufNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_BUF]; }
static inline int Aig_ManAndNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_AND]; }
static inline int Aig_ManExorNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_EXOR]; }
static inline int Aig_ManLatchNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_LATCH]; }
static inline int Aig_ManNodeNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_AND]+p->nObjs[AIG_OBJ_EXOR]; }
static inline int Aig_ManGetCost( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_AND]+3*p->nObjs[AIG_OBJ_EXOR]; }
static inline int Aig_ManObjNum( Aig_Man_t * p ) { return p->nCreated - p->nDeleted; }
static inline int Aig_ManObjNumMax( Aig_Man_t * p ) { return Vec_PtrSize(p->vObjs); }
static inline int Aig_ManRegNum( Aig_Man_t * p ) { return p->nRegs; }
static inline int Aig_ManObjNum( Aig_Man_t * p ) { return p->nCreated - p->nDeleted; }
static inline int Aig_ManObjNumMax( Aig_Man_t * p ) { return Vec_PtrSize(p->vObjs); }
static inline int Aig_ManRegNum( Aig_Man_t * p ) { return p->nRegs; }
static inline Aig_Obj_t * Aig_ManConst0( Aig_Man_t * p ) { return Aig_Not(p->pConst1); }
static inline Aig_Obj_t * Aig_ManConst1( Aig_Man_t * p ) { return p->pConst1; }
static inline Aig_Obj_t * Aig_ManGhost( Aig_Man_t * p ) { return &p->Ghost; }
static inline Aig_Obj_t * Aig_ManPi( Aig_Man_t * p, int i ) { return (Aig_Obj_t *)Vec_PtrEntry(p->vPis, i); }
static inline Aig_Obj_t * Aig_ManPo( Aig_Man_t * p, int i ) { return (Aig_Obj_t *)Vec_PtrEntry(p->vPos, i); }
static inline Aig_Obj_t * Aig_ManConst0( Aig_Man_t * p ) { return Aig_Not(p->pConst1); }
static inline Aig_Obj_t * Aig_ManConst1( Aig_Man_t * p ) { return p->pConst1; }
static inline Aig_Obj_t * Aig_ManGhost( Aig_Man_t * p ) { return &p->Ghost; }
static inline Aig_Obj_t * Aig_ManPi( Aig_Man_t * p, int i ) { return (Aig_Obj_t *)Vec_PtrEntry(p->vPis, i); }
static inline Aig_Obj_t * Aig_ManPo( Aig_Man_t * p, int i ) { return (Aig_Obj_t *)Vec_PtrEntry(p->vPos, i); }
static inline Aig_Obj_t * Aig_ManLo( Aig_Man_t * p, int i ) { return (Aig_Obj_t *)Vec_PtrEntry(p->vPis, Aig_ManPiNum(p)-Aig_ManRegNum(p)+i); }
static inline Aig_Obj_t * Aig_ManLi( Aig_Man_t * p, int i ) { return (Aig_Obj_t *)Vec_PtrEntry(p->vPos, Aig_ManPoNum(p)-Aig_ManRegNum(p)+i); }
static inline Aig_Obj_t * Aig_ManObj( Aig_Man_t * p, int i ) { return p->vObjs ? (Aig_Obj_t *)Vec_PtrEntry(p->vObjs, i) : NULL; }
@ -529,6 +530,7 @@ extern Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSiz
extern Vec_Ptr_t * Aig_ManRegPartitionSimple( Aig_Man_t * pAig, int nPartSize, int nOverSize );
extern Vec_Ptr_t * Aig_ManRegPartitionSmart( Aig_Man_t * pAig, int nPartSize );
extern Aig_Man_t * Aig_ManRegCreatePart( Aig_Man_t * pAig, Vec_Int_t * vPart, int * pnCountPis, int * pnCountRegs, int ** ppMapBack );
extern Vec_Ptr_t * Aig_ManRegProjectOnehots( Aig_Man_t * pAig, Aig_Man_t * pPart, Vec_Ptr_t * vOnehots, int fVerbose );
/*=== aigRepr.c =========================================================*/
extern void Aig_ManReprStart( Aig_Man_t * p, int nIdMax );
extern void Aig_ManReprStop( Aig_Man_t * p );

1
src/aig/aig/aigMan.c
View File

@ -329,6 +329,7 @@ void Aig_ManStop( Aig_Man_t * p )
if ( p->vLevels ) Vec_VecFree( p->vLevels );
if ( p->vFlopNums) Vec_IntFree( p->vFlopNums );
if ( p->pManExdc ) Aig_ManStop( p->pManExdc );
if ( p->vOnehots ) Vec_VecFree( (Vec_Vec_t *)p->vOnehots );
FREE( p->pSeqModel );
FREE( p->pName );
FREE( p->pObjCopies );

62
src/aig/aig/aigPartReg.c
View File

@ -228,6 +228,67 @@ void Aig_ManRegPartitionAdd( Aig_ManPre_t * p, int iReg )
Vec_FltPush( p->vPartCost, 1.0*Vec_IntSize(p->vFreeVars)/Vec_IntSize(p->vRegs) );
}
/**Function*************************************************************
Synopsis [Creates projection of 1-hot registers onto the given partition.]
Description [Assumes that the relevant register outputs are labeled with
the current traversal ID.]
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Aig_ManRegProjectOnehots( Aig_Man_t * pAig, Aig_Man_t * pPart, Vec_Ptr_t * vOnehots, int fVerbose )
{
Vec_Ptr_t * vOnehotsPart = NULL;
Vec_Int_t * vGroup, * vGroupNew;
Aig_Obj_t * pObj, * pObjNew;
int nOffset, iReg, i, k;
// set the PI numbers
Aig_ManForEachPi( pPart, pObj, i )
pObj->iData = i;
// go through each group and check if registers are involved in this one
nOffset = Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig);
Vec_PtrForEachEntry( vOnehots, vGroup, i )
{
vGroupNew = NULL;
Vec_IntForEachEntry( vGroup, iReg, k )
{
pObj = Aig_ManPi( pAig, nOffset+iReg );
if ( !Aig_ObjIsTravIdCurrent(pAig, pObj) )
continue;
if ( vGroupNew == NULL )
vGroupNew = Vec_IntAlloc( Vec_IntSize(vGroup) );
pObjNew = pObj->pData;
Vec_IntPush( vGroupNew, pObjNew->iData );
}
if ( vGroupNew == NULL )
continue;
if ( Vec_IntSize(vGroupNew) > 1 )
{
if ( vOnehotsPart == NULL )
vOnehotsPart = Vec_PtrAlloc( 100 );
Vec_PtrPush( vOnehotsPart, vGroupNew );
}
else
Vec_IntFree( vGroupNew );
}
// clear the PI numbers
Aig_ManForEachPi( pPart, pObj, i )
pObj->iData = 0;
// print out
if ( vOnehotsPart && fVerbose )
{
printf( "Partition contains %d groups of 1-hot registers: { ", Vec_PtrSize(vOnehotsPart) );
Vec_PtrForEachEntry( vOnehotsPart, vGroup, k )
printf( "%d ", Vec_IntSize(vGroup) );
printf( "}\n" );
}
return vOnehotsPart;
}
/**Function*************************************************************
Synopsis [Computes partitioning of registers.]
@ -292,6 +353,7 @@ Aig_Man_t * Aig_ManRegCreatePart( Aig_Man_t * pAig, Vec_Int_t * vPart, int * pnC
pObj = Aig_ManPi(pAig, nOffset+iOut);
pObj->pData = Aig_ObjCreatePi(pNew);
Aig_ObjCreatePo( pNew, pObj->pData );
Aig_ObjSetTravIdCurrent( pAig, pObj ); // added
}
// create the nodes
Vec_PtrForEachEntry( vNodes, pObj, i )

8
src/aig/bdc/bdcInt.h
View File

@ -110,10 +110,10 @@ struct Bdc_Man_t_
};
// working with complemented attributes of objects
static inline int Bdc_IsComplement( Bdc_Fun_t * p ) { return (int)((unsigned long)p & (unsigned long)01); }
static inline Bdc_Fun_t * Bdc_Regular( Bdc_Fun_t * p ) { return (Bdc_Fun_t *)((unsigned long)p & ~(unsigned long)01); }
static inline Bdc_Fun_t * Bdc_Not( Bdc_Fun_t * p ) { return (Bdc_Fun_t *)((unsigned long)p ^ (unsigned long)01); }
static inline Bdc_Fun_t * Bdc_NotCond( Bdc_Fun_t * p, int c ) { return (Bdc_Fun_t *)((unsigned long)p ^ (unsigned long)(c!=0)); }
static inline int Bdc_IsComplement( Bdc_Fun_t * p ) { return (int)((PORT_PTRUINT_T)p & (PORT_PTRUINT_T)01); }
static inline Bdc_Fun_t * Bdc_Regular( Bdc_Fun_t * p ) { return (Bdc_Fun_t *)((PORT_PTRUINT_T)p & ~(PORT_PTRUINT_T)01); }
static inline Bdc_Fun_t * Bdc_Not( Bdc_Fun_t * p ) { return (Bdc_Fun_t *)((PORT_PTRUINT_T)p ^ (PORT_PTRUINT_T)01); }
static inline Bdc_Fun_t * Bdc_NotCond( Bdc_Fun_t * p, int c ) { return (Bdc_Fun_t *)((PORT_PTRUINT_T)p ^ (PORT_PTRUINT_T)(c!=0)); }
static inline Bdc_Fun_t * Bdc_FunNew( Bdc_Man_t * p ) { Bdc_Fun_t * pRes; if ( p->nNodes == p->nNodesLimit ) return NULL; pRes = p->pNodes + p->nNodes++; memset( pRes, 0, sizeof(Bdc_Fun_t) ); p->nNodesNew++; return pRes; }
static inline void Bdc_IsfStart( Bdc_Man_t * p, Bdc_Isf_t * pF ) { pF->puOn = Vec_IntFetch( p->vMemory, p->nWords ); pF->puOff = Vec_IntFetch( p->vMemory, p->nWords ); }

3
src/aig/dar/darCore.c
View File

@ -95,11 +95,11 @@ int Dar_ManRewrite( Aig_Man_t * pAig, Dar_RwrPar_t * pPars )
// Aig_ManForEachNodeInOrder( pAig, pObj )
{
// Bar_ProgressUpdate( pProgress, 100*pAig->nAndPrev/pAig->nAndTotal, NULL );
// Bar_ProgressUpdate( pProgress, i, NULL );
if ( !Aig_ObjIsNode(pObj) )
continue;
if ( i > nNodesOld )
// if ( p->pPars->fUseZeros && i > nNodesOld )
break;
// consider freeing the cuts
@ -109,6 +109,7 @@ int Dar_ManRewrite( Aig_Man_t * pAig, Dar_RwrPar_t * pPars )
// compute cuts for the node
p->nNodesTried++;
clk = clock();
Dar_ObjSetCuts( pObj, NULL );
Dar_ObjComputeCuts_rec( p, pObj );
p->timeCuts += clock() - clk;

1
src/aig/fra/fra.h
View File

@ -297,6 +297,7 @@ extern int Fra_OneHotRefineUsingCex( Fra_Man_t * p, Vec_Int_t *
extern int Fra_OneHotCount( Fra_Man_t * p, Vec_Int_t * vOneHots );
extern void Fra_OneHotEstimateCoverage( Fra_Man_t * p, Vec_Int_t * vOneHots );
extern Aig_Man_t * Fra_OneHotCreateExdc( Fra_Man_t * p, Vec_Int_t * vOneHots );
extern void Fra_OneHotAddKnownConstraint( Fra_Man_t * p, Vec_Ptr_t * vOnehots );
/*=== fraImp.c ========================================================*/
extern Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, int fLatchCorr );
extern void Fra_ImpAddToSolver( Fra_Man_t * p, Vec_Int_t * vImps, int * pSatVarNums );

43
src/aig/fra/fraHot.c
View File

@ -420,6 +420,49 @@ Aig_Man_t * Fra_OneHotCreateExdc( Fra_Man_t * p, Vec_Int_t * vOneHots )
return pNew;
}
/**Function*************************************************************
Synopsis [Assumes one-hot implications in the SAT solver.]
Description []
SideEffects []
SeeAlso []
**********************************************************************/
void Fra_OneHotAddKnownConstraint( Fra_Man_t * p, Vec_Ptr_t * vOnehots )
{
Vec_Int_t * vGroup;
Aig_Obj_t * pObj1, * pObj2;
int k, i, j, Out1, Out2, pLits[2];
//
// these constrants should be added to different timeframes!
// (also note that PIs follow first - then registers)
//
Vec_PtrForEachEntry( vOnehots, vGroup, k )
{
Vec_IntForEachEntry( vGroup, Out1, i )
Vec_IntForEachEntryStart( vGroup, Out2, j, i+1 )
{
pObj1 = Aig_ManPi( p->pManFraig, Out1 );
pObj2 = Aig_ManPi( p->pManFraig, Out2 );
pLits[0] = toLitCond( Fra_ObjSatNum(pObj1), 1 );
pLits[1] = toLitCond( Fra_ObjSatNum(pObj2), 1 );
// add contraint to solver
if ( !sat_solver_addclause( p->pSat, pLits, pLits + 2 ) )
{
printf( "Fra_OneHotAddKnownConstraint(): Adding clause makes SAT solver unsat.\n" );
sat_solver_delete( p->pSat );
p->pSat = NULL;
return;
}
}
}
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

10
src/aig/fra/fraInd.c
View File

@ -253,6 +253,7 @@ Aig_Man_t * Fra_FraigInductionPart( Aig_Man_t * pAig, Fra_Ssw_t * pPars )
int * pMapBack;
int i, nCountPis, nCountRegs;
int nClasses, nPartSize, fVerbose;
int clk = clock();
// save parameters
nPartSize = pPars->nPartSize; pPars->nPartSize = 0;
@ -281,6 +282,9 @@ Aig_Man_t * Fra_FraigInductionPart( Aig_Man_t * pAig, Fra_Ssw_t * pPars )
Vec_PtrForEachEntry( vResult, vPart, i )
{
pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, &pMapBack );
// create the projection of 1-hot registers
if ( pAig->vOnehots )
pTemp->vOnehots = Aig_ManRegProjectOnehots( pAig, pTemp, pAig->vOnehots, fVerbose );
// run SSW
pNew = Fra_FraigInduction( pTemp, pPars );
nClasses = Aig_TransferMappedClasses( pAig, pTemp, pMapBack );
@ -299,6 +303,10 @@ Aig_Man_t * Fra_FraigInductionPart( Aig_Man_t * pAig, Fra_Ssw_t * pPars )
Vec_VecFree( (Vec_Vec_t *)vResult );
pPars->nPartSize = nPartSize;
pPars->fVerbose = fVerbose;
if ( fVerbose )
{
PRT( "Total time", clock() - clk );
}
return pNew;
}
@ -485,6 +493,8 @@ p->timeTrav += clock() - clk2;
// add one-hotness clauses
if ( p->pPars->fUse1Hot )
Fra_OneHotAssume( p, p->vOneHots );
// if ( p->pManAig->vOnehots )
// Fra_OneHotAddKnownConstraint( p, p->pManAig->vOnehots );
// report the intermediate results
if ( pPars->fVerbose )

8
src/aig/hop/hop.h
View File

@ -124,10 +124,10 @@ static inline void Hop_InfoXorBit( unsigned * p, int i ) { p[(i)>>5] ^=
static inline int Hop_Base2Log( unsigned n ) { int r; assert( n >= 0 ); if ( n < 2 ) return n; for ( r = 0, n--; n; n >>= 1, r++ ); return r; }
static inline int Hop_Base10Log( unsigned n ) { int r; assert( n >= 0 ); if ( n < 2 ) return n; for ( r = 0, n--; n; n /= 10, r++ ); return r; }
static inline Hop_Obj_t * Hop_Regular( Hop_Obj_t * p ) { return (Hop_Obj_t *)((unsigned long)(p) & ~01); }
static inline Hop_Obj_t * Hop_Not( Hop_Obj_t * p ) { return (Hop_Obj_t *)((unsigned long)(p) ^ 01); }
static inline Hop_Obj_t * Hop_NotCond( Hop_Obj_t * p, int c ) { return (Hop_Obj_t *)((unsigned long)(p) ^ (c)); }
static inline int Hop_IsComplement( Hop_Obj_t * p ) { return (int)((unsigned long)(p) & 01); }
static inline Hop_Obj_t * Hop_Regular( Hop_Obj_t * p ) { return (Hop_Obj_t *)((PORT_PTRUINT_T)(p) & ~01); }
static inline Hop_Obj_t * Hop_Not( Hop_Obj_t * p ) { return (Hop_Obj_t *)((PORT_PTRUINT_T)(p) ^ 01); }
static inline Hop_Obj_t * Hop_NotCond( Hop_Obj_t * p, int c ) { return (Hop_Obj_t *)((PORT_PTRUINT_T)(p) ^ (c)); }
static inline int Hop_IsComplement( Hop_Obj_t * p ) { return (int)((PORT_PTRUINT_T)(p) & 01); }
static inline Hop_Obj_t * Hop_ManConst0( Hop_Man_t * p ) { return Hop_Not(p->pConst1); }
static inline Hop_Obj_t * Hop_ManConst1( Hop_Man_t * p ) { return p->pConst1; }

8
src/aig/ivy/ivy.h
View File

@ -186,10 +186,10 @@ static inline int Ivy_InfoHasBit( unsigned * p, int i ) { return (p[(i
static inline void Ivy_InfoSetBit( unsigned * p, int i ) { p[(i)>>5] |= (1<<((i) & 31)); }
static inline void Ivy_InfoXorBit( unsigned * p, int i ) { p[(i)>>5] ^= (1<<((i) & 31)); }
static inline Ivy_Obj_t * Ivy_Regular( Ivy_Obj_t * p ) { return (Ivy_Obj_t *)((unsigned long)(p) & ~01); }
static inline Ivy_Obj_t * Ivy_Not( Ivy_Obj_t * p ) { return (Ivy_Obj_t *)((unsigned long)(p) ^ 01); }
static inline Ivy_Obj_t * Ivy_NotCond( Ivy_Obj_t * p, int c ) { return (Ivy_Obj_t *)((unsigned long)(p) ^ (c)); }
static inline int Ivy_IsComplement( Ivy_Obj_t * p ) { return (int)((unsigned long)(p) & 01); }
static inline Ivy_Obj_t * Ivy_Regular( Ivy_Obj_t * p ) { return (Ivy_Obj_t *)((PORT_PTRUINT_T)(p) & ~01); }
static inline Ivy_Obj_t * Ivy_Not( Ivy_Obj_t * p ) { return (Ivy_Obj_t *)((PORT_PTRUINT_T)(p) ^ 01); }
static inline Ivy_Obj_t * Ivy_NotCond( Ivy_Obj_t * p, int c ) { return (Ivy_Obj_t *)((PORT_PTRUINT_T)(p) ^ (c)); }
static inline int Ivy_IsComplement( Ivy_Obj_t * p ) { return (int)((PORT_PTRUINT_T)(p) & 01); }
static inline Ivy_Obj_t * Ivy_ManConst0( Ivy_Man_t * p ) { return Ivy_Not(p->pConst1); }
static inline Ivy_Obj_t * Ivy_ManConst1( Ivy_Man_t * p ) { return p->pConst1; }

8
src/aig/rwt/rwt.h
View File

@ -112,10 +112,10 @@ struct Rwt_Node_t_ // 24 bytes
};
// manipulation of complemented attributes
static inline int Rwt_IsComplement( Rwt_Node_t * p ) { return (int)(((unsigned long)p) & 01); }
static inline Rwt_Node_t * Rwt_Regular( Rwt_Node_t * p ) { return (Rwt_Node_t *)((unsigned long)(p) & ~01); }
static inline Rwt_Node_t * Rwt_Not( Rwt_Node_t * p ) { return (Rwt_Node_t *)((unsigned long)(p) ^ 01); }
static inline Rwt_Node_t * Rwt_NotCond( Rwt_Node_t * p, int c ) { return (Rwt_Node_t *)((unsigned long)(p) ^ (c)); }
static inline int Rwt_IsComplement( Rwt_Node_t * p ) { return (int)(((PORT_PTRUINT_T)p) & 01); }
static inline Rwt_Node_t * Rwt_Regular( Rwt_Node_t * p ) { return (Rwt_Node_t *)((PORT_PTRUINT_T)(p) & ~01); }
static inline Rwt_Node_t * Rwt_Not( Rwt_Node_t * p ) { return (Rwt_Node_t *)((PORT_PTRUINT_T)(p) ^ 01); }
static inline Rwt_Node_t * Rwt_NotCond( Rwt_Node_t * p, int c ) { return (Rwt_Node_t *)((PORT_PTRUINT_T)(p) ^ (c)); }
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///

20
src/base/abc/abc.h
View File

@ -201,9 +201,10 @@ struct Abc_Ntk_t_
Abc_Ntk_t * pExdc; // the EXDC network (if given)
void * pExcare; // the EXDC network (if given)
void * pData; // misc
Abc_Ntk_t * pCopy;
Abc_Ntk_t * pCopy; // copy of this network
Hop_Man_t * pHaig; // history AIG
float * pLutTimes; // arrivals/requireds/slacks using LUT-delay model
Vec_Ptr_t * vOnehots; // names of one-hot-encoded registers
// node attributes
Vec_Ptr_t * vAttrs; // managers of various node attributes (node functionality, global BDDs, etc)
};
@ -328,10 +329,10 @@ static inline Abc_Obj_t * Abc_NtkAssert( Abc_Ntk_t * pNtk, int i ) { return (A
static inline Abc_Obj_t * Abc_NtkBox( Abc_Ntk_t * pNtk, int i ) { return (Abc_Obj_t *)Vec_PtrEntry( pNtk->vBoxes, i ); }
// working with complemented attributes of objects
static inline bool Abc_ObjIsComplement( Abc_Obj_t * p ) { return (bool)((unsigned long)p & (unsigned long)01); }
static inline Abc_Obj_t * Abc_ObjRegular( Abc_Obj_t * p ) { return (Abc_Obj_t *)((unsigned long)p & ~(unsigned long)01); }
static inline Abc_Obj_t * Abc_ObjNot( Abc_Obj_t * p ) { return (Abc_Obj_t *)((unsigned long)p ^ (unsigned long)01); }
static inline Abc_Obj_t * Abc_ObjNotCond( Abc_Obj_t * p, int c ) { return (Abc_Obj_t *)((unsigned long)p ^ (unsigned long)(c!=0)); }
static inline bool Abc_ObjIsComplement( Abc_Obj_t * p ) { return (bool)((PORT_PTRUINT_T)p & (PORT_PTRUINT_T)01); }
static inline Abc_Obj_t * Abc_ObjRegular( Abc_Obj_t * p ) { return (Abc_Obj_t *)((PORT_PTRUINT_T)p & ~(PORT_PTRUINT_T)01); }
static inline Abc_Obj_t * Abc_ObjNot( Abc_Obj_t * p ) { return (Abc_Obj_t *)((PORT_PTRUINT_T)p ^ (PORT_PTRUINT_T)01); }
static inline Abc_Obj_t * Abc_ObjNotCond( Abc_Obj_t * p, int c ) { return (Abc_Obj_t *)((PORT_PTRUINT_T)p ^ (PORT_PTRUINT_T)(c!=0)); }
// reading data members of the object
static inline unsigned Abc_ObjType( Abc_Obj_t * pObj ) { return pObj->Type; }
@ -441,9 +442,6 @@ static inline void * Abc_ObjMvVar( Abc_Obj_t * pObj ) { return
static inline int Abc_ObjMvVarNum( Abc_Obj_t * pObj ) { return (Abc_NtkMvVar(pObj->pNtk) && Abc_ObjMvVar(pObj))? *((int*)Abc_ObjMvVar(pObj)) : 2; }
static inline void Abc_ObjSetMvVar( Abc_Obj_t * pObj, void * pV) { Vec_AttWriteEntry( (Vec_Att_t *)Abc_NtkMvVar(pObj->pNtk), pObj->Id, pV ); }
// outputs the runtime in seconds
#define PRT(a,t) printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC))
////////////////////////////////////////////////////////////////////////
/// ITERATORS ///
////////////////////////////////////////////////////////////////////////
@ -523,7 +521,7 @@ extern Abc_Obj_t * Abc_AigMuxLookup( Abc_Aig_t * pMan, Abc_Obj_t * pC, Ab
extern Abc_Obj_t * Abc_AigOr( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 );
extern Abc_Obj_t * Abc_AigXor( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 );
extern Abc_Obj_t * Abc_AigMux( Abc_Aig_t * pMan, Abc_Obj_t * pC, Abc_Obj_t * p1, Abc_Obj_t * p0 );
extern Abc_Obj_t * Abc_AigMiter( Abc_Aig_t * pMan, Vec_Ptr_t * vPairs );
extern Abc_Obj_t * Abc_AigMiter( Abc_Aig_t * pMan, Vec_Ptr_t * vPairs, int fImplic );
extern void Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, bool fUpdateLevel );
extern void Abc_AigDeleteNode( Abc_Aig_t * pMan, Abc_Obj_t * pOld );
extern void Abc_AigRehash( Abc_Aig_t * pMan );
@ -635,6 +633,7 @@ extern Vec_Int_t * Abc_NtkCollectLatchValues( Abc_Ntk_t * pNtk );
extern void Abc_NtkInsertLatchValues( Abc_Ntk_t * pNtk, Vec_Int_t * vValues );
extern Abc_Obj_t * Abc_NtkAddLatch( Abc_Ntk_t * pNtk, Abc_Obj_t * pDriver, Abc_InitType_t Init );
extern void Abc_NtkConvertDcLatches( Abc_Ntk_t * pNtk );
extern Vec_Ptr_t * Abc_NtkConverLatchNamesIntoNumbers( Abc_Ntk_t * pNtk );
/*=== abcLib.c ==========================================================*/
extern Abc_Lib_t * Abc_LibCreate( char * pName );
extern void Abc_LibFree( Abc_Lib_t * pLib, Abc_Ntk_t * pNtk );
@ -649,7 +648,7 @@ extern int Abc_NodeMinimumBase( Abc_Obj_t * pNode );
extern int Abc_NtkRemoveDupFanins( Abc_Ntk_t * pNtk );
extern int Abc_NodeRemoveDupFanins( Abc_Obj_t * pNode );
/*=== abcMiter.c ==========================================================*/
extern Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, int nPartSize );
extern Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, int nPartSize, int fImplic );
extern void Abc_NtkMiterAddCone( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter, Abc_Obj_t * pNode );
extern Abc_Ntk_t * Abc_NtkMiterAnd( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fOr, int fCompl2 );
extern Abc_Ntk_t * Abc_NtkMiterCofactor( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues );
@ -739,6 +738,7 @@ extern void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int
extern void Abc_NtkPrintIo( FILE * pFile, Abc_Ntk_t * pNtk );
extern void Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk );
extern void Abc_NtkPrintFanio( FILE * pFile, Abc_Ntk_t * pNtk );
extern void Abc_NtkPrintFanioNew( FILE * pFile, Abc_Ntk_t * pNtk );
extern void Abc_NodePrintFanio( FILE * pFile, Abc_Obj_t * pNode );
extern void Abc_NtkPrintFactor( FILE * pFile, Abc_Ntk_t * pNtk, int fUseRealNames );
extern void Abc_NodePrintFactor( FILE * pFile, Abc_Obj_t * pNode, int fUseRealNames );

14
src/base/abc/abcAig.c
View File

@ -786,15 +786,23 @@ Abc_Obj_t * Abc_AigMiter_rec( Abc_Aig_t * pMan, Abc_Obj_t ** ppObjs, int nObjs )
SeeAlso []
***********************************************************************/
Abc_Obj_t * Abc_AigMiter( Abc_Aig_t * pMan, Vec_Ptr_t * vPairs )
Abc_Obj_t * Abc_AigMiter( Abc_Aig_t * pMan, Vec_Ptr_t * vPairs, int fImplic )
{
int i;
if ( vPairs->nSize == 0 )
return Abc_ObjNot( Abc_AigConst1(pMan->pNtkAig) );
assert( vPairs->nSize % 2 == 0 );
// go through the cubes of the node's SOP
for ( i = 0; i < vPairs->nSize; i += 2 )
vPairs->pArray[i/2] = Abc_AigXor( pMan, vPairs->pArray[i], vPairs->pArray[i+1] );
if ( fImplic )
{
for ( i = 0; i < vPairs->nSize; i += 2 )
vPairs->pArray[i/2] = Abc_AigAnd( pMan, vPairs->pArray[i], Abc_ObjNot(vPairs->pArray[i+1]) );
}
else
{
for ( i = 0; i < vPairs->nSize; i += 2 )
vPairs->pArray[i/2] = Abc_AigXor( pMan, vPairs->pArray[i], vPairs->pArray[i+1] );
}
vPairs->nSize = vPairs->nSize/2;
return Abc_AigMiter_rec( pMan, (Abc_Obj_t **)vPairs->pArray, vPairs->nSize );
}

2
src/base/abc/abcDfs.c
View File

@ -121,6 +121,8 @@ Vec_Ptr_t * Abc_NtkDfsNodes( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes
// go through the PO nodes and call for each of them
for ( i = 0; i < nNodes; i++ )
{
if ( Abc_NtkIsStrash(pNtk) && Abc_AigNodeIsConst(ppNodes[i]) )
continue;
if ( Abc_ObjIsCo(ppNodes[i]) )
{
Abc_NodeSetTravIdCurrent(ppNodes[i]);

52
src/base/abc/abcLatch.c
View File

@ -318,6 +318,58 @@ void Abc_NtkConvertDcLatches( Abc_Ntk_t * pNtk )
printf( "The number of converted latches with DC values = %d.\n", Counter );
}
/**Function*************************************************************
Synopsis [Transfors the array of latch names into that of latch numbers.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Abc_NtkConverLatchNamesIntoNumbers( Abc_Ntk_t * pNtk )
{
Vec_Ptr_t * vResult, * vNames;
Vec_Int_t * vNumbers;
Abc_Obj_t * pObj;
char * pName;
int i, k, Num;
if ( pNtk->vOnehots == NULL )
return NULL;
// set register numbers
Abc_NtkForEachLatch( pNtk, pObj, i )
pObj->pNext = (Abc_Obj_t *)i;
// add the numbers
vResult = Vec_PtrAlloc( Vec_PtrSize(pNtk->vOnehots) );
Vec_PtrForEachEntry( pNtk->vOnehots, vNames, i )
{
vNumbers = Vec_IntAlloc( Vec_PtrSize(vNames) );
Vec_PtrForEachEntry( vNames, pName, k )
{
Num = Nm_ManFindIdByName( pNtk->pManName, pName, ABC_OBJ_BO );
if ( Num < 0 )
continue;
pObj = Abc_NtkObj( pNtk, Num );
if ( Abc_ObjFaninNum(pObj) != 1 || !Abc_ObjIsLatch(Abc_ObjFanin0(pObj)) )
continue;
Vec_IntPush( vNumbers, (int)pObj->pNext );
}
if ( Vec_IntSize( vNumbers ) > 1 )
{
Vec_PtrPush( vResult, vNumbers );
printf( "Converted %d one-hot registers.\n", Vec_IntSize(vNumbers) );
}
else
Vec_IntFree( vNumbers );
}
// clean the numbers
Abc_NtkForEachLatch( pNtk, pObj, i )
pObj->pNext = NULL;
return vResult;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///

6
src/base/abc/abcNtk.c
View File

@ -125,6 +125,8 @@ Abc_Ntk_t * Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_
// transfer the names
// Abc_NtkTrasferNames( pNtk, pNtkNew );
Abc_ManTimeDup( pNtk, pNtkNew );
if ( pNtk->vOnehots )
pNtkNew->vOnehots = (Vec_Ptr_t *)Vec_VecDupInt( (Vec_Vec_t *)pNtk->vOnehots );
// check that the CI/CO/latches are copied correctly
assert( Abc_NtkCiNum(pNtk) == Abc_NtkCiNum(pNtkNew) );
assert( Abc_NtkCoNum(pNtk) == Abc_NtkCoNum(pNtkNew) );
@ -520,7 +522,7 @@ Abc_Ntk_t * Abc_NtkCreateCone( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, char * pNode
int i, k;
assert( Abc_NtkIsLogic(pNtk) || Abc_NtkIsStrash(pNtk) );
assert( Abc_ObjIsNode(pNode) );
assert( Abc_ObjIsNode(pNode) || (Abc_NtkIsStrash(pNtk) && Abc_AigNodeIsConst(pNode)) );
// start the network
pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 );
@ -1032,6 +1034,8 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
FREE( pNtk->pName );
FREE( pNtk->pSpec );
FREE( pNtk->pLutTimes );
if ( pNtk->vOnehots )
Vec_VecFree( (Vec_Vec_t *)pNtk->vOnehots );
free( pNtk );
}

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

@ -685,7 +685,7 @@ int Abc_CommandPrintLatch( Abc_Frame_t * pAbc, int argc, char ** argv )
pErr = Abc_FrameReadErr(pAbc);
// set defaults
fPrintSccs = 1;
fPrintSccs = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "sh" ) ) != EOF )
{
@ -736,17 +736,22 @@ int Abc_CommandPrintFanio( Abc_Frame_t * pAbc, int argc, char ** argv )
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk;
int c;
int fVerbose;
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
{
switch ( c )
{
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
@ -761,12 +766,16 @@ int Abc_CommandPrintFanio( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// print the nodes
Abc_NtkPrintFanio( pOut, pNtk );
if ( fVerbose )
Abc_NtkPrintFanio( pOut, pNtk );
else
Abc_NtkPrintFanioNew( pOut, pNtk );
return 0;
usage:
fprintf( pErr, "usage: print_fanio [-h]\n" );
fprintf( pErr, "usage: print_fanio [-vh]\n" );
fprintf( pErr, "\t prints the statistics about fanins/fanouts of all nodes\n" );
fprintf( pErr, "\t-v : toggles verbose way of printing the stats [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
@ -2066,10 +2075,12 @@ int Abc_CommandStrash( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk, * pNtkRes;
Abc_Obj_t * pObj;
int c;
int fAllNodes;
int fRecord;
int fCleanup;
int fComplOuts;
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
@ -2079,8 +2090,9 @@ int Abc_CommandStrash( Abc_Frame_t * pAbc, int argc, char ** argv )
fAllNodes = 0;
fCleanup = 1;
fRecord = 0;
fComplOuts= 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "acrh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "acrih" ) ) != EOF )
{
switch ( c )
{
@ -2093,6 +2105,9 @@ int Abc_CommandStrash( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'r':
fRecord ^= 1;
break;
case 'i':
fComplOuts ^= 1;
break;
case 'h':
goto usage;
default:
@ -2113,16 +2128,20 @@ int Abc_CommandStrash( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Strashing has failed.\n" );
return 1;
}
if ( fComplOuts )
Abc_NtkForEachCo( pNtkRes, pObj, c )
Abc_ObjXorFaninC( pObj, 0 );
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
return 0;
usage:
fprintf( pErr, "usage: strash [-acrh]\n" );
fprintf( pErr, "usage: strash [-acrih]\n" );
fprintf( pErr, "\t transforms combinational logic into an AIG\n" );
fprintf( pErr, "\t-a : toggles between using all nodes and DFS nodes [default = %s]\n", fAllNodes? "all": "DFS" );
fprintf( pErr, "\t-c : toggles cleanup to remove the dagling AIG nodes [default = %s]\n", fCleanup? "all": "DFS" );
fprintf( pErr, "\t-r : enables using the record of AIG subgraphs [default = %s]\n", fRecord? "yes": "no" );
fprintf( pErr, "\t-r : toggles using the record of AIG subgraphs [default = %s]\n", fRecord? "yes": "no" );
fprintf( pErr, "\t-i : toggles complementing the COs of the AIG [default = %s]\n", fComplOuts? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
@ -3281,20 +3300,21 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
pErr = Abc_FrameReadErr(pAbc);
// set defaults
pPars->nWinTfoLevs = 2;
pPars->nFanoutsMax = 10;
pPars->nDepthMax = 20;
pPars->nDivMax = 250;
pPars->nWinSizeMax = 300;
pPars->nGrowthLevel = 0;
pPars->fResub = 1;
pPars->fArea = 0;
pPars->fMoreEffort = 0;
pPars->fSwapEdge = 0;
pPars->fVerbose = 0;
pPars->fVeryVerbose = 0;
pPars->nWinTfoLevs = 2;
pPars->nFanoutsMax = 10;
pPars->nDepthMax = 20;
pPars->nDivMax = 250;
pPars->nWinSizeMax = 300;
pPars->nGrowthLevel = 0;
pPars->nBTLimit =10000;
pPars->fResub = 1;
pPars->fArea = 0;
pPars->fMoreEffort = 0;
pPars->fSwapEdge = 0;
pPars->fVerbose = 0;
pPars->fVeryVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLraesvwh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLCraesvwh" ) ) != EOF )
{
switch ( c )
{
@ -3353,6 +3373,17 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nGrowthLevel < 0 || pPars->nGrowthLevel > ABC_INFINITY )
goto usage;
break;
case 'C':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
goto usage;
}
pPars->nBTLimit = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nBTLimit < 0 )
goto usage;
break;
case 'r':
pPars->fResub ^= 1;
break;
@ -3398,13 +3429,14 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
fprintf( pErr, "usage: mfs [-WFDML <num>] [-raesvh]\n" );
fprintf( pErr, "usage: mfs [-WFDMLC <num>] [-raesvh]\n" );
fprintf( pErr, "\t performs don't-care-based optimization of logic networks\n" );
fprintf( pErr, "\t-W <num> : the number of levels in the TFO cone (0 <= num) [default = %d]\n", pPars->nWinTfoLevs );
fprintf( pErr, "\t-F <num> : the max number of fanouts to skip (1 <= num) [default = %d]\n", pPars->nFanoutsMax );
fprintf( pErr, "\t-D <num> : the max depth nodes to try (0 = no limit) [default = %d]\n", pPars->nDepthMax );
fprintf( pErr, "\t-M <num> : the max node count of windows to consider (0 = no limit) [default = %d]\n", pPars->nWinSizeMax );
fprintf( pErr, "\t-L <num> : the max increase in node level after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel );
fprintf( pErr, "\t-C <num> : the max number of conflicts in one SAT run (0 = no limit) [default = %d]\n", pPars->nBTLimit );
fprintf( pErr, "\t-r : toggle resubstitution and dc-minimization [default = %s]\n", pPars->fResub? "resub": "dc-min" );
fprintf( pErr, "\t-a : toggle minimizing area or area+edges [default = %s]\n", pPars->fArea? "area": "area+edges" );
fprintf( pErr, "\t-e : toggle high-effort resubstitution [default = %s]\n", pPars->fMoreEffort? "yes": "no" );
@ -4423,6 +4455,7 @@ int Abc_CommandMiter( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
int fCheck;
int fComb;
int fImplic;
int nPartSize;
pNtk = Abc_FrameReadNtk(pAbc);
@ -4432,9 +4465,10 @@ int Abc_CommandMiter( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
fComb = 1;
fCheck = 1;
fImplic = 0;
nPartSize = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Pch" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "Pcih" ) ) != EOF )
{
switch ( c )
{
@ -4452,6 +4486,9 @@ int Abc_CommandMiter( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'c':
fComb ^= 1;
break;
case 'i':
fImplic ^= 1;
break;
default:
goto usage;
}
@ -4463,7 +4500,7 @@ int Abc_CommandMiter( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
// compute the miter
pNtkRes = Abc_NtkMiter( pNtk1, pNtk2, fComb, nPartSize );
pNtkRes = Abc_NtkMiter( pNtk1, pNtk2, fComb, nPartSize, fImplic );
if ( fDelete1 ) Abc_NtkDelete( pNtk1 );
if ( fDelete2 ) Abc_NtkDelete( pNtk2 );
@ -4482,10 +4519,11 @@ usage:
strcpy( Buffer, "unused" );
else
sprintf( Buffer, "%d", nPartSize );
fprintf( pErr, "usage: miter [-P num] [-ch] <file1> <file2>\n" );
fprintf( pErr, "usage: miter [-P num] [-cih] <file1> <file2>\n" );
fprintf( pErr, "\t computes the miter of the two circuits\n" );
fprintf( pErr, "\t-P num : output partition size [default = %s]\n", Buffer );
fprintf( pErr, "\t-c : computes combinational miter (latches as POs) [default = %s]\n", fComb? "yes": "no" );
fprintf( pErr, "\t-c : toggles deriving combinational miter (latches as POs) [default = %s]\n", fComb? "yes": "no" );
fprintf( pErr, "\t-i : toggles deriving implication miter (file1 => file2) [default = %s]\n", fImplic? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
fprintf( pErr, "\tfile1 : (optional) the file with the first network\n");
fprintf( pErr, "\tfile2 : (optional) the file with the second network\n");

72
src/base/abci/abcDar.c
View File

@ -85,7 +85,7 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters )
printf( "Warning: %d registers in this network have don't-care init values.\n", nDontCares );
printf( "The don't-care are assumed to be 0. The result may not verify.\n" );
printf( "Use command \"print_latch\" to see the init values of registers.\n" );
printf( "Use command \"init\" to change the values.\n" );
printf( "Use command \"zero\" to convert or \"init\" to change the values.\n" );
}
}
// create the manager
@ -97,6 +97,9 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters )
pMan->nRegs = Abc_NtkLatchNum(pNtk);
pMan->vFlopNums = Vec_IntStartNatural( pMan->nRegs );
// pMan->vFlopNums = NULL;
// pMan->vOnehots = Abc_NtkConverLatchNamesIntoNumbers( pNtk );
if ( pNtk->vOnehots )
pMan->vOnehots = (Vec_Ptr_t *)Vec_VecDupInt( (Vec_Vec_t *)pNtk->vOnehots );
}
// transfer the pointers to the basic nodes
Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Aig_ManConst1(pMan);
@ -974,7 +977,7 @@ int Abc_NtkDarCec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fPartition, int fVe
if ( pNtk2 != NULL )
{
// get the miter of the two networks
pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0 );
pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0, 0 );
if ( pMiter == NULL )
{
printf( "Miter computation has failed.\n" );
@ -1224,7 +1227,7 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fRetim
int RetValue;
// get the miter of the two networks
pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0 );
pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0, 0 );
if ( pMiter == NULL )
{
printf( "Miter computation has failed.\n" );
@ -1525,7 +1528,7 @@ Abc_Ntk_t * Abc_NtkDarEnlarge( Abc_Ntk_t * pNtk, int nFrames, int fVerbose )
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkInter( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbose )
Abc_Ntk_t * Abc_NtkInterOne( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbose )
{
extern Aig_Man_t * Aig_ManInter( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fVerbose );
Abc_Ntk_t * pNtkAig;
@ -1562,6 +1565,67 @@ Abc_Ntk_t * Abc_NtkInter( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbose
return pNtkAig;
}
/**Function*************************************************************
Synopsis [Interplates two networks.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkInter( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbose )
{
Abc_Ntk_t * pNtkOn1, * pNtkOff1, * pNtkInter1, * pNtkInter;
Abc_Obj_t * pObj;
int i;
if ( Abc_NtkCoNum(pNtkOn) != Abc_NtkCoNum(pNtkOff) )
{
printf( "Currently works only for networks with equal number of POs.\n" );
return NULL;
}
if ( Abc_NtkCoNum(pNtkOn) == 1 )
return Abc_NtkInterOne( pNtkOn, pNtkOff, fVerbose );
// start the new newtork
pNtkInter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
pNtkInter->pName = Extra_UtilStrsav(pNtkOn->pName);
Abc_NtkForEachPi( pNtkOn, pObj, i )
Abc_NtkDupObj( pNtkInter, pObj, 1 );
// process each POs separately
Abc_NtkForEachCo( pNtkOn, pObj, i )
{
pNtkOn1 = Abc_NtkCreateCone( pNtkOn, Abc_ObjFanin0(pObj), Abc_ObjName(pObj), 1 );
if ( Abc_ObjFaninC0(pObj) )
Abc_ObjXorFaninC( Abc_NtkPo(pNtkOn1, 0), 0 );
pObj = Abc_NtkCo(pNtkOff, i);
pNtkOff1 = Abc_NtkCreateCone( pNtkOff, Abc_ObjFanin0(pObj), Abc_ObjName(pObj), 1 );
if ( Abc_ObjFaninC0(pObj) )
Abc_ObjXorFaninC( Abc_NtkPo(pNtkOff1, 0), 0 );
if ( Abc_NtkNodeNum(pNtkOn1) == 0 )
pNtkInter1 = Abc_NtkDup( pNtkOn1 );
else if ( Abc_NtkNodeNum(pNtkOff1) == 0 )
{
pNtkInter1 = Abc_NtkDup( pNtkOff1 );
Abc_ObjXorFaninC( Abc_NtkPo(pNtkInter1, 0), 0 );
}
else
pNtkInter1 = Abc_NtkInterOne( pNtkOn1, pNtkOff1, fVerbose );
Abc_NtkAppend( pNtkInter, pNtkInter1, 1 );
Abc_NtkDelete( pNtkOn1 );
Abc_NtkDelete( pNtkOff1 );
Abc_NtkDelete( pNtkInter1 );
}
// return the network
if ( !Abc_NtkCheck( pNtkInter ) )
fprintf( stdout, "Abc_NtkAttachBottom(): Network check has failed.\n" );
return pNtkInter;
}
/**Function*************************************************************
Synopsis [Interplates two networks.]

60
src/base/abci/abcGen.c
View File

@ -1,12 +1,12 @@
/**CFile****************************************************************
FileName [abc_.c]
FileName [abcGen.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Network and node package.]
Synopsis []
Synopsis [Procedures to generate various type of circuits.]
Author [Alan Mishchenko]
@ -14,7 +14,7 @@
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: abc_.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
Revision [$Id: abcGen.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
@ -545,6 +545,60 @@ void Abc_GenOneHot( char * pFileName, int nVars )
fclose( pFile );
}
/**Function*************************************************************
Synopsis [Generates structure of L K-LUTs implementing an N-var function.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_GenOneHotIntervals( char * pFileName, int nPis, int nRegs, Vec_Ptr_t * vOnehots )
{
Vec_Int_t * vLine;
FILE * pFile;
int i, j, k, iReg1, iReg2, Counter, Counter2, nDigitsIn, nDigitsOut;
pFile = fopen( pFileName, "w" );
fprintf( pFile, "# One-hotness with %d vars and %d regs generated by ABC on %s\n", nPis, nRegs, Extra_TimeStamp() );
fprintf( pFile, "# Used %d intervals of 1-hot registers: { ", Vec_PtrSize(vOnehots) );
Counter = 0;
Vec_PtrForEachEntry( vOnehots, vLine, k )
{
fprintf( pFile, "%d ", Vec_IntSize(vLine) );
Counter += Vec_IntSize(vLine) * (Vec_IntSize(vLine) - 1) / 2;
}
fprintf( pFile, "}\n" );
fprintf( pFile, ".model 1hot_%dvars_%dregs\n", nPis, nRegs );
fprintf( pFile, ".inputs" );
nDigitsIn = Extra_Base10Log( nPis+nRegs );
for ( i = 0; i < nPis+nRegs; i++ )
fprintf( pFile, " i%0*d", nDigitsIn, i );
fprintf( pFile, "\n" );
fprintf( pFile, ".outputs" );
nDigitsOut = Extra_Base10Log( Counter );
for ( i = 0; i < Counter; i++ )
fprintf( pFile, " o%0*d", nDigitsOut, i );
fprintf( pFile, "\n" );
Counter2 = 0;
Vec_PtrForEachEntry( vOnehots, vLine, k )
{
Vec_IntForEachEntry( vLine, iReg1, i )
Vec_IntForEachEntryStart( vLine, iReg2, j, i+1 )
{
fprintf( pFile, ".names i%0*d i%0*d o%0*d\n", nDigitsIn, nPis+iReg1, nDigitsIn, nPis+iReg2, nDigitsOut, Counter2 );
fprintf( pFile, "11 0\n" );
Counter2++;
}
}
assert( Counter == Counter2 );
fprintf( pFile, ".end\n" );
fprintf( pFile, "\n" );
fclose( pFile );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///

18
src/base/abci/abcMiter.c
View File

@ -24,10 +24,10 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, int nPartSize );
static Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, int nPartSize, int fImplic );
static void Abc_NtkMiterPrepare( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb, int nPartSize );
static void Abc_NtkMiterAddOne( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter );
static void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb, int nPartSize );
static void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb, int nPartSize, int fImplic );
static void Abc_NtkAddFrame( Abc_Ntk_t * pNetNew, Abc_Ntk_t * pNet, int iFrame );
// to be exported
@ -50,7 +50,7 @@ static void Abc_NtkAddFrame2( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, i
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, int nPartSize )
Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, int nPartSize, int fImplic )
{
Abc_Ntk_t * pTemp = NULL;
int fRemove1, fRemove2;
@ -63,7 +63,7 @@ Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, int n
fRemove1 = (!Abc_NtkIsStrash(pNtk1)) && (pNtk1 = Abc_NtkStrash(pNtk1, 0, 0, 0));
fRemove2 = (!Abc_NtkIsStrash(pNtk2)) && (pNtk2 = Abc_NtkStrash(pNtk2, 0, 0, 0));
if ( pNtk1 && pNtk2 )
pTemp = Abc_NtkMiterInt( pNtk1, pNtk2, fComb, nPartSize );
pTemp = Abc_NtkMiterInt( pNtk1, pNtk2, fComb, nPartSize, fImplic );
if ( fRemove1 ) Abc_NtkDelete( pNtk1 );
if ( fRemove2 ) Abc_NtkDelete( pNtk2 );
return pTemp;
@ -80,7 +80,7 @@ Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, int n
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, int nPartSize )
Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, int nPartSize, int fImplic )
{
char Buffer[1000];
Abc_Ntk_t * pNtkMiter;
@ -97,7 +97,7 @@ Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, in
Abc_NtkMiterPrepare( pNtk1, pNtk2, pNtkMiter, fComb, nPartSize );
Abc_NtkMiterAddOne( pNtk1, pNtkMiter );
Abc_NtkMiterAddOne( pNtk2, pNtkMiter );
Abc_NtkMiterFinalize( pNtk1, pNtk2, pNtkMiter, fComb, nPartSize );
Abc_NtkMiterFinalize( pNtk1, pNtk2, pNtkMiter, fComb, nPartSize, fImplic );
Abc_AigCleanup(pNtkMiter->pManFunc);
// make sure that everything is okay
@ -250,7 +250,7 @@ void Abc_NtkMiterAddCone( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter, Abc_Obj_t * p
SeeAlso []
***********************************************************************/
void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb, int nPartSize )
void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb, int nPartSize, int fImplic )
{
Vec_Ptr_t * vPairs;
Abc_Obj_t * pMiter, * pNode;
@ -285,7 +285,7 @@ void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNt
// add the miter
if ( nPartSize <= 0 )
{
pMiter = Abc_AigMiter( pNtkMiter->pManFunc, vPairs );
pMiter = Abc_AigMiter( pNtkMiter->pManFunc, vPairs, fImplic );
Abc_ObjAddFanin( Abc_NtkPo(pNtkMiter,0), pMiter );
Vec_PtrFree( vPairs );
}
@ -309,7 +309,7 @@ void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNt
Vec_PtrPush( vPairsPart, Vec_PtrEntry(vPairs, 2*iCur ) );
Vec_PtrPush( vPairsPart, Vec_PtrEntry(vPairs, 2*iCur+1) );
}
pMiter = Abc_AigMiter( pNtkMiter->pManFunc, vPairsPart );
pMiter = Abc_AigMiter( pNtkMiter->pManFunc, vPairsPart, fImplic );
pNode = Abc_NtkCreatePo( pNtkMiter );
Abc_ObjAddFanin( pNode, pMiter );
// assign the name to the node

112
src/base/abci/abcPrint.c
View File

@ -468,6 +468,118 @@ void Abc_NtkPrintFanio( FILE * pFile, Abc_Ntk_t * pNtk )
Vec_IntFree( vFanins );
Vec_IntFree( vFanouts );
}
/**Function*************************************************************
Synopsis [Prints the distribution of fanins/fanouts in the network.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkPrintFanioNew( FILE * pFile, Abc_Ntk_t * pNtk )
{
char Buffer[100];
Abc_Obj_t * pNode;
Vec_Int_t * vFanins, * vFanouts;
int nFanins, nFanouts, nFaninsMax, nFanoutsMax, nFaninsAll, nFanoutsAll;
int i, k, nSizeMax;
// determine the largest fanin and fanout
nFaninsMax = nFanoutsMax = 0;
nFaninsAll = nFanoutsAll = 0;
Abc_NtkForEachNode( pNtk, pNode, i )
{
nFanins = Abc_ObjFaninNum(pNode);
if ( Abc_NtkIsNetlist(pNtk) )
nFanouts = Abc_ObjFanoutNum( Abc_ObjFanout0(pNode) );
else
nFanouts = Abc_ObjFanoutNum(pNode);
nFaninsAll += nFanins;
nFanoutsAll += nFanouts;
nFaninsMax = ABC_MAX( nFaninsMax, nFanins );
nFanoutsMax = ABC_MAX( nFanoutsMax, nFanouts );
}
// allocate storage for fanin/fanout numbers
nSizeMax = ABC_MAX( 10 * (Extra_Base10Log(nFaninsMax) + 1), 10 * (Extra_Base10Log(nFanoutsMax) + 1) );
vFanins = Vec_IntStart( nSizeMax );
vFanouts = Vec_IntStart( nSizeMax );
// count the number of fanins and fanouts
Abc_NtkForEachNode( pNtk, pNode, i )
{
nFanins = Abc_ObjFaninNum(pNode);
if ( Abc_NtkIsNetlist(pNtk) )
nFanouts = Abc_ObjFanoutNum( Abc_ObjFanout0(pNode) );
else
nFanouts = Abc_ObjFanoutNum(pNode);
// nFanouts = Abc_NodeMffcSize(pNode);
if ( nFanins < 10 )
Vec_IntAddToEntry( vFanins, nFanins, 1 );
else if ( nFanins < 100 )
Vec_IntAddToEntry( vFanins, 10 + nFanins/10, 1 );
else if ( nFanins < 1000 )
Vec_IntAddToEntry( vFanins, 20 + nFanins/100, 1 );
else if ( nFanins < 10000 )
Vec_IntAddToEntry( vFanins, 30 + nFanins/1000, 1 );
else if ( nFanins < 100000 )
Vec_IntAddToEntry( vFanins, 40 + nFanins/10000, 1 );
else if ( nFanins < 1000000 )
Vec_IntAddToEntry( vFanins, 50 + nFanins/100000, 1 );
else if ( nFanins < 10000000 )
Vec_IntAddToEntry( vFanins, 60 + nFanins/1000000, 1 );
if ( nFanouts < 10 )
Vec_IntAddToEntry( vFanouts, nFanouts, 1 );
else if ( nFanouts < 100 )
Vec_IntAddToEntry( vFanouts, 10 + nFanouts/10, 1 );
else if ( nFanouts < 1000 )
Vec_IntAddToEntry( vFanouts, 20 + nFanouts/100, 1 );
else if ( nFanouts < 10000 )
Vec_IntAddToEntry( vFanouts, 30 + nFanouts/1000, 1 );
else if ( nFanouts < 100000 )
Vec_IntAddToEntry( vFanouts, 40 + nFanouts/10000, 1 );
else if ( nFanouts < 1000000 )
Vec_IntAddToEntry( vFanouts, 50 + nFanouts/100000, 1 );
else if ( nFanouts < 10000000 )
Vec_IntAddToEntry( vFanouts, 60 + nFanouts/1000000, 1 );
}
fprintf( pFile, "The distribution of fanins and fanouts in the network:\n" );
fprintf( pFile, " Number Nodes with fanin Nodes with fanout\n" );
for ( k = 0; k < nSizeMax; k++ )
{
if ( vFanins->pArray[k] == 0 && vFanouts->pArray[k] == 0 )
continue;
if ( k < 10 )
fprintf( pFile, "%15d : ", k );
else
{
sprintf( Buffer, "%d - %d", (int)pow(10, k/10) * (k%10), (int)pow(10, k/10) * (k%10+1) - 1 );
fprintf( pFile, "%15s : ", Buffer );
}
if ( vFanins->pArray[k] == 0 )
fprintf( pFile, " " );
else
fprintf( pFile, "%12d ", vFanins->pArray[k] );
fprintf( pFile, " " );
if ( vFanouts->pArray[k] == 0 )
fprintf( pFile, " " );
else
fprintf( pFile, "%12d ", vFanouts->pArray[k] );
fprintf( pFile, "\n" );
}
Vec_IntFree( vFanins );
Vec_IntFree( vFanouts );
fprintf( pFile, "Fanins: Max = %d. Ave = %.2f. Fanouts: Max = %d. Ave = %.2f.\n",
nFaninsMax, 1.0*nFaninsAll/Abc_NtkNodeNum(pNtk),
nFanoutsMax, 1.0*nFanoutsAll/Abc_NtkNodeNum(pNtk) );
}
/**Function*************************************************************

2
src/base/abci/abcQuant.c
View File

@ -187,7 +187,7 @@ Abc_Ntk_t * Abc_NtkTransRel( Abc_Ntk_t * pNtk, int fInputs, int fVerbose )
Vec_PtrPush( vPairs, Abc_ObjChild0Copy(pObj) );
Vec_PtrPush( vPairs, Abc_NtkPi(pNtkNew, i+nLatches) );
}
pMiter = Abc_AigMiter( pNtkNew->pManFunc, vPairs );
pMiter = Abc_AigMiter( pNtkNew->pManFunc, vPairs, 0 );
Vec_PtrFree( vPairs );
// add the primary output
Abc_ObjAddFanin( Abc_NtkPo(pNtkNew,0), Abc_ObjNot(pMiter) );

2
src/base/abci/abcRr.c
View File

@ -354,7 +354,7 @@ int Abc_NtkRRProve( Abc_RRMan_t * p )
Abc_NtkRRUpdate( pWndCopy, p->pNode->pCopy->pCopy, p->pFanin->pCopy->pCopy, p->pFanout? p->pFanout->pCopy->pCopy : NULL );
if ( !Abc_NtkIsDfsOrdered(pWndCopy) )
Abc_NtkReassignIds(pWndCopy);
p->pMiter = Abc_NtkMiter( p->pWnd, pWndCopy, 1, 0 );
p->pMiter = Abc_NtkMiter( p->pWnd, pWndCopy, 1, 0, 0 );
Abc_NtkDelete( pWndCopy );
clk = clock();
RetValue = Abc_NtkMiterProve( &p->pMiter, p->pParams );

4
src/base/abci/abcStrash.c
View File

@ -260,7 +260,7 @@ int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fAddPos )
{
Abc_NtkDupObj( pNtk1, pObj, 0 );
Abc_ObjAddFanin( pObj->pCopy, Abc_ObjChild0Copy(pObj) );
Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(pObj->pCopy), NULL );
Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(pObj), NULL );
}
}
else
@ -271,6 +271,8 @@ int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fAddPos )
Abc_NtkForEachCo( pNtk2, pObj, i )
{
iNodeId = Nm_ManFindIdByNameTwoTypes( pNtk1->pManName, Abc_ObjName(pObj), ABC_OBJ_PO, ABC_OBJ_BI );
// if ( iNodeId < 0 )
// continue;
assert( iNodeId >= 0 );
pObjOld = Abc_NtkObj( pNtk1, iNodeId );
// derive the new driver

12
src/base/abci/abcVerify.c
View File

@ -52,7 +52,7 @@ void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI
int RetValue;
// get the miter of the two networks
pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, 0 );
pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, 0, 0 );
if ( pMiter == NULL )
{
printf( "Miter computation has failed.\n" );
@ -120,7 +120,7 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV
int RetValue;
// get the miter of the two networks
pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, 0 );
pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, 0, 0 );
if ( pMiter == NULL )
{
printf( "Miter computation has failed.\n" );
@ -225,7 +225,7 @@ void Abc_NtkCecFraigPart( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, in
assert( nPartSize > 0 );
// get the miter of the two networks
pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, nPartSize );
pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, nPartSize, 0 );
if ( pMiter == NULL )
{
printf( "Miter computation has failed.\n" );
@ -342,7 +342,7 @@ void Abc_NtkCecFraigPartAuto( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds
// pParams->fVerbose = 1;
// get the miter of the two networks
pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, 1 );
pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, 1, 0 );
if ( pMiter == NULL )
{
printf( "Miter computation has failed.\n" );
@ -456,7 +456,7 @@ void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI
int RetValue;
// get the miter of the two networks
pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0 );
pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0, 0 );
if ( pMiter == NULL )
{
printf( "Miter computation has failed.\n" );
@ -538,7 +538,7 @@ int Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFr
int RetValue;
// get the miter of the two networks
pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0 );
pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0, 0 );
if ( pMiter == NULL )
{
printf( "Miter computation has failed.\n" );

25
src/base/io/io.c
View File

@ -722,14 +722,19 @@ int IoCommandReadPla( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Ntk_t * pNtk;
char * pFileName;
int fCheck;
int fZeros;
int c;
fZeros = 0;
fCheck = 1;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "zch" ) ) != EOF )
{
switch ( c )
{
case 'z':
fZeros ^= 1;
break;
case 'c':
fCheck ^= 1;
break;
@ -744,7 +749,20 @@ int IoCommandReadPla( Abc_Frame_t * pAbc, int argc, char ** argv )
// get the input file name
pFileName = argv[globalUtilOptind];
// read the file using the corresponding file reader
pNtk = Io_Read( pFileName, IO_FILE_PLA, fCheck );
if ( fZeros )
{
Abc_Ntk_t * pTemp;
pNtk = Io_ReadPla( pFileName, fZeros, fCheck );
if ( pNtk == NULL )
{
printf( "Reading PLA file has failed.\n" );
return 1;
}
pNtk = Abc_NtkToLogic( pTemp = pNtk );
Abc_NtkDelete( pTemp );
}
else
pNtk = Io_Read( pFileName, IO_FILE_PLA, fCheck );
if ( pNtk == NULL )
return 1;
// replace the current network
@ -752,8 +770,9 @@ int IoCommandReadPla( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
fprintf( pAbc->Err, "usage: read_pla [-ch] <file>\n" );
fprintf( pAbc->Err, "usage: read_pla [-zch] <file>\n" );
fprintf( pAbc->Err, "\t read the network in PLA\n" );
fprintf( pAbc->Err, "\t-z : toggle reading on-set and off-set [default = %s]\n", fZeros? "off-set":"on-set" );
fprintf( pAbc->Err, "\t-c : toggle network check after reading [default = %s]\n", fCheck? "yes":"no" );
fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
fprintf( pAbc->Err, "\tfile : the name of a file to read\n" );

2
src/base/io/io.h
View File

@ -83,7 +83,7 @@ extern Abc_Ntk_t * Io_ReadEdif( char * pFileName, int fCheck );
/*=== abcReadEqn.c ============================================================*/
extern Abc_Ntk_t * Io_ReadEqn( char * pFileName, int fCheck );
/*=== abcReadPla.c ============================================================*/
extern Abc_Ntk_t * Io_ReadPla( char * pFileName, int fCheck );
extern Abc_Ntk_t * Io_ReadPla( char * pFileName, int fZeros, int fCheck );
/*=== abcReadVerilog.c ========================================================*/
extern Abc_Ntk_t * Io_ReadVerilog( char * pFileName, int fCheck );
/*=== abcWriteAiger.c =========================================================*/

99
src/base/io/ioReadBlifMv.c
View File

@ -49,6 +49,7 @@ struct Io_MvMod_t_
Vec_Ptr_t * vResets; // .reset lines
Vec_Ptr_t * vNames; // .names lines
Vec_Ptr_t * vSubckts; // .subckt lines
Vec_Ptr_t * vOnehots; // .onehot lines
Vec_Ptr_t * vMvs; // .mv lines
int fBlackBox; // indicates blackbox model
// the resulting network
@ -97,6 +98,7 @@ static int Io_MvParseLineInputs( Io_MvMod_t * p, char * pLine );
static int Io_MvParseLineOutputs( Io_MvMod_t * p, char * pLine );
static int Io_MvParseLineLatch( Io_MvMod_t * p, char * pLine );
static int Io_MvParseLineSubckt( Io_MvMod_t * p, char * pLine );
static Vec_Int_t * Io_MvParseLineOnehot( Io_MvMod_t * p, char * pLine );
static int Io_MvParseLineMv( Io_MvMod_t * p, char * pLine );
static int Io_MvParseLineNamesMv( Io_MvMod_t * p, char * pLine, int fReset );
static int Io_MvParseLineNamesBlif( Io_MvMod_t * p, char * pLine );
@ -295,6 +297,7 @@ static Io_MvMod_t * Io_MvModAlloc()
p->vResets = Vec_PtrAlloc( 512 );
p->vNames = Vec_PtrAlloc( 512 );
p->vSubckts = Vec_PtrAlloc( 512 );
p->vOnehots = Vec_PtrAlloc( 512 );
p->vMvs = Vec_PtrAlloc( 512 );
return p;
}
@ -320,6 +323,7 @@ static void Io_MvModFree( Io_MvMod_t * p )
Vec_PtrFree( p->vResets );
Vec_PtrFree( p->vNames );
Vec_PtrFree( p->vSubckts );
Vec_PtrFree( p->vOnehots );
Vec_PtrFree( p->vMvs );
free( p );
}
@ -597,6 +601,8 @@ static void Io_MvReadPreparse( Io_MvMan_t * p )
Vec_PtrPush( p->pLatest->vOutputs, pCur );
else if ( !strncmp(pCur, "subckt", 6) )
Vec_PtrPush( p->pLatest->vSubckts, pCur );
else if ( !strncmp(pCur, "onehot", 6) )
Vec_PtrPush( p->pLatest->vOnehots, pCur );
else if ( p->fBlifMv && !strncmp(pCur, "mv", 2) )
Vec_PtrPush( p->pLatest->vMvs, pCur );
else if ( !strncmp(pCur, "blackbox", 8) )
@ -743,6 +749,42 @@ static Abc_Lib_t * Io_MvParse( Io_MvMan_t * p )
return NULL;
// finalize the network
Abc_NtkFinalizeRead( pMod->pNtk );
// read the one-hotness lines
if ( Vec_PtrSize(pMod->vOnehots) > 0 )
{
Vec_Int_t * vLine;
Abc_Obj_t * pObj;
// set register numbers
Abc_NtkForEachLatch( pMod->pNtk, pObj, k )
pObj->pNext = (Abc_Obj_t *)k;
// derive register
pMod->pNtk->vOnehots = Vec_PtrAlloc( Vec_PtrSize(pMod->vOnehots) );
Vec_PtrForEachEntry( pMod->vOnehots, pLine, k )
{
vLine = Io_MvParseLineOnehot( pMod, pLine );
if ( vLine == NULL )
return NULL;
Vec_PtrPush( pMod->pNtk->vOnehots, vLine );
// printf( "Parsed %d one-hot registers.\n", Vec_IntSize(vLine) );
}
// reset register numbers
Abc_NtkForEachLatch( pMod->pNtk, pObj, k )
pObj->pNext = NULL;
// print the result
printf( "Parsed %d groups of 1-hot registers: { ", Vec_PtrSize(pMod->pNtk->vOnehots) );
Vec_PtrForEachEntry( pMod->pNtk->vOnehots, vLine, k )
printf( "%d ", Vec_IntSize(vLine) );
printf( "}\n" );
printf( "The total number of 1-hot registers = %d. (%.2f %%)\n",
Vec_VecSizeSize( (Vec_Vec_t *)pMod->pNtk->vOnehots ),
100.0 * Vec_VecSizeSize( (Vec_Vec_t *)pMod->pNtk->vOnehots ) / Abc_NtkLatchNum(pMod->pNtk) );
{
extern void Abc_GenOneHotIntervals( char * pFileName, int nPis, int nRegs, Vec_Ptr_t * vOnehots );
char * pFileName = Extra_FileNameGenericAppend( pMod->pMan->pFileName, "_1h.blif" );
Abc_GenOneHotIntervals( pFileName, Abc_NtkPiNum(pMod->pNtk), Abc_NtkLatchNum(pMod->pNtk), pMod->pNtk->vOnehots );
printf( "One-hotness condition is written into file \"%s\".\n", pFileName );
}
}
}
if ( p->nNDnodes )
// printf( "Warning: The parser added %d PIs to replace non-deterministic nodes.\n", p->nNDnodes );
@ -995,6 +1037,63 @@ static int Io_MvParseLineSubckt( Io_MvMod_t * p, char * pLine )
return 1;
}
/**Function*************************************************************
Synopsis [Parses the subckt line.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static Vec_Int_t * Io_MvParseLineOnehot( Io_MvMod_t * p, char * pLine )
{
Vec_Ptr_t * vTokens = p->pMan->vTokens;
// Vec_Ptr_t * vResult;
Vec_Int_t * vResult;
Abc_Obj_t * pNet, * pTerm;
char * pToken;
int nEquals, i;
// split the line into tokens
nEquals = Io_MvCountChars( pLine, '=' );
Io_MvSplitIntoTokensAndClear( vTokens, pLine, '\0', '=' );
pToken = Vec_PtrEntry(vTokens,0);
assert( !strcmp(pToken, "onehot") );
// iterate through the register names
// vResult = Vec_PtrAlloc( Vec_PtrSize(vTokens) );
vResult = Vec_IntAlloc( Vec_PtrSize(vTokens) );
Vec_PtrForEachEntryStart( vTokens, pToken, i, 1 )
{
// check if this register exists
pNet = Abc_NtkFindNet( p->pNtk, pToken );
if ( pNet == NULL )
{
sprintf( p->pMan->sError, "Line %d: Signal with name \"%s\" does not exist in the model \"%s\".",
Io_MvGetLine(p->pMan, pToken), pToken, Abc_NtkName(p->pNtk) );
return NULL;
}
// check if this is register output net
pTerm = Abc_ObjFanin0( pNet );
if ( pTerm == NULL || Abc_ObjFanin0(pTerm) == NULL || !Abc_ObjIsLatch(Abc_ObjFanin0(pTerm)) )
{
sprintf( p->pMan->sError, "Line %d: Signal with name \"%s\" is not a register in the model \"%s\".",
Io_MvGetLine(p->pMan, pToken), pToken, Abc_NtkName(p->pNtk) );
return NULL;
}
// save register name
// Vec_PtrPush( vResult, Abc_ObjName(pNet) );
Vec_IntPush( vResult, (int)Abc_ObjFanin0(pTerm)->pNext );
// printf( "%d(%d) ", (int)Abc_ObjFanin0(pTerm)->pNext, ((int)Abc_ObjFanin0(pTerm)->pData) -1 );
printf( "%d", ((int)Abc_ObjFanin0(pTerm)->pData)-1 );
}
printf( "\n" );
return vResult;
}
/**Function*************************************************************

30
src/base/io/ioReadPla.c
View File

@ -24,7 +24,7 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p );
static Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p, int fZeros );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@ -41,7 +41,7 @@ static Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p );
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Io_ReadPla( char * pFileName, int fCheck )
Abc_Ntk_t * Io_ReadPla( char * pFileName, int fZeros, int fCheck )
{
Extra_FileReader_t * p;
Abc_Ntk_t * pNtk;
@ -52,7 +52,7 @@ Abc_Ntk_t * Io_ReadPla( char * pFileName, int fCheck )
return NULL;
// read the network
pNtk = Io_ReadPlaNetwork( p );
pNtk = Io_ReadPlaNetwork( p, fZeros );
Extra_FileReaderFree( p );
if ( pNtk == NULL )
return NULL;
@ -77,7 +77,7 @@ Abc_Ntk_t * Io_ReadPla( char * pFileName, int fCheck )
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p )
Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p, int fZeros )
{
ProgressBar * pProgress;
Vec_Ptr_t * vTokens;
@ -205,12 +205,26 @@ Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p )
Abc_NtkDelete( pNtk );
return NULL;
}
for ( i = 0; i < nOutputs; i++ )
if ( fZeros )
{
if ( pCubeOut[i] == '1' )
for ( i = 0; i < nOutputs; i++ )
{
Vec_StrAppend( ppSops[i], pCubeIn );
Vec_StrAppend( ppSops[i], " 1\n" );
if ( pCubeOut[i] == '0' )
{
Vec_StrAppend( ppSops[i], pCubeIn );
Vec_StrAppend( ppSops[i], " 1\n" );
}
}
}
else
{
for ( i = 0; i < nOutputs; i++ )
{
if ( pCubeOut[i] == '1' )
{
Vec_StrAppend( ppSops[i], pCubeIn );
Vec_StrAppend( ppSops[i], " 1\n" );
}
}
}
nCubes++;

2
src/base/io/ioUtil.c
View File

@ -134,7 +134,7 @@ Abc_Ntk_t * Io_ReadNetlist( char * pFileName, Io_FileType_t FileType, int fCheck
else if ( FileType == IO_FILE_EQN )
pNtk = Io_ReadEqn( pFileName, fCheck );
else if ( FileType == IO_FILE_PLA )
pNtk = Io_ReadPla( pFileName, fCheck );
pNtk = Io_ReadPla( pFileName, 0, fCheck );
else if ( FileType == IO_FILE_VERILOG )
pNtk = Io_ReadVerilog( pFileName, fCheck );
else

2
src/base/main/mainUtils.c
View File

@ -21,7 +21,7 @@
#include "mainInt.h"
#ifndef _WIN32
#include "readline/readline.h"
#include <readline/readline.h>
#endif
////////////////////////////////////////////////////////////////////////

8
src/bdd/dsd/dsd.h
View File

@ -63,10 +63,10 @@ enum Dsd_Type_t_ {
////////////////////////////////////////////////////////////////////////
// complementation and testing for pointers for decomposition entries
#define Dsd_IsComplement(p) (((int)((unsigned long) (p) & 01)))
#define Dsd_Regular(p) ((Dsd_Node_t *)((unsigned long)(p) & ~01))
#define Dsd_Not(p) ((Dsd_Node_t *)((unsigned long)(p) ^ 01))
#define Dsd_NotCond(p,c) ((Dsd_Node_t *)((unsigned long)(p) ^ (c)))
#define Dsd_IsComplement(p) (((int)((PORT_PTRUINT_T) (p) & 01)))
#define Dsd_Regular(p) ((Dsd_Node_t *)((PORT_PTRUINT_T)(p) & ~01))
#define Dsd_Not(p) ((Dsd_Node_t *)((PORT_PTRUINT_T)(p) ^ 01))
#define Dsd_NotCond(p,c) ((Dsd_Node_t *)((PORT_PTRUINT_T)(p) ^ (c)))
////////////////////////////////////////////////////////////////////////
/// ITERATORS ///

6
src/bdd/reo/reo.h
View File

@ -171,9 +171,9 @@ struct _reo_man
};
// used to manipulate units
#define Unit_Regular(u) ((reo_unit *)((unsigned long)(u) & ~01))
#define Unit_Not(u) ((reo_unit *)((unsigned long)(u) ^ 01))
#define Unit_NotCond(u,c) ((reo_unit *)((unsigned long)(u) ^ (c)))
#define Unit_Regular(u) ((reo_unit *)((PORT_PTRUINT_T)(u) & ~01))
#define Unit_Not(u) ((reo_unit *)((PORT_PTRUINT_T)(u) ^ 01))
#define Unit_NotCond(u,c) ((reo_unit *)((PORT_PTRUINT_T)(u) ^ (c)))
#define Unit_IsConstant(u) ((int)((u)->lev == REO_CONST_LEVEL))
////////////////////////////////////////////////////////////////////////

8
src/map/fpga/fpga.h
View File

@ -52,10 +52,10 @@ typedef struct Fpga_LutLibStruct_t_ Fpga_LutLib_t;
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
#define Fpga_IsComplement(p) (((int)((unsigned long) (p) & 01)))
#define Fpga_Regular(p) ((Fpga_Node_t *)((unsigned long)(p) & ~01))
#define Fpga_Not(p) ((Fpga_Node_t *)((unsigned long)(p) ^ 01))
#define Fpga_NotCond(p,c) ((Fpga_Node_t *)((unsigned long)(p) ^ (c)))
#define Fpga_IsComplement(p) (((int)((PORT_PTRUINT_T) (p) & 01)))
#define Fpga_Regular(p) ((Fpga_Node_t *)((PORT_PTRUINT_T)(p) & ~01))
#define Fpga_Not(p) ((Fpga_Node_t *)((PORT_PTRUINT_T)(p) ^ 01))
#define Fpga_NotCond(p,c) ((Fpga_Node_t *)((PORT_PTRUINT_T)(p) ^ (c)))
#define Fpga_Ref(p)
#define Fpga_Deref(p)

3
src/map/fpga/fpgaInt.h
View File

@ -88,9 +88,6 @@
// generating random unsigned (#define RAND_MAX 0x7fff)
#define FPGA_RANDOM_UNSIGNED ((((unsigned)rand()) << 24) ^ (((unsigned)rand()) << 12) ^ ((unsigned)rand()))
// outputs the runtime in seconds
#define PRT(a,t) printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC))
////////////////////////////////////////////////////////////////////////
/// STRUCTURE DEFINITIONS ///
////////////////////////////////////////////////////////////////////////

11
src/map/if/if.h
View File

@ -221,10 +221,10 @@ struct If_Obj_t_
If_Cut_t CutBest; // the best cut selected
};
static inline If_Obj_t * If_Regular( If_Obj_t * p ) { return (If_Obj_t *)((unsigned long)(p) & ~01); }
static inline If_Obj_t * If_Not( If_Obj_t * p ) { return (If_Obj_t *)((unsigned long)(p) ^ 01); }
static inline If_Obj_t * If_NotCond( If_Obj_t * p, int c ) { return (If_Obj_t *)((unsigned long)(p) ^ (c)); }
static inline int If_IsComplement( If_Obj_t * p ) { return (int )(((unsigned long)p) & 01); }
static inline If_Obj_t * If_Regular( If_Obj_t * p ) { return (If_Obj_t *)((PORT_PTRUINT_T)(p) & ~01); }
static inline If_Obj_t * If_Not( If_Obj_t * p ) { return (If_Obj_t *)((PORT_PTRUINT_T)(p) ^ 01); }
static inline If_Obj_t * If_NotCond( If_Obj_t * p, int c ) { return (If_Obj_t *)((PORT_PTRUINT_T)(p) ^ (c)); }
static inline int If_IsComplement( If_Obj_t * p ) { return (int )(((PORT_PTRUINT_T)p) & 01); }
static inline int If_ManCiNum( If_Man_t * p ) { return p->nObjs[IF_CI]; }
static inline int If_ManCoNum( If_Man_t * p ) { return p->nObjs[IF_CO]; }
@ -399,6 +399,9 @@ extern Vec_Ptr_t * If_ManReverseOrder( If_Man_t * p );
extern void If_ManMarkMapping( If_Man_t * p );
extern Vec_Ptr_t * If_ManCollectMappingDirect( If_Man_t * p );
extern int If_ManCountSpecialPos( If_Man_t * p );
#ifdef __cplusplus
}

1
src/map/if/ifCore.c
View File

@ -138,6 +138,7 @@ int If_ManPerformMappingComb( If_Man_t * p )
}
// printf( "Cross cut memory = %d.\n", Mem_FixedReadMaxEntriesUsed(p->pMemSet) );
s_MappingTime = clock() - clkTotal;
// printf( "Special POs = %d.\n", If_ManCountSpecialPos(p) );
return 1;
}

32
src/map/if/ifUtil.c
View File

@ -651,6 +651,38 @@ Vec_Ptr_t * If_ManCollectMappingDirect( If_Man_t * p )
return vOrder;
}
/**Function*************************************************************
Synopsis [Returns the number of POs pointing to the same internal nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int If_ManCountSpecialPos( If_Man_t * p )
{
If_Obj_t * pObj;
int i, Counter = 0;
// clean all marks
If_ManForEachPo( p, pObj, i )
If_ObjFanin0(pObj)->fMark = 0;
// label nodes
If_ManForEachPo( p, pObj, i )
if ( !If_ObjFaninC0(pObj) )
If_ObjFanin0(pObj)->fMark = 1;
// label nodes
If_ManForEachPo( p, pObj, i )
if ( If_ObjFaninC0(pObj) )
Counter += If_ObjFanin0(pObj)->fMark;
// clean all marks
If_ManForEachPo( p, pObj, i )
If_ObjFanin0(pObj)->fMark = 0;
return Counter;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

8
src/map/mapper/mapper.h
View File

@ -63,10 +63,10 @@ struct Map_TimeStruct_t_
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
#define Map_IsComplement(p) (((int)((unsigned long) (p) & 01)))
#define Map_Regular(p) ((Map_Node_t *)((unsigned long)(p) & ~01))
#define Map_Not(p) ((Map_Node_t *)((unsigned long)(p) ^ 01))
#define Map_NotCond(p,c) ((Map_Node_t *)((unsigned long)(p) ^ (c)))
#define Map_IsComplement(p) (((int)((PORT_PTRUINT_T) (p) & 01)))
#define Map_Regular(p) ((Map_Node_t *)((PORT_PTRUINT_T)(p) & ~01))
#define Map_Not(p) ((Map_Node_t *)((PORT_PTRUINT_T)(p) ^ 01))
#define Map_NotCond(p,c) ((Map_Node_t *)((PORT_PTRUINT_T)(p) ^ (c)))
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///

8
src/map/mapper/mapperInt.h
View File

@ -61,10 +61,10 @@
#define MAP_RANDOM_UNSIGNED ((((unsigned)rand()) << 24) ^ (((unsigned)rand()) << 12) ^ ((unsigned)rand()))
// internal macros to work with cuts
#define Map_CutIsComplement(p) (((int)((unsigned long) (p) & 01)))
#define Map_CutRegular(p) ((Map_Cut_t *)((unsigned long)(p) & ~01))
#define Map_CutNot(p) ((Map_Cut_t *)((unsigned long)(p) ^ 01))
#define Map_CutNotCond(p,c) ((Map_Cut_t *)((unsigned long)(p) ^ (c)))
#define Map_CutIsComplement(p) (((int)((PORT_PTRUINT_T) (p) & 01)))
#define Map_CutRegular(p) ((Map_Cut_t *)((PORT_PTRUINT_T)(p) & ~01))
#define Map_CutNot(p) ((Map_Cut_t *)((PORT_PTRUINT_T)(p) ^ 01))
#define Map_CutNotCond(p,c) ((Map_Cut_t *)((PORT_PTRUINT_T)(p) ^ (c)))
// internal macros for referencing of nodes
#define Map_NodeReadRef(p) ((Map_Regular(p))->nRefs)

8
src/map/super/superAnd.c
View File

@ -61,10 +61,10 @@ struct Super2_GateStruct_t_
// manipulation of complemented attributes
#define Super2_IsComplement(p) (((int)((unsigned long) (p) & 01)))
#define Super2_Regular(p) ((Super2_Gate_t *)((unsigned long)(p) & ~01))
#define Super2_Not(p) ((Super2_Gate_t *)((unsigned long)(p) ^ 01))
#define Super2_NotCond(p,c) ((Super2_Gate_t *)((unsigned long)(p) ^ (c)))
#define Super2_IsComplement(p) (((int)((PORT_PTRUINT_T) (p) & 01)))
#define Super2_Regular(p) ((Super2_Gate_t *)((PORT_PTRUINT_T)(p) & ~01))
#define Super2_Not(p) ((Super2_Gate_t *)((PORT_PTRUINT_T)(p) ^ 01))
#define Super2_NotCond(p,c) ((Super2_Gate_t *)((PORT_PTRUINT_T)(p) ^ (c)))
// iterating through the gates in the library
#define Super2_LibForEachGate( Lib, Gate ) \

2
src/misc/extra/extra.h
View File

@ -52,6 +52,7 @@ extern "C" {
#include <time.h>
#include "st.h"
#include "cuddInt.h"
#include "port_type.h"
/*---------------------------------------------------------------------------*/
/* Constant declarations */
@ -314,6 +315,7 @@ extern char * Extra_FileGetSimilarName( char * pFileNameWrong, char * pS1,
extern char * Extra_FileNameExtension( char * FileName );
extern char * Extra_FileNameAppend( char * pBase, char * pSuffix );
extern char * Extra_FileNameGeneric( char * FileName );
extern char * Extra_FileNameGenericAppend( char * pBase, char * pSuffix );
extern int Extra_FileSize( char * pFileName );
extern char * Extra_FileRead( FILE * pFile );
extern char * Extra_TimeStamp();

23
src/misc/extra/extraUtilFile.c
View File

@ -177,6 +177,29 @@ char * Extra_FileNameGeneric( char * FileName )
return pRes;
}
/**Function*************************************************************
Synopsis [Returns the composite name of the file.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
char * Extra_FileNameGenericAppend( char * pBase, char * pSuffix )
{
static char Buffer[1000];
char * pDot;
strcpy( Buffer, pBase );
pDot = strstr( Buffer, "." );
if ( pDot )
*pDot = 0;
strcat( Buffer, pSuffix );
return Buffer;
}
/**Function*************************************************************
Synopsis [Returns the file size.]

5
src/misc/st/st.c
View File

@ -10,6 +10,7 @@
#include <stdio.h>
#include <stdlib.h>
#include "st.h"
#include "port_type.h"
#ifndef ABS
# define ABS(a) ((a) < 0 ? -(a) : (a))
@ -31,8 +32,8 @@
#define ST_NUMCMP(x,y) ((x) != (y))
#define ST_NUMHASH(x,size) (ABS((long)x)%(size))
//#define ST_PTRHASH(x,size) ((int)((unsigned long)(x)>>2)%size) // 64-bit bug fix 9/17/2007
#define ST_PTRHASH(x,size) ((int)(((unsigned long)(x)>>2)%size))
//#define ST_PTRHASH(x,size) ((int)((PORT_PTRUINT_T)(x)>>2)%size) // 64-bit bug fix 9/17/2007
#define ST_PTRHASH(x,size) ((int)(((PORT_PTRUINT_T)(x)>>2)%size))
#define EQUAL(func, x, y) \
((((func) == st_numcmp) || ((func) == st_ptrcmp)) ?\
(ST_NUMCMP((x),(y)) == 0) : ((*func)((x), (y)) == 0))

5
src/misc/st/stmm.c
View File

@ -10,6 +10,7 @@
#include <stdio.h>
#include "extra.h"
#include "stmm.h"
#include "port_type.h"
#ifndef ABS
# define ABS(a) ((a) < 0 ? -(a) : (a))
@ -17,8 +18,8 @@
#define STMM_NUMCMP(x,y) ((x) != (y))
#define STMM_NUMHASH(x,size) (ABS((long)x)%(size))
//#define STMM_PTRHASH(x,size) ((int)((unsigned long)(x)>>2)%size) // 64-bit bug fix 9/17/2007
#define STMM_PTRHASH(x,size) ((int)(((unsigned long)(x)>>2)%size))
//#define STMM_PTRHASH(x,size) ((int)((PORT_PTRUINT_T)(x)>>2)%size) // 64-bit bug fix 9/17/2007
#define STMM_PTRHASH(x,size) ((int)(((PORT_PTRUINT_T)(x)>>2)%size))
#define EQUAL(func, x, y) \
((((func) == stmm_numcmp) || ((func) == stmm_ptrcmp)) ?\
(STMM_NUMCMP((x),(y)) == 0) : ((*func)((x), (y)) == 0))

5
src/misc/vec/vec.h
View File

@ -83,11 +83,11 @@ typedef long long sint64;
#endif
#ifndef PRT
#define PRT(a,t) printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC))
#define PRT(a,t) printf("%s = ", (a)); printf("%7.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC))
#endif
#ifndef PRTP
#define PRTP(a,t,T) printf("%s = ", (a)); printf("%6.2f sec (%6.2f %%)\n", (float)(t)/(float)(CLOCKS_PER_SEC), (T)? 100.0*(t)/(T) : 0.0)
#define PRTP(a,t,T) printf("%s = ", (a)); printf("%7.2f sec (%6.2f %%)\n", (float)(t)/(float)(CLOCKS_PER_SEC), (T)? 100.0*(t)/(T) : 0.0)
#endif
#include "vecInt.h"
@ -96,6 +96,7 @@ typedef long long sint64;
#include "vecPtr.h"
#include "vecVec.h"
#include "vecAtt.h"
#include "port_type.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///

42
src/misc/vec/vecVec.h
View File

@ -205,6 +205,48 @@ static inline void Vec_VecFree( Vec_Vec_t * p )
Vec_PtrFree( (Vec_Ptr_t *)p );
}
/**Function*************************************************************
Synopsis [Frees the vector.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Vec_Vec_t * Vec_VecDupPtr( Vec_Vec_t * p )
{
Vec_Ptr_t * vNew, * vVec;
int i;
vNew = Vec_PtrAlloc( Vec_VecSize(p) );
Vec_VecForEachLevel( p, vVec, i )
Vec_PtrPush( vNew, Vec_PtrDup(vVec) );
return (Vec_Vec_t *)vNew;
}
/**Function*************************************************************
Synopsis [Frees the vector.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Vec_Vec_t * Vec_VecDupInt( Vec_Vec_t * p )
{
Vec_Ptr_t * vNew, * vVec;
int i;
vNew = Vec_PtrAlloc( Vec_VecSize(p) );
Vec_VecForEachLevel( p, vVec, i )
Vec_PtrPush( vNew, Vec_IntDup((Vec_Int_t *)vVec) );
return (Vec_Vec_t *)vNew;
}
/**Function*************************************************************
Synopsis [Frees the vector of vectors.]

1
src/opt/mfs/mfs.h
View File

@ -47,6 +47,7 @@ struct Mfs_Par_t_
int nDivMax; // the maximum number of divisors
int nWinSizeMax; // the maximum size of the window
int nGrowthLevel; // the maximum allowed growth in level
int nBTLimit; // the maximum number of conflicts in one SAT run
int fResub; // performs resubstitution
int fArea; // performs optimization for area
int fMoreEffort; // performs high-affort minimization

1
src/opt/mfs/mfsInt.h
View File

@ -84,6 +84,7 @@ struct Mfs_Man_t_
int nMintsTotal;
int nNodesBad;
int nTotalDivs;
int nTimeOuts;
// node/edge stats
int nTotalNodesBeg;
int nTotalNodesEnd;

4
src/opt/mfs/mfsInter.c
View File

@ -226,10 +226,10 @@ Hop_Obj_t * Abc_NtkMfsInterplate( Mfs_Man_t * p, int * pCands, int nCands )
pSat = Abc_MfsCreateSolverResub( p, pCands, nCands );
// solve the problem
status = sat_solver_solve( pSat, NULL, NULL, (sint64)0, (sint64)0, (sint64)0, (sint64)0 );
status = sat_solver_solve( pSat, NULL, NULL, (sint64)p->pPars->nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
if ( status != l_False )
{
printf( "Abc_NtkMfsInterplate(): Internal error. The problem is not UNSAT.\n" );
p->nTimeOuts++;
return NULL;
}
// get the learned clauses

4
src/opt/mfs/mfsMan.c
View File

@ -115,8 +115,8 @@ void Mfs_ManPrint( Mfs_Man_t * p )
p->nTotalEdgesBeg-p->nTotalEdgesEnd,
100.0*(p->nTotalEdgesBeg-p->nTotalEdgesEnd)/p->nTotalEdgesBeg );
printf( "\n" );
printf( "Nodes = %d. Tried = %d. Resub = %d. Divs = %d. SAT calls = %d.\n",
Abc_NtkNodeNum(p->pNtk), p->nNodesTried, p->nNodesResub, p->nTotalDivs, p->nSatCalls );
printf( "Nodes = %d. Try = %d. Resub = %d. Div = %d. SAT calls = %d. Timeouts = %d.\n",
Abc_NtkNodeNum(p->pNtk), p->nNodesTried, p->nNodesResub, p->nTotalDivs, p->nSatCalls, p->nTimeOuts );
if ( p->pPars->fSwapEdge )
printf( "Swappable edges = %d. Total edges = %d. Ratio = %5.2f.\n",
p->nNodesResub, Abc_NtkGetTotalFanins(p->pNtk), 1.00 * p->nNodesResub / Abc_NtkGetTotalFanins(p->pNtk) );

41
src/opt/mfs/mfsResub.c
View File

@ -100,10 +100,15 @@ int Abc_NtkMfsTryResubOnce( Mfs_Man_t * p, int * pCands, int nCands )
unsigned * pData;
int RetValue, iVar, i;
p->nSatCalls++;
RetValue = sat_solver_solve( p->pSat, pCands, pCands + nCands, (sint64)0, (sint64)0, (sint64)0, (sint64)0 );
assert( RetValue == l_False || RetValue == l_True );
RetValue = sat_solver_solve( p->pSat, pCands, pCands + nCands, (sint64)p->pPars->nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
// assert( RetValue == l_False || RetValue == l_True );
if ( RetValue == l_False )
return 1;
if ( RetValue != l_True )
{
p->nTimeOuts++;
return -1;
}
p->nSatCexes++;
// store the counter-example
Vec_IntForEachEntry( p->vProjVars, iVar, i )
@ -135,7 +140,7 @@ int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int f
int fVeryVerbose = p->pPars->fVeryVerbose && Vec_PtrSize(p->vDivs) < 80;
unsigned * pData;
int pCands[MFS_FANIN_MAX];
int iVar, i, nCands, nWords, w, clk;
int RetValue, iVar, i, nCands, nWords, w, clk;
Abc_Obj_t * pFanin;
Hop_Obj_t * pFunc;
assert( iFanin >= 0 );
@ -163,7 +168,10 @@ int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int f
iVar = Vec_PtrSize(p->vDivs) - Abc_ObjFaninNum(pNode) + i;
pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVars, iVar ), 1 );
}
if ( Abc_NtkMfsTryResubOnce( p, pCands, nCands ) )
RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands );
if ( RetValue == -1 )
return 0;
if ( RetValue == 1 )
{
if ( fVeryVerbose )
printf( "Node %d: Fanin %d can be removed.\n", pNode->Id, iFanin );
@ -173,6 +181,8 @@ int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int f
clk = clock();
// derive the function
pFunc = Abc_NtkMfsInterplate( p, pCands, nCands );
if ( pFunc == NULL )
return 0;
// update the network
Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc );
p->timeInt += clock() - clk;
@ -225,7 +235,10 @@ p->timeInt += clock() - clk;
return 0;
pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVars, iVar), 1 );
if ( Abc_NtkMfsTryResubOnce( p, pCands, nCands+1 ) )
RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands+1 );
if ( RetValue == -1 )
return 0;
if ( RetValue == 1 )
{
if ( fVeryVerbose )
printf( "Node %d: Fanin %d can be replaced by divisor %d.\n", pNode->Id, iFanin, iVar );
@ -235,6 +248,8 @@ p->timeInt += clock() - clk;
clk = clock();
// derive the function
pFunc = Abc_NtkMfsInterplate( p, pCands, nCands+1 );
if ( pFunc == NULL )
return 0;
// update the network
Vec_PtrPush( p->vFanins, Vec_PtrEntry(p->vDivs, iVar) );
Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc );
@ -263,7 +278,7 @@ int Abc_NtkMfsSolveSatResub2( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int
int fVeryVerbose = p->pPars->fVeryVerbose && Vec_PtrSize(p->vDivs) < 80;
unsigned * pData, * pData2;
int pCands[MFS_FANIN_MAX];
int iVar, iVar2, i, w, nCands, clk, nWords, fBreak;
int RetValue, iVar, iVar2, i, w, nCands, clk, nWords, fBreak;
Abc_Obj_t * pFanin;
Hop_Obj_t * pFunc;
assert( iFanin >= 0 );
@ -292,7 +307,10 @@ int Abc_NtkMfsSolveSatResub2( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int
iVar = Vec_PtrSize(p->vDivs) - Abc_ObjFaninNum(pNode) + i;
pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVars, iVar ), 1 );
}
if ( Abc_NtkMfsTryResubOnce( p, pCands, nCands ) )
RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands );
if ( RetValue == -1 )
return 0;
if ( RetValue == 1 )
{
if ( fVeryVerbose )
printf( "Node %d: Fanins %d/%d can be removed.\n", pNode->Id, iFanin, iFanin2 );
@ -300,6 +318,8 @@ int Abc_NtkMfsSolveSatResub2( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int
clk = clock();
// derive the function
pFunc = Abc_NtkMfsInterplate( p, pCands, nCands );
if ( pFunc == NULL )
return 0;
// update the network
Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc );
p->timeInt += clock() - clk;
@ -360,7 +380,10 @@ p->timeInt += clock() - clk;
pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVars, iVar2), 1 );
pCands[nCands+1] = toLitCond( Vec_IntEntry(p->vProjVars, iVar), 1 );
if ( Abc_NtkMfsTryResubOnce( p, pCands, nCands+2 ) )
RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands+2 );
if ( RetValue == -1 )
return 0;
if ( RetValue == 1 )
{
if ( fVeryVerbose )
printf( "Node %d: Fanins %d/%d can be replaced by divisors %d/%d.\n", pNode->Id, iFanin, iFanin2, iVar, iVar2 );
@ -368,6 +391,8 @@ p->timeInt += clock() - clk;
clk = clock();
// derive the function
pFunc = Abc_NtkMfsInterplate( p, pCands, nCands+2 );
if ( pFunc == NULL )
return 0;
// update the network
Vec_PtrPush( p->vFanins, Vec_PtrEntry(p->vDivs, iVar2) );
Vec_PtrPush( p->vFanins, Vec_PtrEntry(p->vDivs, iVar) );

2
src/opt/res/resStrash.c
View File

@ -89,7 +89,7 @@ Abc_Ntk_t * Res_WndStrash( Res_Win_t * p )
Vec_PtrForEachEntry( p->vRoots, pObj, i )
Vec_PtrWriteEntry( vPairs, 2 * i + 1, pObj->pCopy );
// add the miter
pMiter = Abc_AigMiter( pAig->pManFunc, vPairs );
pMiter = Abc_AigMiter( pAig->pManFunc, vPairs, 0 );
Abc_ObjAddFanin( Abc_NtkCreatePo(pAig), pMiter );
Vec_PtrFree( vPairs );
// add the node

8
src/opt/rwr/rwr.h
View File

@ -111,10 +111,10 @@ struct Rwr_Node_t_ // 24 bytes
};
// manipulation of complemented attributes
static inline bool Rwr_IsComplement( Rwr_Node_t * p ) { return (bool)(((unsigned long)p) & 01); }
static inline Rwr_Node_t * Rwr_Regular( Rwr_Node_t * p ) { return (Rwr_Node_t *)((unsigned long)(p) & ~01); }
static inline Rwr_Node_t * Rwr_Not( Rwr_Node_t * p ) { return (Rwr_Node_t *)((unsigned long)(p) ^ 01); }
static inline Rwr_Node_t * Rwr_NotCond( Rwr_Node_t * p, int c ) { return (Rwr_Node_t *)((unsigned long)(p) ^ (c)); }
static inline bool Rwr_IsComplement( Rwr_Node_t * p ) { return (bool)(((PORT_PTRUINT_T)p) & 01); }
static inline Rwr_Node_t * Rwr_Regular( Rwr_Node_t * p ) { return (Rwr_Node_t *)((PORT_PTRUINT_T)(p) & ~01); }
static inline Rwr_Node_t * Rwr_Not( Rwr_Node_t * p ) { return (Rwr_Node_t *)((PORT_PTRUINT_T)(p) ^ 01); }
static inline Rwr_Node_t * Rwr_NotCond( Rwr_Node_t * p, int c ) { return (Rwr_Node_t *)((PORT_PTRUINT_T)(p) ^ (c)); }
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///

9
src/sat/bsat/satSolver.c
View File

@ -25,6 +25,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#include <math.h>
#include "satSolver.h"
#include "port_type.h"
//#define SAT_USE_SYSTEM_MEMORY_MANAGEMENT
@ -90,9 +91,9 @@ static inline void clause_setactivity(clause* c, float a) { *((float*)&c->lits[
//=================================================================================================
// Encode literals in clause pointers:
static inline clause* clause_from_lit (lit l) { return (clause*)((unsigned long)l + (unsigned long)l + 1); }
static inline bool clause_is_lit (clause* c) { return ((unsigned long)c & 1); }
static inline lit clause_read_lit (clause* c) { return (lit)((unsigned long)c >> 1); }
static inline clause* clause_from_lit (lit l) { return (clause*)((PORT_PTRUINT_T)l + (PORT_PTRUINT_T)l + 1); }
static inline bool clause_is_lit (clause* c) { return ((PORT_PTRUINT_T)c & 1); }
static inline lit clause_read_lit (clause* c) { return (lit)((PORT_PTRUINT_T)c >> 1); }
//=================================================================================================
// Simple helpers:
@ -285,7 +286,7 @@ static clause* clause_new(sat_solver* s, lit* begin, lit* end, int learnt)
#endif
c->size_learnt = (size << 1) | learnt;
assert(((unsigned long)c & 1) == 0);
assert(((PORT_PTRUINT_T)c & 1) == 0);
for (i = 0; i < size; i++)
c->lits[i] = begin[i];

8
src/sat/fraig/fraig.h
View File

@ -113,10 +113,10 @@ struct Prove_ParamsStruct_t_
////////////////////////////////////////////////////////////////////////
// macros working with complemented attributes of the nodes
#define Fraig_IsComplement(p) (((int)((unsigned long) (p) & 01)))
#define Fraig_Regular(p) ((Fraig_Node_t *)((unsigned long)(p) & ~01))
#define Fraig_Not(p) ((Fraig_Node_t *)((unsigned long)(p) ^ 01))
#define Fraig_NotCond(p,c) ((Fraig_Node_t *)((unsigned long)(p) ^ (c)))
#define Fraig_IsComplement(p) (((int)((PORT_PTRUINT_T) (p) & 01)))
#define Fraig_Regular(p) ((Fraig_Node_t *)((PORT_PTRUINT_T)(p) & ~01))
#define Fraig_Not(p) ((Fraig_Node_t *)((PORT_PTRUINT_T)(p) ^ 01))
#define Fraig_NotCond(p,c) ((Fraig_Node_t *)((PORT_PTRUINT_T)(p) ^ (c)))
// these are currently not used
#define Fraig_Ref(p)

1
src/sat/fraig/fraigInt.h
View File

@ -32,6 +32,7 @@
#include "fraig.h"
#include "msat.h"
#include "port_type.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///