summaryrefslogtreecommitdiffstats
path: root/src/aig/cec/cecChoice.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/cec/cecChoice.c')
-rw-r--r--src/aig/cec/cecChoice.c443
1 files changed, 441 insertions, 2 deletions
diff --git a/src/aig/cec/cecChoice.c b/src/aig/cec/cecChoice.c
index 2a619e39..0662d73d 100644
--- a/src/aig/cec/cecChoice.c
+++ b/src/aig/cec/cecChoice.c
@@ -19,17 +19,172 @@
***********************************************************************/
#include "cecInt.h"
+#include "giaAig.h"
+#include "dch.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
+static void Cec_ManCombSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj );
+
+extern int Cec_ManResimulateCounterExamplesComb( Cec_ManSim_t * pSim, Vec_Int_t * vCexStore );
+extern int Gia_ManCheckRefinements( Gia_Man_t * p, Vec_Str_t * vStatus, Vec_Int_t * vOutputs, Cec_ManSim_t * pSim, int fRings );
+
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
+ Synopsis [Computes the real value of the literal w/o spec reduction.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Cec_ManCombSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+ assert( Gia_ObjIsAnd(pObj) );
+ Cec_ManCombSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj) );
+ Cec_ManCombSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj) );
+ return Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Recursively performs speculative reduction for the object.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cec_ManCombSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+ Gia_Obj_t * pRepr;
+ if ( ~pObj->Value )
+ return;
+ if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
+ {
+ Cec_ManCombSpecReduce_rec( pNew, p, pRepr );
+ pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
+ return;
+ }
+ pObj->Value = Cec_ManCombSpecReal( pNew, p, pObj );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Derives SRM for signal correspondence.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Gia_Man_t * Cec_ManCombSpecReduce( Gia_Man_t * p, Vec_Int_t ** pvOutputs, int fRings )
+{
+ Gia_Man_t * pNew, * pTemp;
+ Gia_Obj_t * pObj, * pRepr;
+ Vec_Int_t * vXorLits;
+ int i, iPrev, iObj, iPrevNew, iObjNew;
+ assert( p->pReprs != NULL );
+ Gia_ManSetPhase( p );
+ Gia_ManFillValue( p );
+ pNew = Gia_ManStart( Gia_ManObjNum(p) );
+ pNew->pName = Gia_UtilStrsav( p->pName );
+ Gia_ManHashAlloc( pNew );
+ Gia_ManConst0(p)->Value = 0;
+ Gia_ManForEachCi( p, pObj, i )
+ pObj->Value = Gia_ManAppendCi(pNew);
+ *pvOutputs = Vec_IntAlloc( 1000 );
+ vXorLits = Vec_IntAlloc( 1000 );
+ if ( fRings )
+ {
+ Gia_ManForEachObj1( p, pObj, i )
+ {
+ if ( Gia_ObjIsConst( p, i ) )
+ {
+ iObjNew = Cec_ManCombSpecReal( pNew, p, pObj );
+ iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pObj) );
+ if ( iObjNew != 0 )
+ {
+ Vec_IntPush( *pvOutputs, 0 );
+ Vec_IntPush( *pvOutputs, i );
+ Vec_IntPush( vXorLits, iObjNew );
+ }
+ }
+ else if ( Gia_ObjIsHead( p, i ) )
+ {
+ iPrev = i;
+ Gia_ClassForEachObj1( p, i, iObj )
+ {
+ iPrevNew = Cec_ManCombSpecReal( pNew, p, Gia_ManObj(p, iPrev) );
+ iObjNew = Cec_ManCombSpecReal( pNew, p, Gia_ManObj(p, iObj) );
+ iPrevNew = Gia_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) );
+ iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) );
+ if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 )
+ {
+ Vec_IntPush( *pvOutputs, iPrev );
+ Vec_IntPush( *pvOutputs, iObj );
+ Vec_IntPush( vXorLits, Gia_ManHashAnd(pNew, iPrevNew, Gia_LitNot(iObjNew)) );
+ }
+ iPrev = iObj;
+ }
+ iObj = i;
+ iPrevNew = Cec_ManCombSpecReal( pNew, p, Gia_ManObj(p, iPrev) );
+ iObjNew = Cec_ManCombSpecReal( pNew, p, Gia_ManObj(p, iObj) );
+ iPrevNew = Gia_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) );
+ iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) );
+ if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 )
+ {
+ Vec_IntPush( *pvOutputs, iPrev );
+ Vec_IntPush( *pvOutputs, iObj );
+ Vec_IntPush( vXorLits, Gia_ManHashAnd(pNew, iPrevNew, Gia_LitNot(iObjNew)) );
+ }
+ }
+ }
+ }
+ else
+ {
+ Gia_ManForEachObj1( p, pObj, i )
+ {
+ pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
+ if ( pRepr == NULL )
+ continue;
+ iPrevNew = Gia_ObjIsConst(p, i)? 0 : Cec_ManCombSpecReal( pNew, p, pRepr );
+ iObjNew = Cec_ManCombSpecReal( pNew, p, pObj );
+ iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
+ if ( iPrevNew != iObjNew )
+ {
+ Vec_IntPush( *pvOutputs, Gia_ObjId(p, pRepr) );
+ Vec_IntPush( *pvOutputs, Gia_ObjId(p, pObj) );
+ Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, iPrevNew, iObjNew) );
+ }
+ }
+ }
+ Vec_IntForEachEntry( vXorLits, iObjNew, i )
+ Gia_ManAppendCo( pNew, iObjNew );
+ Vec_IntFree( vXorLits );
+ Gia_ManHashStop( pNew );
+//printf( "Before sweeping = %d\n", Gia_ManAndNum(pNew) );
+ pNew = Gia_ManCleanup( pTemp = pNew );
+//printf( "After sweeping = %d\n", Gia_ManAndNum(pNew) );
+ Gia_ManStop( pTemp );
+ return pNew;
+}
+
+
+/**Function*************************************************************
+
Synopsis []
Description []
@@ -39,9 +194,293 @@
SeeAlso []
***********************************************************************/
-Gia_Man_t * Cec_ManChoiceComputation( Gia_Man_t * pAig, Cec_ParChc_t * pPars )
+int Cec_ManChoiceComputation_int( Gia_Man_t * pAig, Cec_ParChc_t * pPars )
+{
+ int nItersMax = 1000;
+ Vec_Str_t * vStatus;
+ Vec_Int_t * vOutputs;
+ Vec_Int_t * vCexStore;
+ Cec_ParSim_t ParsSim, * pParsSim = &ParsSim;
+ Cec_ParSat_t ParsSat, * pParsSat = &ParsSat;
+ Cec_ManSim_t * pSim;
+ Gia_Man_t * pSrm;
+ int r, RetValue;
+ int clkSat = 0, clkSim = 0, clkSrm = 0, clkTotal = clock();
+ int clk2, clk = clock();
+ ABC_FREE( pAig->pReprs );
+ ABC_FREE( pAig->pNexts );
+ Gia_ManRandom( 1 );
+ // prepare simulation manager
+ Cec_ManSimSetDefaultParams( pParsSim );
+ pParsSim->nWords = pPars->nWords;
+ pParsSim->nRounds = pPars->nRounds;
+ pParsSim->fVerbose = pPars->fVerbose;
+ pParsSim->fLatchCorr = 0;
+ pParsSim->fSeqSimulate = 0;
+ // create equivalence classes of registers
+ pSim = Cec_ManSimStart( pAig, pParsSim );
+ Cec_ManSimClassesPrepare( pSim );
+ Cec_ManSimClassesRefine( pSim );
+ // prepare SAT solving
+ Cec_ManSatSetDefaultParams( pParsSat );
+ pParsSat->nBTLimit = pPars->nBTLimit;
+ pParsSat->fVerbose = pPars->fVerbose;
+ if ( pPars->fVerbose )
+ {
+ printf( "Obj = %7d. And = %7d. Conf = %5d. Ring = %d. CSat = %d.\n",
+ Gia_ManObjNum(pAig), Gia_ManAndNum(pAig), pPars->nBTLimit, pPars->fUseRings, pPars->fUseCSat );
+ Cec_ManRefinedClassPrintStats( pAig, NULL, 0, clock() - clk );
+ }
+ // perform refinement of equivalence classes
+ for ( r = 0; r < nItersMax; r++ )
+ {
+ clk = clock();
+ // perform speculative reduction
+ clk2 = clock();
+ pSrm = Cec_ManCombSpecReduce( pAig, &vOutputs, pPars->fUseRings );
+ assert( Gia_ManRegNum(pSrm) == 0 && Gia_ManCiNum(pSrm) == Gia_ManCiNum(pAig) );
+ clkSrm += clock() - clk2;
+ if ( Gia_ManCoNum(pSrm) == 0 )
+ {
+ if ( pPars->fVerbose )
+ Cec_ManRefinedClassPrintStats( pAig, NULL, r+1, clock() - clk );
+ Vec_IntFree( vOutputs );
+ Gia_ManStop( pSrm );
+ break;
+ }
+//Gia_DumpAiger( pSrm, "choicesrm", r, 2 );
+ // found counter-examples to speculation
+ clk2 = clock();
+ if ( pPars->fUseCSat )
+ vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 );
+ else
+ vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus );
+ Gia_ManStop( pSrm );
+ clkSat += clock() - clk2;
+ if ( Vec_IntSize(vCexStore) == 0 )
+ {
+ if ( pPars->fVerbose )
+ Cec_ManRefinedClassPrintStats( pAig, vStatus, r+1, clock() - clk );
+ Vec_IntFree( vCexStore );
+ Vec_StrFree( vStatus );
+ Vec_IntFree( vOutputs );
+ break;
+ }
+ // refine classes with these counter-examples
+ clk2 = clock();
+ RetValue = Cec_ManResimulateCounterExamplesComb( pSim, vCexStore );
+ Vec_IntFree( vCexStore );
+ clkSim += clock() - clk2;
+ Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings );
+ if ( pPars->fVerbose )
+ Cec_ManRefinedClassPrintStats( pAig, vStatus, r+1, clock() - clk );
+ Vec_StrFree( vStatus );
+ Vec_IntFree( vOutputs );
+//Gia_ManEquivPrintClasses( pAig, 1, 0 );
+ }
+ // check the overflow
+ if ( r == nItersMax )
+ printf( "The refinement was not finished. The result may be incorrect.\n" );
+ Cec_ManSimStop( pSim );
+ clkTotal = clock() - clkTotal;
+ // report the results
+ if ( pPars->fVerbose )
+ {
+ ABC_PRTP( "Srm ", clkSrm, clkTotal );
+ ABC_PRTP( "Sat ", clkSat, clkTotal );
+ ABC_PRTP( "Sim ", clkSim, clkTotal );
+ ABC_PRTP( "Other", clkTotal-clkSat-clkSrm-clkSim, clkTotal );
+ ABC_PRT( "TOTAL", clkTotal );
+ }
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Duplicates the AIG in the DFS order.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Gia_ManChoiceMiter_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+ if ( ~pObj->Value )
+ return pObj->Value;
+ Gia_ManChoiceMiter_rec( pNew, p, Gia_ObjFanin0(pObj) );
+ if ( Gia_ObjIsCo(pObj) )
+ return pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+ Gia_ManChoiceMiter_rec( pNew, p, Gia_ObjFanin1(pObj) );
+ return pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Derives the miter of several AIGs for choice computation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManChoiceMiter( Vec_Ptr_t * vGias )
+{
+ Gia_Man_t * pNew, * pGia, * pGia0;
+ int i, k, iNode, nNodes;
+ // make sure they have equal parameters
+ assert( Vec_PtrSize(vGias) > 0 );
+ pGia0 = Vec_PtrEntry( vGias, 0 );
+ Vec_PtrForEachEntry( vGias, pGia, i )
+ {
+ assert( Gia_ManCiNum(pGia) == Gia_ManCiNum(pGia0) );
+ assert( Gia_ManCoNum(pGia) == Gia_ManCoNum(pGia0) );
+ assert( Gia_ManRegNum(pGia) == Gia_ManRegNum(pGia0) );
+ Gia_ManFillValue( pGia );
+ Gia_ManConst0(pGia)->Value = 0;
+ }
+ // start the new manager
+ pNew = Gia_ManStart( Vec_PtrSize(vGias) * Gia_ManObjNum(pGia0) );
+ pNew->pName = Gia_UtilStrsav( pGia0->pName );
+ // create new CIs and assign them to the old manager CIs
+ for ( k = 0; k < Gia_ManCiNum(pGia0); k++ )
+ {
+ iNode = Gia_ManAppendCi(pNew);
+ Vec_PtrForEachEntry( vGias, pGia, i )
+ Gia_ManCi( pGia, k )->Value = iNode;
+ }
+ // create internal nodes
+ Gia_ManHashAlloc( pNew );
+ for ( k = 0; k < Gia_ManCoNum(pGia0); k++ )
+ {
+ Vec_PtrForEachEntry( vGias, pGia, i )
+ Gia_ManChoiceMiter_rec( pNew, pGia, Gia_ManCo( pGia, k ) );
+ }
+ Gia_ManHashStop( pNew );
+ // check the presence of dangling nodes
+ nNodes = Gia_ManHasDandling( pNew );
+ assert( nNodes == 0 );
+ // finalize
+// Gia_ManSetRegNum( pNew, Gia_ManRegNum(pGia0) );
+ return pNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes choices for the vector of AIGs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Gia_Man_t * Cec_ManChoiceComputationVec( Vec_Ptr_t * vGias, Cec_ParChc_t * pPars )
+{
+ Gia_Man_t * pMiter, * pNew;
+ int RetValue;
+ // compute equivalences of the miter
+ pMiter = Gia_ManChoiceMiter( vGias );
+ RetValue = Cec_ManChoiceComputation_int( pMiter, pPars );
+ // derive AIG with choices
+ pNew = Gia_ManEquivToChoices( pMiter, Vec_PtrSize(vGias) );
+ Gia_ManHasChoices( pNew );
+ Gia_ManStop( pMiter );
+ // report the results
+ if ( pPars->fVerbose )
+ {
+// printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n",
+// Gia_ManAndNum(pAig), Gia_ManAndNum(pNew),
+// 100.0*(Gia_ManAndNum(pAig)-Gia_ManAndNum(pNew))/(Gia_ManAndNum(pAig)?Gia_ManAndNum(pAig):1),
+// Gia_ManRegNum(pAig), Gia_ManRegNum(pNew),
+// 100.0*(Gia_ManRegNum(pAig)-Gia_ManRegNum(pNew))/(Gia_ManRegNum(pAig)?Gia_ManRegNum(pAig):1) );
+ }
+ return pNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes choices for one AIGs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Gia_Man_t * Cec_ManChoiceComputation( Gia_Man_t * pAig, Cec_ParChc_t * pParsChc )
+{
+ extern Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars );
+ Dch_Pars_t Pars, * pPars = &Pars;
+ Aig_Man_t * pMan, * pManNew;
+ Gia_Man_t * pGia;
+ if ( 0 )
+ {
+ Vec_Ptr_t * vGias;
+ vGias = Vec_PtrAlloc( 1 );
+ Vec_PtrPush( vGias, pAig );
+ pGia = Cec_ManChoiceComputationVec( vGias, pParsChc );
+ Vec_PtrFree( vGias );
+ }
+ else
+ {
+ pMan = Gia_ManToAig( pAig, 0 );
+ Dch_ManSetDefaultParams( pPars );
+ pPars->fUseGia = 1;
+ pPars->nBTLimit = pParsChc->nBTLimit;
+ pPars->fUseCSat = pParsChc->fUseCSat;
+ pPars->fVerbose = pParsChc->fVerbose;
+ pManNew = Dar_ManChoiceNew( pMan, pPars );
+ pGia = Gia_ManFromAig( pManNew );
+ Aig_ManStop( pManNew );
+ Aig_ManStop( pMan );
+ }
+ return pGia;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs computation of AIGs with choices.]
+
+ Description [Takes several AIGs and performs choicing.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Cec_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars )
{
- return NULL;
+ Cec_ParChc_t ParsChc, * pParsChc = &ParsChc;
+ Vec_Ptr_t * vGias;
+ Gia_Man_t * pGia;
+ Aig_Man_t * pAig;
+ int i;
+ if ( pPars->fVerbose )
+ ABC_PRT( "Synthesis time", pPars->timeSynth );
+ Cec_ManChcSetDefaultParams( pParsChc );
+ pParsChc->nBTLimit = pPars->nBTLimit;
+ pParsChc->fUseCSat = pPars->fUseCSat;
+ if ( pParsChc->fUseCSat && pParsChc->nBTLimit > 100 )
+ pParsChc->nBTLimit = 100;
+ pParsChc->fVerbose = pPars->fVerbose;
+ vGias = Vec_PtrAlloc( 10 );
+ Vec_PtrForEachEntry( vAigs, pAig, i )
+ Vec_PtrPush( vGias, Gia_ManFromAig(pAig) );
+ pGia = Cec_ManChoiceComputationVec( vGias, pParsChc );
+ Gia_ManSetRegNum( pGia, Gia_ManRegNum(Vec_PtrEntry(vGias, 0)) );
+ Vec_PtrForEachEntry( vGias, pAig, i )
+ Gia_ManStop( (Gia_Man_t *)pAig );
+ Vec_PtrFree( vGias );
+ pAig = Gia_ManToAig( pGia, 1 );
+ Gia_ManStop( pGia );
+ return pAig;
}
////////////////////////////////////////////////////////////////////////