diff options
58 files changed, 995 insertions, 177 deletions
diff --git a/regtest_output.txt b/regtest_output.txt index 6e0ffec3..45fc6ff8 100644 --- a/regtest_output.txt +++ b/regtest_output.txt @@ -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>
\ No newline at end of file +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>
\ No newline at end of file diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h index 744a044e..bd77c0a4 100644 --- a/src/aig/aig/aig.h +++ b/src/aig/aig/aig.h @@ -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 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 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_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 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 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_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 ); diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c index 57032703..12f2e702 100644 --- a/src/aig/aig/aigMan.c +++ b/src/aig/aig/aigMan.c @@ -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 ); diff --git a/src/aig/aig/aigPartReg.c b/src/aig/aig/aigPartReg.c index 88ae66ee..3a008d12 100644 --- a/src/aig/aig/aigPartReg.c +++ b/src/aig/aig/aigPartReg.c @@ -230,6 +230,67 @@ void Aig_ManRegPartitionAdd( Aig_ManPre_t * p, int iReg ) /**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.] Description [] @@ -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 ) diff --git a/src/aig/bdc/bdcInt.h b/src/aig/bdc/bdcInt.h index 9649f870..5f7b1186 100644 --- a/src/aig/bdc/bdcInt.h +++ b/src/aig/bdc/bdcInt.h @@ -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 ); } diff --git a/src/aig/dar/darCore.c b/src/aig/dar/darCore.c index 141d9b79..b13c7313 100644 --- a/src/aig/dar/darCore.c +++ b/src/aig/dar/darCore.c @@ -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; diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h index cc64b024..48588eb2 100644 --- a/src/aig/fra/fra.h +++ b/src/aig/fra/fra.h @@ -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 ); diff --git a/src/aig/fra/fraHot.c b/src/aig/fra/fraHot.c index 4a3f9b03..222f5bcc 100644 --- a/src/aig/fra/fraHot.c +++ b/src/aig/fra/fraHot.c @@ -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 /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c index 0715524e..7e0d080c 100644 --- a/src/aig/fra/fraInd.c +++ b/src/aig/fra/fraInd.c @@ -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 ) diff --git a/src/aig/hop/hop.h b/src/aig/hop/hop.h index af1d9cd3..6390ff70 100644 --- a/src/aig/hop/hop.h +++ b/src/aig/hop/hop.h @@ -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; } diff --git a/src/aig/ivy/ivy.h b/src/aig/ivy/ivy.h index c7435a63..9832e061 100644 --- a/src/aig/ivy/ivy.h +++ b/src/aig/ivy/ivy.h @@ -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; } diff --git a/src/aig/rwt/rwt.h b/src/aig/rwt/rwt.h index 9199ff2a..56f66f34 100644 --- a/src/aig/rwt/rwt.h +++ b/src/aig/rwt/rwt.h @@ -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 /// diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index 86cc7e62..1d5195c7 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -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 ); diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c index 89026863..3cc4d59c 100644 --- a/src/base/abc/abcAig.c +++ b/src/base/abc/abcAig.c @@ -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 ); } diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c index 778581c2..4c6a7fb0 100644 --- a/src/base/abc/abcDfs.c +++ b/src/base/abc/abcDfs.c @@ -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]); diff --git a/src/base/abc/abcLatch.c b/src/base/abc/abcLatch.c index d96bbfac..4529d9f3 100644 --- a/src/base/abc/abcLatch.c +++ b/src/base/abc/abcLatch.c @@ -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 /// diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c index 5c565ce6..1e88859c 100644 --- a/src/base/abc/abcNtk.c +++ b/src/base/abc/abcNtk.c @@ -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 ); } diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 99da9201..11ef85f9 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -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"); diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 6f5138c8..d69a7097 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -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; @@ -1573,6 +1576,67 @@ Abc_Ntk_t * Abc_NtkInter( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbose 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.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ void Abc_NtkPrintSccs( Abc_Ntk_t * pNtk, int fVerbose ) { // extern Vec_Ptr_t * Aig_ManRegPartitionLinear( Aig_Man_t * pAig, int nPartSize ); diff --git a/src/base/abci/abcGen.c b/src/base/abci/abcGen.c index 0b66c476..7c18ca2c 100644 --- a/src/base/abci/abcGen.c +++ b/src/base/abci/abcGen.c @@ -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 /// diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c index a054a474..3e3c9580 100644 --- a/src/base/abci/abcMiter.c +++ b/src/base/abci/abcMiter.c @@ -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 diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c index 239b155c..e5f028fe 100644 --- a/src/base/abci/abcPrint.c +++ b/src/base/abci/abcPrint.c @@ -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************************************************************* diff --git a/src/base/abci/abcQuant.c b/src/base/abci/abcQuant.c index 0f2bd72f..24981d1c 100644 --- a/src/base/abci/abcQuant.c +++ b/src/base/abci/abcQuant.c @@ -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) ); diff --git a/src/base/abci/abcRr.c b/src/base/abci/abcRr.c index 92adc718..80d234f1 100644 --- a/src/base/abci/abcRr.c +++ b/src/base/abci/abcRr.c @@ -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 ); diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c index c77f8dea..744d9c95 100644 --- a/src/base/abci/abcStrash.c +++ b/src/base/abci/abcStrash.c @@ -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 diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c index 9c9bbcfd..1d72a767 100644 --- a/src/base/abci/abcVerify.c +++ b/src/base/abci/abcVerify.c @@ -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" ); diff --git a/src/base/io/io.c b/src/base/io/io.c index fe88a285..628ef2b9 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -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" ); diff --git a/src/base/io/io.h b/src/base/io/io.h index 126de332..eea76efe 100644 --- a/src/base/io/io.h +++ b/src/base/io/io.h @@ -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 =========================================================*/ diff --git a/src/base/io/ioReadBlifMv.c b/src/base/io/ioReadBlifMv.c index 8a1fe309..84378024 100644 --- a/src/base/io/ioReadBlifMv.c +++ b/src/base/io/ioReadBlifMv.c @@ -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************************************************************* diff --git a/src/base/io/ioReadPla.c b/src/base/io/ioReadPla.c index fdfdb4f6..288c3704 100644 --- a/src/base/io/ioReadPla.c +++ b/src/base/io/ioReadPla.c @@ -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++ ) + { + if ( pCubeOut[i] == '0' ) + { + Vec_StrAppend( ppSops[i], pCubeIn ); + Vec_StrAppend( ppSops[i], " 1\n" ); + } + } + } + else + { + for ( i = 0; i < nOutputs; i++ ) { - Vec_StrAppend( ppSops[i], pCubeIn ); - Vec_StrAppend( ppSops[i], " 1\n" ); + if ( pCubeOut[i] == '1' ) + { + Vec_StrAppend( ppSops[i], pCubeIn ); + Vec_StrAppend( ppSops[i], " 1\n" ); + } } } nCubes++; diff --git a/src/base/io/ioUtil.c b/src/base/io/ioUtil.c index 4f9f2e9f..51a00274 100644 --- a/src/base/io/ioUtil.c +++ b/src/base/io/ioUtil.c @@ -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 diff --git a/src/base/main/mainUtils.c b/src/base/main/mainUtils.c index 58cc33ec..1f090cf4 100644 --- a/src/base/main/mainUtils.c +++ b/src/base/main/mainUtils.c @@ -21,7 +21,7 @@ #include "mainInt.h" #ifndef _WIN32 -#include "readline/readline.h" +#include <readline/readline.h> #endif //////////////////////////////////////////////////////////////////////// diff --git a/src/bdd/dsd/dsd.h b/src/bdd/dsd/dsd.h index b73b81ab..4a16bfc1 100644 --- a/src/bdd/dsd/dsd.h +++ b/src/bdd/dsd/dsd.h @@ -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 /// diff --git a/src/bdd/reo/reo.h b/src/bdd/reo/reo.h index 1a31242a..24e12c32 100644 --- a/src/bdd/reo/reo.h +++ b/src/bdd/reo/reo.h @@ -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)) //////////////////////////////////////////////////////////////////////// diff --git a/src/map/fpga/fpga.h b/src/map/fpga/fpga.h index 708cf385..b2ca4882 100644 --- a/src/map/fpga/fpga.h +++ b/src/map/fpga/fpga.h @@ -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) diff --git a/src/map/fpga/fpgaInt.h b/src/map/fpga/fpgaInt.h index c01d1e3d..be790a55 100644 --- a/src/map/fpga/fpgaInt.h +++ b/src/map/fpga/fpgaInt.h @@ -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 /// //////////////////////////////////////////////////////////////////////// diff --git a/src/map/if/if.h b/src/map/if/if.h index 19222f3b..acda5d51 100644 --- a/src/map/if/if.h +++ b/src/map/if/if.h @@ -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 } diff --git a/src/map/if/ifCore.c b/src/map/if/ifCore.c index f7124703..16a14153 100644 --- a/src/map/if/ifCore.c +++ b/src/map/if/ifCore.c @@ -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; } diff --git a/src/map/if/ifUtil.c b/src/map/if/ifUtil.c index 2624efd0..c114236d 100644 --- a/src/map/if/ifUtil.c +++ b/src/map/if/ifUtil.c @@ -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 /// //////////////////////////////////////////////////////////////////////// diff --git a/src/map/mapper/mapper.h b/src/map/mapper/mapper.h index 8eade761..673f7538 100644 --- a/src/map/mapper/mapper.h +++ b/src/map/mapper/mapper.h @@ -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 /// diff --git a/src/map/mapper/mapperInt.h b/src/map/mapper/mapperInt.h index 37cca3d3..541077d5 100644 --- a/src/map/mapper/mapperInt.h +++ b/src/map/mapper/mapperInt.h @@ -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) diff --git a/src/map/super/superAnd.c b/src/map/super/superAnd.c index 52473fba..26235a0e 100644 --- a/src/map/super/superAnd.c +++ b/src/map/super/superAnd.c @@ -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 ) \ diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h index 314257a2..dc2aac28 100644 --- a/src/misc/extra/extra.h +++ b/src/misc/extra/extra.h @@ -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(); diff --git a/src/misc/extra/extraUtilFile.c b/src/misc/extra/extraUtilFile.c index 4c51b8b5..243f3457 100644 --- a/src/misc/extra/extraUtilFile.c +++ b/src/misc/extra/extraUtilFile.c @@ -179,6 +179,29 @@ char * Extra_FileNameGeneric( char * FileName ) /**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.] Description [The file should be closed.] diff --git a/src/misc/st/st.c b/src/misc/st/st.c index 872fe51b..2798ae99 100644 --- a/src/misc/st/st.c +++ b/src/misc/st/st.c @@ -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)) diff --git a/src/misc/st/stmm.c b/src/misc/st/stmm.c index 8dfacfe4..7a52c1cd 100644 --- a/src/misc/st/stmm.c +++ b/src/misc/st/stmm.c @@ -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)) diff --git a/src/misc/vec/vec.h b/src/misc/vec/vec.h index a4bd4771..4091ac7f 100644 --- a/src/misc/vec/vec.h +++ b/src/misc/vec/vec.h @@ -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 /// diff --git a/src/misc/vec/vecVec.h b/src/misc/vec/vecVec.h index 55ffdf4f..13880c21 100644 --- a/src/misc/vec/vecVec.h +++ b/src/misc/vec/vecVec.h @@ -207,6 +207,48 @@ static inline void Vec_VecFree( Vec_Vec_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.] Description [] diff --git a/src/opt/mfs/mfs.h b/src/opt/mfs/mfs.h index cb2da431..d3f7277d 100644 --- a/src/opt/mfs/mfs.h +++ b/src/opt/mfs/mfs.h @@ -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 diff --git a/src/opt/mfs/mfsInt.h b/src/opt/mfs/mfsInt.h index 3c0349bb..f98f6239 100644 --- a/src/opt/mfs/mfsInt.h +++ b/src/opt/mfs/mfsInt.h @@ -84,6 +84,7 @@ struct Mfs_Man_t_ int nMintsTotal; int nNodesBad; int nTotalDivs; + int nTimeOuts; // node/edge stats int nTotalNodesBeg; int nTotalNodesEnd; diff --git a/src/opt/mfs/mfsInter.c b/src/opt/mfs/mfsInter.c index 65acd4eb..24617cd9 100644 --- a/src/opt/mfs/mfsInter.c +++ b/src/opt/mfs/mfsInter.c @@ -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 diff --git a/src/opt/mfs/mfsMan.c b/src/opt/mfs/mfsMan.c index 421f62af..99a60ef6 100644 --- a/src/opt/mfs/mfsMan.c +++ b/src/opt/mfs/mfsMan.c @@ -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) ); diff --git a/src/opt/mfs/mfsResub.c b/src/opt/mfs/mfsResub.c index 4171c111..8908da2f 100644 --- a/src/opt/mfs/mfsResub.c +++ b/src/opt/mfs/mfsResub.c @@ -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) ); diff --git a/src/opt/res/resStrash.c b/src/opt/res/resStrash.c index fde842a4..a75b84cc 100644 --- a/src/opt/res/resStrash.c +++ b/src/opt/res/resStrash.c @@ -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 diff --git a/src/opt/rwr/rwr.h b/src/opt/rwr/rwr.h index f24f9535..64e916e2 100644 --- a/src/opt/rwr/rwr.h +++ b/src/opt/rwr/rwr.h @@ -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 /// diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index 8a13d203..a04921c9 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -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]; diff --git a/src/sat/fraig/fraig.h b/src/sat/fraig/fraig.h index 1dad21e2..c08e7e3a 100644 --- a/src/sat/fraig/fraig.h +++ b/src/sat/fraig/fraig.h @@ -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) diff --git a/src/sat/fraig/fraigInt.h b/src/sat/fraig/fraigInt.h index 9c6e0d47..dc7bc815 100644 --- a/src/sat/fraig/fraigInt.h +++ b/src/sat/fraig/fraigInt.h @@ -32,6 +32,7 @@ #include "fraig.h" #include "msat.h" +#include "port_type.h" //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// |