From 4b4646283fef561671191949cfb7149d87e06696 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 3 Sep 2020 16:43:53 -0700 Subject: Experiments with ICCAD CAD benchmarks (Problem A). --- src/base/acb/acbFunc.c | 23 +- src/base/acb/acbTest.c | 611 +++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 627 insertions(+), 7 deletions(-) (limited to 'src/base') diff --git a/src/base/acb/acbFunc.c b/src/base/acb/acbFunc.c index 4d7df1b5..eced70e7 100644 --- a/src/base/acb/acbFunc.c +++ b/src/base/acb/acbFunc.c @@ -35,8 +35,6 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -#define ACB_LAST_NAME_ID 14 - typedef enum { ACB_NONE = 0, // 0: unused ACB_MODULE, // 1: "module" @@ -52,6 +50,8 @@ typedef enum { ACB_NOR, // 11: "nor" ACB_XOR, // 12: "xor" ACB_XNOR, // 13: "xnor" + ACB_MUX, // 14: "_HMUX" + ACB_DC, // 15: "_DC" ACB_UNUSED // 14: unused } Acb_KeyWords_t; @@ -70,6 +70,8 @@ static inline char * Acb_Num2Name( int i ) if ( i == 11 ) return "nor"; if ( i == 12 ) return "xor"; if ( i == 13 ) return "xnor"; + if ( i == 14 ) return "_HMUX"; + if ( i == 15 ) return "_DC"; return NULL; } @@ -83,6 +85,8 @@ static inline int Acb_Type2Oper( int i ) if ( i == 11 ) return ABC_OPER_BIT_NOR; if ( i == 12 ) return ABC_OPER_BIT_XOR; if ( i == 13 ) return ABC_OPER_BIT_NXOR; + if ( i == 14 ) return ABC_OPER_BIT_MUX; + if ( i == 15 ) return ABC_OPER_TRI; assert( 0 ); return -1; } @@ -91,6 +95,7 @@ static inline char * Acb_Oper2Name( int i ) { if ( i == ABC_OPER_CONST_F ) return "const0"; if ( i == ABC_OPER_CONST_T ) return "const1"; + if ( i == ABC_OPER_CONST_X ) return "constX"; if ( i == ABC_OPER_BIT_BUF ) return "buf"; if ( i == ABC_OPER_BIT_INV ) return "not"; if ( i == ABC_OPER_BIT_AND ) return "and"; @@ -99,6 +104,8 @@ static inline char * Acb_Oper2Name( int i ) if ( i == ABC_OPER_BIT_NOR ) return "nor"; if ( i == ABC_OPER_BIT_XOR ) return "xor"; if ( i == ABC_OPER_BIT_NXOR ) return "xnor"; + if ( i == ABC_OPER_BIT_MUX ) return "mux"; + if ( i == ABC_OPER_TRI ) return "_DC"; assert( 0 ); return NULL; } @@ -245,14 +252,11 @@ void * Acb_VerilogSimpleParse( Vec_Int_t * vBuffer, Abc_Nam_t * pNames ) vCur = vOutputs; else if ( Token == ACB_WIRE ) vCur = vWires; - else if ( Token >= ACB_BUF && Token <= ACB_XNOR ) + else if ( Token >= ACB_BUF && Token < ACB_UNUSED ) { - //char * pToken = Abc_NamStr(pNames, Vec_IntEntry(vBuffer, i+1)); Vec_IntPush( vTypes, Token ); Vec_IntPush( vTypes, Vec_IntSize(vFanins) ); vCur = vFanins; - //if ( pToken[1] == 'z' && pToken[2] == '_' && pToken[3] == 'g' && pToken[4] == '_' ) - // i++; } else Vec_IntPush( vCur, Token ); @@ -288,6 +292,8 @@ void * Acb_VerilogSimpleParse( Vec_Int_t * vBuffer, Abc_Nam_t * pNames ) Ndr_AddObject( pDesign, ModuleID, ABC_OPER_CONST_F, 0, 0, 0, 0, 0, NULL, 1, &Token, NULL ); // no fanins if ( (Token = Abc_NamStrFind(pNames, "1\'b1")) ) Ndr_AddObject( pDesign, ModuleID, ABC_OPER_CONST_T, 0, 0, 0, 0, 0, NULL, 1, &Token, NULL ); // no fanins + if ( (Token = Abc_NamStrFind(pNames, "1\'bx")) ) + Ndr_AddObject( pDesign, ModuleID, ABC_OPER_CONST_X, 0, 0, 0, 0, 0, NULL, 1, &Token, NULL ); // no fanins Vec_IntForEachEntryDouble( vTypes, Token, Size, i ) if ( Token > 0 ) { @@ -440,7 +446,10 @@ void Acb_VerilogSimpleWrite( Acb_Ntk_t * p, char * pFileName ) { assert( Acb_ObjType(p, iObj) == ABC_OPER_CONST_F || Acb_ObjType(p, iObj) == ABC_OPER_CONST_T ); fprintf( pFile, " %s (", Acb_Oper2Name( ABC_OPER_BIT_BUF ) ); - fprintf( pFile, " 1\'b%d", Acb_ObjType(p, iObj) == ABC_OPER_CONST_T ); + if ( Acb_ObjType(p, iObj) == ABC_OPER_CONST_X ) + fprintf( pFile, " 1\'bx" ); + else + fprintf( pFile, " 1\'b%d", Acb_ObjType(p, iObj) == ABC_OPER_CONST_T ); fprintf( pFile, " );\n" ); } diff --git a/src/base/acb/acbTest.c b/src/base/acb/acbTest.c index fa632ca0..340e3551 100644 --- a/src/base/acb/acbTest.c +++ b/src/base/acb/acbTest.c @@ -19,6 +19,11 @@ ***********************************************************************/ #include "acb.h" +#include "aig/saig/saig.h" +#include "aig/gia/giaAig.h" +#include "base/abc/abc.h" +#include "proof/fraig/fraig.h" +#include "misc/util/utilTruth.h" ABC_NAMESPACE_IMPL_START @@ -26,10 +31,571 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +static int fForceZero = 0; + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManSimTry( Gia_Man_t * pF, Gia_Man_t * pG ) +{ + int i, j, n, nWords = 500; + Vec_Wrd_t * vSimsF, * vSimsG; + Abc_Random(1); + Vec_WrdFreeP( &pF->vSimsPi ); + Vec_WrdFreeP( &pG->vSimsPi ); + pF->vSimsPi = Vec_WrdStartRandom( Gia_ManCiNum(pF) * nWords ); + pG->vSimsPi = Vec_WrdDup( pF->vSimsPi ); + vSimsF = Gia_ManSimPatSim( pF ); + vSimsG = Gia_ManSimPatSim( pG ); + assert( Gia_ManObjNum(pF) * nWords == Vec_WrdSize(vSimsF) ); + for ( i = 0; i < Gia_ManCoNum(pF)/2; i++ ) + { + Gia_Obj_t * pObjFb = Gia_ManCo( pF, 2*i+0 ); + Gia_Obj_t * pObjFx = Gia_ManCo( pF, 2*i+1 ); + Gia_Obj_t * pObjGb = Gia_ManCo( pG, 2*i+0 ); + Gia_Obj_t * pObjGx = Gia_ManCo( pG, 2*i+1 ); + word * pSimFb = Vec_WrdEntryP(vSimsF, Gia_ObjId(pF, pObjFb)*nWords); + word * pSimFx = Vec_WrdEntryP(vSimsF, Gia_ObjId(pF, pObjFx)*nWords); + word * pSimGb = Vec_WrdEntryP(vSimsG, Gia_ObjId(pG, pObjGb)*nWords); + word * pSimGx = Vec_WrdEntryP(vSimsG, Gia_ObjId(pG, pObjGx)*nWords); + + int nBitsFx = Abc_TtCountOnesVec(pSimFx, nWords); + int nBitsF1 = Abc_TtCountOnesVecMask(pSimFx, pSimFb, nWords, 1); + int nBitsF0 = nWords*64 - nBitsFx - nBitsF1; + + int nBitsGx = Abc_TtCountOnesVec(pSimGx, nWords); + int nBitsG1 = Abc_TtCountOnesVecMask(pSimGx, pSimGb, nWords, 1); + int nBitsG0 = nWords*64 - nBitsGx - nBitsG1; + + printf( "Output %4d : ", i ); + + printf( " RF : " ); + printf( "0 =%7.3f %% ", 100.0*nBitsF0/64/nWords ); + printf( "1 =%7.3f %% ", 100.0*nBitsF1/64/nWords ); + printf( "X =%7.3f %% ", 100.0*nBitsFx/64/nWords ); + + printf( " GF : " ); + printf( "0 =%7.3f %% ", 100.0*nBitsG0/64/nWords ); + printf( "1 =%7.3f %% ", 100.0*nBitsG1/64/nWords ); + printf( "X =%7.3f %% ", 100.0*nBitsGx/64/nWords ); + + printf( "\n" ); + if ( i == 20 ) + break; + } + + printf( "\n" ); + for ( j = 0; j < 20; j++ ) + { + for ( n = 0; n < 2; n++ ) + { + for ( i = 0; i < Gia_ManCoNum(pF)/2; i++ ) + { + Gia_Obj_t * pObjFb = Gia_ManCo( pF, 2*i+0 ); + Gia_Obj_t * pObjFx = Gia_ManCo( pF, 2*i+1 ); + Gia_Obj_t * pObjGb = Gia_ManCo( pG, 2*i+0 ); + Gia_Obj_t * pObjGx = Gia_ManCo( pG, 2*i+1 ); + word * pSimFb = Vec_WrdEntryP(vSimsF, Gia_ObjId(pF, pObjFb)*nWords); + word * pSimFx = Vec_WrdEntryP(vSimsF, Gia_ObjId(pF, pObjFx)*nWords); + word * pSimGb = Vec_WrdEntryP(vSimsG, Gia_ObjId(pG, pObjGb)*nWords); + word * pSimGx = Vec_WrdEntryP(vSimsG, Gia_ObjId(pG, pObjGx)*nWords); + word * pSimb = n ? pSimGb : pSimFb; + word * pSimx = n ? pSimGx : pSimFx; + if ( Abc_TtGetBit(pSimx, j) ) + printf( "x" ); + else if ( Abc_TtGetBit(pSimb, j) ) + printf( "1" ); + else + printf( "0" ); + } + printf( "\n" ); + } + printf( "\n" ); + } + + Vec_WrdFree( vSimsF ); + Vec_WrdFree( vSimsG ); + printf( "\n" ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManDualNot( Gia_Man_t * p, int LitA[2], int LitZ[2] ) +{ + LitZ[0] = Abc_LitNot(LitA[0]); + LitZ[1] = LitA[1]; + + if ( fForceZero ) LitZ[0] = Gia_ManHashAnd( p, LitZ[0], Abc_LitNot(LitZ[1]) ); +} +// computes Z = XOR(A, B) where A, B, Z belong to {0,1,x} encoded as 0=00, 1=01, x=1- +void Gia_ManDualXor2( Gia_Man_t * p, int LitA[2], int LitB[2], int LitZ[2] ) +{ + LitZ[0] = Gia_ManHashXor( p, LitA[0], LitB[0] ); + LitZ[1] = Gia_ManHashOr( p, LitA[1], LitB[1] ); + + if ( fForceZero ) LitZ[0] = Gia_ManHashAnd( p, LitZ[0], Abc_LitNot(LitZ[1]) ); +} +void Gia_ManDualXorN( Gia_Man_t * p, int * pLits, int n, int LitZ[2] ) +{ + int i; + LitZ[0] = 0; + LitZ[1] = 0; + for ( i = 0; i < n; i++ ) + { + LitZ[0] = Gia_ManHashXor( p, LitZ[0], pLits[2*i] ); + LitZ[1] = Gia_ManHashOr ( p, LitZ[1], pLits[2*i+1] ); + } +} +// computes Z = AND(A, B) where A, B, Z belong to {0,1,x} encoded as 0=00, 1=01, z=1- +void Gia_ManDualAnd2( Gia_Man_t * p, int LitA[2], int LitB[2], int LitZ[2] ) +{ + int ZeroA = Gia_ManHashAnd( p, Abc_LitNot(LitA[0]), Abc_LitNot(LitA[1]) ); + int ZeroB = Gia_ManHashAnd( p, Abc_LitNot(LitB[0]), Abc_LitNot(LitB[1]) ); + int ZeroZ = Gia_ManHashOr( p, ZeroA, ZeroB ); + LitZ[0] = Gia_ManHashAnd( p, LitA[0], LitB[0] ); + LitZ[1] = Gia_ManHashAnd( p, Gia_ManHashOr( p, LitA[1], LitB[1] ), Abc_LitNot(ZeroZ) ); + + //LitZ[0] = Gia_ManHashAnd( p, Gia_ManHashAnd(p, LitA[0], Abc_LitNot(LitA[1])), Gia_ManHashAnd(p, LitB[0], Abc_LitNot(LitB[1])) ); + //LitZ[1] = Gia_ManHashAnd( p, Gia_ManHashOr(p, LitA[0], LitA[1]), Gia_ManHashOr(p, LitB[0], LitB[1]) ); + //LitZ[1] = Gia_ManHashAnd( p, LitZ[1], Abc_LitNot(LitZ[0]) ); +} +void Gia_ManDualAndN( Gia_Man_t * p, int * pLits, int n, int LitZ[2] ) +{ + int i, LitZero = 0, LitOne = 0; + LitZ[0] = 1; + for ( i = 0; i < n; i++ ) + { + int Lit = Gia_ManHashAnd( p, Abc_LitNot(pLits[2*i]), Abc_LitNot(pLits[2*i+1]) ); + LitZero = Gia_ManHashOr( p, LitZero, Lit ); + LitOne = Gia_ManHashOr( p, LitOne, pLits[2*i+1] ); + LitZ[0] = Gia_ManHashAnd( p, LitZ[0], pLits[2*i] ); + } + LitZ[1] = Gia_ManHashAnd( p, LitOne, Abc_LitNot(LitZero) ); + + if ( fForceZero ) LitZ[0] = Gia_ManHashAnd( p, LitZ[0], Abc_LitNot(LitZ[1]) ); +} +/* +module _DC(O, C, D); + output O; + input C, D; + assign O = D ? 1'bx : C; +endmodule +*/ +void Gia_ManDualDc( Gia_Man_t * p, int LitC[2], int LitD[2], int LitZ[2] ) +{ + LitZ[0] = LitC[0]; +// LitZ[0] = Gia_ManHashMux( p, LitD[0], 0, LitC[0] ); + LitZ[1] = Gia_ManHashOr(p, Gia_ManHashOr(p,LitD[0],LitD[1]), LitC[1] ); + + if ( fForceZero ) LitZ[0] = Gia_ManHashAnd( p, LitZ[0], Abc_LitNot(LitZ[1]) ); +} +void Gia_ManDualMux( Gia_Man_t * p, int LitC[2], int LitT[2], int LitE[2], int LitZ[2] ) +{ +/* + // total logic size: 18 nodes + int Xnor = Gia_ManHashXor( p, Abc_LitNot(LitT[0]), LitE[0] ); + int Cond = Gia_ManHashAnd( p, Abc_LitNot(LitT[1]), Abc_LitNot(LitE[1]) ); + int pTempE[2], pTempT[2]; + pTempE[0] = Gia_ManHashMux( p, LitC[0], LitT[0], LitE[0] ); + pTempE[1] = Gia_ManHashMux( p, LitC[0], LitT[1], LitE[1] ); + //pTempT[0] = LitT[0]; + pTempT[0] = Gia_ManHashAnd( p, LitT[0], LitE[0] ); + pTempT[1] = Gia_ManHashAnd( p, Cond, Xnor ); + LitZ[0] = Gia_ManHashMux( p, LitC[1], pTempT[0], pTempE[0] ); + LitZ[1] = Gia_ManHashMux( p, LitC[1], pTempT[1], pTempE[1] ); +*/ + // total logic size: 14 nodes + int Xnor = Gia_ManHashXor( p, Abc_LitNot(LitT[0]), LitE[0] ); + int Cond = Gia_ManHashAnd( p, Abc_LitNot(LitT[1]), Abc_LitNot(LitE[1]) ); + int XVal1 = Abc_LitNot( Gia_ManHashAnd( p, Cond, Xnor ) ); + int XVal0 = Gia_ManHashMux( p, LitC[0], LitT[1], LitE[1] ); + LitZ[0] = Gia_ManHashMux( p, LitC[0], LitT[0], LitE[0] ); + LitZ[1] = Gia_ManHashMux( p, LitC[1], XVal1, XVal0 ); + + if ( fForceZero ) LitZ[0] = Gia_ManHashAnd( p, LitZ[0], Abc_LitNot(LitZ[1]) ); +} +int Gia_ManDualCompare( Gia_Man_t * p, int LitF[2], int LitS[2] ) +{ + int iMiter = Gia_ManHashXor( p, LitF[0], LitS[0] ); + iMiter = Gia_ManHashOr( p, LitF[1], iMiter ); + iMiter = Gia_ManHashAnd( p, Abc_LitNot(LitS[1]), iMiter ); + return iMiter; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Acb_ObjToGiaDual( Gia_Man_t * pNew, Acb_Ntk_t * p, int iObj, Vec_Int_t * vTemp, Vec_Int_t * vCopies, int pRes[2] ) +{ + //char * pName = Abc_NamStr( p->pDesign->pStrs, Acb_ObjName(p, iObj) ); + int * pFanin, iFanin, k, Type; + assert( !Acb_ObjIsCio(p, iObj) ); + Vec_IntClear( vTemp ); + Acb_ObjForEachFaninFast( p, iObj, pFanin, iFanin, k ) + { + int * pLits = Vec_IntEntryP( vCopies, 2*iFanin ); + assert( pLits[0] >= 0 && pLits[1] >= 0 ); + Vec_IntPushTwo( vTemp, pLits[0], pLits[1] ); + } + Type = Acb_ObjType( p, iObj ); + if ( Type == ABC_OPER_CONST_F ) + { + pRes[0] = 0; + pRes[1] = 0; + return; + } + if ( Type == ABC_OPER_CONST_T ) + { + pRes[0] = 1; + pRes[1] = 0; + return; + } + if ( Type == ABC_OPER_CONST_X ) + { + pRes[0] = 0; + pRes[1] = 1; + return; + } + if ( Type == ABC_OPER_BIT_BUF ) + { + pRes[0] = Vec_IntEntry(vTemp, 0); + pRes[1] = Vec_IntEntry(vTemp, 1); + return; + } + if ( Type == ABC_OPER_BIT_INV ) + { + Gia_ManDualNot( pNew, Vec_IntArray(vTemp), pRes ); + return; + } + if ( Type == ABC_OPER_TRI ) + { + // in the file inputs are ordered as follows: _DC \n6_5[9] ( .O(\108 ), .C(\96 ), .D(\107 )); + // in this code, we expect them as follows: void Gia_ManDualDc( Gia_Man_t * p, int LitC[2], int LitD[2], int LitZ[2] ) + assert( Vec_IntSize(vTemp) == 4 ); + Gia_ManDualDc( pNew, Vec_IntArray(vTemp), Vec_IntArray(vTemp) + 2, pRes ); + return; + } + if ( Type == ABC_OPER_BIT_MUX ) + { + // in the file inputs are ordered as follows: _HMUX \U$1 ( .O(\282 ), .I0(1'b1), .I1(\277 ), .S(\281 )); + // in this code, we expect them as follows: void Gia_ManDualMux( Gia_Man_t * p, int LitC[2], int LitT[2], int LitE[2], int LitZ[2] ) + assert( Vec_IntSize(vTemp) == 6 ); + ABC_SWAP( int, Vec_IntArray(vTemp)[0], Vec_IntArray(vTemp)[4] ); + ABC_SWAP( int, Vec_IntArray(vTemp)[1], Vec_IntArray(vTemp)[5] ); + Gia_ManDualMux( pNew, Vec_IntArray(vTemp), Vec_IntArray(vTemp) + 2, Vec_IntArray(vTemp) + 4, pRes ); + return; + } + if ( Type == ABC_OPER_BIT_AND || Type == ABC_OPER_BIT_NAND ) + { + Gia_ManDualAndN( pNew, Vec_IntArray(vTemp), Vec_IntSize(vTemp)/2, pRes ); + if ( Type == ABC_OPER_BIT_NAND ) + pRes[0] = Abc_LitNot( pRes[0] ); + return; + } + if ( Type == ABC_OPER_BIT_OR || Type == ABC_OPER_BIT_NOR ) + { + int * pArray = Vec_IntArray( vTemp ); + for ( k = 0; k < Vec_IntSize(vTemp)/2; k++ ) + pArray[2*k] = Abc_LitNot( pArray[2*k] ); + Gia_ManDualAndN( pNew, pArray, Vec_IntSize(vTemp)/2, pRes ); + if ( Type == ABC_OPER_BIT_OR ) + pRes[0] = Abc_LitNot( pRes[0] ); + return; + } + if ( Type == ABC_OPER_BIT_XOR || Type == ABC_OPER_BIT_NXOR ) + { + assert( Vec_IntSize(vTemp) == 4 ); + Gia_ManDualXor2( pNew, Vec_IntArray(vTemp), Vec_IntArray(vTemp) + 2, pRes ); + if ( Type == ABC_OPER_BIT_NXOR ) + pRes[0] = Abc_LitNot( pRes[0] ); + return; + } + assert( 0 ); +} +Gia_Man_t * Acb_NtkGiaDeriveDual( Acb_Ntk_t * p ) +{ + extern Vec_Int_t * Acb_NtkFindNodes2( Acb_Ntk_t * p ); + Gia_Man_t * pNew, * pOne; + Vec_Int_t * vFanins, * vNodes; + Vec_Int_t * vCopies = Vec_IntStartFull( 2*Acb_NtkObjNum(p) ); + int i, iObj, * pLits; + pNew = Gia_ManStart( 5 * Acb_NtkObjNum(p) ); + pNew->pName = Abc_UtilStrsav(Acb_NtkName(p)); + Gia_ManHashAlloc( pNew ); + pLits = Vec_IntEntryP( vCopies, 0 ); + pLits[0] = 0; + pLits[1] = 0; + Acb_NtkForEachCi( p, iObj, i ) + { + pLits = Vec_IntEntryP( vCopies, 2*iObj ); + pLits[0] = Gia_ManAppendCi(pNew); + pLits[1] = 0; + } + vFanins = Vec_IntAlloc( 4 ); + vNodes = Acb_NtkFindNodes2( p ); + Vec_IntForEachEntry( vNodes, iObj, i ) + { + pLits = Vec_IntEntryP( vCopies, 2*iObj ); + Acb_ObjToGiaDual( pNew, p, iObj, vFanins, vCopies, pLits ); + } + Vec_IntFree( vNodes ); + Vec_IntFree( vFanins ); + Acb_NtkForEachCo( p, iObj, i ) + { + pLits = Vec_IntEntryP( vCopies, 2*Acb_ObjFanin(p, iObj, 0) ); + Gia_ManAppendCo( pNew, pLits[0] ); + Gia_ManAppendCo( pNew, pLits[1] ); + } + Vec_IntFree( vCopies ); + pNew = Gia_ManCleanup( pOne = pNew ); + Gia_ManStop( pOne ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Acb_NtkGiaDeriveMiter( Gia_Man_t * pOne, Gia_Man_t * pTwo, int Type ) +{ + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj; + int i; + assert( Gia_ManCiNum(pOne) == Gia_ManCiNum(pTwo) ); + assert( Gia_ManCoNum(pOne) == Gia_ManCoNum(pTwo) ); + pNew = Gia_ManStart( Gia_ManObjNum(pOne) + Gia_ManObjNum(pTwo) + 5*Gia_ManCoNum(pOne)/2 ); + pNew->pName = Abc_UtilStrsav( "miter" ); + pNew->pSpec = NULL; + Gia_ManHashAlloc( pNew ); + Gia_ManConst0(pOne)->Value = 0; + Gia_ManConst0(pTwo)->Value = 0; + Gia_ManForEachCi( pOne, pObj, i ) + pObj->Value = Gia_ManAppendCi( pNew ); + Gia_ManForEachCi( pTwo, pObj, i ) + pObj->Value = Gia_ManCi(pOne, i)->Value; + Gia_ManForEachAnd( pOne, pObj, i ) + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManForEachAnd( pTwo, pObj, i ) + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManForEachCo( pOne, pObj, i ) + pObj->Value = Gia_ObjFanin0Copy(pObj); + Gia_ManForEachCo( pTwo, pObj, i ) + pObj->Value = Gia_ObjFanin0Copy(pObj); + if ( Type == 0 ) // only main circuit + { + for ( i = 0; i < Gia_ManCoNum(pOne); i += 2 ) + { + int pLitsF[2] = { Gia_ManCo(pOne, i)->Value, Gia_ManCo(pOne, i+1)->Value }; + int pLitsS[2] = { Gia_ManCo(pTwo, i)->Value, Gia_ManCo(pTwo, i+1)->Value }; + Gia_ManAppendCo( pNew, pLitsF[0] ); + Gia_ManAppendCo( pNew, pLitsS[0] ); + } + } + else if ( Type == 1 ) // only shadow circuit + { + for ( i = 0; i < Gia_ManCoNum(pOne); i += 2 ) + { + int pLitsF[2] = { Gia_ManCo(pOne, i)->Value, Gia_ManCo(pOne, i+1)->Value }; + int pLitsS[2] = { Gia_ManCo(pTwo, i)->Value, Gia_ManCo(pTwo, i+1)->Value }; + Gia_ManAppendCo( pNew, pLitsF[1] ); + Gia_ManAppendCo( pNew, pLitsS[1] ); + } + } + else // comparator of the two + { + for ( i = 0; i < Gia_ManCoNum(pOne); i += 2 ) + { + int pLitsF[2] = { Gia_ManCo(pOne, i)->Value, Gia_ManCo(pOne, i+1)->Value }; + int pLitsS[2] = { Gia_ManCo(pTwo, i)->Value, Gia_ManCo(pTwo, i+1)->Value }; + Gia_ManAppendCo( pNew, Gia_ManDualCompare( pNew, pLitsF, pLitsS ) ); + } + } + Gia_ManHashStop( pNew ); + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + return pNew; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Acb_OutputFile( char * pFileName, Acb_Ntk_t * pNtkF, int * pModel ) +{ + char * pFileName0 = pFileName? pFileName : "output"; + FILE * pFile = fopen( pFileName0, "wb" ); + if ( pFile == NULL ) + { + printf( "Cannot open results file \"%s\".\n", pFileName0 ); + return; + } + if ( pModel == NULL ) + fprintf( pFile, "EQ\n" ); + else + { + /* + NEQ + in 1 + a 1 + b 0 + */ + int i, iObj; + fprintf( pFile, "NEQ\n" ); + Acb_NtkForEachPi( pNtkF, iObj, i ) + fprintf( pFile, "%s %d\n", Acb_ObjNameStr(pNtkF, iObj), pModel[i] ); + } + fclose( pFile ); + printf( "Produced output file \"%s\".\n\n", pFileName0 ); +} +int * Acb_NtkSolve( Gia_Man_t * p ) +{ + extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan ); + Aig_Man_t * pMan = Gia_ManToAig( p, 0 ); + Abc_Ntk_t * pNtkTemp = Abc_NtkFromAigPhase( pMan ); + Prove_Params_t Params, * pParams = &Params; + Prove_ParamsSetDefault( pParams ); + pParams->fUseRewriting = 1; + pParams->fVerbose = 0; + Aig_ManStop( pMan ); + if ( pNtkTemp ) + { + abctime clk = Abc_Clock(); + int RetValue = Abc_NtkIvyProve( &pNtkTemp, pParams ); + int * pModel = pNtkTemp->pModel; + pNtkTemp->pModel = NULL; + Abc_NtkDelete( pNtkTemp ); + printf( "The networks are %s. ", RetValue == 1 ? "equivalent" : (RetValue == 0 ? "NOT equivalent" : "UNDECIDED") ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + if ( RetValue == 0 ) + return pModel; + } + return NULL; +} + +/**Function************************************************************* + + Synopsis [Various statistics.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Acb_NtkPrintCecStats( Acb_Ntk_t * pNtk ) +{ + int iObj, nDcs = 0, nMuxes = 0; + Acb_NtkForEachNode( pNtk, iObj ) + if ( Acb_ObjType( pNtk, iObj ) == ABC_OPER_TRI ) + nDcs++; + else if ( Acb_ObjType( pNtk, iObj ) == ABC_OPER_BIT_MUX ) + nMuxes++; + + printf( "PI = %6d ", Acb_NtkCiNum(pNtk) ); + printf( "PO = %6d ", Acb_NtkCoNum(pNtk) ); + printf( "Obj = %6d ", Acb_NtkObjNum(pNtk) ); + printf( "DC = %4d ", nDcs ); + printf( "Mux = %4d ", nMuxes ); + printf( "\n" ); +} + +/**Function************************************************************* + + Synopsis [Changing the PI order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Acb_NtkUpdateCiOrder( Acb_Ntk_t * pNtkF, Acb_Ntk_t * pNtkG ) +{ + int i, iObj; + Vec_Int_t * vMap = Vec_IntStartFull( Acb_ManNameIdMax(pNtkG->pDesign) ); + Vec_Int_t * vOrder = Vec_IntStartFull( Acb_NtkCiNum(pNtkG) ); + Acb_NtkForEachCi( pNtkG, iObj, i ) + Vec_IntWriteEntry( vMap, Acb_ObjName(pNtkG, iObj), i ); + Acb_NtkForEachCi( pNtkF, iObj, i ) + { + int NameIdG = Acb_ManStrId( pNtkG->pDesign, Acb_ObjNameStr(pNtkF, iObj) ); + int iPerm = NameIdG < Vec_IntSize(vMap) ? Vec_IntEntry( vMap, NameIdG ) : -1; + if ( iPerm == -1 ) + printf( "Cannot find name \"%s\" of PI %d of F among PIs of G.\n", Acb_ObjNameStr(pNtkF, iObj), i ); + else + Vec_IntWriteEntry( vOrder, iPerm, iObj ); + } + Vec_IntClear( &pNtkF->vCis ); + Vec_IntAppend( &pNtkF->vCis, vOrder ); + Vec_IntFree( vOrder ); + Vec_IntFree( vMap ); +} +int Acb_NtkCheckPiOrder( Acb_Ntk_t * pNtkF, Acb_Ntk_t * pNtkG ) +{ + int i, nPis = Acb_NtkCiNum(pNtkF); + for ( i = 0; i < nPis; i++ ) + { + char * pNameF = Acb_ObjNameStr( pNtkF, Acb_NtkCi(pNtkF, i) ); + char * pNameG = Acb_ObjNameStr( pNtkG, Acb_NtkCi(pNtkG, i) ); + if ( strcmp(pNameF, pNameG) ) + { +// printf( "PI %d has different names (%s and %s) in these networks.\n", i, pNameF, pNameG ); + printf( "Networks have different PI names. Reordering PIs of the implementation network.\n" ); + Acb_NtkUpdateCiOrder( pNtkF, pNtkG ); + break; + } + } + if ( i == nPis ) + printf( "Networks have the same PI names.\n" ); + return i == nPis; +} + /**Function************************************************************* Synopsis [] @@ -43,6 +609,51 @@ ABC_NAMESPACE_IMPL_START ***********************************************************************/ void Acb_NtkRunTest( char * pFileNames[4], int fFancy, int fVerbose ) { + extern Acb_Ntk_t * Acb_VerilogSimpleRead( char * pFileName, char * pFileNameW ); + extern void Gia_AigerWrite( Gia_Man_t * p, char * pFileName, int fWriteSymbols, int fCompact, int fWriteNewLine ); + + int fSolve = 1; + int * pModel = NULL; + Gia_Man_t * pGiaF = NULL; + Gia_Man_t * pGiaG = NULL; + Gia_Man_t * pGia = NULL; + Acb_Ntk_t * pNtkF = Acb_VerilogSimpleRead( pFileNames[0], NULL ); + Acb_Ntk_t * pNtkG = Acb_VerilogSimpleRead( pFileNames[1], NULL ); + if ( !pNtkF || !pNtkG ) + return; + + assert( Acb_NtkCiNum(pNtkF) == Acb_NtkCiNum(pNtkG) ); + assert( Acb_NtkCoNum(pNtkF) == Acb_NtkCoNum(pNtkG) ); + + Acb_NtkCheckPiOrder( pNtkF, pNtkG ); + //Acb_NtkCheckPiOrder( pNtkG, pNtkF ); + Acb_NtkPrintCecStats( pNtkF ); + Acb_NtkPrintCecStats( pNtkG ); + + pGiaF = Acb_NtkGiaDeriveDual( pNtkF ); + pGiaG = Acb_NtkGiaDeriveDual( pNtkG ); + pGia = Acb_NtkGiaDeriveMiter( pGiaF, pGiaG, 0 ); + //Gia_AigerWrite( pGiaF, Extra_FileNameGenericAppend(pFileNames[1], "_f2.aig"), 0, 0, 0 ); + //Gia_AigerWrite( pGiaG, Extra_FileNameGenericAppend(pFileNames[1], "_g2.aig"), 0, 0, 0 ); + //Gia_AigerWrite( pGia, Extra_FileNameGenericAppend(pFileNames[1], "_miter_0.aig"), 0, 0, 0 ); + //printf( "Written the miter info file \"%s\".\n", Extra_FileNameGenericAppend(pFileNames[1], "_miter_0.aig") ); + + //Gia_ManPrintStats( pGia, NULL ); + //Gia_ManSimTry( pGiaF, pGiaG ); + + if ( fSolve ) + { + pModel = Acb_NtkSolve( pGia ); + Acb_OutputFile( pFileNames[2], pNtkF, pModel ); + ABC_FREE( pModel ); + } + + Gia_ManStop( pGia ); + Gia_ManStop( pGiaF ); + Gia_ManStop( pGiaG ); + + Acb_ManFree( pNtkF->pDesign ); + Acb_ManFree( pNtkG->pDesign ); } -- cgit v1.2.3