From 7629fd6aea2ff9cf27c16b235da7d90bec0f3e7e Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 24 Jun 2012 18:45:42 -0700 Subject: Added min-cut-based refinement of gate-level abstraction (command &gla_refine). --- src/aig/gia/gia.h | 1 + src/aig/gia/giaAbsGla.c | 179 ++++++++++++++++++++++++++++++++++++++++ src/aig/gia/giaDup.c | 46 +++++++++++ src/aig/gia/module.make | 1 + src/aig/saig/saigAbsCba.c | 2 + src/base/abci/abc.c | 65 +++++++++++++++ src/map/if/ifCheck.c | 204 ++++++++++++++++++++++++++++++++++++++++++++++ src/opt/nwk/nwkAig.c | 185 +++++++++++++++++++++++++++++++++++++++++ src/proof/pdr/pdrCore.c | 3 + 9 files changed, 686 insertions(+) create mode 100644 src/aig/gia/giaAbsGla.c create mode 100644 src/map/if/ifCheck.c (limited to 'src') diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 1bb883fa..b4ce11e6 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -691,6 +691,7 @@ extern Gia_Man_t * Gia_ManDupWithConstraints( Gia_Man_t * p, Vec_Int_t * extern Gia_Man_t * Gia_ManDupAbsFlops( Gia_Man_t * p, Vec_Int_t * vFlopClasses ); extern Gia_Man_t * Gia_ManDupAbsGates( Gia_Man_t * p, Vec_Int_t * vGateClasses ); extern Vec_Int_t * Gia_GlaCollectAssigned( Gia_Man_t * p, Vec_Int_t * vGateClasses ); +extern void Gia_GlaCollectInputs( Gia_Man_t * p, Vec_Int_t * vGateClasses, Vec_Int_t ** pvPis, Vec_Int_t ** pvPPis ); extern Gia_Man_t * Gia_ManDupCones( Gia_Man_t * p, int * pPos, int nPos, int fTrimPis ); /*=== giaEnable.c ==========================================================*/ extern void Gia_ManDetectSeqSignals( Gia_Man_t * p, int fSetReset, int fVerbose ); diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c new file mode 100644 index 00000000..5dac89a6 --- /dev/null +++ b/src/aig/gia/giaAbsGla.c @@ -0,0 +1,179 @@ +/**CFile**************************************************************** + + FileName [giaAbsGla.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Scalable AIG package.] + + Synopsis [Gate-level abstraction.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: giaAbsGla.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "gia.h" +#include "giaAig.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Derive a new counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Cex_t * Gia_ManCexRemap( Gia_Man_t * p, Gia_Man_t * pAbs, Abc_Cex_t * pCexAbs, Vec_Int_t * vPis ) +{ + Abc_Cex_t * pCex; + int i, f, iPiNum; + assert( pCexAbs->iPo == 0 ); + // start the counter-example + pCex = Abc_CexAlloc( Gia_ManRegNum(p), Gia_ManPiNum(p), pCexAbs->iFrame+1 ); + pCex->iFrame = pCexAbs->iFrame; + pCex->iPo = pCexAbs->iPo; + // copy the bit data + for ( f = 0; f <= pCexAbs->iFrame; f++ ) + for ( i = 0; i < Vec_IntSize(vPis); i++ ) + { + if ( Abc_InfoHasBit( pCexAbs->pData, pCexAbs->nRegs + pCexAbs->nPis * f + i ) ) + { + iPiNum = Gia_ObjCioId( Gia_ManObj(p, Vec_IntEntry(vPis, i)) ); + Abc_InfoSetBit( pCex->pData, pCex->nRegs + pCex->nPis * f + iPiNum ); + } + } + // verify the counter example + if ( !Gia_ManVerifyCex( p, pCex, 0 ) ) + { + printf( "Gia_ManCexRemap(): Counter-example is invalid.\n" ); + Abc_CexFree( pCex ); + pCex = NULL; + } + else + { + printf( "Counter-example verification is successful.\n" ); + printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). \n", pCex->iPo, pCex->iFrame ); + } + return pCex; +} + +/**Function************************************************************* + + Synopsis [Refines gate-level abstraction using the counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManGlaRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int fMinCut, int fVerbose ) +{ + extern void Nwk_ManDeriveMinCut( Gia_Man_t * p, int fVerbose ); + extern Abc_Cex_t * Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fVerbose ); + Gia_Man_t * pAbs; + Aig_Man_t * pAig; + Abc_Cex_t * pCare; + Vec_Int_t * vPis, * vPPis; + int f, i, iObjId, nOnes = 0, Counter = 0; + if ( p->vGateClasses == NULL ) + { + printf( "Gia_ManGlaRefine(): Abstraction gate map is missing.\n" ); + return -1; + } + // derive abstraction + pAbs = Gia_ManDupAbsGates( p, p->vGateClasses ); + Gia_ManStop( pAbs ); + pAbs = Gia_ManDupAbsGates( p, p->vGateClasses ); + if ( Gia_ManPiNum(pAbs) != pCex->nPis ) + { + printf( "Gia_ManGlaRefine(): The PI counts in GLA and in CEX do not match.\n" ); + Gia_ManStop( pAbs ); + return -1; + } + if ( !Gia_ManVerifyCex( pAbs, pCex, 0 ) ) + { + printf( "Gia_ManGlaRefine(): The initial counter-example is invalid.\n" ); + Gia_ManStop( pAbs ); + return -1; + } +// else +// printf( "Gia_ManGlaRefine(): The initial counter-example is correct.\n" ); + // get inputs + Gia_GlaCollectInputs( p, p->vGateClasses, &vPis, &vPPis ); + assert( Vec_IntSize(vPis) + Vec_IntSize(vPPis) == Gia_ManPiNum(pAbs) ); + // minimize the CEX + pAig = Gia_ManToAigSimple( pAbs ); + pCare = Saig_ManCbaFindCexCareBits( pAig, pCex, Vec_IntSize(vPis), fVerbose ); + Aig_ManStop( pAig ); + if ( pCare == NULL ) + printf( "Counter-example minimization has failed.\n" ); + // add new objects to the map + iObjId = -1; + for ( f = 0; f <= pCare->iFrame; f++ ) + for ( i = 0; i < pCare->nPis; i++ ) + if ( Abc_InfoHasBit( pCare->pData, pCare->nRegs + f * pCare->nPis + i ) ) + { + nOnes++; + assert( i >= Vec_IntSize(vPis) ); + iObjId = Vec_IntEntry( vPPis, i - Vec_IntSize(vPis) ); + assert( iObjId > 0 && iObjId < Gia_ManObjNum(p) ); + if ( Vec_IntEntry( p->vGateClasses, iObjId ) == 1 ) + continue; + assert( Vec_IntEntry( p->vGateClasses, iObjId ) == 0 ); + Vec_IntWriteEntry( p->vGateClasses, iObjId, 1 ); +// printf( "Adding object %d.\n", iObjId ); +// Gia_ObjPrint( p, Gia_ManObj(p, iObjId) ); + Counter++; + } + Abc_CexFree( pCare ); + if ( fVerbose ) + printf( "Essential bits = %d. Additional objects = %d.\n", nOnes, Counter ); + // consider the case of SAT + if ( iObjId == -1 ) + { + ABC_FREE( p->pCexSeq ); + p->pCexSeq = Gia_ManCexRemap( p, pAbs, pCex, vPis ); + Vec_IntFree( vPis ); + Vec_IntFree( vPPis ); + Gia_ManStop( pAbs ); + return 0; + } + Vec_IntFree( vPis ); + Vec_IntFree( vPPis ); + Gia_ManStop( pAbs ); + + // extract abstraction to include min-cut + if ( fMinCut ) + Nwk_ManDeriveMinCut( p, fVerbose ); + return -1; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 7d11eff9..a5c246cb 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -1783,6 +1783,52 @@ Gia_Man_t * Gia_ManDupAbsGates( Gia_Man_t * p, Vec_Int_t * vGateClasses ) return pNew; } +/**Function************************************************************* + + Synopsis [Collects PIs and PPIs of the abstraction.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_GlaCollectInputs( Gia_Man_t * p, Vec_Int_t * vGateClasses, Vec_Int_t ** pvPis, Vec_Int_t ** pvPPis ) +{ + Vec_Int_t * vAssigned, * vPis, * vPPis; + Gia_Obj_t * pObj; + int i; + assert( Gia_ManPoNum(p) == 1 ); + assert( Vec_IntSize(vGateClasses) == Gia_ManObjNum(p) ); + // create included objects and their fanins + vAssigned = Gia_GlaCollectAssigned( p, vGateClasses ); + // create additional arrays + vPis = Vec_IntAlloc( 1000 ); + vPPis = Vec_IntAlloc( 1000 ); + Gia_ManForEachObjVec( vAssigned, p, pObj, i ) + { + if ( Gia_ObjIsPi(p, pObj) ) + Vec_IntPush( vPis, Gia_ObjId(p,pObj) ); + else if ( !Vec_IntEntry(vGateClasses, Gia_ObjId(p,pObj)) ) + Vec_IntPush( vPPis, Gia_ObjId(p,pObj) ); + else if ( Gia_ObjIsAnd(pObj) ) + {} + else if ( Gia_ObjIsRo(p, pObj) ) + {} + else assert( Gia_ObjIsConst0(pObj) ); + } + Vec_IntFree( vAssigned ); + if ( pvPis ) + *pvPis = vPis; + else + Vec_IntFree( vPis ); + if ( pvPPis ) + *pvPPis = vPPis; + else + Vec_IntFree( vPPis ); +} + /**Function************************************************************* Synopsis [Returns the array of neighbors.] diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make index aec38f40..e54a30d4 100644 --- a/src/aig/gia/module.make +++ b/src/aig/gia/module.make @@ -1,5 +1,6 @@ SRC += src/aig/gia/gia.c \ src/aig/gia/giaAbs.c \ + src/aig/gia/giaAbsGla.c \ src/aig/gia/giaAbsVta.c \ src/aig/gia/giaAig.c \ src/aig/gia/giaAiger.c \ diff --git a/src/aig/saig/saigAbsCba.c b/src/aig/saig/saigAbsCba.c index 7863069f..55a429e1 100644 --- a/src/aig/saig/saigAbsCba.c +++ b/src/aig/saig/saigAbsCba.c @@ -761,11 +761,13 @@ if ( fVerbose ) printf( "Care " ); Abc_CexPrintStats( pCare ); } +/* // verify the reduced counter-example using ternary simulation if ( !Saig_ManCexVerifyUsingTernary( pAig, pCex, pCare ) ) printf( "Saig_ManCbaFindCexCareBits(): Minimized counter-example verification has failed!!!\n" ); else if ( fVerbose ) printf( "Saig_ManCbaFindCexCareBits(): Minimized counter-example verification is successful.\n" ); +*/ Aig_ManCleanMarkAB( pAig ); return pCare; } diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index d3fb8d5a..c7c811f0 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -346,6 +346,7 @@ static int Abc_CommandAbc9AbsRefine ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9AbsCba ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9AbsPba ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9GlaDerive ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9GlaRefine ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9GlaCba ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9GlaPba ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Vta ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -789,6 +790,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&abs_cba", Abc_CommandAbc9AbsCba, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&abs_pba", Abc_CommandAbc9AbsPba, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&gla_derive", Abc_CommandAbc9GlaDerive, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&gla_refine", Abc_CommandAbc9GlaRefine, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&gla_cba", Abc_CommandAbc9GlaCba, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&gla_pba", Abc_CommandAbc9GlaPba, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&vta", Abc_CommandAbc9Vta, 0 ); @@ -27013,6 +27015,8 @@ int Abc_CommandAbc9GlaDerive( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; } pTemp = Gia_ManDupAbsGates( pAbc->pGia, pAbc->pGia->vGateClasses ); + Gia_ManStop( pTemp ); + pTemp = Gia_ManDupAbsGates( pAbc->pGia, pAbc->pGia->vGateClasses ); Abc_CommandUpdate9( pAbc, pTemp ); // printf( "This command is currently not enabled.\n" ); return 0; @@ -27025,6 +27029,67 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc9GlaRefine( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern int Gia_ManGlaRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int fMinCut, int fVerbose ); + int fMinCut = 1; + int c, fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "mvh" ) ) != EOF ) + { + switch ( c ) + { + case 'm': + fMinCut ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9GlaRefine(): There is no AIG.\n" ); + return 1; + } + if ( Gia_ManRegNum(pAbc->pGia) == 0 ) + { + Abc_Print( -1, "The network is combinational.\n" ); + return 0; + } + if ( pAbc->pCex == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9GlaRefine(): There is no counter-example.\n" ); + return 1; + } + pAbc->Status = Gia_ManGlaRefine( pAbc->pGia, pAbc->pCex, fMinCut, fVerbose ); + Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq ); + return 0; + +usage: + Abc_Print( -2, "usage: &gla_refine [-mvh]\n" ); + Abc_Print( -2, "\t refines the pre-computed gate map using the counter-example\n" ); + Abc_Print( -2, "\t-m : toggle using min-cut to derive the refinements [default = %s]\n", fMinCut? "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 [] diff --git a/src/map/if/ifCheck.c b/src/map/if/ifCheck.c new file mode 100644 index 00000000..317b6ffd --- /dev/null +++ b/src/map/if/ifCheck.c @@ -0,0 +1,204 @@ +/**CFile**************************************************************** + + FileName [ifCheck.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [FPGA mapping based on priority cuts.] + + Synopsis [Sequential mapping.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - November 21, 2006.] + + Revision [$Id: ifCheck.c,v 1.00 2006/11/21 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "if.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +#ifdef WIN32 +typedef unsigned __int64 word; +#else +typedef unsigned long long word; +#endif + +// elementary truth tables +static word Truths6[6] = { + 0xAAAAAAAAAAAAAAAA, + 0xCCCCCCCCCCCCCCCC, + 0xF0F0F0F0F0F0F0F0, + 0xFF00FF00FF00FF00, + 0xFFFF0000FFFF0000, + 0xFFFFFFFF00000000 +}; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Returns 1 if the node Leaf is reachable on the path.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int If_ManCutReach_rec( If_Obj_t * pPath, If_Obj_t * pLeaf ) +{ + if ( pPath == pLeaf ) + return 1; + if ( pPath->fMark ) + return 0; + assert( If_ObjIsAnd(pPath) ); + if ( If_ManCutReach_rec( If_ObjFanin0(pPath), pLeaf ) ) + return 1; + if ( If_ManCutReach_rec( If_ObjFanin1(pPath), pLeaf ) ) + return 1; + return 0; +} +int If_ManCutReach( If_Man_t * p, If_Cut_t * pCut, If_Obj_t * pPath, If_Obj_t * pLeaf ) +{ + If_Obj_t * pTemp; + int i, RetValue; + If_CutForEachLeaf( p, pCut, pTemp, i ) + pTemp->fMark = 1; + RetValue = If_ManCutReach_rec( pPath, pLeaf ); + If_CutForEachLeaf( p, pCut, pTemp, i ) + pTemp->fMark = 0; + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Derive truth table for each cofactor.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int If_ManCutTruthCheck_rec( If_Obj_t * pObj, word * pTruths ) +{ + word T0, T1; + if ( pObj->fMark ) + return pTruths[If_ObjId(pObj)]; + assert( If_ObjIsAnd(pObj) ); + T0 = If_ManCutTruthCheck_rec( If_ObjFanin0(pObj), pTruths ); + T1 = If_ManCutTruthCheck_rec( If_ObjFanin1(pObj), pTruths ); + T0 = If_ObjFaninC0(pObj) ? ~T0 : T0; + T1 = If_ObjFaninC1(pObj) ? ~T1 : T1; + return T0 & T1; +} +int If_ManCutTruthCheck( If_Man_t * p, If_Obj_t * pObj, If_Cut_t * pCut, If_Obj_t * pLeaf, int Cof, word * pTruths ) +{ + word Truth; + If_Obj_t * pTemp; + int i, k = 0; + assert( Cof == 0 || Cof == 1 ); + If_CutForEachLeaf( p, pCut, pTemp, i ) + { + assert( pTemp->fMark == 0 ); + pTemp->fMark = 1; + if ( pLeaf == pTemp ) + pTruths[If_ObjId(pTemp)] = (Cof ? ~((word)0) : 0); + else + pTruths[If_ObjId(pTemp)] = Truths6[k++] ; + } + assert( k + 1 == If_CutLeaveNum(pCut) ); + // compute truth table + Truth = If_ManCutTruthCheck_rec( pObj, pTruths ); + If_CutForEachLeaf( p, pCut, pTemp, i ) + pTemp->fMark = 0; + return Truth == 0 || Truth == ~((word)0); +} + + +/**Function************************************************************* + + Synopsis [Checks if cut can be structurally/functionally decomposed.] + + Description [The decomposition is Fn(a,b,c,...) = F2(a, Fn-1(b,c,...)).] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void If_ManCutCheck( If_Man_t * p, If_Obj_t * pObj, If_Cut_t * pCut ) +{ + static int nDecCalls = 0; + static int nDecStruct = 0; + static int nDecStruct2 = 0; + static int nDecFunction = 0; + word * pTruths; + If_Obj_t * pLeaf, * pPath; + int i; + if ( pCut == NULL ) + { + printf( "DecStr = %9d (%6.2f %%).\n", nDecStruct, 100.0*nDecStruct/nDecCalls ); + printf( "DecStr2 = %9d (%6.2f %%).\n", nDecStruct2, 100.0*nDecStruct2/nDecCalls ); + printf( "DecFunc = %9d (%6.2f %%).\n", nDecFunction, 100.0*nDecFunction/nDecCalls ); + printf( "Total = %9d (%6.2f %%).\n", nDecCalls, 100.0*nDecCalls/nDecCalls ); + return; + } + assert( If_ObjIsAnd(pObj) ); + assert( pCut->nLeaves <= 7 ); + nDecCalls++; + // check structural decomposition + If_CutForEachLeaf( p, pCut, pLeaf, i ) + if ( pLeaf == If_ObjFanin0(pObj) || pLeaf == If_ObjFanin1(pObj) ) + break; + if ( i < If_CutLeaveNum(pCut) ) + { + pPath = (pLeaf == If_ObjFanin0(pObj)) ? If_ObjFanin1(pObj) : If_ObjFanin0(pObj); + if ( !If_ManCutReach( p, pCut, pPath, pLeaf ) ) + { + nDecStruct++; +// nDecFunction++; +// return; + } + else + nDecStruct2++; + } + // check functional decomposition + pTruths = malloc( sizeof(word) * If_ManObjNum(p) ); + If_CutForEachLeaf( p, pCut, pLeaf, i ) + { + if ( If_ManCutTruthCheck( p, pObj, pCut, pLeaf, 0, pTruths ) ) + { + nDecFunction++; + break; + } + if ( If_ManCutTruthCheck( p, pObj, pCut, pLeaf, 1, pTruths ) ) + { + nDecFunction++; + break; + } + } + free( pTruths ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/opt/nwk/nwkAig.c b/src/opt/nwk/nwkAig.c index 6254bc41..a4959c9a 100644 --- a/src/opt/nwk/nwkAig.c +++ b/src/opt/nwk/nwkAig.c @@ -103,6 +103,191 @@ Vec_Ptr_t * Nwk_ManDeriveRetimingCut( Aig_Man_t * p, int fForward, int fVerbose return vNodes; } + + +#include "src/aig/gia/gia.h" + +/**Function************************************************************* + + Synopsis [Collects reachable nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ManColleacReached_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vNodes, Vec_Int_t * vLeaves ) +{ + if ( Gia_ObjIsTravIdCurrent(p, pObj) ) + return; + Gia_ObjSetTravIdCurrent(p, pObj); + if ( Gia_ObjIsCi(pObj) ) + { + Vec_IntPush( vLeaves, Gia_ObjId(p, pObj) ); + return; + } + assert( Gia_ObjIsAnd(pObj) ); + Nwk_ManColleacReached_rec( p, Gia_ObjFanin0(pObj), vNodes, vLeaves ); + Nwk_ManColleacReached_rec( p, Gia_ObjFanin1(pObj), vNodes, vLeaves ); + Vec_IntPush( vNodes, Gia_ObjId(p, pObj) ); +} + + +/**Function************************************************************* + + Synopsis [Converts AIG into the network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Nwk_Man_t * Nwk_ManCreateFromGia( Gia_Man_t * p, Vec_Int_t * vPPis, Vec_Int_t * vNodes, Vec_Int_t * vLeaves, Vec_Int_t ** pvMapInv ) +{ + Nwk_Man_t * pNtk; + Nwk_Obj_t ** ppCopies; + Gia_Obj_t * pObj; + Vec_Int_t * vMaps; + int i; + assert( Vec_IntSize(vLeaves) >= Vec_IntSize(vPPis) ); + Gia_ManCreateRefs( p ); + pNtk = Nwk_ManAlloc(); + pNtk->pName = Abc_UtilStrsav( p->pName ); + pNtk->nFanioPlus = 0; + Hop_ManStop( pNtk->pManHop ); + pNtk->pManHop = NULL; + // allocate + vMaps = Vec_IntAlloc( Vec_IntSize(vNodes) + Abc_MaxInt(Vec_IntSize(vPPis), Vec_IntSize(vLeaves)) + 1 ); + ppCopies = ABC_ALLOC( Nwk_Obj_t *, Gia_ManObjNum(p) ); + // copy objects + pObj = Gia_ManConst0(p); + ppCopies[Gia_ObjId(p,pObj)] = Nwk_ManCreateNode( pNtk, 0, Gia_ObjRefs(p,pObj) ); + Vec_IntPush( vMaps, Gia_ObjId(p,pObj) ); + Gia_ManForEachObjVec( vLeaves, p, pObj, i ) + { + ppCopies[Gia_ObjId(p,pObj)] = Nwk_ManCreateCi( pNtk, Gia_ObjRefs(p,pObj) ); + assert( Vec_IntSize(vMaps) == Nwk_ObjId(ppCopies[Gia_ObjId(p,pObj)]) ); + Vec_IntPush( vMaps, Gia_ObjId(p,pObj) ); + } +/* + for ( i = Vec_IntSize(vLeaves); i < Vec_IntSize(vPPis); i++ ) + { + pTemp = Nwk_ManCreateCi( pNtk, Gia_ObjRefs(p,pObj) ); + Vec_IntPush( vMaps, 0 );// ??? + } +*/ + Gia_ManForEachObjVec( vNodes, p, pObj, i ) + { + ppCopies[Gia_ObjId(p,pObj)] = Nwk_ManCreateNode( pNtk, 2, Gia_ObjRefs(p,pObj) ); + Nwk_ObjAddFanin( ppCopies[Gia_ObjId(p,pObj)], ppCopies[Gia_ObjFaninId0p(p,pObj)] ); + Nwk_ObjAddFanin( ppCopies[Gia_ObjId(p,pObj)], ppCopies[Gia_ObjFaninId1p(p,pObj)] ); + assert( Vec_IntSize(vMaps) == Nwk_ObjId(ppCopies[Gia_ObjId(p,pObj)]) ); + Vec_IntPush( vMaps, Gia_ObjId(p,pObj) ); + } + Gia_ManForEachObjVec( vPPis, p, pObj, i ) + { + assert( ppCopies[Gia_ObjId(p,pObj)] != NULL ); + Nwk_ObjAddFanin( Nwk_ManCreateCo(pNtk), ppCopies[Gia_ObjId(p,pObj)] ); + } + for ( i = Vec_IntSize(vPPis); i < Vec_IntSize(vLeaves); i++ ) + Nwk_ObjAddFanin( Nwk_ManCreateCo(pNtk), ppCopies[0] ); + assert( Vec_IntSize(vMaps) == Vec_IntSize(vNodes) + Abc_MaxInt(Vec_IntSize(vPPis), Vec_IntSize(vLeaves)) + 1 ); + ABC_FREE( ppCopies ); + *pvMapInv = vMaps; + return pNtk; +} + + +/**Function************************************************************* + + Synopsis [Returns min-cut in the AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ManDeriveMinCut( Gia_Man_t * p, int fVerbose ) +{ + Nwk_Man_t * pNtk; + Nwk_Obj_t * pNode; + Vec_Ptr_t * vMinCut; + Vec_Int_t * vPPis, * vNodes, * vLeaves, * vNodes2, * vLeaves2, * vMapInv; + Vec_Int_t * vCommon, * vDiff0, * vDiff1; + Gia_Obj_t * pObj; + int i, iObjId; + // get inputs + Gia_GlaCollectInputs( p, p->vGateClasses, NULL, &vPPis ); + // collect nodes rechable from PPIs + vNodes = Vec_IntAlloc( 100 ); + vLeaves = Vec_IntAlloc( 100 ); + Gia_ManIncrementTravId( p ); + Gia_ManForEachObjVec( vPPis, p, pObj, i ) + Nwk_ManColleacReached_rec( p, pObj, vNodes, vLeaves ); + // derive the new network + pNtk = Nwk_ManCreateFromGia( p, vPPis, vNodes, vLeaves, &vMapInv ); + assert( Nwk_ManPiNum(pNtk) == Nwk_ManPoNum(pNtk) ); + // create min-cut + vMinCut = Nwk_ManRetimeCutBackward( pNtk, Nwk_ManPiNum(pNtk), fVerbose ); + // copy from the GIA back +// Aig_ManForEachObj( p, pObj, i ) +// ((Nwk_Obj_t *)pObj->pData)->pCopy = pObj; + // mark min-cut nodes + vNodes2 = Vec_IntAlloc( 100 ); + vLeaves2 = Vec_IntAlloc( 100 ); + Gia_ManIncrementTravId( p ); + Vec_PtrForEachEntry( Nwk_Obj_t *, vMinCut, pNode, i ) + { + pObj = Gia_ManObj( p, Vec_IntEntry(vMapInv, Nwk_ObjId(pNode)) ); + if ( Gia_ObjIsConst0(pObj) ) + continue; + Nwk_ManColleacReached_rec( p, pObj, vNodes2, vLeaves2 ); + } + if ( fVerbose ) + printf( "Min-cut: %d -> %d. Nodes %d -> %d. ", Vec_IntSize(vPPis)+1, Vec_PtrSize(vMinCut), Vec_IntSize(vNodes), Vec_IntSize(vNodes2) ); + Vec_IntFree( vPPis ); + Vec_PtrFree( vMinCut ); + Vec_IntFree( vMapInv ); + Nwk_ManFree( pNtk ); + + // sort the results + Vec_IntSort( vNodes, 0 ); + Vec_IntSort( vNodes2, 0 ); + vCommon = Vec_IntAlloc( Vec_IntSize(vNodes) ); + vDiff0 = Vec_IntAlloc( 100 ); + vDiff1 = Vec_IntAlloc( 100 ); + Vec_IntTwoSplit( vNodes, vNodes2, vCommon, vDiff0, vDiff1 ); + if ( fVerbose ) + printf( "Common = %d. Diff0 = %d. Diff1 = %d.\n", Vec_IntSize(vCommon), Vec_IntSize(vDiff0), Vec_IntSize(vDiff1) ); + + // fill in + Vec_IntForEachEntry( vDiff0, iObjId, i ) + Vec_IntWriteEntry( p->vGateClasses, iObjId, 1 ); + + Vec_IntFree( vLeaves ); + Vec_IntFree( vNodes ); + Vec_IntFree( vLeaves2 ); + Vec_IntFree( vNodes2 ); + + Vec_IntFree( vCommon ); + Vec_IntFree( vDiff0 ); + Vec_IntFree( vDiff1 ); + + // check abstraction + Gia_ManForEachObj( p, pObj, i ) + { + if ( Vec_IntEntry( p->vGateClasses, i ) == 0 ) + continue; + assert( Gia_ObjIsConst0(pObj) || Gia_ObjIsRo(p, pObj) || Gia_ObjIsAnd(pObj) ); + } +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c index 3cf47a92..f863a881 100644 --- a/src/proof/pdr/pdrCore.c +++ b/src/proof/pdr/pdrCore.c @@ -706,6 +706,8 @@ int Pdr_ManSolve_( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t ** pvPrioInit, ***********************************************************************/ int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex ) { + if ( pPars->fVerbose ) + { // Abc_Print( 1, "Running PDR by Niklas Een (aka IC3 by Aaron Bradley) with these parameters:\n" ); Abc_Print( 1, "VarMax = %d. FrameMax = %d. QueueMax = %d. TimeMax = %d. ", pPars->nRecycle, pPars->nFrameMax, pPars->nRestLimit, pPars->nTimeOut ); @@ -713,6 +715,7 @@ int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex ) Abc_Print( 1, "Output = %d. ", pPars->iOutput ); Abc_Print( 1, "MonoCNF = %s. SkipGen = %s.\n", pPars->fMonoCnf ? "yes" : "no", pPars->fSkipGeneral ? "yes" : "no" ); + } /* Vec_Int_t * vPrioInit = NULL; -- cgit v1.2.3