From 8888e8e82e189a599a340e83ac8094bdef1ceb51 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 23 Jun 2022 07:48:10 -0700 Subject: Experiments with the mapper. --- abc.rc | 2 ++ src/bool/kit/kitDsd.c | 2 +- src/map/if/if.h | 2 ++ src/map/if/ifCore.c | 2 ++ src/map/if/ifCut.c | 62 ++++++++++++++++++++++++++++++++++++++++++++++++ src/map/if/ifMan.c | 2 ++ src/map/mio/mioUtils.c | 5 ++++ src/proof/acec/acecXor.c | 43 +++++++++++++++++++++++++++++++++ 8 files changed, 119 insertions(+), 1 deletion(-) diff --git a/abc.rc b/abc.rc index e50d1270..a3efc0b0 100644 --- a/abc.rc +++ b/abc.rc @@ -132,7 +132,9 @@ alias src_rw "st; rw -l; rwz -l; rwz -l" alias src_rs "st; rs -K 6 -N 2 -l; rs -K 9 -N 2 -l; rs -K 12 -N 2 -l" alias src_rws "st; rw -l; rs -K 6 -N 2 -l; rwz -l; rs -K 9 -N 2 -l; rwz -l; rs -K 12 -N 2 -l" alias resyn2rs "b; rs -K 6; rw; rs -K 6 -N 2; rf; rs -K 8; b; rs -K 8 -N 2; rw; rs -K 10; rwz; rs -K 10 -N 2; b; rs -K 12; rfz; rs -K 12 -N 2; rwz; b" +alias r2rs "b; rs -K 6; rw; rs -K 6 -N 2; rf; rs -K 8; b; rs -K 8 -N 2; rw; rs -K 10; rwz; rs -K 10 -N 2; b; rs -K 12; rfz; rs -K 12 -N 2; rwz; b" alias compress2rs "b -l; rs -K 6 -l; rw -l; rs -K 6 -N 2 -l; rf -l; rs -K 8 -l; b -l; rs -K 8 -N 2 -l; rw -l; rs -K 10 -l; rwz -l; rs -K 10 -N 2 -l; b -l; rs -K 12 -l; rfz -l; rs -K 12 -N 2 -l; rwz -l; b -l" +alias c2rs "b -l; rs -K 6 -l; rw -l; rs -K 6 -N 2 -l; rf -l; rs -K 8 -l; b -l; rs -K 8 -N 2 -l; rw -l; rs -K 10 -l; rwz -l; rs -K 10 -N 2 -l; b -l; rs -K 12 -l; rfz -l; rs -K 12 -N 2 -l; rwz -l; b -l" # use this script to convert 1-valued and DC-valued flops for an AIG alias fix_aig "logic; undc; strash; zero" diff --git a/src/bool/kit/kitDsd.c b/src/bool/kit/kitDsd.c index 7d85214b..cd02db67 100644 --- a/src/bool/kit/kitDsd.c +++ b/src/bool/kit/kitDsd.c @@ -2497,7 +2497,7 @@ void Kit_DsdVerify( Kit_DsdNtk_t * pNtk, unsigned * pTruth, int nVars ) p = Kit_DsdManAlloc( nVars, Kit_DsdNtkObjNum(pNtk)+2 ); pTruthC = Kit_DsdTruthCompute( p, pNtk ); if ( !Extra_TruthIsEqual( pTruth, pTruthC, nVars ) ) - printf( "Verification failed.\n" ); + printf( "Verification failed for gate with %d inputs.\n", nVars ); Kit_DsdManFree( p ); } diff --git a/src/map/if/if.h b/src/map/if/if.h index 3c2ba703..13fa4108 100644 --- a/src/map/if/if.h +++ b/src/map/if/if.h @@ -275,6 +275,8 @@ struct If_Man_t_ void * pUserMan; Vec_Int_t * vDump; int pDumpIns[16]; + Vec_Str_t * vMarks; + Vec_Int_t * vVisited2; // timing manager Tim_Man_t * pManTim; diff --git a/src/map/if/ifCore.c b/src/map/if/ifCore.c index 0c9287a1..c03061af 100644 --- a/src/map/if/ifCore.c +++ b/src/map/if/ifCore.c @@ -106,6 +106,8 @@ int If_ManPerformMappingComb( If_Man_t * p ) If_Obj_t * pObj; abctime clkTotal = Abc_Clock(); int i; + //p->vVisited2 = Vec_IntAlloc( 100 ); + //p->vMarks = Vec_StrStart( If_ManObjNum(p) ); // set arrival times and fanout estimates If_ManForEachCi( p, pObj, i ) diff --git a/src/map/if/ifCut.c b/src/map/if/ifCut.c index 2d6889c0..079781e0 100644 --- a/src/map/if/ifCut.c +++ b/src/map/if/ifCut.c @@ -1494,6 +1494,68 @@ int If_CutCountTotalFanins( If_Man_t * p ) return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int If_CutFilter2_rec( If_Man_t * p, If_Obj_t * pObj, int LevelMin ) +{ + char * pVisited = Vec_StrEntryP(p->vMarks, pObj->Id); + if ( *pVisited ) + return *pVisited; + Vec_IntPush( p->vVisited2, pObj->Id ); + if ( (int)pObj->Level <= LevelMin ) + return (*pVisited = 1); + if ( If_CutFilter2_rec( p, pObj->pFanin0, LevelMin ) == 1 ) + return (*pVisited = 1); + if ( If_CutFilter2_rec( p, pObj->pFanin1, LevelMin ) == 1 ) + return (*pVisited = 1); + return (*pVisited = 2); +} +int If_CutFilter2( If_Man_t * p, If_Obj_t * pNode, If_Cut_t * pCut ) +{ + If_Obj_t * pLeaf, * pTemp; int i, Count = 0; +// printf( "Considering node %d and cut {", pNode->Id ); +// If_CutForEachLeaf( p, pCut, pLeaf, i ) +// printf( " %d", pLeaf->Id ); +// printf( " }\n" ); + If_CutForEachLeaf( p, pCut, pLeaf, i ) + { + int k, iObj, RetValue, nLevelMin = ABC_INFINITY; + Vec_IntClear( p->vVisited2 ); + If_CutForEachLeaf( p, pCut, pTemp, k ) + { + if ( pTemp == pLeaf ) + continue; + nLevelMin = Abc_MinInt( nLevelMin, (int)pTemp->Level ); + assert( Vec_StrEntry(p->vMarks, pTemp->Id) == 0 ); + Vec_StrWriteEntry( p->vMarks, pTemp->Id, 2 ); + Vec_IntPush( p->vVisited2, pTemp->Id ); + } + RetValue = If_CutFilter2_rec( p, pLeaf, nLevelMin ); + Vec_IntForEachEntry( p->vVisited2, iObj, k ) + Vec_StrWriteEntry( p->vMarks, iObj, 0 ); + if ( RetValue == 2 ) + { + Count++; + pCut->nLeaves--; + for ( k = i; k < (int)pCut->nLeaves; k++ ) + pCut->pLeaves[k] = pCut->pLeaves[k+1]; + i--; + } + } + //if ( Count ) + // printf( "%d", Count ); + return 0; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c index 4027b780..6ecd0eb8 100644 --- a/src/map/if/ifMan.c +++ b/src/map/if/ifMan.c @@ -273,6 +273,8 @@ void If_ManStop( If_Man_t * p ) Vec_IntFreeP( &p->vPairRes ); Vec_StrFreeP( &p->vPairPerms ); Vec_PtrFreeP( &p->vVisited ); + Vec_StrFreeP( &p->vMarks ); + Vec_IntFreeP( &p->vVisited2 ); if ( p->vPairHash ) Hash_IntManStop( p->vPairHash ); for ( i = 6; i <= Abc_MaxInt(6,p->pPars->nLutSize); i++ ) diff --git a/src/map/mio/mioUtils.c b/src/map/mio/mioUtils.c index c7180e1c..06e880c2 100644 --- a/src/map/mio/mioUtils.c +++ b/src/map/mio/mioUtils.c @@ -224,6 +224,7 @@ void Mio_WritePin( FILE * pFile, Mio_Pin_t * pPin, int NameLen, int fAllPins ) ***********************************************************************/ void Mio_WriteGate( FILE * pFile, Mio_Gate_t * pGate, int GateLen, int NameLen, int FormLen, int fPrintSops, int fAllPins ) { + //Vec_Int_t * vCover = Vec_IntAlloc( 1 << 10 ); int nLits; char Buffer[5000]; Mio_Pin_t * pPin; assert( NameLen+FormLen+2 < 5000 ); @@ -239,7 +240,11 @@ void Mio_WriteGate( FILE * pFile, Mio_Gate_t * pGate, int GateLen, int NameLen, else // different pins Mio_GateForEachPin( pGate, pPin ) Mio_WritePin( pFile, pPin, NameLen, 0 ); + //nLits = 2*Kit_TruthLitNum((unsigned*)&pGate->uTruth, Mio_GateReadPinNum(pGate), vCover); + //if ( nLits != Mio_GateReadArea(pGate) ) + // printf( " # %d ", nLits ); fprintf( pFile, "\n" ); + //Vec_IntFree( vCover ); } /**Function************************************************************* diff --git a/src/proof/acec/acecXor.c b/src/proof/acec/acecXor.c index 71e0b7b3..963ea15b 100644 --- a/src/proof/acec/acecXor.c +++ b/src/proof/acec/acecXor.c @@ -21,6 +21,7 @@ #include "acecInt.h" #include "misc/vec/vecWec.h" #include "misc/extra/extra.h" +#include "misc/util/utilTruth.h" ABC_NAMESPACE_IMPL_START @@ -425,6 +426,48 @@ Acec_Box_t * Acec_ProduceBox( Gia_Man_t * p, int fVerbose ) } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManTestXor( Gia_Man_t * p ) +{ + Vec_Wrd_t * vSimsPi = Vec_WrdStartTruthTables( Gia_ManCiNum(p) ); + Vec_Wrd_t * vSims = Gia_ManSimPatSimOut( p, vSimsPi, 1 ); + int n, i, nWords = Vec_WrdSize(vSimsPi) / Gia_ManCiNum(p); + Gia_Obj_t * pObj; Vec_Wrd_t * vSims2; + Gia_ManForEachAnd( p, pObj, i ) + { + Gia_Obj_t Obj = *pObj; + for ( n = 0; n < 2; n++ ) + { + if ( n ) + { + pObj->iDiff1 = pObj->iDiff0; + pObj->fCompl1 = pObj->fCompl0; + } + else + { + pObj->iDiff0 = pObj->iDiff1; + pObj->fCompl0 = pObj->fCompl1; + } + vSims2 = Gia_ManSimPatSimOut( p, vSimsPi, 1 ); + printf( "%2d %2d : %5d\n", i, n, Abc_TtCountOnesVecXor(Vec_WrdArray(vSims), Vec_WrdArray(vSims2), Vec_WrdSize(vSims2)) ); + Vec_WrdFree( vSims2 ); + *pObj = Obj; + } + } + Vec_WrdFree( vSimsPi ); + Vec_WrdFree( vSims ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -- cgit v1.2.3