diff options
author | Mathias Soeken <mathias.soeken@gmail.com> | 2017-02-22 19:00:28 -0800 |
---|---|---|
committer | Mathias Soeken <mathias.soeken@gmail.com> | 2017-02-22 19:00:28 -0800 |
commit | 28e8e7f3e79d1391a2f3a31cefe3afe234aa3b8e (patch) | |
tree | 6b7962dc72653e3bf615c5901854774eca9d23c8 /src/base/wlc | |
parent | 5af44731bff0061c724912cf76e86dddbb4f2c7a (diff) | |
parent | dd8cc7e9a27e2bd962d612911c6fd9508c6c1e0d (diff) | |
download | abc-28e8e7f3e79d1391a2f3a31cefe3afe234aa3b8e.tar.gz abc-28e8e7f3e79d1391a2f3a31cefe3afe234aa3b8e.tar.bz2 abc-28e8e7f3e79d1391a2f3a31cefe3afe234aa3b8e.zip |
Merged alanmi/abc into default
Diffstat (limited to 'src/base/wlc')
-rw-r--r-- | src/base/wlc/module.make | 3 | ||||
-rw-r--r-- | src/base/wlc/wlc.h | 58 | ||||
-rw-r--r-- | src/base/wlc/wlcAbc.c | 181 | ||||
-rw-r--r-- | src/base/wlc/wlcAbs.c | 701 | ||||
-rw-r--r-- | src/base/wlc/wlcAbs2.c | 410 | ||||
-rw-r--r-- | src/base/wlc/wlcBlast.c | 51 | ||||
-rw-r--r-- | src/base/wlc/wlcCom.c | 949 | ||||
-rw-r--r-- | src/base/wlc/wlcNtk.c | 570 | ||||
-rw-r--r-- | src/base/wlc/wlcReadSmt.c | 336 | ||||
-rw-r--r-- | src/base/wlc/wlcReadVer.c | 5 | ||||
-rw-r--r-- | src/base/wlc/wlcShow.c | 337 | ||||
-rw-r--r-- | src/base/wlc/wlcSim.c | 22 | ||||
-rw-r--r-- | src/base/wlc/wlcUif.c | 290 | ||||
-rw-r--r-- | src/base/wlc/wlcWriteVer.c | 2 |
14 files changed, 3473 insertions, 442 deletions
diff --git a/src/base/wlc/module.make b/src/base/wlc/module.make index 5a95a63f..c4330264 100644 --- a/src/base/wlc/module.make +++ b/src/base/wlc/module.make @@ -1,4 +1,5 @@ SRC += src/base/wlc/wlcAbs.c \ + src/base/wlc/wlcAbs2.c \ src/base/wlc/wlcAbc.c \ src/base/wlc/wlcBlast.c \ src/base/wlc/wlcCom.c \ @@ -7,6 +8,8 @@ SRC += src/base/wlc/wlcAbs.c \ src/base/wlc/wlcReadSmt.c \ src/base/wlc/wlcReadVer.c \ src/base/wlc/wlcSim.c \ + src/base/wlc/wlcShow.c \ src/base/wlc/wlcStdin.c \ + src/base/wlc/wlcUif.c \ src/base/wlc/wlcWin.c \ src/base/wlc/wlcWriteVer.c diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h index 1df3e5e9..686d9f00 100644 --- a/src/base/wlc/wlc.h +++ b/src/base/wlc/wlc.h @@ -140,6 +140,7 @@ struct Wlc_Ntk_t_ int nObjs[WLC_OBJ_NUMBER]; // counter of objects of each type int nAnds[WLC_OBJ_NUMBER]; // counter of AND gates after blasting int fSmtLib; // the network comes from an SMT-LIB file + int nAssert; // the number of asserts // memory for objects Wlc_Obj_t * pObjs; int iObj; @@ -156,6 +157,23 @@ struct Wlc_Ntk_t_ Vec_Int_t vTravIds; // trav IDs of the objects Vec_Int_t vCopies; // object first bits Vec_Int_t vBits; // object mapping into AIG nodes + Vec_Int_t vLevels; // object levels + Vec_Int_t vRefs; // object reference counters +}; + +typedef struct Wlc_Par_t_ Wlc_Par_t; +struct Wlc_Par_t_ +{ + int nBitsAdd; // adder bit-width + int nBitsMul; // multiplier bit-widht + int nBitsMux; // MUX bit-width + int nBitsFlop; // flop bit-width + int nIterMax; // the max number of iterations + int fXorOutput; // XOR outputs of word-level miter + int fCheckClauses; // Check clauses in the reloaded trace + int fPushClauses; // Push clauses in the reloaded trace + int fVerbose; // verbose output + int fPdrVerbose; // verbose output }; static inline int Wlc_NtkObjNum( Wlc_Ntk_t * p ) { return p->iObj - 1; } @@ -205,6 +223,8 @@ static inline int Wlc_ObjSign( Wlc_Obj_t * p ) static inline int * Wlc_ObjConstValue( Wlc_Obj_t * p ) { assert(p->Type == WLC_OBJ_CONST); return Wlc_ObjFanins(p); } static inline int Wlc_ObjTableId( Wlc_Obj_t * p ) { assert(p->Type == WLC_OBJ_TABLE); return p->Fanins[1]; } static inline word * Wlc_ObjTable( Wlc_Ntk_t * p, Wlc_Obj_t * pObj ) { return (word *)Vec_PtrEntry( p->vTables, Wlc_ObjTableId(pObj) ); } +static inline int Wlc_ObjLevelId( Wlc_Ntk_t * p, int iObj ) { return Vec_IntEntry( &p->vLevels, iObj ); } +static inline int Wlc_ObjLevel( Wlc_Ntk_t * p, Wlc_Obj_t * pObj ) { return Wlc_ObjLevelId( p, Wlc_ObjId(p, pObj) ); } static inline void Wlc_NtkCleanCopy( Wlc_Ntk_t * p ) { Vec_IntFill( &p->vCopies, p->nObjsAlloc, 0 ); } static inline int Wlc_NtkHasCopy( Wlc_Ntk_t * p ) { return Vec_IntSize( &p->vCopies ) > 0; } @@ -217,7 +237,8 @@ static inline int Wlc_NtkHasNameId( Wlc_Ntk_t * p ) static inline void Wlc_ObjSetNameId( Wlc_Ntk_t * p, int iObj, int i ) { Vec_IntWriteEntry( &p->vNameIds, iObj, i ); } static inline int Wlc_ObjNameId( Wlc_Ntk_t * p, int iObj ) { return Vec_IntEntry( &p->vNameIds, iObj ); } -static inline Wlc_Obj_t * Wlc_ObjFoToFi( Wlc_Ntk_t * p, Wlc_Obj_t * pObj ) { assert( pObj->Type == WLC_OBJ_FO ); return Wlc_NtkCo(p, Wlc_NtkCoNum(p) - Wlc_NtkCiNum(p) + Wlc_ObjCiId(pObj)); } +static inline Wlc_Obj_t * Wlc_ObjFo2Fi( Wlc_Ntk_t * p, Wlc_Obj_t * pObj ) { assert( pObj->Type == WLC_OBJ_FO ); return Wlc_NtkCo(p, Wlc_NtkPoNum(p) + Wlc_ObjCiId(pObj) - Wlc_NtkPiNum(p)); } +static inline Wlc_Obj_t * Wlc_ObjCo2PoFo( Wlc_Ntk_t * p, int iCoId ) { return iCoId < Wlc_NtkPoNum(p) ? Wlc_NtkPo(p, iCoId) : Wlc_NtkCi(p, Wlc_NtkPiNum(p) + iCoId - Wlc_NtkPoNum(p)); } //////////////////////////////////////////////////////////////////////// /// MACRO DEFINITIONS /// @@ -229,6 +250,8 @@ static inline Wlc_Obj_t * Wlc_ObjFoToFi( Wlc_Ntk_t * p, Wlc_Obj_t * pObj ) #define Wlc_NtkForEachObj( p, pObj, i ) \ for ( i = 1; (i < Wlc_NtkObjNumMax(p)) && (((pObj) = Wlc_NtkObj(p, i)), 1); i++ ) +#define Wlc_NtkForEachObjReverse( p, pObj, i ) \ + for ( i = Wlc_NtkObjNumMax(p) - 1; (i > 0) && (((pObj) = Wlc_NtkObj(p, i)), 1); i-- ) #define Wlc_NtkForEachObjVec( vVec, p, pObj, i ) \ for ( i = 0; (i < Vec_IntSize(vVec)) && (((pObj) = Wlc_NtkObj(p, Vec_IntEntry(vVec, i))), 1); i++ ) #define Wlc_NtkForEachPi( p, pPi, i ) \ @@ -255,16 +278,17 @@ static inline Wlc_Obj_t * Wlc_ObjFoToFi( Wlc_Ntk_t * p, Wlc_Obj_t * pObj ) //////////////////////////////////////////////////////////////////////// /*=== wlcAbs.c ========================================================*/ -extern int Wlc_NtkPairIsUifable( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Wlc_Obj_t * pObj2 ); -extern Vec_Int_t * Wlc_NtkCollectMultipliers( Wlc_Ntk_t * p ); -extern Vec_Int_t * Wlc_NtkFindUifableMultiplierPairs( Wlc_Ntk_t * p ); -extern Wlc_Ntk_t * Wlc_NtkAbstractNodes( Wlc_Ntk_t * pNtk, Vec_Int_t * vNodes ); -extern Wlc_Ntk_t * Wlc_NtkUifNodePairs( Wlc_Ntk_t * pNtk, Vec_Int_t * vPairs ); +extern int Wlc_NtkAbsCore( Wlc_Ntk_t * p, Wlc_Par_t * pPars ); +extern int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ); +/*=== wlcAbs2.c ========================================================*/ +extern int Wlc_NtkAbsCore2( Wlc_Ntk_t * p, Wlc_Par_t * pPars ); /*=== wlcBlast.c ========================================================*/ extern Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, int nRange, int fGiaSimple, int fAddOutputs, int fBooth ); /*=== wlcCom.c ========================================================*/ extern void Wlc_SetNtk( Abc_Frame_t * pAbc, Wlc_Ntk_t * pNtk ); /*=== wlcNtk.c ========================================================*/ +extern void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars ); +extern char * Wlc_ObjTypeName( Wlc_Obj_t * p ); extern Wlc_Ntk_t * Wlc_NtkAlloc( char * pName, int nObjsAlloc ); extern int Wlc_ObjAlloc( Wlc_Ntk_t * p, int Type, int Signed, int End, int Beg ); extern int Wlc_ObjCreate( Wlc_Ntk_t * p, int Type, int Signed, int End, int Beg, Vec_Int_t * vFanins ); @@ -274,13 +298,25 @@ extern char * Wlc_ObjName( Wlc_Ntk_t * p, int iObj ); extern void Wlc_ObjUpdateType( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, int Type ); extern void Wlc_ObjAddFanins( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Int_t * vFanins ); extern void Wlc_NtkFree( Wlc_Ntk_t * p ); +extern int Wlc_NtkCreateLevels( Wlc_Ntk_t * p ); +extern int Wlc_NtkCreateLevelsRev( Wlc_Ntk_t * p ); +extern int Wlc_NtkCountRealPis( Wlc_Ntk_t * p ); extern void Wlc_NtkPrintNode( Wlc_Ntk_t * p, Wlc_Obj_t * pObj ); extern void Wlc_NtkPrintNodeArray( Wlc_Ntk_t * p, Vec_Int_t * vArray ); extern void Wlc_NtkPrintNodes( Wlc_Ntk_t * p, int Type ); -extern void Wlc_NtkPrintStats( Wlc_Ntk_t * p, int fDistrib, int fVerbose ); -extern Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p ); +extern void Wlc_NtkPrintStats( Wlc_Ntk_t * p, int fDistrib, int fTwoSides, int fVerbose ); extern void Wlc_NtkTransferNames( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p ); +extern char * Wlc_NtkNewName( Wlc_Ntk_t * p, int iCoId, int fSeq ); +extern Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p, int fMarked, int fSeq ); +extern Wlc_Ntk_t * Wlc_NtkDupDfsAbs( Wlc_Ntk_t * p, Vec_Int_t * vPisOld, Vec_Int_t * vPisNew, Vec_Int_t * vFlops ); +extern void Wlc_NtkCleanMarks( Wlc_Ntk_t * p ); +extern void Wlc_NtkMarkCone( Wlc_Ntk_t * p, int iCoId, int Range, int fSeq, int fAllPis ); +extern void Wlc_NtkProfileCones( Wlc_Ntk_t * p ); extern Wlc_Ntk_t * Wlc_NtkDupSingleNodes( Wlc_Ntk_t * p ); +extern void Wlc_NtkShortNames( Wlc_Ntk_t * p ); +extern int Wlc_NtkDcFlopNum( Wlc_Ntk_t * p ); +extern void Wlc_NtkSetRefs( Wlc_Ntk_t * p ); +extern int Wlc_NtkCountObjBits( Wlc_Ntk_t * p, Vec_Int_t * vPisNew ); /*=== wlcReadSmt.c ========================================================*/ extern Wlc_Ntk_t * Wlc_ReadSmtBuffer( char * pFileName, char * pBuffer, char * pLimit, int fOldParser, int fPrintTree ); extern Wlc_Ntk_t * Wlc_ReadSmt( char * pFileName, int fOldParser, int fPrintTree ); @@ -291,6 +327,12 @@ extern void Wlc_NtkDeleteSim( Vec_Ptr_t * p ); extern int Wlc_StdinProcessSmt( Abc_Frame_t * pAbc, char * pCmd ); /*=== wlcReadVer.c ========================================================*/ extern Wlc_Ntk_t * Wlc_ReadVer( char * pFileName, char * pStr ); +/*=== wlcUif.c ========================================================*/ +extern int Wlc_NtkPairIsUifable( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Wlc_Obj_t * pObj2 ); +extern Vec_Int_t * Wlc_NtkCollectMultipliers( Wlc_Ntk_t * p ); +extern Vec_Int_t * Wlc_NtkFindUifableMultiplierPairs( Wlc_Ntk_t * p ); +extern Wlc_Ntk_t * Wlc_NtkAbstractNodes( Wlc_Ntk_t * pNtk, Vec_Int_t * vNodes ); +extern Wlc_Ntk_t * Wlc_NtkUifNodePairs( Wlc_Ntk_t * pNtk, Vec_Int_t * vPairs ); /*=== wlcWin.c =============================================================*/ extern void Wlc_WinProfileArith( Wlc_Ntk_t * p ); /*=== wlcWriteVer.c ========================================================*/ diff --git a/src/base/wlc/wlcAbc.c b/src/base/wlc/wlcAbc.c index 0bf27f7b..1836f4ed 100644 --- a/src/base/wlc/wlcAbc.c +++ b/src/base/wlc/wlcAbc.c @@ -42,7 +42,7 @@ ABC_NAMESPACE_IMPL_START SeeAlso [] ***********************************************************************/ -void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, int fVerbose ) +void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vCounts, int fVerbose ) { Wlc_Obj_t * pObj; int i, k, nNum, nRange, nBits = 0; @@ -53,7 +53,7 @@ void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, int fVerbose ) nRange = Wlc_ObjRange(pObj); for ( k = 0; k < nRange; k++ ) { - nNum = Vec_IntEntry(vInv, nBits + k); + nNum = Vec_IntEntry(vCounts, nBits + k); if ( nNum ) break; } @@ -65,7 +65,7 @@ void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, int fVerbose ) printf( "%s[%d:%d] : ", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), pObj->End, pObj->Beg ); for ( k = 0; k < nRange; k++ ) { - nNum = Vec_IntEntry( vInv, nBits + k ); + nNum = Vec_IntEntry( vCounts, nBits + k ); if ( nNum == 0 ) continue; printf( " [%d] -> %d", k, nNum ); @@ -73,8 +73,8 @@ void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, int fVerbose ) printf( "\n"); nBits += nRange; } - //printf( "%d %d\n", Vec_IntSize(vInv), nBits ); - assert( Vec_IntSize(vInv) == nBits ); + //printf( "%d %d\n", Vec_IntSize(vCounts), nBits ); + assert( Vec_IntSize(vCounts) == nBits ); } /**Function************************************************************* @@ -88,8 +88,14 @@ void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, int fVerbose ) SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, Vec_Str_t * vSop, int fVerbose ) +Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv ) { + extern Vec_Int_t * Pdr_InvCounts( Vec_Int_t * vInv ); + extern Vec_Str_t * Pdr_InvPrintStr( Vec_Int_t * vInv, Vec_Int_t * vCounts ); + + Vec_Int_t * vCounts = Pdr_InvCounts( vInv ); + Vec_Str_t * vSop = Pdr_InvPrintStr( vInv, vCounts ); + Wlc_Obj_t * pObj; int i, k, nNum, nRange, nBits = 0; Abc_Ntk_t * pMainNtk = NULL; @@ -98,46 +104,69 @@ Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, Vec_Str_t * vSop, // start the network pMainNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 ); // duplicate the name and the spec - pMainNtk->pName = Extra_UtilStrsav(pNtk->pName); + pMainNtk->pName = Extra_UtilStrsav(pNtk ? pNtk->pName : "inv"); // create primary inputs - Wlc_NtkForEachCi( pNtk, pObj, i ) + if ( pNtk == NULL ) { - if ( pObj->Type != WLC_OBJ_FO ) - continue; - nRange = Wlc_ObjRange(pObj); - for ( k = 0; k < nRange; k++ ) + int Entry, nInputs = Abc_SopGetVarNum( Vec_StrArray(vSop) ); + Vec_IntForEachEntry( vCounts, Entry, i ) { - nNum = Vec_IntEntry(vInv, nBits + k); - if ( nNum ) - break; + if ( Entry == 0 ) + continue; + pMainObj = Abc_NtkCreatePi( pMainNtk ); + sprintf( Buffer, "pi%d", i ); + Abc_ObjAssignName( pMainObj, Buffer, NULL ); } - if ( k == nRange ) + if ( Abc_NtkPiNum(pMainNtk) != nInputs ) { - nBits += nRange; - continue; + printf( "Mismatch between number of inputs and the number of literals in the invariant.\n" ); + Abc_NtkDelete( pMainNtk ); + return NULL; } - //printf( "%s[%d:%d] : ", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), pObj->End, pObj->Beg ); - for ( k = 0; k < nRange; k++ ) + } + else + { + Wlc_NtkForEachCi( pNtk, pObj, i ) { - nNum = Vec_IntEntry( vInv, nBits + k ); - if ( nNum == 0 ) + if ( pObj->Type != WLC_OBJ_FO ) continue; - //printf( " [%d] -> %d", k, nNum ); - pMainObj = Abc_NtkCreatePi( pMainNtk ); - sprintf( Buffer, "%s[%d]", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), k ); - Abc_ObjAssignName( pMainObj, Buffer, NULL ); + nRange = Wlc_ObjRange(pObj); + for ( k = 0; k < nRange; k++ ) + { + nNum = Vec_IntEntry(vCounts, nBits + k); + if ( nNum ) + break; + } + if ( k == nRange ) + { + nBits += nRange; + continue; + } + //printf( "%s[%d:%d] : ", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), pObj->End, pObj->Beg ); + for ( k = 0; k < nRange; k++ ) + { + nNum = Vec_IntEntry( vCounts, nBits + k ); + if ( nNum == 0 ) + continue; + //printf( " [%d] -> %d", k, nNum ); + pMainObj = Abc_NtkCreatePi( pMainNtk ); + sprintf( Buffer, "%s[%d]", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), k ); + Abc_ObjAssignName( pMainObj, Buffer, NULL ); + } + //printf( "\n"); + nBits += nRange; } - //printf( "\n"); - nBits += nRange; } - //printf( "%d %d\n", Vec_IntSize(vInv), nBits ); - assert( Vec_IntSize(vInv) == nBits ); + //printf( "%d %d\n", Vec_IntSize(vCounts), nBits ); + assert( pNtk == NULL || Vec_IntSize(vCounts) == nBits ); // create node pMainObj = Abc_NtkCreateNode( pMainNtk ); Abc_NtkForEachPi( pMainNtk, pMainTemp, i ) Abc_ObjAddFanin( pMainObj, pMainTemp ); pMainObj->pData = Abc_SopRegister( (Mem_Flex_t *)pMainNtk->pManFunc, Vec_StrArray(vSop) ); + Vec_IntFree( vCounts ); + Vec_StrFree( vSop ); // create PO pMainTemp = Abc_NtkCreatePo( pMainNtk ); Abc_ObjAddFanin( pMainTemp, pMainObj ); @@ -145,6 +174,98 @@ Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, Vec_Str_t * vSop, return pMainNtk; } +/**Function************************************************************* + + Synopsis [Translate current network into an invariant.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Wlc_NtkGetPut( Abc_Ntk_t * pNtk, Gia_Man_t * pGia ) +{ + int nRegs = Gia_ManRegNum(pGia); + Vec_Int_t * vRes = NULL; + if ( Abc_NtkPoNum(pNtk) != 1 ) + printf( "The number of outputs is other than 1.\n" ); + else if ( Abc_NtkNodeNum(pNtk) != 1 ) + printf( "The number of internal nodes is other than 1.\n" ); + else + { + Abc_Nam_t * pNames = NULL; + Abc_Obj_t * pFanin, * pNode = Abc_ObjFanin0( Abc_NtkCo(pNtk, 0) ); + char * pName, * pCube, * pSop = (char *)pNode->pData; + Vec_Int_t * vFanins = Vec_IntAlloc( Abc_ObjFaninNum(pNode) ); + int i, k, Value, nLits, Counter = 0; + if ( pGia->vNamesIn ) + { + // hash the names + pNames = Abc_NamStart( 100, 16 ); + Vec_PtrForEachEntry( char *, pGia->vNamesIn, pName, i ) + { + Value = Abc_NamStrFindOrAdd( pNames, pName, NULL ); + assert( Value == i+1 ); + //printf( "%s(%d) ", pName, i ); + } + //printf( "\n" ); + } + Abc_ObjForEachFanin( pNode, pFanin, i ) + { + assert( Abc_ObjIsCi(pFanin) ); + pName = Abc_ObjName(pFanin); + if ( pNames ) + { + Value = Abc_NamStrFind(pNames, pName) - 1 - Gia_ManPiNum(pGia); + if ( Value < 0 ) + { + if ( Counter++ == 0 ) + printf( "Cannot read input name \"%s\" of fanin %d.\n", pName, i ); + Value = i; + } + } + else + { + for ( k = (int)strlen(pName)-1; k >= 0; k-- ) + if ( pName[k] < '0' || pName[k] > '9' ) + break; + if ( k == (int)strlen(pName)-1 ) + { + if ( Counter++ == 0 ) + printf( "Cannot read input name \"%s\" of fanin %d.\n", pName, i ); + Value = i; + } + else + Value = atoi(pName + k + 1); + } + Vec_IntPush( vFanins, Value ); + } + if ( Counter ) + printf( "Cannot read names for %d inputs of the invariant.\n", Counter ); + if ( pNames ) + Abc_NamStop( pNames ); + assert( Vec_IntSize(vFanins) == Abc_ObjFaninNum(pNode) ); + vRes = Vec_IntAlloc( 1000 ); + Vec_IntPush( vRes, Abc_SopGetCubeNum(pSop) ); + Abc_SopForEachCube( pSop, Abc_ObjFaninNum(pNode), pCube ) + { + nLits = 0; + Abc_CubeForEachVar( pCube, Value, k ) + if ( Value != '-' ) + nLits++; + Vec_IntPush( vRes, nLits ); + Abc_CubeForEachVar( pCube, Value, k ) + if ( Value != '-' ) + Vec_IntPush( vRes, Abc_Var2Lit(Vec_IntEntry(vFanins, k), (int)Value == '0') ); + } + Vec_IntPush( vRes, nRegs ); + Vec_IntFree( vFanins ); + } + return vRes; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index 73ff7328..e33424f7 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -8,7 +8,7 @@ Synopsis [Abstraction for word-level networks.] - Author [Alan Mishchenko] + Author [Yen-Sheng Ho, Alan Mishchenko] Affiliation [UC Berkeley] @@ -19,6 +19,10 @@ ***********************************************************************/ #include "wlc.h" +#include "proof/pdr/pdr.h" +#include "proof/pdr/pdrInt.h" +#include "aig/gia/giaAig.h" +#include "sat/bmc/bmc.h" ABC_NAMESPACE_IMPL_START @@ -26,161 +30,330 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +extern Vec_Vec_t * IPdr_ManSaveClauses( Pdr_Man_t * p, int fDropLast ); +extern int IPdr_ManRestore( Pdr_Man_t * p, Vec_Vec_t * vClauses, Vec_Int_t * vMap ); +extern int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses ); + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* - Synopsis [Check if two objects have the same input/output signatures.] + Synopsis [Mark operators that meet the abstraction criteria.] - Description [] + Description [This procedure returns the array of objects (vLeaves) that + should be abstracted because of their high bit-width. It uses input array (vUnmark) + to not abstract those objects that have been refined in the previous rounds.] SideEffects [] SeeAlso [] ***********************************************************************/ -int Wlc_NtkPairIsUifable( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Wlc_Obj_t * pObj2 ) +static Vec_Bit_t * Wlc_NtkAbsMarkOpers( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t * vUnmark, int fVerbose ) { - Wlc_Obj_t * pFanin, * pFanin2; int k; - if ( Wlc_ObjRange(pObj) != Wlc_ObjRange(pObj2) ) - return 0; - if ( Wlc_ObjIsSigned(pObj) != Wlc_ObjIsSigned(pObj2) ) - return 0; - if ( Wlc_ObjFaninNum(pObj) != Wlc_ObjFaninNum(pObj2) ) - return 0; - for ( k = 0; k < Wlc_ObjFaninNum(pObj); k++ ) + Vec_Bit_t * vLeaves = Vec_BitStart( Wlc_NtkObjNumMax(p) ); + Wlc_Obj_t * pObj; int i, Count[4] = {0}; + Wlc_NtkForEachObj( p, pObj, i ) { - pFanin = Wlc_ObjFanin(p, pObj, k); - pFanin2 = Wlc_ObjFanin(p, pObj2, k); - if ( Wlc_ObjRange(pFanin) != Wlc_ObjRange(pFanin2) ) - return 0; - if ( Wlc_ObjIsSigned(pFanin) != Wlc_ObjIsSigned(pFanin2) ) - return 0; + if ( vUnmark && Vec_BitEntry(vUnmark, i) ) // not allow this object to be abstracted away + continue; + if ( pObj->Type == WLC_OBJ_ARI_ADD || pObj->Type == WLC_OBJ_ARI_SUB || pObj->Type == WLC_OBJ_ARI_MINUS ) + { + if ( Wlc_ObjRange(pObj) >= pPars->nBitsAdd ) + Vec_BitWriteEntry( vLeaves, Wlc_ObjId(p, pObj), 1 ), Count[0]++; + continue; + } + if ( pObj->Type == WLC_OBJ_ARI_MULTI || pObj->Type == WLC_OBJ_ARI_DIVIDE || pObj->Type == WLC_OBJ_ARI_REM || pObj->Type == WLC_OBJ_ARI_MODULUS ) + { + if ( Wlc_ObjRange(pObj) >= pPars->nBitsMul ) + Vec_BitWriteEntry( vLeaves, Wlc_ObjId(p, pObj), 1 ), Count[1]++; + continue; + } + if ( pObj->Type == WLC_OBJ_MUX ) + { + if ( Wlc_ObjRange(pObj) >= pPars->nBitsMux ) + Vec_BitWriteEntry( vLeaves, Wlc_ObjId(p, pObj), 1 ), Count[2]++; + continue; + } + if ( Wlc_ObjIsCi(pObj) && !Wlc_ObjIsPi(pObj) ) + { + if ( Wlc_ObjRange(pObj) >= pPars->nBitsFlop ) + Vec_BitWriteEntry( vLeaves, Wlc_ObjId(p, pObj), 1 ), Count[3]++; + continue; + } } - return 1; + if ( fVerbose ) + printf( "Abstraction engine marked %d adds/subs, %d muls/divs, %d muxes, and %d flops to be abstracted away.\n", Count[0], Count[1], Count[2], Count[3] ); + return vLeaves; } /**Function************************************************************* - Synopsis [Collect IDs of the multipliers.] + Synopsis [Marks nodes to be included in the abstracted network.] - Description [] + Description [Marks all objects that will be included in the abstracted model. + Stops at the objects (vLeaves) that are abstracted away. Returns three arrays: + a subset of original PIs (vPisOld), a subset of pseudo-PIs (vPisNew) and the + set of flops present as flops in the abstracted network.] SideEffects [] SeeAlso [] ***********************************************************************/ -Vec_Int_t * Wlc_NtkCollectMultipliers( Wlc_Ntk_t * p ) +static void Wlc_NtkAbsMarkNodes_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Bit_t * vLeaves, Vec_Int_t * vPisOld, Vec_Int_t * vPisNew, Vec_Int_t * vFlops ) { - Wlc_Obj_t * pObj; int i; - Vec_Int_t * vBoxIds = Vec_IntAlloc( 100 ); + int i, iFanin; + if ( pObj->Mark ) + return; + pObj->Mark = 1; + if ( Vec_BitEntry(vLeaves, Wlc_ObjId(p, pObj)) ) + { + assert( !Wlc_ObjIsPi(pObj) ); + Vec_IntPush( vPisNew, Wlc_ObjId(p, pObj) ); + return; + } + if ( Wlc_ObjIsCi(pObj) ) + { + if ( Wlc_ObjIsPi(pObj) ) + Vec_IntPush( vPisOld, Wlc_ObjId(p, pObj) ); + else + Vec_IntPush( vFlops, Wlc_ObjId(p, pObj) ); + return; + } + Wlc_ObjForEachFanin( pObj, iFanin, i ) + Wlc_NtkAbsMarkNodes_rec( p, Wlc_NtkObj(p, iFanin), vLeaves, vPisOld, vPisNew, vFlops ); +} +static void Wlc_NtkAbsMarkNodes( Wlc_Ntk_t * p, Vec_Bit_t * vLeaves, Vec_Int_t * vPisOld, Vec_Int_t * vPisNew, Vec_Int_t * vFlops ) +{ + Wlc_Obj_t * pObj; + int i, Count = 0; + Wlc_NtkCleanMarks( p ); + Wlc_NtkForEachCo( p, pObj, i ) + Wlc_NtkAbsMarkNodes_rec( p, pObj, vLeaves, vPisOld, vPisNew, vFlops ); + +/* + Vec_IntClear(vFlops); + Wlc_NtkForEachCi( p, pObj, i ) { + if ( !Wlc_ObjIsPi(pObj) ) { + Vec_IntPush( vFlops, Wlc_ObjId(p, pObj) ); + pObj->Mark = 1; + } + } +*/ + + Wlc_NtkForEachObjVec( vFlops, p, pObj, i ) + Wlc_NtkAbsMarkNodes_rec( p, Wlc_ObjFo2Fi(p, pObj), vLeaves, vPisOld, vPisNew, vFlops ); Wlc_NtkForEachObj( p, pObj, i ) - if ( pObj->Type == WLC_OBJ_ARI_MULTI ) - Vec_IntPush( vBoxIds, i ); - if ( Vec_IntSize( vBoxIds ) > 0 ) - return vBoxIds; - Vec_IntFree( vBoxIds ); - return NULL; + Count += pObj->Mark; +// printf( "Collected %d old PIs, %d new PIs, %d flops, and %d other objects.\n", +// Vec_IntSize(vPisOld), Vec_IntSize(vPisNew), Vec_IntSize(vFlops), +// Count - Vec_IntSize(vPisOld) - Vec_IntSize(vPisNew) - Vec_IntSize(vFlops) ); + Vec_IntSort( vPisOld, 0 ); + Vec_IntSort( vPisNew, 0 ); + Vec_IntSort( vFlops, 0 ); + Wlc_NtkCleanMarks( p ); } /**Function************************************************************* - Synopsis [Returns all pairs of uifable multipliers.] + Synopsis [Derive word-level abstracted model based on the parameter values.] - Description [] + Description [Retuns the word-level abstracted network and the set of pseudo-PIs + (vPisNew), which were created during abstraction. If the abstraction is + satisfiable, some of the pseudo-PIs will be un-abstracted. These pseudo-PIs + and their MFFC cones will be listed in the array (vUnmark), which will + force the abstraction to not stop at these pseudo-PIs in the future.] SideEffects [] SeeAlso [] ***********************************************************************/ -Vec_Int_t * Wlc_NtkFindUifableMultiplierPairs( Wlc_Ntk_t * p ) +static Wlc_Ntk_t * Wlc_NtkAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t * vUnmark, Vec_Int_t ** pvPisNew, Vec_Int_t ** pvFlops, int fVerbose ) { - Vec_Int_t * vMultis = Wlc_NtkCollectMultipliers( p ); - Vec_Int_t * vPairs = Vec_IntAlloc( 2 ); - Wlc_Obj_t * pObj, * pObj2; int i, k; - // iterate through unique pairs - Wlc_NtkForEachObjVec( vMultis, p, pObj, i ) - Wlc_NtkForEachObjVec( vMultis, p, pObj2, k ) - { - if ( k == i ) - break; - if ( Wlc_NtkPairIsUifable( p, pObj, pObj2 ) ) - { - Vec_IntPush( vPairs, Wlc_ObjId(p, pObj) ); - Vec_IntPush( vPairs, Wlc_ObjId(p, pObj2) ); - } - } - Vec_IntFree( vMultis ); - if ( Vec_IntSize( vPairs ) > 0 ) - return vPairs; - Vec_IntFree( vPairs ); - return NULL; + Wlc_Ntk_t * pNtkNew = NULL; + Vec_Int_t * vPisOld = Vec_IntAlloc( 100 ); + Vec_Int_t * vPisNew = Vec_IntAlloc( 100 ); + Vec_Int_t * vFlops = Vec_IntAlloc( 100 ); + Vec_Bit_t * vLeaves = Wlc_NtkAbsMarkOpers( p, pPars, vUnmark, fVerbose ); + Wlc_NtkAbsMarkNodes( p, vLeaves, vPisOld, vPisNew, vFlops ); + Vec_BitFree( vLeaves ); + pNtkNew = Wlc_NtkDupDfsAbs( p, vPisOld, vPisNew, vFlops ); + Vec_IntFree( vPisOld ); + if ( pvFlops ) + *pvFlops = vFlops; + else + Vec_IntFree( vFlops ); + if ( pvPisNew ) + *pvPisNew = vPisNew; + else + Vec_IntFree( vPisNew ); + return pNtkNew; } +/**Function************************************************************* + + Synopsis [Find what objects need to be un-abstracted.] + + Description [Returns a subset of pseudo-PIs (vPisNew), which will be + prevented from being abstracted in the future rounds of abstraction. + The AIG manager (pGia) is a bit-level view of the abstracted model. + The counter-example (pCex) is used to find waht PPIs to refine.] + + SideEffects [] + SeeAlso [] + +***********************************************************************/ +static Vec_Int_t * Wlc_NtkAbsRefinement( Wlc_Ntk_t * p, Gia_Man_t * pGia, Abc_Cex_t * pCex, Vec_Int_t * vPisNew ) +{ + Vec_Int_t * vRefine = Vec_IntAlloc( 100 ); + Abc_Cex_t * pCexCare; + Wlc_Obj_t * pObj; + // count the number of bit-level PPIs and map them into word-level objects they were derived from + int f, i, b, nRealPis, nPpiBits = 0; + Vec_Int_t * vMap = Vec_IntStartFull( pCex->nPis ); + Wlc_NtkForEachObjVec( vPisNew, p, pObj, i ) + for ( b = 0; b < Wlc_ObjRange(pObj); b++ ) + Vec_IntWriteEntry( vMap, nPpiBits++, Wlc_ObjId(p, pObj) ); + // since PPIs are ordered last, the previous bits are real PIs + nRealPis = pCex->nPis - nPpiBits; + // find the care-set + pCexCare = Bmc_CexCareMinimizeAig( pGia, nRealPis, pCex, 1, 0, 0 ); + assert( pCexCare->nPis == pCex->nPis ); + // detect care PPIs + for ( f = 0; f <= pCexCare->iFrame; f++ ) + for ( i = nRealPis; i < pCexCare->nPis; i++ ) + if ( Abc_InfoHasBit(pCexCare->pData, pCexCare->nRegs + pCexCare->nPis * f + i) ) + Vec_IntPushUniqueOrder( vRefine, Vec_IntEntry(vMap, i-nRealPis) ); + Abc_CexFree( pCexCare ); + Vec_IntFree( vMap ); + if ( Vec_IntSize(vRefine) == 0 )// real CEX + Vec_IntFreeP( &vRefine ); + return vRefine; +} /**Function************************************************************* - Synopsis [Abstracts nodes by replacing their outputs with new PIs.] + Synopsis [Mark MFFC cones of the un-abstracted objects.] - Description [If array is NULL, abstract all multipliers.] + Description [The MFFC cones of the objects in vRefine are traversed + and all their nodes are marked in vUnmark.] SideEffects [] SeeAlso [] ***********************************************************************/ -Wlc_Ntk_t * Wlc_NtkAbstractNodes( Wlc_Ntk_t * p, Vec_Int_t * vNodesInit ) +static int Wlc_NtkNodeDeref_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pNode, Vec_Bit_t * vUnmark ) { - Vec_Int_t * vNodes = vNodesInit; - Wlc_Ntk_t * pNew; - Wlc_Obj_t * pObj; - int i, k, iObj, iFanin; - // get multipliers if not given - if ( vNodes == NULL ) - vNodes = Wlc_NtkCollectMultipliers( p ); - if ( vNodes == NULL ) - return NULL; - // mark nodes - Wlc_NtkForEachObjVec( vNodes, p, pObj, i ) - pObj->Mark = 1; - // iterate through the nodes in the DFS order - Wlc_NtkCleanCopy( p ); - Wlc_NtkForEachObj( p, pObj, i ) + int i, Fanin, Counter = 1; + if ( Wlc_ObjIsCi(pNode) ) + return 0; + Vec_BitWriteEntry( vUnmark, Wlc_ObjId(p, pNode), 1 ); + Wlc_ObjForEachFanin( pNode, Fanin, i ) { - if ( i == Vec_IntSize(&p->vCopies) ) - break; - if ( pObj->Mark ) { - // clean - pObj->Mark = 0; - // add fresh PI with the same number of bits - iObj = Wlc_ObjAlloc( p, WLC_OBJ_PI, Wlc_ObjIsSigned(pObj), Wlc_ObjRange(pObj) - 1, 0 ); - } - else { - // update fanins - Wlc_ObjForEachFanin( pObj, iFanin, k ) - Wlc_ObjFanins(pObj)[k] = Wlc_ObjCopy(p, iFanin); - // node to remain - iObj = i; - } - Wlc_ObjSetCopy( p, i, iObj ); + Vec_IntAddToEntry( &p->vRefs, Fanin, -1 ); + if ( Vec_IntEntry(&p->vRefs, Fanin) == 0 ) + Counter += Wlc_NtkNodeDeref_rec( p, Wlc_NtkObj(p, Fanin), vUnmark ); } - // POs do not change in this procedure - if ( vNodes != vNodesInit ) - Vec_IntFree( vNodes ); - // reconstruct topological order - pNew = Wlc_NtkDupDfs( p ); - Wlc_NtkTransferNames( pNew, p ); - return pNew; + return Counter; +} +static int Wlc_NtkNodeRef_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pNode ) +{ + int i, Fanin, Counter = 1; + if ( Wlc_ObjIsCi(pNode) ) + return 0; + Wlc_ObjForEachFanin( pNode, Fanin, i ) + { + if ( Vec_IntEntry(&p->vRefs, Fanin) == 0 ) + Counter += Wlc_NtkNodeRef_rec( p, Wlc_NtkObj(p, Fanin) ); + Vec_IntAddToEntry( &p->vRefs, Fanin, 1 ); + } + return Counter; +} +static int Wlc_NtkMarkMffc( Wlc_Ntk_t * p, Wlc_Obj_t * pNode, Vec_Bit_t * vUnmark ) +{ + int Count1, Count2; + // if this is a flop output, compute MFFC of the corresponding flop input + while ( Wlc_ObjIsCi(pNode) ) + { + Vec_BitWriteEntry( vUnmark, Wlc_ObjId(p, pNode), 1 ); + pNode = Wlc_ObjFo2Fi(p, pNode); + } + assert( !Wlc_ObjIsCi(pNode) ); + // dereference the node (and set the bits in vUnmark) + Count1 = Wlc_NtkNodeDeref_rec( p, pNode, vUnmark ); + // reference it back + Count2 = Wlc_NtkNodeRef_rec( p, pNode ); + assert( Count1 == Count2 ); + return Count1; +} +static int Wlc_NtkRemoveFromAbstraction( Wlc_Ntk_t * p, Vec_Int_t * vRefine, Vec_Bit_t * vUnmark ) +{ + Wlc_Obj_t * pObj; int i, nNodes = 0; + if ( Vec_IntSize(&p->vRefs) == 0 ) + Wlc_NtkSetRefs( p ); + Wlc_NtkForEachObjVec( vRefine, p, pObj, i ) + nNodes += Wlc_NtkMarkMffc( p, pObj, vUnmark ); + return nNodes; } /**Function************************************************************* - Synopsis [Adds UIF constraints to node pairs and updates POs.] + Synopsis [Computes the map for remapping flop IDs used in the clauses.] + + Description [Takes the original network (Wlc_Ntk_t) and the array of word-level + flops used in the old abstraction (vFfOld) and those used in the new abstraction + (vFfNew). Returns the integer map, which remaps every binary flop found + in the old abstraction into a binary flop found in the new abstraction.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Wlc_NtkFlopsRemap( Wlc_Ntk_t * p, Vec_Int_t * vFfOld, Vec_Int_t * vFfNew ) +{ + Vec_Int_t * vMap = Vec_IntAlloc( 1000 ); // the resulting map + Vec_Int_t * vMapFfNew2Bit1 = Vec_IntAlloc( 1000 ); // first binary bit of each new word-level flop + int i, b, iFfOld, iFfNew, iBit1New, nBits = 0; + // map object IDs of old flops into their flop indexes + Vec_Int_t * vMapFfObj2FfId = Vec_IntStartFull( Wlc_NtkObjNumMax(p) ); + Vec_IntForEachEntry( vFfNew, iFfNew, i ) + Vec_IntWriteEntry( vMapFfObj2FfId, iFfNew, i ); + // map each new flop index into its first bit + Vec_IntForEachEntry( vFfNew, iFfNew, i ) + { + Wlc_Obj_t * pObj = Wlc_NtkObj( p, iFfNew ); + int nRange = Wlc_ObjRange( pObj ); + Vec_IntPush( vMapFfNew2Bit1, nBits ); + nBits += nRange; + } + assert( Vec_IntSize(vMapFfNew2Bit1) == Vec_IntSize(vFfNew) ); + // remap old binary flops into new binary flops + Vec_IntForEachEntry( vFfOld, iFfOld, i ) + { + Wlc_Obj_t * pObj = Wlc_NtkObj( p, iFfOld ); + int nRange = Wlc_ObjRange( pObj ); + iFfNew = Vec_IntEntry( vMapFfObj2FfId, iFfOld ); + assert( iFfNew >= 0 ); // every old flop should be present in the new abstraction + // find the first bit of this new flop + iBit1New = Vec_IntEntry( vMapFfNew2Bit1, iFfNew ); + for ( b = 0; b < nRange; b++ ) + Vec_IntPush( vMap, iBit1New + b ); + } + Vec_IntFree( vMapFfNew2Bit1 ); + Vec_IntFree( vMapFfObj2FfId ); + return vMap; +} + +/**Function************************************************************* + + Synopsis [Performs PDR with word-level abstraction.] Description [] @@ -189,98 +362,266 @@ Wlc_Ntk_t * Wlc_NtkAbstractNodes( Wlc_Ntk_t * p, Vec_Int_t * vNodesInit ) SeeAlso [] ***********************************************************************/ -Wlc_Ntk_t * Wlc_NtkUifNodePairs( Wlc_Ntk_t * p, Vec_Int_t * vPairsInit ) +int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) { - Vec_Int_t * vPairs = vPairsInit; - Wlc_Ntk_t * pNew; - Wlc_Obj_t * pObj, * pObj2; - Vec_Int_t * vUifConstrs, * vCompares, * vFanins; - int i, k, iObj, iObj2, iObjNew, iObjNew2; - int iFanin, iFanin2, iFaninNew; - // get multiplier pairs if not given - if ( vPairs == NULL ) - vPairs = Wlc_NtkFindUifableMultiplierPairs( p ); - if ( vPairs == NULL ) - return NULL; - // sanity checks - assert( Vec_IntSize(vPairs) > 0 && Vec_IntSize(vPairs) % 2 == 0 ); - // iterate through node pairs - vFanins = Vec_IntAlloc( 100 ); - vCompares = Vec_IntAlloc( 100 ); - vUifConstrs = Vec_IntAlloc( 100 ); - Vec_IntForEachEntryDouble( vPairs, iObj, iObj2, i ) + abctime clk = Abc_Clock(); + abctime pdrClk; + Pdr_Man_t * pPdr; + Vec_Vec_t * vClauses = NULL; + Vec_Int_t * vFfOld = NULL, * vFfNew = NULL, * vMap = NULL; + int nIters, nNodes, nDcFlops, RetValue = -1, nGiaFfNumOld = -1; + // start the bitmap to mark objects that cannot be abstracted because of refinement + // currently, this bitmap is empty because abstraction begins without refinement + Vec_Bit_t * vUnmark = Vec_BitStart( Wlc_NtkObjNumMax(p) ); + // set up parameters to run PDR + Pdr_Par_t PdrPars, * pPdrPars = &PdrPars; + Pdr_ManSetDefaultParams( pPdrPars ); + pPdrPars->fVerbose = pPars->fPdrVerbose; + pPdrPars->fVeryVerbose = 0; + + // perform refinement iterations + for ( nIters = 1; nIters < pPars->nIterMax; nIters++ ) { - // get two nodes - pObj = Wlc_NtkObj( p, iObj ); - pObj2 = Wlc_NtkObj( p, iObj2 ); - assert( Wlc_NtkPairIsUifable(p, pObj, pObj2) ); - // create fanin comparator nodes - Vec_IntClear( vCompares ); - Wlc_ObjForEachFanin( pObj, iFanin, k ) + Aig_Man_t * pAig; + Abc_Cex_t * pCex; + Vec_Int_t * vPisNew, * vRefine; + Gia_Man_t * pGia, * pTemp; + Wlc_Ntk_t * pAbs; + + if ( pPars->fVerbose ) + printf( "\nIteration %d:\n", nIters ); + + // get abstracted GIA and the set of pseudo-PIs (vPisNew) + pAbs = Wlc_NtkAbs( p, pPars, vUnmark, &vPisNew, &vFfNew, pPars->fVerbose ); + pGia = Wlc_NtkBitBlast( pAbs, NULL, -1, 0, 0, 0, 0 ); + + // map old flops into new flops + if ( vFfOld ) { - iFanin2 = Wlc_ObjFaninId( pObj2, k ); - Vec_IntFillTwo( vFanins, 2, iFanin, iFanin2 ); - iFaninNew = Wlc_ObjCreate( p, WLC_OBJ_COMP_NOTEQU, 0, 0, 0, vFanins ); - Vec_IntPush( vCompares, iFaninNew ); - // note that a pointer to Wlc_Obj_t (for example, pObj) can be invalidated after a call to - // Wlc_ObjCreate() due to a possible realloc of the internal array of objects... - pObj = Wlc_NtkObj( p, iObj ); + assert( nGiaFfNumOld >= 0 ); + vMap = Wlc_NtkFlopsRemap( p, vFfOld, vFfNew ); + //Vec_IntPrint( vMap ); + // if reset flop was added in the previous iteration, it will be added again in this iteration + // remap the last flop (reset flop) into the last flop (reset flop) of the current AIG + if ( Vec_IntSize(vMap) + 1 == nGiaFfNumOld ) + Vec_IntPush( vMap, Gia_ManRegNum(pGia)-1 ); + assert( Vec_IntSize(vMap) == nGiaFfNumOld ); + Vec_IntFreeP( &vFfOld ); } - // concatenate fanin comparators - iObjNew = Wlc_ObjCreate( p, WLC_OBJ_BIT_CONCAT, 0, Vec_IntSize(vCompares) - 1, 0, vCompares ); - // create reduction-OR node - Vec_IntFill( vFanins, 1, iObjNew ); - iObjNew = Wlc_ObjCreate( p, WLC_OBJ_REDUCT_OR, 0, 0, 0, vFanins ); - // craete output comparator node - Vec_IntFillTwo( vFanins, 2, iObj, iObj2 ); - iObjNew2 = Wlc_ObjCreate( p, WLC_OBJ_COMP_EQU, 0, 0, 0, vFanins ); - // create implication node (iObjNew is already complemented above) - Vec_IntFillTwo( vFanins, 2, iObjNew, iObjNew2 ); - iObjNew = Wlc_ObjCreate( p, WLC_OBJ_LOGIC_OR, 0, 0, 0, vFanins ); - // save the constraint - Vec_IntPush( vUifConstrs, iObjNew ); - } - // derive the AND of the UIF contraints - assert( Vec_IntSize(vUifConstrs) > 0 ); - if ( Vec_IntSize(vUifConstrs) == 1 ) - iObjNew = Vec_IntEntry( vUifConstrs, 0 ); - else - { - // concatenate - iObjNew = Wlc_ObjCreate( p, WLC_OBJ_BIT_CONCAT, 0, Vec_IntSize(vUifConstrs) - 1, 0, vUifConstrs ); - // create reduction-AND node - Vec_IntFill( vFanins, 1, iObjNew ); - iObjNew = Wlc_ObjCreate( p, WLC_OBJ_REDUCT_AND, 0, 0, 0, vFanins ); + ABC_SWAP( Vec_Int_t *, vFfOld, vFfNew ); + nGiaFfNumOld = Gia_ManRegNum(pGia); + + // if the abstraction has flops with DC-init state, + // new PIs were introduced by bit-blasting at the end of the PI list + // here we move these variables to be *before* PPIs, because + // PPIs are supposed to be at the end of the PI list for refinement + nDcFlops = Wlc_NtkDcFlopNum(pAbs); + if ( nDcFlops > 0 ) // DC-init flops are present + { + pGia = Gia_ManPermuteInputs( pTemp = pGia, Wlc_NtkCountObjBits(p, vPisNew), nDcFlops ); + Gia_ManStop( pTemp ); + } + // if the word-level outputs have to be XORs, this is a place to do it + if ( pPars->fXorOutput ) + { + pGia = Gia_ManTransformMiter2( pTemp = pGia ); + Gia_ManStop( pTemp ); + } + if ( pPars->fVerbose ) + { + printf( "Derived abstraction with %d objects and %d PPIs. Bit-blasted AIG stats are:\n", Wlc_NtkObjNum(pAbs), Vec_IntSize(vPisNew) ); + Gia_ManPrintStats( pGia, NULL ); + } + Wlc_NtkFree( pAbs ); + + // try to prove abstracted GIA by converting it to AIG and calling PDR + pAig = Gia_ManToAigSimple( pGia ); + + pPdr = Pdr_ManStart( pAig, pPdrPars, NULL ); + pdrClk = Abc_Clock(); + + if ( vClauses ) { + assert( Vec_VecSize( vClauses) >= 2 ); + IPdr_ManRestore( pPdr, vClauses, vMap ); + } + Vec_IntFreeP( &vMap ); + + RetValue = IPdr_ManSolveInt( pPdr, pPars->fCheckClauses, pPars->fPushClauses ); + pPdr->tTotal += Abc_Clock() - pdrClk; + + pCex = pAig->pSeqModel; pAig->pSeqModel = NULL; + + // consider outcomes + if ( pCex == NULL ) + { + assert( RetValue ); // proved or undecided + Gia_ManStop( pGia ); + Vec_IntFree( vPisNew ); + Pdr_ManStop( pPdr ); + Aig_ManStop( pAig ); + break; + } + + // perform refinement + vRefine = Wlc_NtkAbsRefinement( p, pGia, pCex, vPisNew ); + Gia_ManStop( pGia ); + Vec_IntFree( vPisNew ); + if ( vRefine == NULL ) // real CEX + { + Abc_CexFree( pCex ); // return CEX in the future + Pdr_ManStop( pPdr ); + Aig_ManStop( pAig ); + break; + } + + // spurious CEX, continue solving + vClauses = IPdr_ManSaveClauses( pPdr, 0 ); + + Pdr_ManStop( pPdr ); + + // update the set of objects to be un-abstracted + nNodes = Wlc_NtkRemoveFromAbstraction( p, vRefine, vUnmark ); + if ( pPars->fVerbose ) + printf( "Refinement of CEX in frame %d came up with %d un-abstacted PPIs, whose MFFCs include %d objects.\n", pCex->iFrame, Vec_IntSize(vRefine), nNodes ); + Vec_IntFree( vRefine ); + Abc_CexFree( pCex ); + Aig_ManStop( pAig ); } - // update each PO to point to the new node - Wlc_NtkForEachPo( p, pObj, i ) + + Vec_IntFreeP( &vFfOld ); + Vec_BitFree( vUnmark ); + // report the result + if ( pPars->fVerbose ) + printf( "\n" ); + printf( "Abstraction " ); + if ( RetValue == 0 ) + printf( "resulted in a real CEX" ); + else if ( RetValue == 1 ) + printf( "is successfully proved" ); + else + printf( "timed out" ); + printf( " after %d iterations. ", nIters ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Performs abstraction.] + + Description [Derives initial abstraction based on user-specified + parameter values, which tell what is the smallest bit-width of a + primitive that is being abstracted away. Currently only add/sub, + mul/div, mux, and flop are supported with individual parameters. + The second step is to refine the initial abstraction until the + point when the property is proved.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Wlc_NtkAbsCore( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) +{ + abctime clk = Abc_Clock(); + int nIters, nNodes, nDcFlops, RetValue = -1; + // start the bitmap to mark objects that cannot be abstracted because of refinement + // currently, this bitmap is empty because abstraction begins without refinement + Vec_Bit_t * vUnmark = Vec_BitStart( Wlc_NtkObjNumMax(p) ); + // set up parameters to run PDR + Pdr_Par_t PdrPars, * pPdrPars = &PdrPars; + Pdr_ManSetDefaultParams( pPdrPars ); + //pPdrPars->fUseAbs = 1; // use 'pdr -t' (on-the-fly abstraction) + //pPdrPars->fCtgs = 1; // use 'pdr -nc' (improved generalization) + //pPdrPars->fSkipDown = 0; // use 'pdr -nc' (improved generalization) + //pPdrPars->nRestLimit = 500; // reset queue or proof-obligations when it gets larger than this + pPdrPars->fVerbose = pPars->fPdrVerbose; + pPdrPars->fVeryVerbose = 0; + // perform refinement iterations + for ( nIters = 1; nIters < pPars->nIterMax; nIters++ ) { - iObj = Wlc_ObjId(p, pObj); - Vec_IntFillTwo( vFanins, 2, iObj, iObjNew ); - iObjNew = Wlc_ObjCreate( p, WLC_OBJ_LOGIC_AND, 0, 0, 0, vFanins ); - // note that a pointer to Wlc_Obj_t (for example, pObj) can be invalidated after a call to - // Wlc_ObjCreate() due to a possible realloc of the internal array of objects... - pObj = Wlc_NtkObj( p, iObj ); - // update PO/CO arrays - assert( Vec_IntEntry(&p->vPos, i) == iObj ); - assert( Vec_IntEntry(&p->vCos, i) == iObj ); - Vec_IntWriteEntry( &p->vPos, i, iObjNew ); - Vec_IntWriteEntry( &p->vCos, i, iObjNew ); - // transfer the PO attribute - Wlc_NtkObj(p, iObjNew)->fIsPo = 1; - assert( pObj->fIsPo ); - pObj->fIsPo = 0; + Aig_Man_t * pAig; + Abc_Cex_t * pCex; + Vec_Int_t * vPisNew, * vRefine; + Gia_Man_t * pGia, * pTemp; + Wlc_Ntk_t * pAbs; + + if ( pPars->fVerbose ) + printf( "\nIteration %d:\n", nIters ); + + // get abstracted GIA and the set of pseudo-PIs (vPisNew) + pAbs = Wlc_NtkAbs( p, pPars, vUnmark, &vPisNew, NULL, pPars->fVerbose ); + pGia = Wlc_NtkBitBlast( pAbs, NULL, -1, 0, 0, 0, 0 ); + + // if the abstraction has flops with DC-init state, + // new PIs were introduced by bit-blasting at the end of the PI list + // here we move these variables to be *before* PPIs, because + // PPIs are supposed to be at the end of the PI list for refinement + nDcFlops = Wlc_NtkDcFlopNum(pAbs); + if ( nDcFlops > 0 ) // DC-init flops are present + { + pGia = Gia_ManPermuteInputs( pTemp = pGia, Wlc_NtkCountObjBits(p, vPisNew), nDcFlops ); + Gia_ManStop( pTemp ); + } + // if the word-level outputs have to be XORs, this is a place to do it + if ( pPars->fXorOutput ) + { + pGia = Gia_ManTransformMiter2( pTemp = pGia ); + Gia_ManStop( pTemp ); + } + if ( pPars->fVerbose ) + { + printf( "Derived abstraction with %d objects and %d PPIs. Bit-blasted AIG stats are:\n", Wlc_NtkObjNum(pAbs), Vec_IntSize(vPisNew) ); + Gia_ManPrintStats( pGia, NULL ); + } + Wlc_NtkFree( pAbs ); + + // try to prove abstracted GIA by converting it to AIG and calling PDR + pAig = Gia_ManToAigSimple( pGia ); + RetValue = Pdr_ManSolve( pAig, pPdrPars ); + pCex = pAig->pSeqModel; pAig->pSeqModel = NULL; + Aig_ManStop( pAig ); + + // consider outcomes + if ( pCex == NULL ) + { + assert( RetValue ); // proved or undecided + Gia_ManStop( pGia ); + Vec_IntFree( vPisNew ); + break; + } + + // perform refinement + vRefine = Wlc_NtkAbsRefinement( p, pGia, pCex, vPisNew ); + Gia_ManStop( pGia ); + Vec_IntFree( vPisNew ); + if ( vRefine == NULL ) // real CEX + { + Abc_CexFree( pCex ); // return CEX in the future + break; + } + + // update the set of objects to be un-abstracted + nNodes = Wlc_NtkRemoveFromAbstraction( p, vRefine, vUnmark ); + if ( pPars->fVerbose ) + printf( "Refinement of CEX in frame %d came up with %d un-abstacted PPIs, whose MFFCs include %d objects.\n", pCex->iFrame, Vec_IntSize(vRefine), nNodes ); + Vec_IntFree( vRefine ); + Abc_CexFree( pCex ); } - // cleanup - Vec_IntFree( vUifConstrs ); - Vec_IntFree( vCompares ); - Vec_IntFree( vFanins ); - if ( vPairs != vPairsInit ) - Vec_IntFree( vPairs ); - // reconstruct topological order - pNew = Wlc_NtkDupDfs( p ); - Wlc_NtkTransferNames( pNew, p ); - return pNew; + Vec_BitFree( vUnmark ); + // report the result + if ( pPars->fVerbose ) + printf( "\n" ); + printf( "Abstraction " ); + if ( RetValue == 0 ) + printf( "resulted in a real CEX" ); + else if ( RetValue == 1 ) + printf( "is successfully proved" ); + else + printf( "timed out" ); + printf( " after %d iterations. ", nIters ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + return RetValue; } //////////////////////////////////////////////////////////////////////// diff --git a/src/base/wlc/wlcAbs2.c b/src/base/wlc/wlcAbs2.c new file mode 100644 index 00000000..9bccdf62 --- /dev/null +++ b/src/base/wlc/wlcAbs2.c @@ -0,0 +1,410 @@ +/**CFile**************************************************************** + + FileName [wlcAbs2.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Verilog parser.] + + Synopsis [Abstraction for word-level networks.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - August 22, 2014.] + + Revision [$Id: wlcAbs2.c,v 1.00 2014/09/12 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "wlc.h" +#include "proof/pdr/pdr.h" +#include "aig/gia/giaAig.h" +#include "sat/bmc/bmc.h" + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Mark operators that meet the abstraction criteria.] + + Description [This procedure returns the array of objects (vLeaves) that + should be abstracted because of their high bit-width. It uses input array (vUnmark) + to not abstract those objects that have been refined in the previous rounds.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static Vec_Bit_t * Wlc_NtkAbsMarkOpers( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t * vUnmark, int fVerbose ) +{ + Vec_Bit_t * vLeaves = Vec_BitStart( Wlc_NtkObjNumMax(p) ); + Wlc_Obj_t * pObj; int i, Count[4] = {0}; + Wlc_NtkForEachObj( p, pObj, i ) + { + if ( vUnmark && Vec_BitEntry(vUnmark, i) ) // not allow this object to be abstracted away + continue; + if ( pObj->Type == WLC_OBJ_ARI_ADD || pObj->Type == WLC_OBJ_ARI_SUB || pObj->Type == WLC_OBJ_ARI_MINUS ) + { + if ( Wlc_ObjRange(pObj) >= pPars->nBitsAdd ) + Vec_BitWriteEntry( vLeaves, Wlc_ObjId(p, pObj), 1 ), Count[0]++; + continue; + } + if ( pObj->Type == WLC_OBJ_ARI_MULTI || pObj->Type == WLC_OBJ_ARI_DIVIDE || pObj->Type == WLC_OBJ_ARI_REM || pObj->Type == WLC_OBJ_ARI_MODULUS ) + { + if ( Wlc_ObjRange(pObj) >= pPars->nBitsMul ) + Vec_BitWriteEntry( vLeaves, Wlc_ObjId(p, pObj), 1 ), Count[1]++; + continue; + } + if ( pObj->Type == WLC_OBJ_MUX ) + { + if ( Wlc_ObjRange(pObj) >= pPars->nBitsMux ) + Vec_BitWriteEntry( vLeaves, Wlc_ObjId(p, pObj), 1 ), Count[2]++; + continue; + } + if ( Wlc_ObjIsCi(pObj) && !Wlc_ObjIsPi(pObj) ) + { + if ( Wlc_ObjRange(pObj) >= pPars->nBitsFlop ) + Vec_BitWriteEntry( vLeaves, Wlc_ObjId(p, pObj), 1 ), Count[3]++; + continue; + } + } + if ( fVerbose ) + printf( "Abstraction engine marked %d adds/subs, %d muls/divs, %d muxes, and %d flops to be abstracted away.\n", Count[0], Count[1], Count[2], Count[3] ); + return vLeaves; +} + +/**Function************************************************************* + + Synopsis [Marks nodes to be included in the abstracted network.] + + Description [Marks all objects that will be included in the abstracted model. + Stops at the objects (vLeaves) that are abstracted away. Returns three arrays: + a subset of original PIs (vPisOld), a subset of pseudo-PIs (vPisNew) and the + set of flops present as flops in the abstracted network.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static void Wlc_NtkAbsMarkNodes_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Bit_t * vLeaves, Vec_Int_t * vPisOld, Vec_Int_t * vPisNew, Vec_Int_t * vFlops ) +{ + int i, iFanin; + if ( pObj->Mark ) + return; + pObj->Mark = 1; + if ( Vec_BitEntry(vLeaves, Wlc_ObjId(p, pObj)) ) + { + assert( !Wlc_ObjIsPi(pObj) ); + Vec_IntPush( vPisNew, Wlc_ObjId(p, pObj) ); + return; + } + if ( Wlc_ObjIsCi(pObj) ) + { + if ( Wlc_ObjIsPi(pObj) ) + Vec_IntPush( vPisOld, Wlc_ObjId(p, pObj) ); + else + Vec_IntPush( vFlops, Wlc_ObjId(p, pObj) ); + return; + } + Wlc_ObjForEachFanin( pObj, iFanin, i ) + Wlc_NtkAbsMarkNodes_rec( p, Wlc_NtkObj(p, iFanin), vLeaves, vPisOld, vPisNew, vFlops ); +} +static void Wlc_NtkAbsMarkNodes( Wlc_Ntk_t * p, Vec_Bit_t * vLeaves, Vec_Int_t * vPisOld, Vec_Int_t * vPisNew, Vec_Int_t * vFlops ) +{ + Wlc_Obj_t * pObj; + int i, Count = 0; + Wlc_NtkCleanMarks( p ); + Wlc_NtkForEachCo( p, pObj, i ) + Wlc_NtkAbsMarkNodes_rec( p, pObj, vLeaves, vPisOld, vPisNew, vFlops ); + Wlc_NtkForEachObjVec( vFlops, p, pObj, i ) + Wlc_NtkAbsMarkNodes_rec( p, Wlc_ObjFo2Fi(p, pObj), vLeaves, vPisOld, vPisNew, vFlops ); + Wlc_NtkForEachObj( p, pObj, i ) + Count += pObj->Mark; +// printf( "Collected %d old PIs, %d new PIs, %d flops, and %d other objects.\n", +// Vec_IntSize(vPisOld), Vec_IntSize(vPisNew), Vec_IntSize(vFlops), +// Count - Vec_IntSize(vPisOld) - Vec_IntSize(vPisNew) - Vec_IntSize(vFlops) ); + Vec_IntSort( vPisOld, 0 ); + Vec_IntSort( vPisNew, 0 ); + Vec_IntSort( vFlops, 0 ); + Wlc_NtkCleanMarks( p ); +} + +/**Function************************************************************* + + Synopsis [Derive word-level abstracted model based on the parameter values.] + + Description [Retuns the word-level abstracted network and the set of pseudo-PIs + (vPisNew), which were created during abstraction. If the abstraction is + satisfiable, some of the pseudo-PIs will be un-abstracted. These pseudo-PIs + and their MFFC cones will be listed in the array (vUnmark), which will + force the abstraction to not stop at these pseudo-PIs in the future.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static Wlc_Ntk_t * Wlc_NtkAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t * vUnmark, Vec_Int_t ** pvPisNew, int fVerbose ) +{ + Wlc_Ntk_t * pNtkNew = NULL; + Vec_Int_t * vPisOld = Vec_IntAlloc( 100 ); + Vec_Int_t * vPisNew = Vec_IntAlloc( 100 ); + Vec_Int_t * vFlops = Vec_IntAlloc( 100 ); + Vec_Bit_t * vLeaves = Wlc_NtkAbsMarkOpers( p, pPars, vUnmark, fVerbose ); + Wlc_NtkAbsMarkNodes( p, vLeaves, vPisOld, vPisNew, vFlops ); + Vec_BitFree( vLeaves ); + pNtkNew = Wlc_NtkDupDfsAbs( p, vPisOld, vPisNew, vFlops ); + Vec_IntFree( vPisOld ); + Vec_IntFree( vFlops ); + if ( pvPisNew ) + *pvPisNew = vPisNew; + else + Vec_IntFree( vPisNew ); + return pNtkNew; +} + +/**Function************************************************************* + + Synopsis [Find what objects need to be un-abstracted.] + + Description [Returns a subset of pseudo-PIs (vPisNew), which will be + prevented from being abstracted in the future rounds of abstraction. + The AIG manager (pGia) is a bit-level view of the abstracted model. + The counter-example (pCex) is used to find waht PPIs to refine.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static Vec_Int_t * Wlc_NtkAbsRefinement( Wlc_Ntk_t * p, Gia_Man_t * pGia, Abc_Cex_t * pCex, Vec_Int_t * vPisNew ) +{ + Vec_Int_t * vRefine = Vec_IntAlloc( 100 ); + Abc_Cex_t * pCexCare; + Wlc_Obj_t * pObj; + // count the number of bit-level PPIs and map them into word-level objects they were derived from + int f, i, b, nRealPis, nPpiBits = 0; + Vec_Int_t * vMap = Vec_IntStartFull( pCex->nPis ); + Wlc_NtkForEachObjVec( vPisNew, p, pObj, i ) + for ( b = 0; b < Wlc_ObjRange(pObj); b++ ) + Vec_IntWriteEntry( vMap, nPpiBits++, Wlc_ObjId(p, pObj) ); + // since PPIs are ordered last, the previous bits are real PIs + nRealPis = pCex->nPis - nPpiBits; + // find the care-set + pCexCare = Bmc_CexCareMinimizeAig( pGia, nRealPis, pCex, 1, 0, 0 ); + assert( pCexCare->nPis == pCex->nPis ); + // detect care PPIs + for ( f = 0; f <= pCexCare->iFrame; f++ ) + for ( i = nRealPis; i < pCexCare->nPis; i++ ) + if ( Abc_InfoHasBit(pCexCare->pData, pCexCare->nRegs + pCexCare->nPis * f + i) ) + Vec_IntPushUniqueOrder( vRefine, Vec_IntEntry(vMap, i-nRealPis) ); + Abc_CexFree( pCexCare ); + Vec_IntFree( vMap ); + if ( Vec_IntSize(vRefine) == 0 )// real CEX + Vec_IntFreeP( &vRefine ); + return vRefine; +} + +/**Function************************************************************* + + Synopsis [Mark MFFC cones of the un-abstracted objects.] + + Description [The MFFC cones of the objects in vRefine are traversed + and all their nodes are marked in vUnmark.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static int Wlc_NtkNodeDeref_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pNode, Vec_Bit_t * vUnmark ) +{ + int i, Fanin, Counter = 1; + if ( Wlc_ObjIsCi(pNode) ) + return 0; + Vec_BitWriteEntry( vUnmark, Wlc_ObjId(p, pNode), 1 ); + Wlc_ObjForEachFanin( pNode, Fanin, i ) + { + Vec_IntAddToEntry( &p->vRefs, Fanin, -1 ); + if ( Vec_IntEntry(&p->vRefs, Fanin) == 0 ) + Counter += Wlc_NtkNodeDeref_rec( p, Wlc_NtkObj(p, Fanin), vUnmark ); + } + return Counter; +} +static int Wlc_NtkNodeRef_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pNode ) +{ + int i, Fanin, Counter = 1; + if ( Wlc_ObjIsCi(pNode) ) + return 0; + Wlc_ObjForEachFanin( pNode, Fanin, i ) + { + if ( Vec_IntEntry(&p->vRefs, Fanin) == 0 ) + Counter += Wlc_NtkNodeRef_rec( p, Wlc_NtkObj(p, Fanin) ); + Vec_IntAddToEntry( &p->vRefs, Fanin, 1 ); + } + return Counter; +} +static int Wlc_NtkMarkMffc( Wlc_Ntk_t * p, Wlc_Obj_t * pNode, Vec_Bit_t * vUnmark ) +{ + int Count1, Count2; + // if this is a flop output, compute MFFC of the corresponding flop input + while ( Wlc_ObjIsCi(pNode) ) + { + Vec_BitWriteEntry( vUnmark, Wlc_ObjId(p, pNode), 1 ); + pNode = Wlc_ObjFo2Fi(p, pNode); + } + assert( !Wlc_ObjIsCi(pNode) ); + // dereference the node (and set the bits in vUnmark) + Count1 = Wlc_NtkNodeDeref_rec( p, pNode, vUnmark ); + // reference it back + Count2 = Wlc_NtkNodeRef_rec( p, pNode ); + assert( Count1 == Count2 ); + return Count1; +} +static int Wlc_NtkRemoveFromAbstraction( Wlc_Ntk_t * p, Vec_Int_t * vRefine, Vec_Bit_t * vUnmark ) +{ + Wlc_Obj_t * pObj; int i, nNodes = 0; + if ( Vec_IntSize(&p->vRefs) == 0 ) + Wlc_NtkSetRefs( p ); + Wlc_NtkForEachObjVec( vRefine, p, pObj, i ) + nNodes += Wlc_NtkMarkMffc( p, pObj, vUnmark ); + return nNodes; +} + +/**Function************************************************************* + + Synopsis [Performs abstraction.] + + Description [Derives initial abstraction based on user-specified + parameter values, which tell what is the smallest bit-width of a + primitive that is being abstracted away. Currently only add/sub, + mul/div, mux, and flop are supported with individual parameters. + The second step is to refine the initial abstraction until the + point when the property is proved.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Wlc_NtkAbsCore2( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) +{ + abctime clk = Abc_Clock(); + int nIters, nNodes, nDcFlops, RetValue = -1; + // start the bitmap to mark objects that cannot be abstracted because of refinement + // currently, this bitmap is empty because abstraction begins without refinement + Vec_Bit_t * vUnmark = Vec_BitStart( Wlc_NtkObjNumMax(p) ); + // set up parameters to run PDR + Pdr_Par_t PdrPars, * pPdrPars = &PdrPars; + Pdr_ManSetDefaultParams( pPdrPars ); + pPdrPars->fUseAbs = 1; // use 'pdr -t' (on-the-fly abstraction) + pPdrPars->fCtgs = 1; // use 'pdr -nc' (improved generalization) + pPdrPars->fSkipDown = 0; // use 'pdr -nc' (improved generalization) + //pPdrPars->nRestLimit = 500; // reset queue or proof-obligations when it gets larger than this + pPdrPars->fVerbose = pPars->fPdrVerbose; + // perform refinement iterations + for ( nIters = 1; nIters < pPars->nIterMax; nIters++ ) + { + Aig_Man_t * pAig; + Abc_Cex_t * pCex; + Vec_Int_t * vPisNew, * vRefine; + Gia_Man_t * pGia, * pTemp; + Wlc_Ntk_t * pAbs; + + if ( pPars->fVerbose ) + printf( "\nIteration %d:\n", nIters ); + + // get abstracted GIA and the set of pseudo-PIs (vPisNew) + pAbs = Wlc_NtkAbs( p, pPars, vUnmark, &vPisNew, pPars->fVerbose ); + pGia = Wlc_NtkBitBlast( pAbs, NULL, -1, 0, 0, 0, 0 ); + + // if the abstraction has flops with DC-init state, + // new PIs were introduced by bit-blasting at the end of the PI list + // here we move these variables to be *before* PPIs, because + // PPIs are supposed to be at the end of the PI list for refinement + nDcFlops = Wlc_NtkDcFlopNum(pAbs); + if ( nDcFlops > 0 ) // DC-init flops are present + { + pGia = Gia_ManPermuteInputs( pTemp = pGia, Wlc_NtkCountObjBits(p, vPisNew), nDcFlops ); + Gia_ManStop( pTemp ); + } + // if the word-level outputs have to be XORs, this is a place to do it + if ( pPars->fXorOutput ) + { + pGia = Gia_ManTransformMiter2( pTemp = pGia ); + Gia_ManStop( pTemp ); + } + if ( pPars->fVerbose ) + { + printf( "Derived abstraction with %d objects and %d PPIs. Bit-blasted AIG stats are:\n", Wlc_NtkObjNum(pAbs), Vec_IntSize(vPisNew) ); + Gia_ManPrintStats( pGia, NULL ); + } + Wlc_NtkFree( pAbs ); + + // try to prove abstracted GIA by converting it to AIG and calling PDR + pAig = Gia_ManToAigSimple( pGia ); + RetValue = Pdr_ManSolve( pAig, pPdrPars ); + pCex = pAig->pSeqModel; pAig->pSeqModel = NULL; + Aig_ManStop( pAig ); + + // consider outcomes + if ( pCex == NULL ) + { + assert( RetValue ); // proved or undecided + Gia_ManStop( pGia ); + Vec_IntFree( vPisNew ); + break; + } + + // perform refinement + vRefine = Wlc_NtkAbsRefinement( p, pGia, pCex, vPisNew ); + Gia_ManStop( pGia ); + Vec_IntFree( vPisNew ); + if ( vRefine == NULL ) // real CEX + { + Abc_CexFree( pCex ); // return CEX in the future + break; + } + + // update the set of objects to be un-abstracted + nNodes = Wlc_NtkRemoveFromAbstraction( p, vRefine, vUnmark ); + if ( pPars->fVerbose ) + printf( "Refinement of CEX in frame %d came up with %d un-abstacted PPIs, whose MFFCs include %d objects.\n", pCex->iFrame, Vec_IntSize(vRefine), nNodes ); + Vec_IntFree( vRefine ); + Abc_CexFree( pCex ); + } + Vec_BitFree( vUnmark ); + // report the result + if ( pPars->fVerbose ) + printf( "\n" ); + printf( "Abstraction " ); + if ( RetValue == 0 ) + printf( "resulted in a real CEX" ); + else if ( RetValue == 1 ) + printf( "is successfully proved" ); + else + printf( "timed out" ); + printf( " after %d iterations. ", nIters ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + return RetValue; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c index ec3b040d..f4de8ee6 100644 --- a/src/base/wlc/wlcBlast.c +++ b/src/base/wlc/wlcBlast.c @@ -643,6 +643,41 @@ void Wlc_IntInsert( Vec_Int_t * vProd, Vec_Int_t * vLevel, int Node, int Level ) Vec_IntInsert( vProd, i + 1, Node ); Vec_IntInsert( vLevel, i + 1, Level ); } +void Wlc_BlastPrintMatrix( Gia_Man_t * p, Vec_Wec_t * vProds ) +{ + int fVerbose = 0; + Vec_Int_t * vSupp = Vec_IntAlloc( 100 ); + Vec_Wrd_t * vTemp = Vec_WrdStart( Gia_ManObjNum(p) ); + Vec_Int_t * vLevel; word Truth; + int i, k, iLit; + Vec_WecForEachLevel( vProds, vLevel, i ) + Vec_IntForEachEntry( vLevel, iLit, k ) + if ( Gia_ObjIsAnd(Gia_ManObj(p, Abc_Lit2Var(iLit))) ) + Vec_IntPushUnique( vSupp, Abc_Lit2Var(iLit) ); + printf( "Booth partial products: %d pps, %d unique, %d nodes.\n", + Vec_WecSizeSize(vProds), Vec_IntSize(vSupp), Gia_ManAndNum(p) ); + Vec_IntPrint( vSupp ); + + if ( fVerbose ) + Vec_WecForEachLevel( vProds, vLevel, i ) + Vec_IntForEachEntry( vLevel, iLit, k ) + { + printf( "Obj = %4d : ", Abc_Lit2Var(iLit) ); + printf( "Compl = %d ", Abc_LitIsCompl(iLit) ); + printf( "Rank = %2d ", i ); + Truth = Gia_ObjComputeTruth6Cis( p, iLit, vSupp, vTemp ); + Extra_PrintHex( stdout, (unsigned*)&Truth, Vec_IntSize(vSupp) ); + if ( Vec_IntSize(vSupp) == 4 ) printf( " " ); + if ( Vec_IntSize(vSupp) == 3 ) printf( " " ); + if ( Vec_IntSize(vSupp) <= 2 ) printf( " " ); + printf( " " ); + Vec_IntPrint( vSupp ); + if ( k == Vec_IntSize(vLevel)-1 ) + printf( "\n" ); + } + Vec_IntFree( vSupp ); + Vec_WrdFree( vTemp ); +} void Wlc_BlastReduceMatrix( Gia_Man_t * pNew, Vec_Wec_t * vProds, Vec_Wec_t * vLevels, Vec_Int_t * vRes ) { Vec_Int_t * vLevel, * vProd; @@ -812,6 +847,7 @@ void Wlc_BlastBooth( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA, int Vec_WecPush( vLevels, k, 0 ); } //Vec_WecPrint( vProds, 0 ); + //Wlc_BlastPrintMatrix( pNew, vProds ); //printf( "Cutoff ID for partial products = %d.\n", Gia_ManObjNum(pNew) ); Wlc_BlastReduceMatrix( pNew, vProds, vLevels, vRes ); @@ -836,6 +872,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in { int fVerbose = 0; int fUseOldMultiplierBlasting = 0; + int fSkipBitRange = 0; Tim_Man_t * pManTime = NULL; Gia_Man_t * pTemp, * pNew, * pExtra = NULL; Wlc_Obj_t * pObj; @@ -1381,7 +1418,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in } else { - pNew = Gia_ManDupZeroUndc( pTemp = pNew, p->pInits, fGiaSimple, 1 ); + pNew = Gia_ManDupZeroUndc( pTemp = pNew, p->pInits, fGiaSimple, 0 ); Gia_ManDupRemapLiterals( vBits, pTemp ); Gia_ManStop( pTemp ); } @@ -1412,7 +1449,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in { char * pName = Wlc_ObjName(p, Wlc_ObjId(p, pObj)); nRange = Wlc_ObjRange( pObj ); - if ( nRange == 1 ) + if ( fSkipBitRange && nRange == 1 ) Vec_PtrPush( pNew->vNamesIn, Abc_UtilStrsav(pName) ); else for ( k = 0; k < nRange; k++ ) @@ -1439,7 +1476,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in { char * pName = Wlc_ObjName(p, Wlc_ObjId(p, pObj)); nRange = Wlc_ObjRange( pObj ); - if ( nRange == 1 ) + if ( fSkipBitRange && nRange == 1 ) Vec_PtrPush( pNew->vNamesIn, Abc_UtilStrsav(pName) ); else for ( k = 0; k < nRange; k++ ) @@ -1462,7 +1499,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in { char * pName = Wlc_ObjName(p, Wlc_ObjId(p, pObj)); nRange = Wlc_ObjRange( pObj ); - if ( nRange == 1 ) + if ( fSkipBitRange && nRange == 1 ) Vec_PtrPush( pNew->vNamesOut, Abc_UtilStrsav(pName) ); else for ( k = 0; k < nRange; k++ ) @@ -1477,7 +1514,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in { char * pName = Wlc_ObjName(p, Wlc_ObjId(p, pObj)); nRange = Wlc_ObjRange( pObj ); - if ( nRange == 1 ) + if ( fSkipBitRange && nRange == 1 ) Vec_PtrPush( pNew->vNamesOut, Abc_UtilStrsav(pName) ); else for ( k = 0; k < nRange; k++ ) @@ -1496,7 +1533,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in { char * pName = Wlc_ObjName(p, Wlc_ObjId(p, pObj)); nRange = Wlc_ObjRange( pObj ); - if ( nRange == 1 ) + if ( fSkipBitRange && nRange == 1 ) Vec_PtrPush( pNew->vNamesOut, Abc_UtilStrsav(pName) ); else for ( k = 0; k < nRange; k++ ) @@ -1509,7 +1546,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in assert( Vec_PtrSize(pNew->vNamesOut) == Gia_ManCoNum(pNew) ); } - pNew->pSpec = Abc_UtilStrsav( p->pSpec ? p->pSpec : p->pName ); + //pNew->pSpec = Abc_UtilStrsav( p->pSpec ? p->pSpec : p->pName ); // dump the miter parts if ( 0 ) { diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c index f3eb6dd7..df736e70 100644 --- a/src/base/wlc/wlcCom.c +++ b/src/base/wlc/wlcCom.c @@ -28,22 +28,31 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static int Abc_CommandReadWlc ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandWriteWlc ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandPs ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandBlast ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandPsInv ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandGetInv ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandProfile ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandTest ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandReadWlc ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandWriteWlc ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandPs ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandCone ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbs ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandPdrAbs ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbs2 ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandBlast ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandProfile ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandShortNames ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandShow ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandTest ( Abc_Frame_t * pAbc, int argc, char ** argv ); + +static int Abc_CommandInvPs ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandInvPrint ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandInvCheck ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandInvGet ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandInvPut ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandInvMin ( Abc_Frame_t * pAbc, int argc, char ** argv ); static inline Wlc_Ntk_t * Wlc_AbcGetNtk( Abc_Frame_t * pAbc ) { return (Wlc_Ntk_t *)pAbc->pAbcWlc; } static inline void Wlc_AbcFreeNtk( Abc_Frame_t * pAbc ) { if ( pAbc->pAbcWlc ) Wlc_NtkFree(Wlc_AbcGetNtk(pAbc)); } static inline void Wlc_AbcUpdateNtk( Abc_Frame_t * pAbc, Wlc_Ntk_t * pNtk ) { Wlc_AbcFreeNtk(pAbc); pAbc->pAbcWlc = pNtk; } static inline Vec_Int_t * Wlc_AbcGetInv( Abc_Frame_t * pAbc ) { return pAbc->pAbcWlcInv; } -static inline Vec_Int_t * Wlc_AbcGetCnf( Abc_Frame_t * pAbc ) { return pAbc->pAbcWlcCnf; } -static inline Vec_Str_t * Wlc_AbcGetStr( Abc_Frame_t * pAbc ) { return pAbc->pAbcWlcStr; } //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -62,14 +71,25 @@ static inline Vec_Str_t * Wlc_AbcGetStr( Abc_Frame_t * pAbc ) ******************************************************************************/ void Wlc_Init( Abc_Frame_t * pAbc ) { - Cmd_CommandAdd( pAbc, "Word level", "%read", Abc_CommandReadWlc, 0 ); - Cmd_CommandAdd( pAbc, "Word level", "%write", Abc_CommandWriteWlc, 0 ); - Cmd_CommandAdd( pAbc, "Word level", "%ps", Abc_CommandPs, 0 ); - Cmd_CommandAdd( pAbc, "Word level", "%blast", Abc_CommandBlast, 0 ); - Cmd_CommandAdd( pAbc, "Word level", "%psinv", Abc_CommandPsInv, 0 ); - Cmd_CommandAdd( pAbc, "Word level", "%getinv", Abc_CommandGetInv, 0 ); - Cmd_CommandAdd( pAbc, "Word level", "%profile", Abc_CommandProfile, 0 ); - Cmd_CommandAdd( pAbc, "Word level", "%test", Abc_CommandTest, 0 ); + Cmd_CommandAdd( pAbc, "Word level", "%read", Abc_CommandReadWlc, 0 ); + Cmd_CommandAdd( pAbc, "Word level", "%write", Abc_CommandWriteWlc, 0 ); + Cmd_CommandAdd( pAbc, "Word level", "%ps", Abc_CommandPs, 0 ); + Cmd_CommandAdd( pAbc, "Word level", "%cone", Abc_CommandCone, 0 ); + Cmd_CommandAdd( pAbc, "Word level", "%abs", Abc_CommandAbs, 0 ); + Cmd_CommandAdd( pAbc, "Word level", "%pdra", Abc_CommandPdrAbs, 0 ); + Cmd_CommandAdd( pAbc, "Word level", "%abs2", Abc_CommandAbs2, 0 ); + Cmd_CommandAdd( pAbc, "Word level", "%blast", Abc_CommandBlast, 0 ); + Cmd_CommandAdd( pAbc, "Word level", "%profile", Abc_CommandProfile, 0 ); + Cmd_CommandAdd( pAbc, "Word level", "%short_names", Abc_CommandShortNames, 0 ); + Cmd_CommandAdd( pAbc, "Word level", "%show", Abc_CommandShow, 0 ); + Cmd_CommandAdd( pAbc, "Word level", "%test", Abc_CommandTest, 0 ); + + Cmd_CommandAdd( pAbc, "Word level", "inv_ps", Abc_CommandInvPs, 0 ); + Cmd_CommandAdd( pAbc, "Word level", "inv_print", Abc_CommandInvPrint, 0 ); + Cmd_CommandAdd( pAbc, "Word level", "inv_check", Abc_CommandInvCheck, 0 ); + Cmd_CommandAdd( pAbc, "Word level", "inv_get", Abc_CommandInvGet, 0 ); + Cmd_CommandAdd( pAbc, "Word level", "inv_put", Abc_CommandInvPut, 0 ); + Cmd_CommandAdd( pAbc, "Word level", "inv_min", Abc_CommandInvMin, 0 ); } /**Function******************************************************************** @@ -275,15 +295,20 @@ usage: int Abc_CommandPs( Abc_Frame_t * pAbc, int argc, char ** argv ) { Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc); + int fShowCones = 0; int fShowMulti = 0; int fShowAdder = 0; int fDistrib = 0; + int fTwoSides = 0; int c, fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "madvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "cmadtvh" ) ) != EOF ) { switch ( c ) { + case 'c': + fShowCones ^= 1; + break; case 'm': fShowMulti ^= 1; break; @@ -293,6 +318,9 @@ int Abc_CommandPs( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'd': fDistrib ^= 1; break; + case 't': + fTwoSides ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -307,18 +335,110 @@ int Abc_CommandPs( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( 1, "Abc_CommandPs(): There is no current design.\n" ); return 0; } - Wlc_NtkPrintStats( pNtk, fDistrib, fVerbose ); + Wlc_NtkPrintStats( pNtk, fDistrib, fTwoSides, fVerbose ); + if ( fShowCones ) + Wlc_NtkProfileCones( pNtk ); if ( fShowMulti ) Wlc_NtkPrintNodes( pNtk, WLC_OBJ_ARI_MULTI ); if ( fShowAdder ) Wlc_NtkPrintNodes( pNtk, WLC_OBJ_ARI_ADD ); return 0; usage: - Abc_Print( -2, "usage: %%ps [-madvh]\n" ); + Abc_Print( -2, "usage: %%ps [-cmadtvh]\n" ); Abc_Print( -2, "\t prints statistics\n" ); - Abc_Print( -2, "\t-m : toggle printing multipliers [default = %s]\n", fShowMulti? "yes": "no" ); - Abc_Print( -2, "\t-a : toggle printing adders [default = %s]\n", fShowAdder? "yes": "no" ); - Abc_Print( -2, "\t-d : toggle printing distrubition [default = %s]\n", fDistrib? "yes": "no" ); + Abc_Print( -2, "\t-c : toggle printing cones [default = %s]\n", fShowCones? "yes": "no" ); + Abc_Print( -2, "\t-m : toggle printing multipliers [default = %s]\n", fShowMulti? "yes": "no" ); + Abc_Print( -2, "\t-a : toggle printing adders [default = %s]\n", fShowAdder? "yes": "no" ); + Abc_Print( -2, "\t-d : toggle printing distrubition [default = %s]\n", fDistrib? "yes": "no" ); + Abc_Print( -2, "\t-t : toggle printing stats for LHS and RHS [default = %s]\n", fTwoSides? "yes": "no" ); + Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + +/**Function******************************************************************** + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int Abc_CommandCone( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc); + int c, iOutput = -1, Range = 1, fAllPis = 0, fSeq = 0, fVerbose = 0; + char * pName; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "ORisvh" ) ) != EOF ) + { + switch ( c ) + { + case 'O': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-O\" should be followed by an integer.\n" ); + goto usage; + } + iOutput = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( iOutput < 0 ) + goto usage; + break; + case 'R': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" ); + goto usage; + } + Range = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( Range < 0 ) + goto usage; + break; + case 'i': + fAllPis ^= 1; + break; + case 's': + fSeq ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pNtk == NULL ) + { + Abc_Print( 1, "Abc_CommandCone(): There is no current design.\n" ); + return 0; + } + if ( iOutput < 0 || iOutput >= Wlc_NtkCoNum(pNtk) ) + { + Abc_Print( 1, "Abc_CommandCone(): Illegal output index (%d) (should be 0 <= num < %d).\n", iOutput, Wlc_NtkCoNum(pNtk) ); + return 0; + } + printf( "Extracting output %d as a %s word-level network.\n", iOutput, fSeq ? "sequential" : "combinational" ); + pName = Wlc_NtkNewName( pNtk, iOutput, fSeq ); + Wlc_NtkMarkCone( pNtk, iOutput, Range, fSeq, fAllPis ); + pNtk = Wlc_NtkDupDfs( pNtk, 1, fSeq ); + ABC_FREE( pNtk->pName ); + pNtk->pName = Abc_UtilStrsav( pName ); + Wlc_AbcUpdateNtk( pAbc, pNtk ); + return 0; +usage: + Abc_Print( -2, "usage: %%cone [-OR num] [-isvh]\n" ); + Abc_Print( -2, "\t extracts logic cone of one or more word-level outputs\n" ); + Abc_Print( -2, "\t-O num : zero-based index of the first word-level output to extract [default = %d]\n", iOutput ); + Abc_Print( -2, "\t-R num : total number of word-level outputs to extract [default = %d]\n", Range ); + Abc_Print( -2, "\t-i : toggle using support composed of all primary inputs [default = %s]\n", fAllPis? "yes": "no" ); + Abc_Print( -2, "\t-s : toggle performing extracting sequential cones [default = %s]\n", fSeq? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; @@ -335,6 +455,357 @@ usage: SeeAlso [] ******************************************************************************/ +int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc); + Wlc_Par_t Pars, * pPars = &Pars; + int c; + Wlc_ManSetDefaultParams( pPars ); + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFIcpxvwh" ) ) != EOF ) + { + switch ( c ) + { + case 'A': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-A\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nBitsAdd = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nBitsAdd < 0 ) + goto usage; + break; + case 'M': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nBitsMul = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nBitsMul < 0 ) + goto usage; + break; + case 'X': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-X\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nBitsMux = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nBitsMux < 0 ) + goto usage; + break; + case 'F': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nBitsFlop = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nBitsFlop < 0 ) + goto usage; + break; + case 'I': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nIterMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nIterMax < 0 ) + goto usage; + break; + case 'x': + pPars->fXorOutput ^= 1; + break; + case 'c': + pPars->fCheckClauses ^= 1; + break; + case 'p': + pPars->fPushClauses ^= 1; + break; + case 'v': + pPars->fVerbose ^= 1; + break; + case 'w': + pPars->fPdrVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pNtk == NULL ) + { + Abc_Print( 1, "Abc_CommandCone(): There is no current design.\n" ); + return 0; + } + Wlc_NtkPdrAbs( pNtk, pPars ); + return 0; +usage: + Abc_Print( -2, "usage: %%pdra [-AMXFI num] [-cpxvwh]\n" ); + Abc_Print( -2, "\t abstraction for word-level networks\n" ); + Abc_Print( -2, "\t-A num : minimum bit-width of an adder/subtractor to abstract [default = %d]\n", pPars->nBitsAdd ); + Abc_Print( -2, "\t-M num : minimum bit-width of a multiplier to abstract [default = %d]\n", pPars->nBitsMul ); + Abc_Print( -2, "\t-X num : minimum bit-width of a MUX operator to abstract [default = %d]\n", pPars->nBitsMux ); + Abc_Print( -2, "\t-F num : minimum bit-width of a flip-flop to abstract [default = %d]\n", pPars->nBitsFlop ); + Abc_Print( -2, "\t-I num : maximum number of CEGAR iterations [default = %d]\n", pPars->nIterMax ); + Abc_Print( -2, "\t-x : toggle XORing outputs of word-level miter [default = %s]\n", pPars->fXorOutput? "yes": "no" ); + Abc_Print( -2, "\t-c : toggle checking clauses in the reloaded trace [default = %s]\n", pPars->fCheckClauses? "yes": "no" ); + Abc_Print( -2, "\t-p : toggle pushing clauses in the reloaded trace [default = %s]\n", pPars->fPushClauses? "yes": "no" ); + Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-w : toggle printing verbose PDR output [default = %s]\n", pPars->fPdrVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + + +/**Function******************************************************************** + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int Abc_CommandAbs( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc); + Wlc_Par_t Pars, * pPars = &Pars; + int c; + Wlc_ManSetDefaultParams( pPars ); + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFIxvwh" ) ) != EOF ) + { + switch ( c ) + { + case 'A': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-A\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nBitsAdd = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nBitsAdd < 0 ) + goto usage; + break; + case 'M': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nBitsMul = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nBitsMul < 0 ) + goto usage; + break; + case 'X': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-X\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nBitsMux = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nBitsMux < 0 ) + goto usage; + break; + case 'F': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nBitsFlop = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nBitsFlop < 0 ) + goto usage; + break; + case 'I': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nIterMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nIterMax < 0 ) + goto usage; + break; + case 'x': + pPars->fXorOutput ^= 1; + break; + case 'v': + pPars->fVerbose ^= 1; + break; + case 'w': + pPars->fPdrVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pNtk == NULL ) + { + Abc_Print( 1, "Abc_CommandCone(): There is no current design.\n" ); + return 0; + } + Wlc_NtkAbsCore( pNtk, pPars ); + return 0; +usage: + Abc_Print( -2, "usage: %%abs [-AMXFI num] [-xvwh]\n" ); + Abc_Print( -2, "\t abstraction for word-level networks\n" ); + Abc_Print( -2, "\t-A num : minimum bit-width of an adder/subtractor to abstract [default = %d]\n", pPars->nBitsAdd ); + Abc_Print( -2, "\t-M num : minimum bit-width of a multiplier to abstract [default = %d]\n", pPars->nBitsMul ); + Abc_Print( -2, "\t-X num : minimum bit-width of a MUX operator to abstract [default = %d]\n", pPars->nBitsMux ); + Abc_Print( -2, "\t-F num : minimum bit-width of a flip-flop to abstract [default = %d]\n", pPars->nBitsFlop ); + Abc_Print( -2, "\t-I num : maximum number of CEGAR iterations [default = %d]\n", pPars->nIterMax ); + Abc_Print( -2, "\t-x : toggle XORing outputs of word-level miter [default = %s]\n", pPars->fXorOutput? "yes": "no" ); + Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-w : toggle printing verbose PDR output [default = %s]\n", pPars->fPdrVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + +/**Function******************************************************************** + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int Abc_CommandAbs2( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc); + Wlc_Par_t Pars, * pPars = &Pars; + int c; + Wlc_ManSetDefaultParams( pPars ); + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFIxvwh" ) ) != EOF ) + { + switch ( c ) + { + case 'A': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-A\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nBitsAdd = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nBitsAdd < 0 ) + goto usage; + break; + case 'M': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nBitsMul = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nBitsMul < 0 ) + goto usage; + break; + case 'X': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-X\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nBitsMux = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nBitsMux < 0 ) + goto usage; + break; + case 'F': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nBitsFlop = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nBitsFlop < 0 ) + goto usage; + break; + case 'I': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nIterMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nIterMax < 0 ) + goto usage; + break; + case 'x': + pPars->fXorOutput ^= 1; + break; + case 'v': + pPars->fVerbose ^= 1; + break; + case 'w': + pPars->fPdrVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pNtk == NULL ) + { + Abc_Print( 1, "Abc_CommandCone(): There is no current design.\n" ); + return 0; + } + Wlc_NtkAbsCore2( pNtk, pPars ); + return 0; +usage: + Abc_Print( -2, "usage: %%abs2 [-AMXFI num] [-xvwh]\n" ); + Abc_Print( -2, "\t abstraction for word-level networks\n" ); + Abc_Print( -2, "\t-A num : minimum bit-width of an adder/subtractor to abstract [default = %d]\n", pPars->nBitsAdd ); + Abc_Print( -2, "\t-M num : minimum bit-width of a multiplier to abstract [default = %d]\n", pPars->nBitsMul ); + Abc_Print( -2, "\t-X num : minimum bit-width of a MUX operator to abstract [default = %d]\n", pPars->nBitsMux ); + Abc_Print( -2, "\t-F num : minimum bit-width of a flip-flop to abstract [default = %d]\n", pPars->nBitsFlop ); + Abc_Print( -2, "\t-I num : maximum number of CEGAR iterations [default = %d]\n", pPars->nIterMax ); + Abc_Print( -2, "\t-x : toggle XORing outputs of word-level miter [default = %s]\n", pPars->fXorOutput? "yes": "no" ); + Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-w : toggle printing verbose PDR output [default = %s]\n", pPars->fPdrVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + +/**Function******************************************************************** + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ int Abc_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv ) { Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc); @@ -440,10 +911,200 @@ usage: SeeAlso [] ******************************************************************************/ -int Abc_CommandPsInv( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandProfile( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc); + int c, fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + { + switch ( c ) + { + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pNtk == NULL ) + { + Abc_Print( 1, "Abc_CommandProfile(): There is no current design.\n" ); + return 0; + } + Wlc_WinProfileArith( pNtk ); + return 0; +usage: + Abc_Print( -2, "usage: %%profile [-vh]\n" ); + Abc_Print( -2, "\t profiles arithmetic components in the word-level networks\n" ); + Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + +/**Function******************************************************************** + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int Abc_CommandShortNames( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc); + int c, fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + { + switch ( c ) + { + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pNtk == NULL ) + { + Abc_Print( 1, "Abc_CommandProfile(): There is no current design.\n" ); + return 0; + } + Wlc_NtkShortNames( pNtk ); + return 0; +usage: + Abc_Print( -2, "usage: %%short_names [-vh]\n" ); + Abc_Print( -2, "\t derives short names for all objects of the network\n" ); + Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandShow( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern void Wlc_NtkShow( Wlc_Ntk_t * p, Vec_Int_t * vBold ); + Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc); + int c, fVerbose = 0; + // set defaults + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + { + switch ( c ) + { + case 'v': + fVerbose ^= 1; + break; + default: + goto usage; + } + } + if ( pNtk == NULL ) + { + Abc_Print( -1, "Empty network.\n" ); + return 1; + } + Wlc_NtkShow( pNtk, NULL ); + return 0; + +usage: + Abc_Print( -2, "usage: %%show [-h]\n" ); + Abc_Print( -2, " visualizes the network structure using DOT and GSVIEW\n" ); +#ifdef WIN32 + Abc_Print( -2, " \"dot.exe\" and \"gsview32.exe\" should be set in the paths\n" ); + Abc_Print( -2, " (\"gsview32.exe\" may be in \"C:\\Program Files\\Ghostgum\\gsview\\\")\n" ); +#endif + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + +/**Function******************************************************************** + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern void Wlc_NtkSimulateTest( Wlc_Ntk_t * p ); + Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc); + int c, fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + { + switch ( c ) + { + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pNtk == NULL ) + { + Abc_Print( 1, "Abc_CommandTest(): There is no current design.\n" ); + return 0; + } + // transform + //pNtk = Wlc_NtkUifNodePairs( pNtk, NULL ); + //pNtk = Wlc_NtkAbstractNodes( pNtk, NULL ); + //Wlc_AbcUpdateNtk( pAbc, pNtk ); + //Wlc_GenerateSmtStdout( pAbc ); + //Wlc_NtkSimulateTest( (Wlc_Ntk_t *)pAbc->pAbcWlc ); + pNtk = Wlc_NtkDupSingleNodes( pNtk ); + Wlc_AbcUpdateNtk( pAbc, pNtk ); + return 0; +usage: + Abc_Print( -2, "usage: %%test [-vh]\n" ); + Abc_Print( -2, "\t experiments with word-level networks\n" ); + Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + +/**Function******************************************************************** + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int Abc_CommandInvPs( Abc_Frame_t * pAbc, int argc, char ** argv ) { + extern Vec_Int_t * Pdr_InvCounts( Vec_Int_t * vInv ); extern void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, int fVerbose ); Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc); + Vec_Int_t * vCounts; int c, fVerbose = 0; Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) @@ -461,24 +1122,66 @@ int Abc_CommandPsInv( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( pNtk == NULL ) { - Abc_Print( 1, "Abc_CommandPsInv(): There is no current design.\n" ); + Abc_Print( 1, "Abc_CommandInvPs(): There is no current design.\n" ); return 0; } - if ( Wlc_AbcGetNtk(pAbc) == NULL ) + if ( Wlc_AbcGetInv(pAbc) == NULL ) { - Abc_Print( 1, "Abc_CommandPsInv(): There is no saved invariant.\n" ); + Abc_Print( 1, "Abc_CommandInvPs(): Invariant is not available.\n" ); return 0; } + vCounts = Pdr_InvCounts( Wlc_AbcGetInv(pAbc) ); + Wlc_NtkPrintInvStats( pNtk, vCounts, fVerbose ); + Vec_IntFree( vCounts ); + return 0; +usage: + Abc_Print( -2, "usage: inv_ps [-vh]\n" ); + Abc_Print( -2, "\t prints statistics for inductive invariant\n" ); + Abc_Print( -2, "\t (in the case of \'sat\' or \'undecided\', inifity clauses are used)\n" ); + Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + +/**Function******************************************************************** + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int Abc_CommandInvPrint( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern void Pdr_InvPrint( Vec_Int_t * vInv, int fVerbose ); + int c, fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + { + switch ( c ) + { + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } if ( Wlc_AbcGetInv(pAbc) == NULL ) { - Abc_Print( 1, "Abc_CommandPsInv(): Invariant is not available.\n" ); + Abc_Print( 1, "Abc_CommandInvPs(): Invariant is not available.\n" ); return 0; } - Wlc_NtkPrintInvStats( pNtk, Wlc_AbcGetInv(pAbc), fVerbose ); + Pdr_InvPrint( Wlc_AbcGetInv(pAbc), fVerbose ); return 0; - usage: - Abc_Print( -2, "usage: %%psinv [-vh]\n" ); - Abc_Print( -2, "\t prints statistics for inductive invariant\n" ); +usage: + Abc_Print( -2, "usage: inv_print [-vh]\n" ); + Abc_Print( -2, "\t prints the current inductive invariant\n" ); Abc_Print( -2, "\t (in the case of \'sat\' or \'undecided\', inifity clauses are used)\n" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); @@ -496,12 +1199,11 @@ int Abc_CommandPsInv( Abc_Frame_t * pAbc, int argc, char ** argv ) SeeAlso [] ******************************************************************************/ -int Abc_CommandGetInv( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandInvCheck( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, Vec_Str_t * vSop, int fVerbose ); - Abc_Ntk_t * pMainNtk; - Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc); - int c, fVerbose = 0; + abctime clk = Abc_Clock(); + extern int Pdr_InvCheck( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose ); + int c, nFailed, fVerbose = 0; Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) { @@ -516,28 +1218,81 @@ int Abc_CommandGetInv( Abc_Frame_t * pAbc, int argc, char ** argv ) goto usage; } } - if ( pNtk == NULL ) + if ( pAbc->pGia == NULL ) { - Abc_Print( 1, "Abc_CommandGetInv(): There is no current design.\n" ); + Abc_Print( 1, "Abc_CommandInvMin(): There is no current design.\n" ); return 0; } - if ( Wlc_AbcGetNtk(pAbc) == NULL ) + if ( Wlc_AbcGetInv(pAbc) == NULL ) { - Abc_Print( 1, "Abc_CommandGetInv(): There is no saved invariant.\n" ); + Abc_Print( 1, "Abc_CommandInvMin(): There is no saved invariant.\n" ); return 0; } + if ( Gia_ManRegNum(pAbc->pGia) != Vec_IntEntryLast(Wlc_AbcGetInv(pAbc)) ) + { + Abc_Print( 1, "Abc_CommandInvMin(): The number of flops in the invariant and in GIA should be the same.\n" ); + return 0; + } + nFailed = Pdr_InvCheck( pAbc->pGia, Wlc_AbcGetInv(pAbc), fVerbose ); + if ( nFailed ) + printf( "Invariant verification failed for %d clauses (out of %d). ", nFailed, Vec_IntEntry(Wlc_AbcGetInv(pAbc),0) ); + else + printf( "Invariant verification succeeded. " ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + return 0; +usage: + Abc_Print( -2, "usage: inv_check [-vh]\n" ); + Abc_Print( -2, "\t checks that the invariant is indeed an inductive invariant\n" ); + Abc_Print( -2, "\t (AIG representing the design should be in the &-space)\n" ); + Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + +/**Function******************************************************************** + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int Abc_CommandInvGet( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv ); + Abc_Ntk_t * pMainNtk; + Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc); + int c, fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + { + switch ( c ) + { + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } if ( Wlc_AbcGetInv(pAbc) == NULL ) { - Abc_Print( 1, "Abc_CommandGetInv(): Invariant is not available.\n" ); + Abc_Print( 1, "Abc_CommandInvGet(): Invariant is not available.\n" ); return 0; } // derive the network - pMainNtk = Wlc_NtkGetInv( pNtk, Wlc_AbcGetInv(pAbc), Wlc_AbcGetStr(pAbc), fVerbose ); + pMainNtk = Wlc_NtkGetInv( pNtk, Wlc_AbcGetInv(pAbc) ); // replace the current network - Abc_FrameReplaceCurrentNetwork( pAbc, pMainNtk ); + if ( pMainNtk ) + Abc_FrameReplaceCurrentNetwork( pAbc, pMainNtk ); return 0; - usage: - Abc_Print( -2, "usage: %%getinv [-vh]\n" ); +usage: + Abc_Print( -2, "usage: inv_get [-vh]\n" ); Abc_Print( -2, "\t places invariant found by PDR as the current network in the main-space\n" ); Abc_Print( -2, "\t (in the case of \'sat\' or \'undecided\', inifity clauses are used)\n" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); @@ -556,34 +1311,45 @@ int Abc_CommandGetInv( Abc_Frame_t * pAbc, int argc, char ** argv ) SeeAlso [] ******************************************************************************/ -int Abc_CommandProfile( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandInvPut( Abc_Frame_t * pAbc, int argc, char ** argv ) { - Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc); + extern Vec_Int_t * Wlc_NtkGetPut( Abc_Ntk_t * pNtk, Gia_Man_t * pGia ); + Vec_Int_t * vInv = NULL; + Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc); int c, fVerbose = 0; Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) { switch ( c ) { - case 'v': - fVerbose ^= 1; - break; - case 'h': - goto usage; - default: - goto usage; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; } } if ( pNtk == NULL ) { - Abc_Print( 1, "Abc_CommandProfile(): There is no current design.\n" ); + Abc_Print( 1, "Abc_CommandInvPut(): There is no current design.\n" ); return 0; } - Wlc_WinProfileArith( pNtk ); + if ( pAbc->pGia == NULL ) + { + Abc_Print( 1, "Abc_CommandInvPut(): There is no current AIG.\n" ); + return 0; + } + // derive the network + vInv = Wlc_NtkGetPut( pNtk, pAbc->pGia ); + if ( vInv ) + Abc_FrameSetInv( vInv ); return 0; usage: - Abc_Print( -2, "usage: %%profile [-vh]\n" ); - Abc_Print( -2, "\t profiles arithmetic components in the word-level networks\n" ); + Abc_Print( -2, "usage: inv_put [-vh]\n" ); + Abc_Print( -2, "\t inputs the current network in the main-space as an invariant\n" ); + Abc_Print( -2, "\t (AIG representing the design should be in the &-space)\n" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; @@ -600,42 +1366,57 @@ usage: SeeAlso [] ******************************************************************************/ -int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandInvMin( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern void Wlc_NtkSimulateTest( Wlc_Ntk_t * p ); - Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc); - int c, fVerbose = 0; + extern Vec_Int_t * Pdr_InvMinimize( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose ); + extern Vec_Int_t * Pdr_InvMinimizeLits( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose ); + Vec_Int_t * vInv, * vInv2; + int c, fLits = 0, fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "lvh" ) ) != EOF ) { switch ( c ) { - case 'v': - fVerbose ^= 1; - break; - case 'h': - goto usage; - default: - goto usage; + case 'l': + fLits ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; } } - if ( pNtk == NULL ) + if ( pAbc->pGia == NULL ) { - Abc_Print( 1, "Abc_CommandTest(): There is no current design.\n" ); + Abc_Print( 1, "Abc_CommandInvMin(): There is no current design.\n" ); return 0; } - // transform - //pNtk = Wlc_NtkUifNodePairs( pNtk, NULL ); - //pNtk = Wlc_NtkAbstractNodes( pNtk, NULL ); - //Wlc_AbcUpdateNtk( pAbc, pNtk ); - //Wlc_GenerateSmtStdout( pAbc ); - //Wlc_NtkSimulateTest( (Wlc_Ntk_t *)pAbc->pAbcWlc ); - pNtk = Wlc_NtkDupSingleNodes( pNtk ); - Wlc_AbcUpdateNtk( pAbc, pNtk ); + if ( Wlc_AbcGetInv(pAbc) == NULL ) + { + Abc_Print( 1, "Abc_CommandInvMin(): Invariant is not available.\n" ); + return 0; + } + vInv = Wlc_AbcGetInv(pAbc); + if ( Gia_ManRegNum(pAbc->pGia) != Vec_IntEntryLast(vInv) ) + { + Abc_Print( 1, "Abc_CommandInvMin(): The number of flops in the invariant and in GIA should be the same.\n" ); + return 0; + } + if ( fLits ) + vInv2 = Pdr_InvMinimizeLits( pAbc->pGia, vInv, fVerbose ); + else + vInv2 = Pdr_InvMinimize( pAbc->pGia, vInv, fVerbose ); + if ( vInv2 ) + Abc_FrameSetInv( vInv2 ); return 0; usage: - Abc_Print( -2, "usage: %%test [-vh]\n" ); - Abc_Print( -2, "\t experiments with word-level networks\n" ); + Abc_Print( -2, "usage: inv_min [-lvh]\n" ); + Abc_Print( -2, "\t performs minimization of the current invariant\n" ); + Abc_Print( -2, "\t (AIG representing the design should be in the &-space)\n" ); + Abc_Print( -2, "\t-l : toggle minimizing literals rather than clauses [default = %s]\n", fLits? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c index 6f396771..c8fc15a7 100644 --- a/src/base/wlc/wlcNtk.c +++ b/src/base/wlc/wlcNtk.c @@ -88,12 +88,40 @@ static char * Wlc_Names[WLC_OBJ_NUMBER+1] = { NULL // 54: unused }; +char * Wlc_ObjTypeName( Wlc_Obj_t * p ) { return Wlc_Names[p->Type]; } + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars ) +{ + memset( pPars, 0, sizeof(Wlc_Par_t) ); + pPars->nBitsAdd = ABC_INFINITY; // adder bit-width + pPars->nBitsMul = ABC_INFINITY; // multiplier bit-widht + pPars->nBitsMux = ABC_INFINITY; // MUX bit-width + pPars->nBitsFlop = ABC_INFINITY; // flop bit-width + pPars->nIterMax = 1000; // the max number of iterations + pPars->fXorOutput = 1; // XOR outputs of word-level miter + pPars->fCheckClauses = 1; // Check clauses in the reloaded trace + pPars->fPushClauses = 0; // Push clauses in the reloaded trace + pPars->fVerbose = 0; // verbose output` + pPars->fPdrVerbose = 0; // show verbose PDR output +} + +/**Function************************************************************* + Synopsis [Working with models.] Description [] @@ -195,14 +223,14 @@ void Wlc_ObjAddFanins( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Int_t * vFanins ) { assert( pObj->nFanins == 0 ); pObj->nFanins = Vec_IntSize(vFanins); - if ( Wlc_ObjHasArray(pObj) ) - pObj->pFanins[0] = (int *)Mem_FlexEntryFetch( p->pMemFanin, Vec_IntSize(vFanins) * sizeof(int) ); - memcpy( Wlc_ObjFanins(pObj), Vec_IntArray(vFanins), sizeof(int) * Vec_IntSize(vFanins) ); // special treatment of CONST, SELECT and TABLE if ( pObj->Type == WLC_OBJ_CONST ) pObj->nFanins = 0; else if ( pObj->Type == WLC_OBJ_BIT_SELECT || pObj->Type == WLC_OBJ_TABLE ) pObj->nFanins = 1; + if ( Wlc_ObjHasArray(pObj) ) + pObj->pFanins[0] = (int *)Mem_FlexEntryFetch( p->pMemFanin, Vec_IntSize(vFanins) * sizeof(int) ); + memcpy( Wlc_ObjFanins(pObj), Vec_IntArray(vFanins), sizeof(int) * Vec_IntSize(vFanins) ); } void Wlc_NtkFree( Wlc_Ntk_t * p ) { @@ -224,6 +252,8 @@ void Wlc_NtkFree( Wlc_Ntk_t * p ) ABC_FREE( p->vValues.pArray ); ABC_FREE( p->vCopies.pArray ); ABC_FREE( p->vBits.pArray ); + ABC_FREE( p->vLevels.pArray ); + ABC_FREE( p->vRefs.pArray ); ABC_FREE( p->pInits ); ABC_FREE( p->pObjs ); ABC_FREE( p->pName ); @@ -246,6 +276,91 @@ int Wlc_NtkMemUsage( Wlc_Ntk_t * p ) /**Function************************************************************* + Synopsis [Assigns object levels.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Wlc_NtkCreateLevels( Wlc_Ntk_t * p ) +{ + Wlc_Obj_t * pObj; + int i, k, iFanin, Level, LevelMax = 0; + Vec_IntFill( &p->vLevels, Wlc_NtkObjNumMax(p), 0 ); + Wlc_NtkForEachObj( p, pObj, i ) + { + Level = 0; + Wlc_ObjForEachFanin( pObj, iFanin, k ) + Level = Abc_MaxInt( Level, Wlc_ObjLevelId(p, iFanin) + 1 ); + Vec_IntWriteEntry( &p->vLevels, i, Level ); + LevelMax = Abc_MaxInt( LevelMax, Level ); + } + return LevelMax; +} +int Wlc_NtkCreateLevelsRev( Wlc_Ntk_t * p ) +{ + Wlc_Obj_t * pObj; + int i, k, iFanin, Level, LevelMax = 0; + Vec_IntFill( &p->vLevels, Wlc_NtkObjNumMax(p), 0 ); + Wlc_NtkForEachObjReverse( p, pObj, i ) + { + if ( Wlc_ObjIsCi(pObj) ) + continue; + Level = Wlc_ObjLevel(p, pObj) + 1; + Wlc_ObjForEachFanin( pObj, iFanin, k ) + Vec_IntUpdateEntry( &p->vLevels, iFanin, Level ); + LevelMax = Abc_MaxInt( LevelMax, Level ); + } + // reverse the values + Wlc_NtkForEachObj( p, pObj, i ) + Vec_IntWriteEntry( &p->vLevels, i, LevelMax - Wlc_ObjLevelId(p, i) ); + Wlc_NtkForEachCi( p, pObj, i ) + Vec_IntWriteEntry( &p->vLevels, Wlc_ObjId(p, pObj), 0 ); + return LevelMax; +} + +/**Function************************************************************* + + Synopsis [Collects statistics for each side of the miter.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Wlc_NtkCollectStats( Wlc_Ntk_t * p, int nObjs[2][WLC_OBJ_NUMBER] ) +{ + Wlc_Obj_t * pObj; + int n, i; + if ( Wlc_NtkPoNum(p) != 2 ) + return; + for ( n = 0; n < 2; n++ ) + { + Wlc_NtkMarkCone( p, n, 1, 1, 0 ); + Wlc_NtkForEachObj( p, pObj, i ) + if ( pObj->Mark ) + nObjs[n][pObj->Type]++; + } + Wlc_NtkCleanMarks( p ); +} +int Wlc_NtkCountRealPis( Wlc_Ntk_t * p ) +{ + Wlc_Obj_t * pObj; + int i, Count = 0; + Wlc_NtkMarkCone( p, -1, -1, 1, 0 ); + Wlc_NtkForEachPi( p, pObj, i ) + Count += pObj->Mark; + Wlc_NtkCleanMarks( p ); + return Count; +} + +/**Function************************************************************* + Synopsis [Prints distribution of operator types.] Description [] @@ -298,13 +413,18 @@ void Wlc_NtkPrintDistribSortOne( Vec_Ptr_t * vTypes, Vec_Ptr_t * vOccurs, int Ty Vec_WrdReverseOrder( vType ); Vec_WrdReverseOrder( vOccur ); } -void Wlc_NtkPrintDistrib( Wlc_Ntk_t * p, int fVerbose ) +void Wlc_NtkPrintDistrib( Wlc_Ntk_t * p, int fTwoSides, int fVerbose ) { + int nObjs[2][WLC_OBJ_NUMBER] = {{0}}; // counter of objects of each type Wlc_Obj_t * pObj, * pObjRange = NULL; int nCountRange = 0; Vec_Ptr_t * vTypes, * vOccurs; Vec_Int_t * vAnds = Vec_IntStart( WLC_OBJ_NUMBER ); word Sign; int i, k, s, s0, s1; + if ( Wlc_NtkPoNum(p) != 2 ) + fTwoSides = 0; + if ( fTwoSides ) + Wlc_NtkCollectStats( p, nObjs ); // allocate statistics arrays vTypes = Vec_PtrStart( WLC_OBJ_NUMBER ); vOccurs = Vec_PtrStart( WLC_OBJ_NUMBER ); @@ -409,11 +529,11 @@ void Wlc_NtkPrintDistrib( Wlc_Ntk_t * p, int fVerbose ) else if ( pObj->Type == WLC_OBJ_REDUCT_XOR ) Vec_IntAddToEntry( vAnds, WLC_OBJ_REDUCT_XOR, 3 * Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) - 3 ); else if ( pObj->Type == WLC_OBJ_REDUCT_NAND ) - Vec_IntAddToEntry( vAnds, WLC_OBJ_REDUCT_NAND, Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) - 1 ); + Vec_IntAddToEntry( vAnds, WLC_OBJ_REDUCT_NAND, Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) - 1 ); else if ( pObj->Type == WLC_OBJ_REDUCT_NOR ) - Vec_IntAddToEntry( vAnds, WLC_OBJ_REDUCT_NOR, Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) - 1 ); + Vec_IntAddToEntry( vAnds, WLC_OBJ_REDUCT_NOR, Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) - 1 ); else if ( pObj->Type == WLC_OBJ_REDUCT_NXOR ) - Vec_IntAddToEntry( vAnds, WLC_OBJ_REDUCT_NXOR, 3 * Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) - 3 ); + Vec_IntAddToEntry( vAnds, WLC_OBJ_REDUCT_NXOR, 3 * Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) - 3 ); else if ( pObj->Type == WLC_OBJ_ARI_ADD ) Vec_IntAddToEntry( vAnds, WLC_OBJ_ARI_ADD, 9 * Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) ); else if ( pObj->Type == WLC_OBJ_ARI_SUB ) @@ -435,28 +555,41 @@ void Wlc_NtkPrintDistrib( Wlc_Ntk_t * p, int fVerbose ) else if ( pObj->Type == WLC_OBJ_ARI_SQUARE ) Vec_IntAddToEntry( vAnds, WLC_OBJ_ARI_SQUARE, 5 * Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) * Wlc_ObjRange(Wlc_ObjFanin1(p, pObj)) ); } - if ( nCountRange ) + if ( nCountRange && Vec_IntSize(&p->vNameIds) > 0 ) { printf( "Warning: %d objects of the design have non-zero-based ranges.\n", nCountRange ); printf( "In particular, object %6d with name \"%s\" has range %d=[%d:%d]\n", Wlc_ObjId(p, pObjRange), Abc_NamStr(p->pManName, Wlc_ObjNameId(p, Wlc_ObjId(p, pObjRange))), Wlc_ObjRange(pObjRange), pObjRange->End, pObjRange->Beg ); } // print by occurrence - printf( "ID : name occurrence and2 (occurrence)<output_range>=<input_range>.<input_range> ...\n" ); + printf( "ID : name occurrence%s and2 (occurrence)<output_range>=<input_range>.<input_range> ...\n", fTwoSides ? " Left Share Right":"" ); for ( i = 0; i < WLC_OBJ_NUMBER; i++ ) { Vec_Wrd_t * vType = (Vec_Wrd_t *)Vec_PtrEntry( vTypes, i ); Vec_Wrd_t * vOccur = (Vec_Wrd_t *)Vec_PtrEntry( vOccurs, i ); if ( p->nObjs[i] == 0 ) continue; - printf( "%2d : %-8s %6d%8d ", i, Wlc_Names[i], p->nObjs[i], Vec_IntEntry(vAnds, i) ); + printf( "%2d : %-8s %6d", i, Wlc_Names[i], p->nObjs[i] ); + if ( fTwoSides ) + { + int nTotal = i == WLC_OBJ_PI ? Wlc_NtkCountRealPis(p) : p->nObjs[i]; + printf( " " ); + printf( "%6d", nObjs[0][i] ); + printf( "%6d", nObjs[0][i]+nObjs[1][i]-nTotal ); + printf( "%6d", nObjs[1][i] ); + } + printf( "%8d ", Vec_IntEntry(vAnds, i) ); // sort by occurence Wlc_NtkPrintDistribSortOne( vTypes, vOccurs, i ); Vec_WrdForEachEntry( vType, Sign, k ) { Wlc_NtkPrintDistribFromSign( Sign, &s, &s0, &s1 ); if ( ((k % 6) == 5 && s1) || ((k % 8) == 7 && !s1) ) + { printf( "\n " ); + if ( fTwoSides ) + printf( " " ); + } printf( "(%d)", (int)Vec_WrdEntry( vOccur, k ) ); printf( "%s%d", Abc_LitIsCompl(s)?"-":"", Abc_Lit2Var(s) ); if ( s0 ) @@ -535,19 +668,19 @@ void Wlc_NtkPrintNodes( Wlc_Ntk_t * p, int Type ) Wlc_NtkPrintNode( p, pObj ); } } -void Wlc_NtkPrintStats( Wlc_Ntk_t * p, int fDistrib, int fVerbose ) +void Wlc_NtkPrintStats( Wlc_Ntk_t * p, int fDistrib, int fTwoSides, int fVerbose ) { int i; printf( "%-20s : ", p->pName ); - printf( "PI = %4d ", Wlc_NtkPiNum(p) ); + printf( "PI = %4d ", Wlc_NtkCountRealPis(p) ); //Wlc_NtkPiNum(p) ); printf( "PO = %4d ", Wlc_NtkPoNum(p) ); printf( "FF = %4d ", Wlc_NtkFfNum(p) ); - printf( "Obj = %6d ", Wlc_NtkObjNum(p) ); + printf( "Obj = %6d ", Wlc_NtkObjNum(p) - Wlc_NtkPiNum(p) - Wlc_NtkPoNum(p) - Wlc_NtkFfNum(p) ); printf( "Mem = %.3f MB", 1.0*Wlc_NtkMemUsage(p)/(1<<20) ); printf( "\n" ); if ( fDistrib ) { - Wlc_NtkPrintDistrib( p, fVerbose ); + Wlc_NtkPrintDistrib( p, fTwoSides, fVerbose ); return; } if ( !fVerbose ) @@ -566,6 +699,80 @@ void Wlc_NtkPrintStats( Wlc_Ntk_t * p, int fDistrib, int fVerbose ) /**Function************************************************************* + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Wlc_NtkTransferNames( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p ) +{ + int i; + assert( !Wlc_NtkHasCopy(pNew) && Wlc_NtkHasCopy(p) ); + assert( !Wlc_NtkHasNameId(pNew) && Wlc_NtkHasNameId(p) ); + assert( pNew->pManName == NULL && p->pManName != NULL ); + Wlc_NtkCleanNameId( pNew ); + for ( i = 0; i < p->nObjsAlloc; i++ ) + if ( Wlc_ObjCopy(p, i) && i < Vec_IntSize(&p->vNameIds) && Wlc_ObjNameId(p, i) ) + Wlc_ObjSetNameId( pNew, Wlc_ObjCopy(p, i), Wlc_ObjNameId(p, i) ); + pNew->pManName = p->pManName; + p->pManName = NULL; + Vec_IntErase( &p->vNameIds ); + // transfer table + pNew->pMemTable = p->pMemTable; p->pMemTable = NULL; + pNew->vTables = p->vTables; p->vTables = NULL; +} +char * Wlc_NtkNewName( Wlc_Ntk_t * p, int iCoId, int fSeq ) +{ + static char pBuffer[1000]; + sprintf( pBuffer, "%s_o%d_%s", p->pName, iCoId, fSeq ? "seq": "comb" ); + return pBuffer; +} + +/**Function************************************************************* + + Synopsis [Reduce init vector.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Wlc_ReduceMarkedInitVec( Wlc_Ntk_t * p, Vec_Int_t * vInit ) +{ + Vec_Int_t * vInitNew = Vec_IntDup( vInit ); + Wlc_Obj_t * pObj; int i, k = 0; + assert( Vec_IntSize(vInit) == Wlc_NtkCiNum(p) - Wlc_NtkPiNum(p) ); + Wlc_NtkForEachCi( p, pObj, i ) + if ( !Wlc_ObjIsPi(pObj) && pObj->Mark ) + Vec_IntWriteEntry( vInitNew, k++, Vec_IntEntry(vInit, i - Wlc_NtkPiNum(p)) ); + Vec_IntShrink( vInitNew, k ); + return vInitNew; +} +char * Wlc_ReduceMarkedInitStr( Wlc_Ntk_t * p, char * pInit ) +{ + char * pInitNew = Abc_UtilStrsav( pInit ); + Wlc_Obj_t * pObj; int i, b, nBits = 0, k = 0; + Wlc_NtkForEachCi( p, pObj, i ) + { + if ( !Wlc_ObjIsPi(pObj) && pObj->Mark ) + for ( b = 0; b < Wlc_ObjRange(pObj); b++ ) + pInitNew[k++] = pInitNew[nBits+b]; + if ( !Wlc_ObjIsPi(pObj) ) + nBits += Wlc_ObjRange(pObj); + } + pInitNew[k] = '\0'; + assert( nBits == (int)strlen(pInit) ); + return pInitNew; +} + +/**Function************************************************************* + Synopsis [Duplicates the network in a topological order.] Description [] @@ -623,47 +830,214 @@ void Wlc_NtkDupDfs_rec( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, int iObj, Vec_Int_t * v Wlc_NtkDupDfs_rec( pNew, p, iFanin, vFanins ); Wlc_ObjDup( pNew, p, iObj, vFanins ); } -Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p ) +Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p, int fMarked, int fSeq ) { Wlc_Ntk_t * pNew; Wlc_Obj_t * pObj; Vec_Int_t * vFanins; int i; - Wlc_NtkCleanCopy( p ); vFanins = Vec_IntAlloc( 100 ); + Wlc_NtkCleanCopy( p ); pNew = Wlc_NtkAlloc( p->pName, p->nObjsAlloc ); pNew->fSmtLib = p->fSmtLib; Wlc_NtkForEachCi( p, pObj, i ) - Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins ); + if ( !fMarked || pObj->Mark ) + { + unsigned Type = pObj->Type; + if ( !fSeq ) pObj->Type = WLC_OBJ_PI; + Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins ); + pObj->Type = Type; + } Wlc_NtkForEachCo( p, pObj, i ) - Wlc_NtkDupDfs_rec( pNew, p, Wlc_ObjId(p, pObj), vFanins ); + if ( !fMarked || pObj->Mark ) + Wlc_NtkDupDfs_rec( pNew, p, Wlc_ObjId(p, pObj), vFanins ); Wlc_NtkForEachCo( p, pObj, i ) - Wlc_ObjSetCo( pNew, Wlc_ObjCopyObj(pNew, p, pObj), pObj->fIsFi ); + if ( !fMarked || pObj->Mark ) + Wlc_ObjSetCo( pNew, Wlc_ObjCopyObj(pNew, p, pObj), fSeq ? pObj->fIsFi : 0 ); + Vec_IntFree( vFanins ); + if ( fSeq ) + { + if ( fMarked ) + { + if ( p->vInits ) + pNew->vInits = Wlc_ReduceMarkedInitVec( p, p->vInits ); + if ( p->pInits ) + pNew->pInits = Wlc_ReduceMarkedInitStr( p, p->pInits ); + } + else + { + if ( p->vInits ) + pNew->vInits = Vec_IntDup( p->vInits ); + if ( p->pInits ) + pNew->pInits = Abc_UtilStrsav( p->pInits ); + } + } + if ( p->pSpec ) + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Wlc_NtkTransferNames( pNew, p ); + return pNew; +} +Wlc_Ntk_t * Wlc_NtkDupDfsAbs( Wlc_Ntk_t * p, Vec_Int_t * vPisOld, Vec_Int_t * vPisNew, Vec_Int_t * vFlops ) +{ + Wlc_Ntk_t * pNew; + Wlc_Obj_t * pObj; + Vec_Int_t * vFanins; + int i; + Wlc_NtkCleanCopy( p ); + pNew = Wlc_NtkAlloc( p->pName, p->nObjsAlloc ); + pNew->fSmtLib = p->fSmtLib; + + // duplicate marked PIs + vFanins = Vec_IntAlloc( 100 ); + Wlc_NtkForEachObjVec( vPisOld, p, pObj, i ) + { + assert( Wlc_ObjIsPi(pObj) ); + Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins ); + } + // duplicate additional PIs + Wlc_NtkForEachObjVec( vPisNew, p, pObj, i ) + { + unsigned Type = pObj->Type; + int nFanins = Wlc_ObjFaninNum(pObj); + assert( !Wlc_ObjIsPi(pObj) ); + pObj->Type = WLC_OBJ_PI; + pObj->nFanins = 0; + Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins ); + pObj->Type = Type; + pObj->nFanins = (unsigned)nFanins; + } + // duplicate flop outputs + Wlc_NtkForEachObjVec( vFlops, p, pObj, i ) + { + assert( !Wlc_ObjIsPi(pObj) && Wlc_ObjIsCi(pObj) ); + Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins ); + } + + // duplicate logic cones of primary outputs + Wlc_NtkForEachPo( p, pObj, i ) + Wlc_NtkDupDfs_rec( pNew, p, Wlc_ObjId(p, pObj), vFanins ); + // duplidate logic cone of flop inputs + Wlc_NtkForEachObjVec( vFlops, p, pObj, i ) + Wlc_NtkDupDfs_rec( pNew, p, Wlc_ObjId(p, Wlc_ObjFo2Fi(p, pObj)), vFanins ); + + // duplicate POs + Wlc_NtkForEachPo( p, pObj, i ) + Wlc_ObjSetCo( pNew, Wlc_ObjCopyObj(pNew, p, pObj), 0 ); + // duplicate flop inputs + Wlc_NtkForEachObjVec( vFlops, p, pObj, i ) + Wlc_ObjSetCo( pNew, Wlc_ObjCopyObj(pNew, p, Wlc_ObjFo2Fi(p, pObj)), 1 ); + Vec_IntFree( vFanins ); + + // mark flop outputs + Wlc_NtkForEachObjVec( vFlops, p, pObj, i ) + pObj->Mark = 1; if ( p->vInits ) - pNew->vInits = Vec_IntDup( p->vInits ); + pNew->vInits = Wlc_ReduceMarkedInitVec( p, p->vInits ); if ( p->pInits ) - pNew->pInits = Abc_UtilStrsav( p->pInits ); - Vec_IntFree( vFanins ); + pNew->pInits = Wlc_ReduceMarkedInitStr( p, p->pInits ); + Wlc_NtkCleanMarks( p ); + if ( p->pSpec ) - pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + //Wlc_NtkTransferNames( pNew, p ); return pNew; } -void Wlc_NtkTransferNames( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p ) + +/**Function************************************************************* + + Synopsis [Select the cone of the given output.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Wlc_NtkCleanMarks( Wlc_Ntk_t * p ) { + Wlc_Obj_t * pObj; int i; - assert( !Wlc_NtkHasCopy(pNew) && Wlc_NtkHasCopy(p) ); - assert( !Wlc_NtkHasNameId(pNew) && Wlc_NtkHasNameId(p) ); - assert( pNew->pManName == NULL && p->pManName != NULL ); - Wlc_NtkCleanNameId( pNew ); - for ( i = 0; i < p->nObjsAlloc; i++ ) - if ( Wlc_ObjCopy(p, i) && i < Vec_IntSize(&p->vNameIds) && Wlc_ObjNameId(p, i) ) - Wlc_ObjSetNameId( pNew, Wlc_ObjCopy(p, i), Wlc_ObjNameId(p, i) ); - pNew->pManName = p->pManName; - p->pManName = NULL; - Vec_IntErase( &p->vNameIds ); - // transfer table - pNew->pMemTable = p->pMemTable; p->pMemTable = NULL; - pNew->vTables = p->vTables; p->vTables = NULL; + Wlc_NtkForEachObj( p, pObj, i ) + pObj->Mark = 0; +} +int Wlc_NtkCountMarked( Wlc_Ntk_t * p, int * pnPis, int * pnFos, int * pnAdders, int * pnMults ) +{ + Wlc_Obj_t * pObj; + int i, nNodes = 0; + *pnPis = *pnFos = *pnAdders = *pnMults = 0; + Wlc_NtkForEachObj( p, pObj, i ) + { + if ( !pObj->Mark ) + continue; + if ( Wlc_ObjIsPi(pObj) ) + (*pnPis)++; + else if ( Wlc_ObjIsCi(pObj) ) + (*pnFos)++; + else if ( pObj->Mark ) + { + nNodes++; + if ( pObj->Type == WLC_OBJ_ARI_ADD || pObj->Type == WLC_OBJ_ARI_SUB ) + (*pnAdders)++; + else if ( pObj->Type == WLC_OBJ_ARI_MULTI ) + (*pnMults)++; + } + } + return nNodes; +} +void Wlc_NtkMarkCone_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Int_t * vFlops ) +{ + int i, iFanin; + if ( pObj->Mark ) + return; + pObj->Mark = 1; + if ( Wlc_ObjIsCi(pObj) ) + { + if ( !Wlc_ObjIsPi(pObj) ) + Vec_IntPush( vFlops, Wlc_ObjCiId(pObj) ); + return; + } + Wlc_ObjForEachFanin( pObj, iFanin, i ) + Wlc_NtkMarkCone_rec( p, Wlc_NtkObj(p, iFanin), vFlops ); +} +void Wlc_NtkMarkCone( Wlc_Ntk_t * p, int iCoId, int Range, int fSeq, int fAllPis ) +{ + Vec_Int_t * vFlops; + Wlc_Obj_t * pObj; + int i, CiId, CoId; + Wlc_NtkCleanMarks( p ); + if ( fAllPis ) + Wlc_NtkForEachPi( p, pObj, i ) + pObj->Mark = 1; + vFlops = Vec_IntAlloc( 100 ); + Wlc_NtkForEachCo( p, pObj, i ) + if ( iCoId == -1 || (i >= iCoId && i < iCoId + Range) ) + Wlc_NtkMarkCone_rec( p, pObj, vFlops ); + if ( fSeq ) + Vec_IntForEachEntry( vFlops, CiId, i ) + { + CoId = Wlc_NtkPoNum(p) + CiId - Wlc_NtkPiNum(p); + Wlc_NtkMarkCone_rec( p, Wlc_NtkCo(p, CoId), vFlops ); + } + Vec_IntFree( vFlops ); +} +void Wlc_NtkProfileCones( Wlc_Ntk_t * p ) +{ + Wlc_Obj_t * pObj; + int i, nPis, nFos, nNodes, nAdders, nMults; + Wlc_NtkForEachCo( p, pObj, i ) + { + Wlc_NtkMarkCone( p, i, 1, 0, 0 ); + nNodes = Wlc_NtkCountMarked( p, &nPis, &nFos, &nAdders, &nMults ); + printf( "Cone %5d : ", i ); + printf( "PI = %4d ", nPis ); + printf( "FO = %4d ", nFos ); + printf( "Node = %6d ", nNodes ); + printf( "Add/Sub = %4d ", nAdders ); + printf( "Mult = %4d ", nMults ); + printf( "\n" ); + } + Wlc_NtkCleanMarks( p ); } /**Function************************************************************* @@ -723,6 +1097,128 @@ Wlc_Ntk_t * Wlc_NtkDupSingleNodes( Wlc_Ntk_t * p ) return pNew; } +/**Function************************************************************* + + Synopsis [Creates short names for all objects.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Wlc_NtkShortNames( Wlc_Ntk_t * p ) +{ + Wlc_Obj_t * pObj; + char pBuffer[100]; + int nDigits, NameId, fFound, i; + int nFlops = Wlc_NtkCoNum(p) - Wlc_NtkPoNum(p); + nDigits = Abc_Base10Log( nFlops ); + Wlc_NtkForEachCo( p, pObj, i ) + { + if ( Wlc_ObjIsPo(pObj) ) + continue; + sprintf( pBuffer, "%s%0*d", "fi", nDigits, i - Wlc_NtkPoNum(p) ); + NameId = Abc_NamStrFindOrAdd( p->pManName, pBuffer, &fFound ); + Wlc_ObjSetNameId( p, Wlc_ObjId(p, pObj), NameId ); + } + Wlc_NtkForEachCi( p, pObj, i ) + { + if ( Wlc_ObjIsPi(pObj) ) + continue; + sprintf( pBuffer, "%s%0*d", "fo", nDigits, i - Wlc_NtkPiNum(p) ); + NameId = Abc_NamStrFindOrAdd( p->pManName, pBuffer, &fFound ); + Wlc_ObjSetNameId( p, Wlc_ObjId(p, pObj), NameId ); + } + nDigits = Abc_Base10Log( Wlc_NtkPoNum(p) ); + Wlc_NtkForEachPo( p, pObj, i ) + { + sprintf( pBuffer, "%s%0*d", "po", nDigits, i ); + NameId = Abc_NamStrFindOrAdd( p->pManName, pBuffer, &fFound ); + Wlc_ObjSetNameId( p, Wlc_ObjId(p, pObj), NameId ); + } + nDigits = Abc_Base10Log( Wlc_NtkPiNum(p) ); + Wlc_NtkForEachPi( p, pObj, i ) + { + sprintf( pBuffer, "%s%0*d", "pi", nDigits, i ); + NameId = Abc_NamStrFindOrAdd( p->pManName, pBuffer, &fFound ); + Wlc_ObjSetNameId( p, Wlc_ObjId(p, pObj), NameId ); + } + nDigits = Abc_Base10Log( Wlc_NtkObjNum(p) ); + Wlc_NtkForEachObj( p, pObj, i ) + { + if ( Wlc_ObjIsCi(pObj) || Wlc_ObjIsCo(pObj) ) + continue; + sprintf( pBuffer, "%s%0*d", "n", nDigits, i ); + NameId = Abc_NamStrFindOrAdd( p->pManName, pBuffer, &fFound ); + Wlc_ObjSetNameId( p, Wlc_ObjId(p, pObj), NameId ); + } +} + +/**Function************************************************************* + + Synopsis [Count the number of flops initialized to DC value.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Wlc_NtkDcFlopNum( Wlc_Ntk_t * p ) +{ + int i, nFlops, Count = 0; + if ( p->pInits == NULL ) + return 0; + nFlops = strlen(p->pInits); + for ( i = 0; i < nFlops; i++ ) + Count += (p->pInits[i] == 'x' || p->pInits[i] == 'X'); + return Count; +} + +/**Function************************************************************* + + Synopsis [Create references.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Wlc_NtkSetRefs( Wlc_Ntk_t * p ) +{ + Wlc_Obj_t * pObj; int i, k, Fanin; + Vec_IntFill( &p->vRefs, Wlc_NtkObjNumMax(p), 0 ); + Wlc_NtkForEachObj( p, pObj, i ) + Wlc_ObjForEachFanin( pObj, Fanin, k ) + Vec_IntAddToEntry( &p->vRefs, Fanin, 1 ); + Wlc_NtkForEachCo( p, pObj, i ) + Vec_IntAddToEntry( &p->vRefs, Wlc_ObjId(p, pObj), 1 ); +} + +/**Function************************************************************* + + Synopsis [This procedure simply count the number of PPI bits.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Wlc_NtkCountObjBits( Wlc_Ntk_t * p, Vec_Int_t * vPisNew ) +{ + Wlc_Obj_t * pObj; + int i, Count = 0; + Wlc_NtkForEachObjVec( vPisNew, p, pObj, i ) + Count += Wlc_ObjRange(pObj); + return Count; +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/base/wlc/wlcReadSmt.c b/src/base/wlc/wlcReadSmt.c index d07a54c4..69a01ab0 100644 --- a/src/base/wlc/wlcReadSmt.c +++ b/src/base/wlc/wlcReadSmt.c @@ -48,6 +48,9 @@ struct Smt_Prs_t_ char ErrorStr[1000]; }; +//#define SMT_GLO_SUFFIX "_glb" +#define SMT_GLO_SUFFIX "" + // parser name types typedef enum { SMT_PRS_NONE = 0, @@ -219,6 +222,8 @@ static inline int Smt_StrToType( char * pName, int * pfSigned ) Type = WLC_OBJ_ARI_REM, *pfSigned = 1; // 40: arithmetic remainder else if ( !strcmp(pName, "bvsmod") ) Type = WLC_OBJ_ARI_MODULUS, *pfSigned = 1; // 40: arithmetic modulus + else if ( !strcmp(pName, "=") ) + Type = WLC_OBJ_COMP_EQU; // 40: arithmetic modulus // else if ( !strcmp(pName, "") ) // Type = WLC_OBJ_ARI_POWER; // 41: arithmetic power else if ( !strcmp(pName, "bvneg") ) @@ -255,6 +260,8 @@ static inline int Smt_PrsReadType( Smt_Prs_t * p, int iSig, int * pfSigned, int } } +static inline int Smt_StrType( char * str ) { return Smt_StrToType(str, NULL); } + /**Function************************************************************* Synopsis [] @@ -274,20 +281,27 @@ static inline int Smt_PrsCreateNodeOld( Wlc_Ntk_t * pNtk, int Type, int fSigned, assert( Type > 0 ); assert( Range >= 0 ); assert( fSigned >= 0 ); - Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj), vFanins ); - if ( fSigned ) - Wlc_NtkObj(pNtk, iObj)->Signed = fSigned; - if ( Type == WLC_OBJ_SHIFT_RA ) - Wlc_NtkObj(pNtk, iObj)->Signed = 1; + + // add node's name if ( pName == NULL ) { sprintf( Buffer, "_n%d_", iObj ); pName = Buffer; } - // add node's name NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pName, &fFound ); assert( !fFound ); assert( iObj == NameId ); + + Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj), vFanins ); + if ( fSigned ) + { + Wlc_NtkObj(pNtk, iObj)->Signed = fSigned; +// if ( Vec_IntSize(vFanins) > 0 ) +// Wlc_NtkObj(pNtk, Vec_IntEntry(vFanins, 0))->Signed = fSigned; +// if ( Vec_IntSize(vFanins) > 1 ) +// Wlc_NtkObj(pNtk, Vec_IntEntry(vFanins, 1))->Signed = fSigned; + } + return iObj; } static inline int Smt_PrsCreateNode( Wlc_Ntk_t * pNtk, int Type, int fSigned, int Range, Vec_Int_t * vFanins, char * pName ) @@ -302,8 +316,7 @@ static inline int Smt_PrsCreateNode( Wlc_Ntk_t * pNtk, int Type, int fSigned, in assert( Range >= 0 ); assert( fSigned >= 0 ); - // allow more than 2 fanins for specific operators - // if (Vec_IntSize(vFanins)<=2 || Type == WLC_OBJ_BIT_CONCAT || Type == WLC_OBJ_MUX ) + //if (Vec_IntSize(vFanins)<=2 || Type == WLC_OBJ_BIT_CONCAT || Type == WLC_OBJ_MUX ) // explicitely secify allowed multi operators if (Vec_IntSize(vFanins)<=2 || !( Type == WLC_OBJ_BIT_AND || // 16:`` bitwise AND @@ -362,17 +375,17 @@ FINISHED_WITH_FANINS: Vec_IntFree(v2Fanins); - // to deal with long shifts create extra bit select (ROTATE as well ??) + //added to deal with long shifts create extra bit select (ROTATE as well ??) // this is a temporary hack - // basically we keep only 32 bits. - // bits 0 - 30 are kept same as original - // bit 31 will be the reduction or of all bits from 31 to Range-1 + // basically we keep only 32 bits. + // bit[31] will be the copy of original MSB (sign bit, just in case) UPDATE: assume it is unsigned first???? + // bit[31] will be the reduction or of any bits from [31] to Range if (Type == WLC_OBJ_SHIFT_R || Type == WLC_OBJ_SHIFT_RA || Type == WLC_OBJ_SHIFT_L) { - int iFanin1 = Vec_IntEntry(vFanins,1); - int range1 = Wlc_ObjRange( Wlc_NtkObj(pNtk, iFanin1) ); - int iObj1, iObj2, iObj3; + int range1, iObj1, iObj2, iObj3; assert(Vec_IntSize(vFanins)>=2); + iFanin1 = Vec_IntEntry(vFanins,1); + range1 = Wlc_ObjRange( Wlc_NtkObj(pNtk, iFanin1) ); if (range1>32) { Vec_Int_t * newFanins = Vec_IntAlloc(10); @@ -389,6 +402,8 @@ FINISHED_WITH_FANINS: Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj1), newFanins ); + //printf("obj1: %d\n",iObj1); + // bit select of larger bits Vec_IntPop(newFanins); Vec_IntPop(newFanins); @@ -402,6 +417,7 @@ FINISHED_WITH_FANINS: assert( iObj2 == NameId ); Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj2), newFanins ); + //printf("obj2: %d\n",iObj2); // reduction or Vec_IntPop( newFanins ); @@ -416,6 +432,7 @@ FINISHED_WITH_FANINS: assert( iObj3 == NameId ); Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj3), newFanins ); + //printf("obj3: %d\n",iObj3); // concat all together Vec_IntWriteEntry( newFanins, 0, iObj3 ); @@ -429,6 +446,7 @@ FINISHED_WITH_FANINS: assert( iObj == NameId ); Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj), newFanins ); + //printf("obj: %d\n",iObj); // pushing the new node Vec_IntWriteEntry(vFanins, 1, iObj); @@ -461,34 +479,22 @@ FINISHED_WITH_FANINS: return iObj; } -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ static inline char * Smt_GetHexFromDecimalString(char * pStr) { int i,k=0, nDigits = strlen(pStr); int digit, carry = 0; - int metNonZeroBit; - int nBits; - char * hex; + int metNonZeroBit = 0; Vec_Int_t * decimal = Vec_IntAlloc(nDigits); Vec_Int_t * rev; + int nBits; + char * hex; for (i=0;i<nDigits;i++) Vec_IntPush(decimal,pStr[i]-'0'); - // firstly fill-in the reversed vector + // firstly fillin the reversed vector rev = Vec_IntAlloc(10); - metNonZeroBit = 0; while(k<nDigits) { digit = Vec_IntEntry(decimal,k); @@ -501,7 +507,7 @@ static inline char * Smt_GetHexFromDecimalString(char * pStr) break; else { - Vec_IntPush(rev,carry); + Vec_IntPush(rev,carry); carry = 0; k = 0; metNonZeroBit = 0; @@ -564,12 +570,17 @@ static inline char * Smt_GetHexFromDecimalString(char * pStr) default: assert(0); } hex[nBits/4-1-k] = letter; + //if (k<Vec_IntSize(rev)) + // Vec_IntPush(vFanins,Vec_IntEntry(rev,k)); + //else + // Vec_IntPush(vFanins,0); } hex[nBits/4] = '\0'; Vec_IntFree(rev); return hex; -} +} + static inline int Smt_PrsBuildConstant( Wlc_Ntk_t * pNtk, char * pStr, int nBits, char * pName ) { int i, nDigits, iObj; @@ -578,6 +589,25 @@ static inline int Smt_PrsBuildConstant( Wlc_Ntk_t * pNtk, char * pStr, int nBits { if ( pStr[0] >= '0' && pStr[0] <= '9' ) { + // added: sanity check for large constants + /* + Vec_Int_t * temp = Vec_IntAlloc(10); + int fullBits = -1; + Smt_GetBinaryFromDecimalString(pStr,temp,&fullBits); + Vec_IntFree(temp); + assert(fullBits < 32);*/ + + char * pHex = Smt_GetHexFromDecimalString(pStr); + + if ( nBits == -1 ) + nBits = strlen(pHex)*4; + + //printf("nbits: %d\n",nBits); + + Vec_IntFill( vFanins, Abc_BitWordNum(nBits), 0 ); + nDigits = Abc_TtReadHexNumber( (word *)Vec_IntArray(vFanins), pHex ); + ABC_FREE( pHex ); + /* int w, nWords, Number = atoi( pStr ); if ( nBits == -1 ) @@ -589,15 +619,6 @@ static inline int Smt_PrsBuildConstant( Wlc_Ntk_t * pNtk, char * pStr, int nBits for ( w = 0; w < nWords; w++ ) Vec_IntPush( vFanins, w ? 0 : Number ); */ - - // convert decimal to hex to parse large constants - char * pHex = Smt_GetHexFromDecimalString(pStr); - - if ( nBits == -1 ) - nBits = strlen(pHex)*4; - - Vec_IntFill( vFanins, Abc_BitWordNum(nBits), 0 ); - nDigits = Abc_TtReadHexNumber( (word *)Vec_IntArray(vFanins), pHex ); } else { @@ -616,7 +637,10 @@ static inline int Smt_PrsBuildConstant( Wlc_Ntk_t * pNtk, char * pStr, int nBits if ( pStr[2+i] == '1' ) Abc_InfoSetBit( (unsigned *)Vec_IntArray(vFanins), nBits-1-i ); else if ( pStr[2+i] != '0' ) + { + Vec_IntFree( vFanins ); return 0; + } } else if ( pStr[1] == 'x' ) // hexadecimal { @@ -625,9 +649,16 @@ static inline int Smt_PrsBuildConstant( Wlc_Ntk_t * pNtk, char * pStr, int nBits Vec_IntFill( vFanins, Abc_BitWordNum(nBits), 0 ); nDigits = Abc_TtReadHexNumber( (word *)Vec_IntArray(vFanins), pStr+2 ); if ( nDigits != (nBits + 3)/4 ) + { + Vec_IntFree( vFanins ); return 0; + } + } + else + { + Vec_IntFree( vFanins ); + return 0; } - else return 0; // create constant node iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_CONST, 0, nBits, vFanins, pName ); Vec_IntFree( vFanins ); @@ -648,12 +679,6 @@ int Smt_PrsBuildNode( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int RangeOut, // s3087 int fFound, iObj = Abc_NamStrFindOrAdd( pNtk->pManName, pStr, &fFound ); assert( fFound ); - // create buffer if the name of the fanin has different name - if ( pName && strcmp(pStr, pName) ) - { - Vec_IntFill( &p->vTempFans, 1, iObj ); - iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_BUF, 0, RangeOut, &p->vTempFans, pName ); - } return iObj; } } @@ -804,13 +829,6 @@ Wlc_Ntk_t * Smt_PrsBuild( Smt_Prs_t * p ) // skip () Fan = Vec_IntEntry(vFans, 2); assert( !Smt_EntryIsName(Fan) ); - vFans2 = Smt_VecEntryNode(p, vFans, 2); - if ( Vec_IntSize(vFans2) > 0 ) - { - printf( "File parsing error: Uninterpreted functions are not supported.\n" ); - Wlc_NtkFree( pNtk ); pNtk = NULL; - goto finish; - } // check type (Bool or BitVec) Fan = Vec_IntEntry(vFans, 3); if ( Smt_EntryIsName(Fan) ) @@ -1006,6 +1024,14 @@ char * Smt_PrsGenName( Smt_Prs_t * p ) } int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev, char * pName ) { + char suffix[100]; + sprintf(suffix,"_as%d",pNtk->nAssert); + + //char * prepStr = Abc_NamStr(p->pStrs, Abc_Lit2Var(iNode)); + //printf("prestr: %s\n",prepStr); + + //printf("inode: %d %d\n",iNode,Smt_EntryIsName(iNode)); + if ( Smt_EntryIsName(iNode) ) { char * pStr = Abc_NamStr(p->pStrs, Abc_Lit2Var(iNode)); @@ -1018,7 +1044,27 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev, return Smt_PrsBuildConstant( pNtk, pStr, -1, pName ? pName : Smt_PrsGenName(p) ); else { - int fFound, iObj = Abc_NamStrFindOrAdd( pNtk->pManName, pStr, &fFound ); + int fFound, iObj; + // look either for global DECLARE-FUN variable or local LET + char * pStr_glb = (char *)malloc(strlen(pStr) + 4 +1); //glb + char * pStr_loc = (char *)malloc(strlen(pStr) + strlen(suffix) +1); + strcpy(pStr_glb,pStr); + strcat(pStr_glb,SMT_GLO_SUFFIX); + strcpy(pStr_loc,pStr); + strcat(pStr_loc,suffix); + + fFound = Abc_NamStrFind( pNtk->pManName, pStr_glb ); + + if (fFound) + pStr = pStr_glb; + else + { + assert( Abc_NamStrFind( pNtk->pManName, pStr_loc )); + pStr = pStr_loc; + } + // FIXME: delete memory of pStr + + iObj = Abc_NamStrFindOrAdd( pNtk->pManName, pStr, &fFound ); assert( fFound ); // create buffer if the name of the fanin has different name if ( pName && strcmp(Wlc_ObjName(pNtk, iObj), pName) ) @@ -1026,9 +1072,11 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev, Vec_IntFill( &p->vTempFans, 1, iObj ); iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_BUF, 0, Wlc_ObjRange(Wlc_NtkObj(pNtk, iObj)), &p->vTempFans, pName ); } + ABC_FREE( pStr_glb ); + ABC_FREE( pStr_loc ); return iObj; } - } + } else { Vec_Int_t * vRoots, * vRoots1, * vFans3; @@ -1039,7 +1087,7 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev, if ( Smt_EntryIsName(iRoot0) ) { char * pName2, * pStr0 = Abc_NamStr(p->pStrs, Abc_Lit2Var(iRoot0)); - if ( Abc_Lit2Var(iRoot0) == SMT_PRS_LET ) + if ( Abc_Lit2Var(iRoot0) == SMT_PRS_LET || Abc_Lit2Var(iRoot0) == SMT_PRS_DEFINE_FUN) //added define-fun is similar to let { // let ((s35550 (bvor s48 s35549))) assert( Vec_IntSize(vRoots) == 3 ); @@ -1051,6 +1099,7 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev, // iterate through the parts Vec_IntForEachEntry( vRoots1, Fan, k ) { + char * temp; // s35550 (bvor s48 s35549) assert( !Smt_EntryIsName(Fan) ); vFans3 = Smt_EntryNode(p, Fan); @@ -1059,11 +1108,26 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev, Fan3 = Vec_IntEntry(vFans3, 0); assert( Smt_EntryIsName(Fan3) ); pName2 = Smt_EntryName(p, Fan3); + // create a local name with suffix + if ( Abc_Lit2Var(iRoot0) == SMT_PRS_LET ) + { + temp = (char *)malloc(strlen(pName2) + strlen(suffix) + 1); + strcpy(temp, pName2); + strcat(temp,suffix); + } + else + { temp = (char *)malloc(strlen(pName2) + 4 + 1); + strcpy(temp, pName2); + strcat(temp,SMT_GLO_SUFFIX); + } + // FIXME: need to delete memory of pName2 + pName2 = temp; // get function Fan3 = Vec_IntEntry(vFans3, 1); //assert( !Smt_EntryIsName(Fan3) ); // solve the problem iObj = Smt_PrsBuild2_rec( pNtk, p, Fan3, -1, pName2 ); // NULL ); //pName2 ); + ABC_FREE( temp ); if ( iObj == 0 ) return 0; // create buffer @@ -1133,7 +1197,6 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev, int iObj = Abc_NamStrFind( pNtk->pManName, pStr0 ); if ( iObj ) return iObj; - Type0 = Smt_StrToType( pStr0, &fSigned ); if ( Type0 == 0 ) return 0; @@ -1151,7 +1214,6 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev, } Vec_IntPush( vFanins, iObj ); } - // find range Range = 0; if ( Type0 >= WLC_OBJ_LOGIC_NOT && Type0 <= WLC_OBJ_REDUCT_XOR ) @@ -1197,7 +1259,7 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p ) Wlc_Ntk_t * pNtk; Vec_Int_t * vFansRoot, * vFans, * vFans2; Vec_Int_t * vAsserts = Vec_IntAlloc(100); - int i, Root, Fan, iObj, NameId, Range, Status, nBits = 0; + int i, Root, Fan, iObj, NameId, Range, nBits = 0; char * pName, * pRange; // start network and create primary inputs pNtk = Wlc_NtkAlloc( p->pName, 1000 ); @@ -1214,22 +1276,22 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p ) // create variables if ( Abc_Lit2Var(Fan) == SMT_PRS_DECLARE_FUN ) { + char * pName_glb; assert( Vec_IntSize(vFans) == 4 ); assert( Smt_VecEntryIsType(vFans, 0, SMT_PRS_DECLARE_FUN) ); // get name Fan = Vec_IntEntry(vFans, 1); assert( Smt_EntryIsName(Fan) ); pName = Smt_EntryName(p, Fan); + // added: giving a global suffix + pName_glb = (char *) malloc(strlen(pName) + 4 + 1); + strcpy(pName_glb,pName); + strcat(pName_glb,SMT_GLO_SUFFIX); + // FIXME: delete memory of pName + pName = pName_glb; // skip () Fan = Vec_IntEntry(vFans, 2); assert( !Smt_EntryIsName(Fan) ); - vFans2 = Smt_VecEntryNode(p, vFans, 2); - if ( Vec_IntSize(vFans2) > 0 ) - { - printf( "File parsing error: Uninterpreted functions are not supported.\n" ); - Wlc_NtkFree( pNtk ); pNtk = NULL; - goto finish; - } // check type (Bool or BitVec) Fan = Vec_IntEntry(vFans, 3); if ( Smt_EntryIsName(Fan) ) @@ -1259,9 +1321,11 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p ) Vec_IntPush( &pNtk->vValues, nBits ); Vec_IntPush( &pNtk->vValues, Range ); nBits += Range; + ABC_FREE( pName_glb ); } // create constants - else if ( Abc_Lit2Var(Fan) == SMT_PRS_DEFINE_FUN ) + /* + else if ( Abc_Lit2Var(Fan) == SMT_PRS_DEFINE_FUN ) // added: we parse DEFINE_FUN in LET { assert( Vec_IntSize(vFans) == 5 ); assert( Smt_VecEntryIsType(vFans, 0, SMT_PRS_DEFINE_FUN) ); @@ -1269,6 +1333,14 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p ) Fan = Vec_IntEntry(vFans, 1); assert( Smt_EntryIsName(Fan) ); pName = Smt_EntryName(p, Fan); + + // added: giving a global suffix + char * pName_glb = (char *) malloc(strlen(pName) + 4 + 1); + strcpy(pName_glb,pName); + strcat(pName_glb,SMT_GLO_SUFFIX); + // FIXME: delete memory of pName + pName = pName_glb; + // skip () Fan = Vec_IntEntry(vFans, 2); assert( !Smt_EntryIsName(Fan) ); @@ -1278,13 +1350,17 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p ) { // (define-fun s_2 () Bool false) assert( !strcmp("Bool", Smt_VecEntryName(p, vFans, 3)) ); - iObj = Smt_PrsBuild2_rec( pNtk, p, Vec_IntEntry(vFans, 4), -1, pName ); - if ( iObj == 0 ) - { - Wlc_NtkFree( pNtk ); pNtk = NULL; - goto finish; - } - continue; + Range = 1; + pValue = Smt_VecEntryName(p, vFans, 4); + + //printf("value: %s\n",pValue); + + if ( !strcmp("false", pValue) ) + pValue = "#b0"; + else if ( !strcmp("true", pValue) ) + pValue = "#b1"; + else assert( 0 ); + Status = Smt_PrsBuildConstant( pNtk, pValue, Range, pName ); } else { @@ -1292,6 +1368,7 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p ) // (define-fun s1 () (_ BitVec 8) (bvneg #x7f)) // get range Fan = Vec_IntEntry(vFans, 3); + assert( !Smt_EntryIsName(Fan) ); vFans2 = Smt_VecEntryNode(p, vFans, 3); assert( Vec_IntSize(vFans2) == 3 ); @@ -1299,11 +1376,24 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p ) assert( !strcmp("BitVec", Smt_VecEntryName(p, vFans2, 1)) ); // get range Fan = Vec_IntEntry(vFans2, 2); + assert( Smt_EntryIsName(Fan) ); pRange = Smt_EntryName(p, Fan); Range = atoi(pRange); + + // added: can parse functions too + Vec_Int_t * vFans3 = Smt_VecEntryNode(p, vFans, 4); + Fan = Vec_IntEntry(vFans3, 0); + // get constant - Fan = Vec_IntEntry(vFans, 4); + //Fan = Vec_IntEntry(vFans, 4); + + //printf("fan3: %s\n",Fan); + //printf("fan0: %s\n",Smt_VecEntryName(p, vFans3, 0)); + //printf("fan1: %s\n",Smt_VecEntryName(p, vFans3, 1)); + //printf("fan2: %s\n",Smt_VecEntryName(p, vFans3, 2)); + //printf("fan3: %s\n",Smt_VecEntryName(p, vFans3, 3)); + Status = Smt_PrsBuildNode( pNtk, p, Fan, Range, pName ); } if ( !Status ) @@ -1312,6 +1402,57 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p ) goto finish; } } + */ + // added: new way to parse define-fun + // create constants + else if ( Abc_Lit2Var(Fan) == SMT_PRS_DEFINE_FUN ) + { + char * pName_glb; + // (define-fun def_16001 () Bool (or def_15999 def_16000)) + // (define-fun def_15990 () (_ BitVec 24) (concat def_15988 def_15989)) + assert( Smt_VecEntryIsType(vFans, 0, SMT_PRS_DEFINE_FUN) ); + assert( Vec_IntSize(vFans) == 5 ); // const or definition + + // get name + Fan = Vec_IntEntry(vFans, 1); + assert( Smt_EntryIsName(Fan) ); + pName = Smt_EntryName(p, Fan); + // added: giving a global suffix + pName_glb = (char *) malloc(strlen(pName) + 4 + 1); + strcpy(pName_glb,pName); + strcat(pName_glb,SMT_GLO_SUFFIX); + // FIXME: delete memory of pName + pName = pName_glb; + + //get range + Fan = Vec_IntEntry(vFans, 3); + if ( Smt_EntryIsName(Fan) ) + { + // (define-fun s_2 () Bool false) + assert( !strcmp("Bool", Smt_VecEntryName(p, vFans, 3)) ); + Range = 1; + } + else + { + // (define-fun s702 () (_ BitVec 4) #xe) + // (define-fun s1 () (_ BitVec 8) (bvneg #x7f)) + assert( !Smt_EntryIsName(Fan) ); + vFans2 = Smt_VecEntryNode(p, vFans, 3); + assert( Vec_IntSize(vFans2) == 3 ); + assert( !strcmp("_", Smt_VecEntryName(p, vFans2, 0)) ); + assert( !strcmp("BitVec", Smt_VecEntryName(p, vFans2, 1)) ); + // get range + Fan = Vec_IntEntry(vFans2, 2); + assert( Smt_EntryIsName(Fan) ); + pRange = Smt_EntryName(p, Fan); + Range = atoi(pRange); + } + + iObj = Smt_PrsBuild2_rec( pNtk, p, Vec_IntEntry(vFans, 4), Range, pName ); + assert( iObj ); + ABC_FREE( pName_glb ); + } + // collect assertion outputs else if ( Abc_Lit2Var(Fan) == SMT_PRS_ASSERT ) { @@ -1321,6 +1462,7 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p ) //(assert (not (= s0 #x00))) assert( Vec_IntSize(vFans) == 2 ); assert( Smt_VecEntryIsType(vFans, 0, SMT_PRS_ASSERT) ); + pNtk->nAssert++; // added iObj = Smt_PrsBuild2_rec( pNtk, p, Vec_IntEntry(vFans, 1), -1, NULL ); if ( iObj == 0 ) { @@ -1336,6 +1478,9 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p ) // build AND of asserts if ( Vec_IntSize(vAsserts) == 1 ) iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_BUF, 0, 1, vAsserts, "miter" ); + // added: 0 asserts + else if ( Vec_IntSize(vAsserts) == 0 ) + iObj = Smt_PrsBuildConstant( pNtk, "#b1", 1, "miter" ); else { iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_BIT_CONCAT, 0, Vec_IntSize(vAsserts), vAsserts, NULL ); @@ -1413,18 +1558,35 @@ static inline char * Smt_PrsLoadFile( char * pFileName, char ** ppLimit ) static inline int Smt_PrsRemoveComments( char * pBuffer, char * pLimit ) { char * pTemp; int nCount1 = 0, nCount2 = 0, fHaveBar = 0; + int backslash = 0; for ( pTemp = pBuffer; pTemp < pLimit; pTemp++ ) { if ( *pTemp == '(' ) - nCount1++; + { if ( !fHaveBar ) nCount1++; } else if ( *pTemp == ')' ) - nCount2++; + { if ( !fHaveBar ) nCount2++; } else if ( *pTemp == '|' ) fHaveBar ^= 1; else if ( *pTemp == ';' && !fHaveBar ) while ( *pTemp && *pTemp != '\n' ) *pTemp++ = ' '; + // added: hack to remove quotes + else if ( *pTemp == '\"' && *(pTemp-1) != '\\' && !fHaveBar ) + { + *pTemp++ = ' '; + while ( *pTemp && (*pTemp != '\"' || backslash)) + { + if (*pTemp == '\\') + backslash = 1; + else + backslash = 0; + *pTemp++ = ' '; + } + // remove the last quote symbol + *pTemp = ' '; + } } + if ( nCount1 != nCount2 ) printf( "The input SMTLIB file has different number of opening and closing parentheses (%d and %d).\n", nCount1, nCount2 ); else if ( nCount1 == 0 ) @@ -1486,6 +1648,7 @@ static inline void Smt_PrsSkipNonSpaces( Smt_Prs_t * p ) } void Smt_PrsReadLines( Smt_Prs_t * p ) { + int fFirstTime = 1; assert( Vec_IntSize(&p->vStack) == 0 ); //assert( Vec_WecSize(&p->vDepth) == 0 ); assert( Vec_WecSize(&p->vObjs) == 0 ); @@ -1499,6 +1662,16 @@ void Smt_PrsReadLines( Smt_Prs_t * p ) for ( p->pCur = p->pBuffer; p->pCur < p->pLimit; p->pCur++ ) { Smt_PrsSkipSpaces( p ); + if ( fFirstTime && *p->pCur == '|' ) + { + fFirstTime = 0; + *p->pCur = ' '; + while ( *p->pCur && *p->pCur != '|' ) + *p->pCur++ = ' '; + if ( *p->pCur == '|' ) + *p->pCur = ' '; + continue; + } if ( *p->pCur == '(' ) { // add new node at this depth @@ -1524,12 +1697,13 @@ void Smt_PrsReadLines( Smt_Prs_t * p ) { // remove strange characters (this can lead to name clashes) int iToken; + /* commented out for SMT comp char * pTemp; if ( *pStart == '?' ) *pStart = '_'; for ( pTemp = pStart; pTemp < p->pCur; pTemp++ ) if ( *pTemp == '.' ) - *pTemp = '_'; + *pTemp = '_';*/ // create and save token for this string iToken = Abc_NamStrFindOrAddLim( p->pStrs, pStart, p->pCur--, NULL ); Vec_IntPush( Vec_WecEntry(&p->vObjs, Vec_IntEntryLast(&p->vStack)), Abc_Var2Lit(iToken, 1) ); diff --git a/src/base/wlc/wlcReadVer.c b/src/base/wlc/wlcReadVer.c index fa3efacd..e4a65ecf 100644 --- a/src/base/wlc/wlcReadVer.c +++ b/src/base/wlc/wlcReadVer.c @@ -28,7 +28,7 @@ ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// // Word-level Verilog file parser -#define WLV_PRS_MAX_LINE 1000 +#define WLV_PRS_MAX_LINE 10000 typedef struct Wlc_Prs_t_ Wlc_Prs_t; struct Wlc_Prs_t_ @@ -1265,8 +1265,7 @@ Wlc_Ntk_t * Wlc_ReadVer( char * pFileName, char * pStr ) if ( !Wlc_PrsDerive( p ) ) goto finish; // derive topological order - pNtk = Wlc_NtkDupDfs( p->pNtk ); - Wlc_NtkTransferNames( pNtk, p->pNtk ); + pNtk = Wlc_NtkDupDfs( p->pNtk, 0, 1 ); pNtk->pSpec = Abc_UtilStrsav( pFileName ); finish: Wlc_PrsPrintErrorMessage( p ); diff --git a/src/base/wlc/wlcShow.c b/src/base/wlc/wlcShow.c new file mode 100644 index 00000000..1601d602 --- /dev/null +++ b/src/base/wlc/wlcShow.c @@ -0,0 +1,337 @@ +/**CFile**************************************************************** + + FileName [wlcShow.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Verilog parser.] + + Synopsis [Parses several flavors of word-level Verilog.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - August 22, 2014.] + + Revision [$Id: wlcShow.c,v 1.00 2014/09/12 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "wlc.h" + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + + +/**Function************************************************************* + + Synopsis [Writes the graph structure of WLC for DOT.] + + Description [Useful for graph visualization using tools such as GraphViz: + http://www.graphviz.org/] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Wlc_NtkDumpDot( Wlc_Ntk_t * p, char * pFileName, Vec_Int_t * vBold ) +{ + FILE * pFile; + Wlc_Obj_t * pNode; + int LevelMax, Prev, Level, i; + + if ( Wlc_NtkObjNum(p) > 2000 ) + { + fprintf( stdout, "Cannot visualize WLC with more than %d nodes.\n", 2000 ); + return; + } + if ( (pFile = fopen( pFileName, "w" )) == NULL ) + { + fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", pFileName ); + return; + } + + // mark the nodes + if ( vBold ) + Wlc_NtkForEachObjVec( vBold, p, pNode, i ) + pNode->Mark = 1; + + // compute levels + LevelMax = 1 + Wlc_NtkCreateLevelsRev( p ); + + // write the DOT header + fprintf( pFile, "# %s\n", "WLC structure generated by ABC" ); + fprintf( pFile, "\n" ); + fprintf( pFile, "digraph WLC {\n" ); + fprintf( pFile, "size = \"7.5,10\";\n" ); +// fprintf( pFile, "ranksep = 0.5;\n" ); +// fprintf( pFile, "nodesep = 0.5;\n" ); + fprintf( pFile, "center = true;\n" ); +// fprintf( pFile, "orientation = landscape;\n" ); +// fprintf( pFile, "edge [fontsize = 10];\n" ); +// fprintf( pFile, "edge [dir = none];\n" ); + fprintf( pFile, "edge [dir = back];\n" ); + fprintf( pFile, "\n" ); + + // labels on the left of the picture + fprintf( pFile, "{\n" ); + fprintf( pFile, " node [shape = plaintext];\n" ); + fprintf( pFile, " edge [style = invis];\n" ); + fprintf( pFile, " LevelTitle1 [label=\"\"];\n" ); + fprintf( pFile, " LevelTitle2 [label=\"\"];\n" ); + // generate node names with labels + for ( Level = LevelMax; Level >= 0; Level-- ) + { + // the visible node name + fprintf( pFile, " Level%d", Level ); + fprintf( pFile, " [label = " ); + // label name + fprintf( pFile, "\"" ); + fprintf( pFile, "\"" ); + fprintf( pFile, "];\n" ); + } + + // genetate the sequence of visible/invisible nodes to mark levels + fprintf( pFile, " LevelTitle1 -> LevelTitle2 ->" ); + for ( Level = LevelMax; Level >= 0; Level-- ) + { + // the visible node name + fprintf( pFile, " Level%d", Level ); + // the connector + if ( Level != 0 ) + fprintf( pFile, " ->" ); + else + fprintf( pFile, ";" ); + } + fprintf( pFile, "\n" ); + fprintf( pFile, "}" ); + fprintf( pFile, "\n" ); + fprintf( pFile, "\n" ); + + // generate title box on top + fprintf( pFile, "{\n" ); + fprintf( pFile, " rank = same;\n" ); + fprintf( pFile, " LevelTitle1;\n" ); + fprintf( pFile, " title1 [shape=plaintext,\n" ); + fprintf( pFile, " fontsize=20,\n" ); + fprintf( pFile, " fontname = \"Times-Roman\",\n" ); + fprintf( pFile, " label=\"" ); + fprintf( pFile, "%s", "WLC structure generated by ABC" ); + fprintf( pFile, "\\n" ); + fprintf( pFile, "Benchmark \\\"%s\\\". ", p->pName ); +// fprintf( pFile, "Time was %s. ", Extra_TimeStamp() ); + fprintf( pFile, "\"\n" ); + fprintf( pFile, " ];\n" ); + fprintf( pFile, "}" ); + fprintf( pFile, "\n" ); + fprintf( pFile, "\n" ); + + // generate statistics box + fprintf( pFile, "{\n" ); + fprintf( pFile, " rank = same;\n" ); + fprintf( pFile, " LevelTitle2;\n" ); + fprintf( pFile, " title2 [shape=plaintext,\n" ); + fprintf( pFile, " fontsize=18,\n" ); + fprintf( pFile, " fontname = \"Times-Roman\",\n" ); + fprintf( pFile, " label=\"" ); + fprintf( pFile, "The word-level network contains %d nodes and spans %d levels.", Wlc_NtkObjNum(p)-Wlc_NtkCiNum(p), LevelMax-1 ); + fprintf( pFile, "\\n" ); + fprintf( pFile, "\"\n" ); + fprintf( pFile, " ];\n" ); + fprintf( pFile, "}" ); + fprintf( pFile, "\n" ); + fprintf( pFile, "\n" ); + + // generate the COs + fprintf( pFile, "{\n" ); + fprintf( pFile, " rank = same;\n" ); + // the labeling node of this level + fprintf( pFile, " Level%d;\n", LevelMax ); + // generate the CO nodes + Wlc_NtkForEachCo( p, pNode, i ) + { + pNode = Wlc_ObjCo2PoFo(p, i); + fprintf( pFile, " NodePo%d [label = \"%s_in %d\"", Wlc_ObjId(p, pNode), Wlc_ObjName(p, Wlc_ObjId(p, pNode)), Wlc_ObjRange(pNode) ); + fprintf( pFile, ", shape = %s", i < Wlc_NtkPoNum(p) ? "invtriangle" : "box" ); + fprintf( pFile, ", color = coral, fillcolor = coral" ); + fprintf( pFile, "];\n" ); + } + fprintf( pFile, "}" ); + fprintf( pFile, "\n" ); + fprintf( pFile, "\n" ); + + // generate nodes of each rank + for ( Level = LevelMax - 1; Level > 0; Level-- ) + { + fprintf( pFile, "{\n" ); + fprintf( pFile, " rank = same;\n" ); + // the labeling node of this level + fprintf( pFile, " Level%d;\n", Level ); + Wlc_NtkForEachObj( p, pNode, i ) + { + if ( (int)Wlc_ObjLevel(p, pNode) != Level ) + continue; + + if ( pNode->Type == WLC_OBJ_CONST ) + { + fprintf( pFile, " Node%d [label = \"0x", i ); + Abc_TtPrintHexArrayRev( pFile, (word *)Wlc_ObjConstValue(pNode), (Wlc_ObjRange(pNode) + 3) / 4 ); + fprintf( pFile, "\"" ); + } + else if ( pNode->Type == WLC_OBJ_BUF || pNode->Type == WLC_OBJ_MUX ) + fprintf( pFile, " Node%d [label = \"%d\"", i, Wlc_ObjRange(pNode) ); + else if ( pNode->Type >= WLC_OBJ_LOGIC_NOT && pNode->Type <= WLC_OBJ_COMP_MOREEQU ) + fprintf( pFile, " Node%d [label = \"%s\"", i, Wlc_ObjTypeName(pNode) ); + else + fprintf( pFile, " Node%d [label = \"%s %d\"", i, Wlc_ObjTypeName(pNode), Wlc_ObjRange(pNode) ); + + if ( pNode->Type == WLC_OBJ_ARI_MULTI ) + fprintf( pFile, ", shape = doublecircle" ); + else if ( pNode->Type >= WLC_OBJ_COMP_EQU && pNode->Type <= WLC_OBJ_COMP_MOREEQU ) + fprintf( pFile, ", shape = diamond" ); + else if ( pNode->Type == WLC_OBJ_BIT_SELECT || pNode->Type == WLC_OBJ_BIT_CONCAT ) + fprintf( pFile, ", shape = box" ); + else if ( pNode->Type == WLC_OBJ_BUF || pNode->Type == WLC_OBJ_BIT_ZEROPAD || pNode->Type == WLC_OBJ_BIT_SIGNEXT ) + fprintf( pFile, ", shape = triangle" ); + else if ( pNode->Type == WLC_OBJ_MUX ) + fprintf( pFile, ", shape = trapezium" ); + else + fprintf( pFile, ", shape = ellipse" ); + + if ( vBold ? pNode->Mark : ((pNode->Type >= WLC_OBJ_ARI_ADD && pNode->Type <= WLC_OBJ_ARI_SQUARE) || pNode->Type == WLC_OBJ_BIT_NOT) ) + fprintf( pFile, ", style = filled" ); + fprintf( pFile, "];\n" ); + } + fprintf( pFile, "}" ); + fprintf( pFile, "\n" ); + fprintf( pFile, "\n" ); + } + + // generate the CI nodes + fprintf( pFile, "{\n" ); + fprintf( pFile, " rank = same;\n" ); + // the labeling node of this level + fprintf( pFile, " Level%d;\n", 0 ); + // generate the CI nodes + Wlc_NtkForEachCi( p, pNode, i ) + { + fprintf( pFile, " Node%d [label = \"%s %d\"", Wlc_ObjId(p, pNode), Wlc_ObjName(p, Wlc_ObjId(p, pNode)), Wlc_ObjRange(pNode) ); + fprintf( pFile, ", shape = %s", i < Wlc_NtkPiNum(p) ? "triangle" : "box" ); + fprintf( pFile, ", color = coral, fillcolor = coral" ); + fprintf( pFile, "];\n" ); + } + fprintf( pFile, "}" ); + fprintf( pFile, "\n" ); + fprintf( pFile, "\n" ); + + // generate invisible edges from the square down + fprintf( pFile, "title1 -> title2 [style = invis];\n" ); + Wlc_NtkForEachCo( p, pNode, i ) + { + pNode = Wlc_ObjCo2PoFo( p, i ); + fprintf( pFile, "title2 -> NodePo%d [style = invis];\n", Wlc_ObjId(p, pNode) ); + } + // generate invisible edges among the COs + Prev = -1; + Wlc_NtkForEachCo( p, pNode, i ) + { + pNode = Wlc_ObjCo2PoFo( p, i ); + if ( i > 0 ) + fprintf( pFile, "NodePo%d -> NodePo%d [style = invis];\n", Prev, Wlc_ObjId(p, pNode) ); + Prev = Wlc_ObjId(p, pNode); + } + // generate invisible edges among the CIs + Prev = -1; + Wlc_NtkForEachCi( p, pNode, i ) + { + if ( i > 0 ) + fprintf( pFile, "Node%d -> Node%d [style = invis];\n", Prev, Wlc_ObjId(p, pNode) ); + Prev = Wlc_ObjId(p, pNode); + } + + // generate edges + Wlc_NtkForEachCo( p, pNode, i ) + { + fprintf( pFile, "NodePo%d", Wlc_ObjId(p, Wlc_ObjCo2PoFo(p, i)) ); + fprintf( pFile, " -> " ); + fprintf( pFile, "Node%d", Wlc_ObjId(p, pNode) ); + fprintf( pFile, " [" ); + fprintf( pFile, "style = %s", pNode->Signed? "dotted" : "solid" ); + fprintf( pFile, "]" ); + fprintf( pFile, ";\n" ); + } + Wlc_NtkForEachObj( p, pNode, i ) + { + int k, iFanin; + if ( Wlc_ObjIsCi(pNode) ) + continue; + // generate the edge from this node to the next + Wlc_ObjForEachFanin( pNode, iFanin, k ) + { + fprintf( pFile, "Node%d", i ); + fprintf( pFile, " -> " ); + fprintf( pFile, "Node%d", iFanin ); + fprintf( pFile, " [" ); + fprintf( pFile, "style = %s", Wlc_NtkObj(p, iFanin)->Signed? "dotted" : "solid" ); + if ( pNode->Type == WLC_OBJ_MUX && k == 0 ) + fprintf( pFile, ", style = %s", "bold" ); + fprintf( pFile, "]" ); + fprintf( pFile, ";\n" ); + } + } + fprintf( pFile, "}" ); + fprintf( pFile, "\n" ); + fprintf( pFile, "\n" ); + fclose( pFile ); + + // unmark nodes + if ( vBold ) + Wlc_NtkCleanMarks( p ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Wlc_NtkShow( Wlc_Ntk_t * p, Vec_Int_t * vBold ) +{ + extern void Abc_ShowFile( char * FileNameDot ); + FILE * pFile; + char FileNameDot[200]; + sprintf( FileNameDot, "%s", Extra_FileNameGenericAppend(p->pName, ".dot") ); + // check that the file can be opened + if ( (pFile = fopen( FileNameDot, "w" )) == NULL ) + { + fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", FileNameDot ); + return; + } + fclose( pFile ); + // generate the file + Wlc_NtkDumpDot( p, FileNameDot, vBold ); + // visualize the file + Abc_ShowFile( FileNameDot ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/base/wlc/wlcSim.c b/src/base/wlc/wlcSim.c index 20ac8c61..e2fcd1f8 100644 --- a/src/base/wlc/wlcSim.c +++ b/src/base/wlc/wlcSim.c @@ -43,13 +43,13 @@ ABC_NAMESPACE_IMPL_START ***********************************************************************/ static inline word * Wlc_ObjSim( Gia_Man_t * p, int iObj ) { - return Vec_WrdEntryP( p->vSims, p->iPatsPi * iObj ); + return Vec_WrdEntryP( p->vSims, p->nSimWords * iObj ); } static inline void Wlc_ObjSimPi( Gia_Man_t * p, int iObj ) { int w; word * pSim = Wlc_ObjSim( p, iObj ); - for ( w = 0; w < p->iPatsPi; w++ ) + for ( w = 0; w < p->nSimWords; w++ ) pSim[w] = Gia_ManRandomW( 0 ); } static inline void Wlc_ObjSimRo( Gia_Man_t * p, int iObj ) @@ -57,7 +57,7 @@ static inline void Wlc_ObjSimRo( Gia_Man_t * p, int iObj ) int w; word * pSimRo = Wlc_ObjSim( p, iObj ); word * pSimRi = Wlc_ObjSim( p, Gia_ObjRoToRiId(p, iObj) ); - for ( w = 0; w < p->iPatsPi; w++ ) + for ( w = 0; w < p->nSimWords; w++ ) pSimRo[w] = pSimRi[w]; } static inline void Wlc_ObjSimCo( Gia_Man_t * p, int iObj ) @@ -67,10 +67,10 @@ static inline void Wlc_ObjSimCo( Gia_Man_t * p, int iObj ) word * pSimCo = Wlc_ObjSim( p, iObj ); word * pSimDri = Wlc_ObjSim( p, Gia_ObjFaninId0(pObj, iObj) ); if ( Gia_ObjFaninC0(pObj) ) - for ( w = 0; w < p->iPatsPi; w++ ) + for ( w = 0; w < p->nSimWords; w++ ) pSimCo[w] = ~pSimDri[w]; else - for ( w = 0; w < p->iPatsPi; w++ ) + for ( w = 0; w < p->nSimWords; w++ ) pSimCo[w] = pSimDri[w]; } static inline void Wlc_ObjSimAnd( Gia_Man_t * p, int iObj ) @@ -81,16 +81,16 @@ static inline void Wlc_ObjSimAnd( Gia_Man_t * p, int iObj ) word * pSim0 = Wlc_ObjSim( p, Gia_ObjFaninId0(pObj, iObj) ); word * pSim1 = Wlc_ObjSim( p, Gia_ObjFaninId1(pObj, iObj) ); if ( Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) ) - for ( w = 0; w < p->iPatsPi; w++ ) + for ( w = 0; w < p->nSimWords; w++ ) pSim[w] = ~pSim0[w] & ~pSim1[w]; else if ( Gia_ObjFaninC0(pObj) && !Gia_ObjFaninC1(pObj) ) - for ( w = 0; w < p->iPatsPi; w++ ) + for ( w = 0; w < p->nSimWords; w++ ) pSim[w] = ~pSim0[w] & pSim1[w]; else if ( !Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) ) - for ( w = 0; w < p->iPatsPi; w++ ) + for ( w = 0; w < p->nSimWords; w++ ) pSim[w] = pSim0[w] & ~pSim1[w]; else - for ( w = 0; w < p->iPatsPi; w++ ) + for ( w = 0; w < p->nSimWords; w++ ) pSim[w] = pSim0[w] & pSim1[w]; } @@ -135,7 +135,7 @@ Vec_Ptr_t * Wlc_NtkSimulate( Wlc_Ntk_t * p, Vec_Int_t * vNodes, int nWords, int // allocate simulation info for one timeframe Vec_WrdFreeP( &pGia->vSims ); pGia->vSims = Vec_WrdStart( Gia_ManObjNum(pGia) * nWords ); - pGia->iPatsPi = nWords; + pGia->nSimWords = nWords; // allocate resulting simulation info vRes = Vec_PtrAlloc( Vec_IntSize(vNodes) ); Wlc_NtkForEachObjVec( vNodes, p, pWlcObj, i ) @@ -188,7 +188,7 @@ Vec_Ptr_t * Wlc_NtkSimulate( Wlc_Ntk_t * p, Vec_Int_t * vNodes, int nWords, int printf( "Replaced %d dangling internal bits with constant 0.\n", Counter ); } Vec_WrdFreeP( &pGia->vSims ); - pGia->iPatsPi = 0; + pGia->nSimWords = 0; Gia_ManStop( pGia ); return vRes; } diff --git a/src/base/wlc/wlcUif.c b/src/base/wlc/wlcUif.c new file mode 100644 index 00000000..78451c17 --- /dev/null +++ b/src/base/wlc/wlcUif.c @@ -0,0 +1,290 @@ +/**CFile**************************************************************** + + FileName [wlcUif.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Verilog parser.] + + Synopsis [Abstraction for word-level networks.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - August 22, 2014.] + + Revision [$Id: wlcUif.c,v 1.00 2014/09/12 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "wlc.h" + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Check if two objects have the same input/output signatures.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Wlc_NtkPairIsUifable( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Wlc_Obj_t * pObj2 ) +{ + Wlc_Obj_t * pFanin, * pFanin2; int k; + if ( Wlc_ObjRange(pObj) != Wlc_ObjRange(pObj2) ) + return 0; + if ( Wlc_ObjIsSigned(pObj) != Wlc_ObjIsSigned(pObj2) ) + return 0; + if ( Wlc_ObjFaninNum(pObj) != Wlc_ObjFaninNum(pObj2) ) + return 0; + for ( k = 0; k < Wlc_ObjFaninNum(pObj); k++ ) + { + pFanin = Wlc_ObjFanin(p, pObj, k); + pFanin2 = Wlc_ObjFanin(p, pObj2, k); + if ( Wlc_ObjRange(pFanin) != Wlc_ObjRange(pFanin2) ) + return 0; + if ( Wlc_ObjIsSigned(pFanin) != Wlc_ObjIsSigned(pFanin2) ) + return 0; + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Collect IDs of the multipliers.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Wlc_NtkCollectMultipliers( Wlc_Ntk_t * p ) +{ + Wlc_Obj_t * pObj; int i; + Vec_Int_t * vBoxIds = Vec_IntAlloc( 100 ); + Wlc_NtkForEachObj( p, pObj, i ) + if ( pObj->Type == WLC_OBJ_ARI_MULTI ) + Vec_IntPush( vBoxIds, i ); + if ( Vec_IntSize( vBoxIds ) > 0 ) + return vBoxIds; + Vec_IntFree( vBoxIds ); + return NULL; +} + +/**Function************************************************************* + + Synopsis [Returns all pairs of uifable multipliers.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Wlc_NtkFindUifableMultiplierPairs( Wlc_Ntk_t * p ) +{ + Vec_Int_t * vMultis = Wlc_NtkCollectMultipliers( p ); + Vec_Int_t * vPairs = Vec_IntAlloc( 2 ); + Wlc_Obj_t * pObj, * pObj2; int i, k; + // iterate through unique pairs + Wlc_NtkForEachObjVec( vMultis, p, pObj, i ) + Wlc_NtkForEachObjVec( vMultis, p, pObj2, k ) + { + if ( k == i ) + break; + if ( Wlc_NtkPairIsUifable( p, pObj, pObj2 ) ) + { + Vec_IntPush( vPairs, Wlc_ObjId(p, pObj) ); + Vec_IntPush( vPairs, Wlc_ObjId(p, pObj2) ); + } + } + Vec_IntFree( vMultis ); + if ( Vec_IntSize( vPairs ) > 0 ) + return vPairs; + Vec_IntFree( vPairs ); + return NULL; +} + + + +/**Function************************************************************* + + Synopsis [Abstracts nodes by replacing their outputs with new PIs.] + + Description [If array is NULL, abstract all multipliers.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Wlc_Ntk_t * Wlc_NtkAbstractNodes( Wlc_Ntk_t * p, Vec_Int_t * vNodesInit ) +{ + Vec_Int_t * vNodes = vNodesInit; + Wlc_Ntk_t * pNew; + Wlc_Obj_t * pObj; + int i, k, iObj, iFanin; + // get multipliers if not given + if ( vNodes == NULL ) + vNodes = Wlc_NtkCollectMultipliers( p ); + if ( vNodes == NULL ) + return NULL; + // mark nodes + Wlc_NtkForEachObjVec( vNodes, p, pObj, i ) + pObj->Mark = 1; + // iterate through the nodes in the DFS order + Wlc_NtkCleanCopy( p ); + Wlc_NtkForEachObj( p, pObj, i ) + { + if ( i == Vec_IntSize(&p->vCopies) ) + break; + if ( pObj->Mark ) { + // clean + pObj->Mark = 0; + // add fresh PI with the same number of bits + iObj = Wlc_ObjAlloc( p, WLC_OBJ_PI, Wlc_ObjIsSigned(pObj), Wlc_ObjRange(pObj) - 1, 0 ); + } + else { + // update fanins + Wlc_ObjForEachFanin( pObj, iFanin, k ) + Wlc_ObjFanins(pObj)[k] = Wlc_ObjCopy(p, iFanin); + // node to remain + iObj = i; + } + Wlc_ObjSetCopy( p, i, iObj ); + } + // POs do not change in this procedure + if ( vNodes != vNodesInit ) + Vec_IntFree( vNodes ); + // reconstruct topological order + pNew = Wlc_NtkDupDfs( p, 0, 1 ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Adds UIF constraints to node pairs and updates POs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Wlc_Ntk_t * Wlc_NtkUifNodePairs( Wlc_Ntk_t * p, Vec_Int_t * vPairsInit ) +{ + Vec_Int_t * vPairs = vPairsInit; + Wlc_Ntk_t * pNew; + Wlc_Obj_t * pObj, * pObj2; + Vec_Int_t * vUifConstrs, * vCompares, * vFanins; + int i, k, iObj, iObj2, iObjNew, iObjNew2; + int iFanin, iFanin2, iFaninNew; + // get multiplier pairs if not given + if ( vPairs == NULL ) + vPairs = Wlc_NtkFindUifableMultiplierPairs( p ); + if ( vPairs == NULL ) + return NULL; + // sanity checks + assert( Vec_IntSize(vPairs) > 0 && Vec_IntSize(vPairs) % 2 == 0 ); + // iterate through node pairs + vFanins = Vec_IntAlloc( 100 ); + vCompares = Vec_IntAlloc( 100 ); + vUifConstrs = Vec_IntAlloc( 100 ); + Vec_IntForEachEntryDouble( vPairs, iObj, iObj2, i ) + { + // get two nodes + pObj = Wlc_NtkObj( p, iObj ); + pObj2 = Wlc_NtkObj( p, iObj2 ); + assert( Wlc_NtkPairIsUifable(p, pObj, pObj2) ); + // create fanin comparator nodes + Vec_IntClear( vCompares ); + Wlc_ObjForEachFanin( pObj, iFanin, k ) + { + iFanin2 = Wlc_ObjFaninId( pObj2, k ); + Vec_IntFillTwo( vFanins, 2, iFanin, iFanin2 ); + iFaninNew = Wlc_ObjCreate( p, WLC_OBJ_COMP_NOTEQU, 0, 0, 0, vFanins ); + Vec_IntPush( vCompares, iFaninNew ); + // note that a pointer to Wlc_Obj_t (for example, pObj) can be invalidated after a call to + // Wlc_ObjCreate() due to a possible realloc of the internal array of objects... + pObj = Wlc_NtkObj( p, iObj ); + } + // concatenate fanin comparators + iObjNew = Wlc_ObjCreate( p, WLC_OBJ_BIT_CONCAT, 0, Vec_IntSize(vCompares) - 1, 0, vCompares ); + // create reduction-OR node + Vec_IntFill( vFanins, 1, iObjNew ); + iObjNew = Wlc_ObjCreate( p, WLC_OBJ_REDUCT_OR, 0, 0, 0, vFanins ); + // craete output comparator node + Vec_IntFillTwo( vFanins, 2, iObj, iObj2 ); + iObjNew2 = Wlc_ObjCreate( p, WLC_OBJ_COMP_EQU, 0, 0, 0, vFanins ); + // create implication node (iObjNew is already complemented above) + Vec_IntFillTwo( vFanins, 2, iObjNew, iObjNew2 ); + iObjNew = Wlc_ObjCreate( p, WLC_OBJ_LOGIC_OR, 0, 0, 0, vFanins ); + // save the constraint + Vec_IntPush( vUifConstrs, iObjNew ); + } + // derive the AND of the UIF contraints + assert( Vec_IntSize(vUifConstrs) > 0 ); + if ( Vec_IntSize(vUifConstrs) == 1 ) + iObjNew = Vec_IntEntry( vUifConstrs, 0 ); + else + { + // concatenate + iObjNew = Wlc_ObjCreate( p, WLC_OBJ_BIT_CONCAT, 0, Vec_IntSize(vUifConstrs) - 1, 0, vUifConstrs ); + // create reduction-AND node + Vec_IntFill( vFanins, 1, iObjNew ); + iObjNew = Wlc_ObjCreate( p, WLC_OBJ_REDUCT_AND, 0, 0, 0, vFanins ); + } + // update each PO to point to the new node + Wlc_NtkForEachPo( p, pObj, i ) + { + iObj = Wlc_ObjId(p, pObj); + Vec_IntFillTwo( vFanins, 2, iObj, iObjNew ); + iObjNew = Wlc_ObjCreate( p, WLC_OBJ_LOGIC_AND, 0, 0, 0, vFanins ); + // note that a pointer to Wlc_Obj_t (for example, pObj) can be invalidated after a call to + // Wlc_ObjCreate() due to a possible realloc of the internal array of objects... + pObj = Wlc_NtkObj( p, iObj ); + // update PO/CO arrays + assert( Vec_IntEntry(&p->vPos, i) == iObj ); + assert( Vec_IntEntry(&p->vCos, i) == iObj ); + Vec_IntWriteEntry( &p->vPos, i, iObjNew ); + Vec_IntWriteEntry( &p->vCos, i, iObjNew ); + // transfer the PO attribute + Wlc_NtkObj(p, iObjNew)->fIsPo = 1; + assert( pObj->fIsPo ); + pObj->fIsPo = 0; + } + // cleanup + Vec_IntFree( vUifConstrs ); + Vec_IntFree( vCompares ); + Vec_IntFree( vFanins ); + if ( vPairs != vPairsInit ) + Vec_IntFree( vPairs ); + // reconstruct topological order + pNew = Wlc_NtkDupDfs( p, 0, 1 ); + return pNew; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/base/wlc/wlcWriteVer.c b/src/base/wlc/wlcWriteVer.c index cf0e528f..c4dee094 100644 --- a/src/base/wlc/wlcWriteVer.c +++ b/src/base/wlc/wlcWriteVer.c @@ -409,7 +409,7 @@ void Wlc_WriteVerInt( FILE * pFile, Wlc_Ntk_t * p, int fNoFlops ) fprintf( pFile, " reg%d (", i ); fprintf( pFile, " .q( %s ),", Wlc_ObjName(p, Wlc_ObjId(p, pObj)) ); fprintf( pFile, " .qbar()," ); - fprintf( pFile, " .d( %s ),", Wlc_ObjName(p, Wlc_ObjId(p, Wlc_ObjFoToFi(p, pObj))) ); + fprintf( pFile, " .d( %s ),", Wlc_ObjName(p, Wlc_ObjId(p, Wlc_ObjFo2Fi(p, pObj))) ); fprintf( pFile, " .clk( %s ),", "1\'b0" ); fprintf( pFile, " .arst( %s ),", "1\'b0" ); if ( p->vInits ) |