117 int i, k, nDontCares;
129 Abc_Print( 1,
"Warning: %d registers in this network have don't-care init values.\n", nDontCares );
130 Abc_Print( 1,
"The don't-care are assumed to be 0. The result may not verify.\n" );
131 Abc_Print( 1,
"Use command \"print_latch\" to see the init values of registers.\n" );
132 Abc_Print( 1,
"Use command \"zero\" to convert or \"init\" to change the values.\n" );
188 Abc_Print( 1,
"Abc_NtkToDarBmc: AIG check has failed.\n" );
239 int i, nNodes, nDontCares;
249 Abc_Print( 1,
"Abc_NtkToDar(): Temporary bug: The PI ordering is wrong!\n" );
258 Abc_Print( 1,
"Abc_NtkToDar(): Temporary bug: The PO ordering is wrong!\n" );
272 Abc_Print( 1,
"Warning: %d registers in this network have don't-care init values.\n", nDontCares );
273 Abc_Print( 1,
"The don't-care are assumed to be 0. The result may not verify.\n" );
274 Abc_Print( 1,
"Use command \"print_latch\" to see the init values of registers.\n" );
275 Abc_Print( 1,
"Use command \"zero\" to convert or \"init\" to change the values.\n" );
280 pMan->fCatchExor = fExors;
309 pMan->fAddStrash = 0;
321 if ( !fExors && nNodes )
322 Abc_Print( 1,
"Abc_NtkToDar(): Unexpected %d dangling nodes when converting to AIG!\n", nNodes );
336 Abc_Print( 1,
"Abc_NtkToDar: AIG check has failed.\n" );
396 Abc_Print( 1,
"Abc_NtkToDar: AIG check has failed.\n" );
420 assert( pMan->nAsserts == 0 );
445 if ( pMan->nAsserts && i ==
Aig_ManCoNum(pMan) - pMan->nAsserts )
451 Abc_Print( 1,
"Abc_NtkFromDar(): Network check has failed.\n" );
474 int i, iNodeId, nDigits;
475 assert( pMan->nAsserts == 0 );
528 if ( pMan->vFlopNums == NULL )
574 Abc_Print( 1,
"Abc_NtkFromDar(): Network check has failed.\n" );
597 assert( pMan->nAsserts == 0 );
611 pObj->
pData = pObjNew;
618 pObj->
pData = pObjNew;
655 Abc_Print( 1,
"Abc_NtkFromAigPhase(): Network check has failed.\n" );
719 Abc_Obj_t * pObjNew, * pObjNewLi, * pObjNewLo, * pConst0 = NULL;
722 int i, k, iFan, nDupGates;
821 printf(
"Added %d buffers/inverters to decouple the CO drivers.\n", nDupGates );
823 printf(
"Duplicated %d gates to decouple the CO drivers.\n", nDupGates );
835 Abc_Print( 1,
"Abc_NtkFromMappedGia(): Network check has failed.\n" );
878 Abc_Obj_t * pObjNew, * pObjNewLi, * pObjNewLo;
880 int i, k, iLit, iFanLit, nDupGates, nCells, fNeedConst[2] = {0};
933 pObjNew->
pData = NULL;
992 printf(
"Added %d buffers/inverters to decouple the CO drivers.\n", nDupGates );
994 printf(
"Duplicated %d gates to decouple the CO drivers.\n", nDupGates );
1004 Abc_Print( 1,
"Abc_NtkFromMappedGia(): Network check has failed.\n" );
1028 assert( pMan->nAsserts == 0 );
1033 assert( pMan->vCiNumsOrig != NULL );
1036 pNtkNew->
nConstrs = pMan->nConstrs;
1037 pNtkNew->
nBarBufs = pMan->nBarBufs;
1046 pObj->
pData = pObjNew;
1055 pObj->
pData = pObjNew;
1094 Abc_Print( 1,
"Abc_NtkAfterTrim(): Network check has failed.\n" );
1114 assert( pMan->pEquivs != NULL );
1118 pNtkNew->
nConstrs = pMan->nConstrs;
1139 Abc_Print( 1,
"Abc_NtkFromDar(): Network check has failed.\n" );
1151 printf(
"%d ", Counter );
1173 Abc_Obj_t * pObjNew, * pFaninNew, * pFaninNew0, * pFaninNew1;
1180 pNtkNew->
nConstrs = pMan->nConstrs;
1181 pNtkNew->
nBarBufs = pMan->nBarBufs;
1228 Abc_Print( 1,
"Abc_NtkFromIvySeq(): Network check has failed.\n" );
1338 Abc_Print( 1,
"Abc_NtkDar: The network check has failed.\n" );
1366 pPars->nBTLimitNode = nConfLimit;
1367 pPars->fChoicing = fChoicing;
1368 pPars->fDoSparse = fDoSparse;
1369 pPars->fSpeculate = fSpeculate;
1370 pPars->fProve = fProve;
1371 pPars->fVerbose = fVerbose;
1426 pMan =
Csw_Sweep( pTemp = pMan, nCutsMax, nLeafMax, fVerbose );
1537 pMan =
Dar_ManCompress2( pTemp = pMan, fBalance, fUpdateLevel, fFanout, fPower, fVerbose );
1566 pMan =
Dar_ManChoice( pTemp = pMan, fBalance, fUpdateLevel, fConstruct, nConfMax, nLevelMax, fVerbose );
1598 if ( pPars->fSynthesis )
1606 if ( pPars->fUseGia )
1643 pMan =
Dar_ManRwsat( pTemp = pMan, fBalance, fVerbose );
1672 int i, k, nDupGates;
1699 pObj->
pData = pNodeNew;
1721 Abc_Print( 1,
"Abc_NtkConstructFromCnf(): Network check has failed.\n" );
1752 Abc_Print( 1,
"Abc_NtkDarToCnf: AIG check has failed.\n" );
1804 int Abc_NtkDSat(
Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit,
int nLearnedStart,
int nLearnedDelta,
int nLearnedPerce,
int fAlignPol,
int fAndOuts,
int fNewSolver,
int fVerbose )
1812 RetValue =
Fra_FraigSat( pMan, nConfLimit, nInsLimit, nLearnedStart, nLearnedDelta, nLearnedPerce, fAlignPol, fAndOuts, fNewSolver, fVerbose );
1813 pNtk->
pModel = (
int *)pMan->pData, pMan->pData = NULL;
1831 extern int Aig_ManPartitionedSat(
Aig_Man_t * pNtk,
int nAlgo,
int nPartSize,
int nConfPart,
int nConfTotal,
int fAlignPol,
int fSynthesize,
int fVerbose );
1837 RetValue =
Aig_ManPartitionedSat( pMan, nAlgo, nPartSize, nConfPart, nConfTotal, fAlignPol, fSynthesize, fVerbose );
1838 pNtk->pModel = (
int *)pMan->pData, pMan->pData = NULL;
1872 if ( pNtk2 == NULL && fPartition == 1 )
1874 Abc_Print( 1,
"Abc_NtkDarCec(): Switching to non-partitioned CEC for the miter.\n" );
1889 if ( pNtk2 != NULL )
1893 if ( pMiter == NULL )
1895 Abc_Print( 1,
"Miter computation has failed.\n" );
1904 if ( RetValue == 0 )
1907 Abc_Print( 1,
"Networks are NOT EQUIVALENT after structural hashing.\n" );
1909 if ( pNtk2 == NULL )
1917 if ( RetValue == 1 )
1920 Abc_Print( 1,
"Networks are equivalent after structural hashing.\n" );
1929 Abc_Print( 1,
"Converting miter into AIG has failed.\n" );
1935 if ( pNtk2 == NULL )
1936 pNtk1->
pModel = (
int *)pMan->pData, pMan->pData = NULL;
1941 if ( RetValue == 1 )
1943 Abc_Print( 1,
"Networks are equivalent. " );
1946 else if ( RetValue == 0 )
1948 Abc_Print( 1,
"Networks are NOT EQUIVALENT. " );
1953 Abc_Print( 1,
"Networks are UNDECIDED. " );
1974 Abc_Ntk_t * pNtkAig = NULL, * pNtkFraig;
2032 int header_dumped = 0;
2034 char **pNames =
ABC_ALLOC(
char *, num_orig_latches );
2035 int *p_irrelevant =
ABC_ALLOC(
int, num_orig_latches );
2036 char * pFlopName, * pReprName;
2046 strcpy(pNames[i], temp_name);
2053 p_irrelevant[i] =
false;
2055 pFlopName = pNames[i];
2059 if ( pRepr == NULL )
2068 Abc_Print( 1,
"Here are the flop equivalences:\n");
2069 header_dumped =
true;
2075 Abc_Print( 1,
"Original flop %s is proved equivalent to constant.\n", pFlopName );
2082 pReprName = pNames[repr_idx];
2083 Abc_Print( 1,
"Original flop %s is proved equivalent to flop %s.\n", pFlopName, pReprName );
2087 header_dumped =
false;
2088 for (i=0; i<num_orig_latches; ++i)
2090 if (p_irrelevant[i])
2094 Abc_Print( 1,
"The following flops have been deemed irrelevant:\n");
2095 header_dumped =
true;
2131 if ( pPars->fFlopVerbose )
2209 pPars->fLatchCorrOpt = 1;
2210 pPars->nBTLimit = nConfMax;
2211 pPars->nSatVarMax = nVarsMax;
2212 pPars->fVerbose = fVerbose;
2255 int Abc_NtkDarBmc(
Abc_Ntk_t * pNtk,
int nStart,
int nFrames,
int nSizeMax,
int nNodeDelta,
int nTimeOut,
int nBTLimit,
int nBTLimitAll,
int fRewrite,
int fNewAlgo,
int fOrDecomp,
int nCofFanLit,
int fVerbose,
int * piFrames )
2259 int status, RetValue = -1;
2261 abctime nTimeLimit = nTimeOut ? nTimeOut * CLOCKS_PER_SEC +
Abc_Clock(): 0;
2269 Abc_Print( 1,
"Converting miter into AIG has failed.\n" );
2272 assert( pMan->nRegs > 0 );
2281 RetValue =
Saig_ManBmcSimple( pMan, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, &iFrame, nCofFanLit );
2286 pNtk->
pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
2287 if ( RetValue == 1 )
2288 Abc_Print( 1,
"Incorrect return value. " );
2289 else if ( RetValue == -1 )
2291 Abc_Print( 1,
"No output asserted in %d frames. Resource limit reached ",
Abc_MaxInt(iFrame+1,0) );
2292 if ( nTimeLimit &&
Abc_Clock() > nTimeLimit )
2293 Abc_Print( 1,
"(timeout %d sec). ", nTimeLimit );
2295 Abc_Print( 1,
"(conf limit %d). ", nBTLimit );
2300 Abc_Print( 1,
"Output %d of miter \"%s\" was asserted in frame %d. ", pCex->iPo, pNtk->
pName, pCex->iFrame );
2306 RetValue =
Saig_BmcPerform( pMan, nStart, nFrames, nNodeDelta, nTimeOut, nBTLimit, nBTLimitAll, fVerbose, 0, piFrames, 0 );
2309 pNtk->
pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
2316 Abc_Print( 1,
"Abc_NtkDarBmc(): Counter-example verification has FAILED.\n" );
2341 int status, RetValue = -1;
2350 Abc_Print( 1,
"Converting miter into AIG has failed.\n" );
2353 assert( pMan->nRegs > 0 );
2360 pNtk->
pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
2363 if ( RetValue == 1 )
2367 else if ( RetValue == -1 )
2372 if ( nTimeOut &&
Abc_Clock() > nTimeOut )
2379 Abc_Print( 1,
"The total of %d outputs asserted in %d frames. Resource limit reached ", pPars->
nFailOuts, pPars->
iFrame );
2391 Abc_Print( 1,
"Output %d of miter \"%s\" was asserted in frame %d. ", pCex->iPo, pNtk->
pName, pCex->iFrame );
2396 if ( pMan->vSeqModelVec == NULL ||
Vec_PtrCountZero(pMan->vSeqModelVec) == nOutputs )
2397 Abc_Print( 1,
"None of the %d outputs is found to be SAT", nOutputs );
2399 Abc_Print( 1,
"All %d outputs are found to be SAT", nOutputs );
2404 Abc_Print( 1,
" while others timed out (%d out of %d)", pPars->
nDropOuts, nOutputs );
2412 if ( RetValue == 0 && pPars->
fSolveAll )
2416 pNtk->
vSeqModelVec = pMan->vSeqModelVec; pMan->vSeqModelVec = NULL;
2422 Abc_Print( 1,
"Abc_NtkDarBmc3(): Counter-example verification has FAILED.\n" );
2445 int RetValue = -1, iFrame;
2447 int nTotalProvedSat = 0;
2448 assert( pMan->nRegs > 0 );
2451 if ( pPars->fUseSeparate )
2460 if ( pPars->fVerbose )
2463 pTemp =
Aig_ManScl( pAux = pTemp, 1, 1, 0, -1, -1, 0, 0 );
2467 pTemp->pSeqModel = NULL;
2468 RetValue =
Fra_FraigSat( pTemp, pPars->nBTLimit, 0, 0, 0, 0, 0, 0, 0, 0 );
2475 if ( pTemp->pSeqModel )
2477 if ( pPars->fDropSatOuts )
2479 Abc_Print( 1,
"Output %d proved SAT in frame %d (replacing by const 0 and continuing...)\n", i, pTemp->pSeqModel->iFrame );
2488 pCex = pMan->pSeqModel = pTemp->pSeqModel; pTemp->pSeqModel = NULL;
2495 if ( RetValue == 1 )
2510 if ( pMan->pSeqModel == NULL )
2519 *ppNtkRes =
Aig_ManScl( pTemp, 1, 1, 0, -1, -1, 0, 0 );
2527 if ( nTotalProvedSat )
2528 Abc_Print( 1,
"The total of %d outputs proved SAT and replaced by const 0 in this run.\n", nTotalProvedSat );
2529 if ( RetValue == 1 )
2531 else if ( RetValue == 0 )
2532 Abc_Print( 1,
"Output %d of miter \"%s\" was asserted in frame %d. ", pMan->pSeqModel ? pMan->pSeqModel->iPo : -1, pMan->pName, iFrame );
2533 else if ( RetValue == -1 )
2561 Abc_Print( 1,
"Converting miter into AIG has failed.\n" );
2564 if ( pPars->fUseSeparate && ppNtkRes )
2577 pNtk->
pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
2595 char * pFileNameGeneric, pFileName0[1000], pFileName1[1000];
2601 Abc_Print( 1,
"Converting network into AIG has failed.\n" );
2608 Abc_Print( 1,
"Demitering has failed.\n" );
2615 sprintf( pFileName0,
"%s",
"part0.aig" );
2616 sprintf( pFileName1,
"%s",
"part1.aig" );
2621 Abc_Print( 1,
"Demitering produced two files \"%s\" and \"%s\".\n", pFileName0, pFileName1 );
2646 char * pFileNameGeneric, pFileName0[1000], pFileName1[1000];
2652 Abc_Print( 1,
"Converting network into AIG has failed.\n" );
2663 Abc_Print( 1,
"Demitering has failed.\n" );
2668 sprintf( pFileName0,
"%s%s", pFileNameGeneric,
"_part0.aig" );
2669 sprintf( pFileName1,
"%s%s", pFileNameGeneric,
"_part1.aig" );
2674 Abc_Print( 1,
"Demitering produced two files \"%s\" and \"%s\".\n", pFileName0, pFileName1 );
2699 char * pFileNameGeneric, pFileName0[1000], pFileName1[1000];
2703 Abc_Print( 1,
"The number of POs should be even.\n" );
2710 Abc_Print( 1,
"Converting network into AIG has failed.\n" );
2716 Abc_Print( 1,
"Demitering has failed.\n" );
2729 sprintf( pFileName0,
"%s",
"part0.aig" );
2730 sprintf( pFileName1,
"%s",
"part1.aig" );
2734 Abc_Print( 1,
"Demitering produced two files \"%s\" and \"%s\".\n", pFileName0, pFileName1 );
2770 int iFrame = -1, RetValue = -1;
2779 Abc_Print( 1,
"The network has no latches. Running CEC.\n" );
2792 Abc_Print( 1,
"Networks are not equivalent.\n" );
2803 if ( RetValue == 1 )
2805 Abc_Print( 1,
"Networks are equivalent after CEC. " );
2819 Abc_Print( 1,
"Converting miter into AIG has failed.\n" );
2822 assert( pMan->nRegs > 0 );
2826 RetValue =
Saig_BmcPerform( pMan, 0, nBmcFramesMax, 2000, 0, nBmcConfMax, 0, pSecPar->
fVerbose, 0, &iFrame, 0 );
2827 if ( RetValue == 0 )
2829 Abc_Print( 1,
"Networks are not equivalent.\n" );
2838 pNtk->
pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
2853 pNtk->
pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
2857 Abc_Print( 1,
"Output %d of miter \"%s\" was asserted in frame %d.\n", pCex->iPo, pNtk->
pName, pCex->iFrame );
2859 Abc_Print( 1,
"Abc_NtkDarProve(): Counter-example verification has FAILED.\n" );
2886 if ( pMiter == NULL )
2888 Abc_Print( 1,
"Miter computation has failed.\n" );
2892 if ( RetValue == 0 )
2895 Abc_Print( 1,
"Networks are NOT EQUIVALENT after structural hashing.\n" );
2903 if ( RetValue == 1 )
2906 Abc_Print( 1,
"Networks are equivalent after structural hashing.\n" );
2943 Abc_Print( 1,
"Converting miter into AIG has failed.\n" );
2946 assert( pMan->nRegs > 0 );
2973 Abc_Print( 1,
"Converting network into AIG has failed.\n" );
2977 pPars->nDropOuts =
Saig_ManPoNum(pMan) - pPars->nProveOuts - pPars->nFailOuts;
2978 if ( !pPars->fSilent )
2980 if ( pPars->fSolveAll )
2981 Abc_Print( 1,
"Properties: All = %d. Proved = %d. Disproved = %d. Undecided = %d. ",
2982 Saig_ManPoNum(pMan), pPars->nProveOuts, pPars->nFailOuts, pPars->nDropOuts );
2983 else if ( RetValue == 1 )
2987 if ( RetValue == 0 )
2989 if ( pMan->pSeqModel == NULL )
2990 Abc_Print( 1,
"Abc_NtkDarPdr(): Counter-example is not available.\n" );
2993 Abc_Print( 1,
"Output %d of miter \"%s\" was asserted in frame %d. ", pMan->pSeqModel->iPo, pNtk->
pName, pMan->pSeqModel->iFrame );
2995 Abc_Print( 1,
"Abc_NtkDarPdr(): Counter-example verification has FAILED.\n" );
2998 else if ( RetValue == -1 )
3023 pMan->pSeqModel = NULL;
3027 pMan->vSeqModelVec = NULL;
3049 if ( pMan1 == NULL )
3051 Abc_Print( 1,
"Converting miter into AIG has failed.\n" );
3059 if ( pMan2 == NULL )
3062 Abc_Print( 1,
"Converting miter into AIG has failed.\n" );
3070 Abc_Print( 1,
"The networks have different number of PIs.\n" );
3077 Abc_Print( 1,
"The networks have different number of POs.\n" );
3084 Abc_Print( 1,
"The networks have different number of flops.\n" );
3114 if ( pMan1 == NULL )
3116 Abc_Print( 1,
"Converting miter into AIG has failed.\n" );
3124 if ( pMan2 == NULL )
3126 Abc_Print( 1,
"Converting miter into AIG has failed.\n" );
3155 Aig_Man_t * pMan1, * pMan2 = NULL, * pManRes;
3160 if ( pMan1 == NULL )
3162 Abc_Print( 1,
"Converting miter into AIG has failed.\n" );
3170 if ( pMan2 == NULL )
3172 Abc_Print( 1,
"Converting miter into AIG has failed.\n" );
3214 if ( fLatchConst && pMan->nRegs )
3215 pMan =
Aig_ManConstReduce( pMan, fUseMvSweep, nFramesSymb, nFramesSatur, fVerbose, fVeryVerbose );
3216 if ( fLatchEqual && pMan->nRegs )
3221 if ( pMan->vFlopNums )
3223 pMan->vFlopNums = NULL;
3224 pMan =
Aig_ManScl( pTemp = pMan, fLatchConst, fLatchEqual, fUseMvSweep, nFramesSymb, nFramesSatur, fVerbose, fVeryVerbose );
3253 if ( pMan->vFlopNums )
3255 pMan->vFlopNums = NULL;
3257 pMan =
Rtm_ManRetime( pTemp = pMan, 1, nStepsMax, fVerbose );
3287 if ( pMan->vFlopNums )
3289 pMan->vFlopNums = NULL;
3323 if ( pMan->vFlopNums )
3325 pMan->vFlopNums = NULL;
3357 if ( pMan->vFlopNums )
3359 pMan->vFlopNums = NULL;
3361 pMan =
Saig_ManRetimeMinArea( pTemp = pMan, nMaxIters, fForwardOnly, fBackwardOnly, fInitial, fVerbose );
3388 if ( pMan->vFlopNums )
3390 pMan->vFlopNums = NULL;
3448 int status, RetValue = -1;
3471 Abc_Print( 1,
"Simulation of %d frames with %d words asserted output %d in frame %d. ",
3475 Abc_Print( 1,
"Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
3484 Abc_Print( 1,
"Simulation of %d frames with %d words did not assert the outputs. ",
3492 if ( pFileSim != NULL )
3506 Abc_Print( 1,
"Simulation of %d frame%s with %d word%s asserted output %d in frame %d. ",
3509 pCex->iPo, pCex->iFrame );
3512 Abc_Print( 1,
"Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
3521 Abc_Print( 1,
"Simulation of %d frames with %d words did not assert the outputs. ",
3545 int status, RetValue = -1;
3555 if ( pMan->pSeqModel )
3561 Abc_Print( 1,
"Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
3565 pNtk->
pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
3575 pNtk->
vSeqModelVec = pMan->vSeqModelVec; pMan->vSeqModelVec = NULL;
3577 pNtk->
pData = pMan->pData; pMan->pData = NULL;
3593 int Abc_NtkDarClau(
Abc_Ntk_t * pNtk,
int nFrames,
int nPref,
int nClauses,
int nLutSize,
int nLevels,
int nCutsMax,
int nBatches,
int fStepUp,
int fBmc,
int fRefs,
int fTarget,
int fVerbose,
int fVeryVerbose )
3595 extern int Fra_Clau(
Aig_Man_t * pMan,
int nIters,
int fVerbose,
int fVeryVerbose );
3596 extern int Fra_Claus(
Aig_Man_t * pAig,
int nFrames,
int nPref,
int nClauses,
int nLutSize,
int nLevels,
int nCutsMax,
int nBatches,
int fStepUp,
int fBmc,
int fRefs,
int fTarget,
int fVerbose,
int fVeryVerbose );
3600 Abc_Print( 1,
"The number of outputs should be 1.\n" );
3607 if ( pMan->vFlopNums )
3609 pMan->vFlopNums = NULL;
3612 Fra_Claus( pMan, nFrames, nPref, nClauses, nLutSize, nLevels, nCutsMax, nBatches, fStepUp, fBmc, fRefs, fTarget, fVerbose, fVeryVerbose );
3635 pMan =
Aig_ManFrames( pTemp = pMan, nFrames, 0, 1, 1, 1, NULL );
3655 extern Aig_Man_t *
Saig_ManTempor(
Aig_Man_t * pAig,
int nFrames,
int TimeOut,
int nConfLimit,
int fUseBmc,
int fUseTransSigs,
int fVerbose,
int fVeryVerbose );
3661 pTemp =
Saig_ManTempor( pMan, nFrames, TimeOut, nConfLimit, fUseBmc, fUseTransSigs, fVerbose, fVeryVerbose );
3663 if ( pTemp == NULL )
3681 int Abc_NtkDarInduction(
Abc_Ntk_t * pNtk,
int nTimeOut,
int nFramesMax,
int nConfMax,
int fUnique,
int fUniqueAll,
int fGetCex,
int fVerbose,
int fVeryVerbose )
3689 RetValue =
Saig_ManInduction( pMan, nTimeOut, nFramesMax, nConfMax, fUnique, fUniqueAll, fGetCex, fVerbose, fVeryVerbose );
3690 if ( RetValue == 1 )
3692 Abc_Print( 1,
"Networks are equivalent. " );
3695 else if ( RetValue == 0 )
3697 Abc_Print( 1,
"Networks are NOT EQUIVALENT. " );
3702 Abc_Print( 1,
"Networks are UNDECIDED. " );
3709 pNtk->
pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
3731 Aig_Man_t * pManOn, * pManOff, * pManAig;
3734 Abc_Print( 1,
"Currently works only for single-output networks.\n" );
3739 Abc_Print( 1,
"The number of PIs should be the same.\n" );
3744 if ( pManOn == NULL )
3747 if ( pManOff == NULL )
3750 pManAig =
Aig_ManInter( pManOn, pManOff, fRelation, fVerbose );
3751 if ( pManAig == NULL )
3753 Abc_Print( 1,
"Interpolant computation failed.\n" );
3788 if ( pManOn == NULL )
3791 if ( pManOff == NULL )
3815 Abc_Ntk_t * pNtkOn1, * pNtkOff1, * pNtkInter1, * pNtkInter;
3820 Abc_Print( 1,
"Currently works only for networks with equal number of POs.\n" );
3873 Abc_Print( 1,
"Abc_NtkAttachBottom(): Network check has failed.\n" );
4063 if ( pMan1 == NULL )
4066 if ( pMan2 == NULL )
4097 Aig_Man_t * pMan1, * pMan2 = NULL, * pMan;
4099 if ( pMan1 == NULL )
4104 if ( pMan2 == NULL )
4138 if ( pMan1 == NULL )
4143 Abc_Print( 1,
"Selected object %d as a window pivot.\n", pObj->
Id );
4150 Abc_Print( 1,
"The ID is too large.\n" );
4157 Abc_Print( 1,
"Object with ID %d does not exist.\n", nObjId );
4163 Abc_Print( 1,
"Object with ID %d is not a node or reg output.\n", nObjId );
4192 Aig_Man_t * pMan1, * pMan2 = NULL, * pMan;
4195 if ( pMan1 == NULL )
4200 Abc_Print( 1,
"Selected object %d as a window pivot.\n", pObj->
Id );
4207 Abc_Print( 1,
"The ID is too large.\n" );
4214 Abc_Print( 1,
"Object with ID %d does not exist.\n", nObjId );
4220 Abc_Print( 1,
"Object with ID %d is not a node or reg output.\n", nObjId );
4227 if ( pMan2 == NULL )
4295 Abc_Print( 1,
"Cleanup removed %d primary inputs without fanout.\n", Temp );
4301 Abc_Print( 1,
"Cleanup removed %d primary outputs driven by const-0.\n", Temp );
4331 pNtk->
pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
4363 int i, k, iPis, iPos, nDupGates;
4368 Abc_Print( 1,
"Current library does not contain gate \"%s\".\n", pRes->
pName );
4378 if ( pRes->
Type == -1 )
4379 pNodeNew =
Abc_NtkCi( pNtkNew, iPis++ );
4380 else if ( pRes->
Type == 1 )
4381 pNodeNew =
Abc_NtkCo( pNtkNew, iPos++ );
4387 for ( k = 0; k < pRes->
nFans; k++ )
4432 if ( vMapping == NULL )
4442 Abc_Print( 1,
"Abc_NtkDar: The network check has failed.\n" );
4631 extern void Llb_ManComputeDomsTest(
Aig_Man_t * pAig,
int Num );
4686 extern void Llb_BddStructAnalysis(
Aig_Man_t * pMan );
Aig_Obj_t * Aig_ObjCreateCo(Aig_Man_t *p, Aig_Obj_t *pDriver)
static int Gia_ObjIsCellBuf(Gia_Man_t *p, int iLit)
ABC_NAMESPACE_IMPL_START void Fra_ManPartitionTest(Aig_Man_t *p, int nComLim)
DECLARATIONS ///.
Vec_Ptr_t * Amap_ManTest(Aig_Man_t *pAig, Amap_Par_t *pPars)
static unsigned Abc_ObjId(Abc_Obj_t *pObj)
Aig_Man_t * Saig_ManDupUnfoldConstrs(Aig_Man_t *pAig)
Mio_Gate_t * Mio_LibraryReadGateByName(Mio_Library_t *pLib, char *pName, char *pOutName)
static void Aig_ObjSetEquiv(Aig_Man_t *p, Aig_Obj_t *pObj, Aig_Obj_t *pEqu)
static Vec_Ptr_t * Vec_PtrStart(int nSize)
static int Gia_ObjFaninC2(Gia_Man_t *p, Gia_Obj_t *pObj)
int Nm_ManFindIdByName(Nm_Man_t *p, char *pName, int Type)
static int Abc_NtkIsStrash(Abc_Ntk_t *pNtk)
Vec_Ptr_t * Abc_NtkCollectCiNames(Abc_Ntk_t *pNtk)
static int Gia_ObjCellId(Gia_Man_t *p, int iLit)
int Abc_NtkDarReach(Abc_Ntk_t *pNtk, Saig_ParBbr_t *pPars)
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Abc_Ntk_t * Abc_NtkDarFold(Abc_Ntk_t *pNtk, int fCompl, int fVerbose)
ABC_DLL int Aig_ManCheck(Aig_Man_t *p)
FUNCTION DECLARATIONS ///.
void Abc_CollectTopOr(Abc_Obj_t *pObj, Vec_Ptr_t *vSuper)
ABC_DLL void Abc_NtkMakeComb(Abc_Ntk_t *pNtk, int fRemoveLatches)
static Aig_Obj_t * Aig_ObjRepr(Aig_Man_t *p, Aig_Obj_t *pObj)
ABC_DLL void * Abc_FrameReadLibGen()
void Llb_NonlinExperiment(Aig_Man_t *pAig, int Num)
int Abc_NtkDarBmcInter_int(Aig_Man_t *pMan, Inter_ManParams_t *pPars, Aig_Man_t **ppNtkRes)
Vec_Int_t * Abc_NtkFindDcLatches(Abc_Ntk_t *pNtk)
int Saig_ManBmcScalable(Aig_Man_t *pAig, Saig_ParBmc_t *pPars)
void Gia_ManStop(Gia_Man_t *p)
Abc_Ntk_t * Abc_NtkDch(Abc_Ntk_t *pNtk, Dch_Pars_t *pPars)
Abc_Ntk_t * Abc_NtkFromDar(Abc_Ntk_t *pNtkOld, Aig_Man_t *pMan)
int Abc_NtkPartitionedSat(Abc_Ntk_t *pNtk, int nAlgo, int nPartSize, int nConfPart, int nConfTotal, int fAlignPol, int fSynthesize, int fVerbose)
#define Gia_ManForEachCo(p, pObj, i)
typedefABC_NAMESPACE_HEADER_START struct Vec_Vec_t_ Vec_Vec_t
INCLUDES ///.
ABC_NAMESPACE_IMPL_START int Abc_ObjCompareById(Abc_Obj_t **pp1, Abc_Obj_t **pp2)
DECLARATIONS ///.
static int Saig_ManPoNum(Aig_Man_t *p)
ABC_DLL int * Abc_NtkVerifyGetCleanModel(Abc_Ntk_t *pNtk, int nFrames)
static int Saig_ObjIsLo(Aig_Man_t *p, Aig_Obj_t *pObj)
Aig_Man_t * Saig_ManRetimeMinArea(Aig_Man_t *p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose)
int Aig_ManCoCleanup(Aig_Man_t *p)
static int Abc_ObjIsBo(Abc_Obj_t *pObj)
ABC_DLL Abc_Obj_t * Abc_AigConst1(Abc_Ntk_t *pNtk)
static int Gia_ManPoNum(Gia_Man_t *p)
Abc_Ntk_t * Abc_NtkFromMappedGia(Gia_Man_t *p)
static int Gia_ObjFaninC1(Gia_Obj_t *pObj)
Cnf_Dat_t * Cnf_Derive(Aig_Man_t *pAig, int nOutputs)
Hop_Obj_t * Hop_And(Hop_Man_t *p, Hop_Obj_t *p0, Hop_Obj_t *p1)
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
void Abc_NtkDarConstrProfile(Abc_Ntk_t *pNtk, int fVerbose)
Abc_Ntk_t * Abc_NtkDarEnlarge(Abc_Ntk_t *pNtk, int nFrames, int fVerbose)
Abc_Ntk_t * Abc_NtkDarTestNtk(Abc_Ntk_t *pNtk)
int Saig_ManRetimeSteps(Aig_Man_t *p, int nSteps, int fForward, int fAddBugs)
void Abc_NtkPrintSccs(Abc_Ntk_t *pNtk, int fVerbose)
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
void Aig_ManStop(Aig_Man_t *p)
int Abc_NtkDarDemiterNew(Abc_Ntk_t *pNtk)
int Gia_ManSimSimulate(Gia_Man_t *pAig, Gia_ParSim_t *pPars)
typedefABC_NAMESPACE_HEADER_START struct Pdr_Par_t_ Pdr_Par_t
INCLUDES ///.
void Cnf_DataWriteIntoFile(Cnf_Dat_t *p, char *pFileName, int fReadable, Vec_Int_t *vForAlls, Vec_Int_t *vExists)
Fra_Sml_t * Fra_SmlSimulateSeq(Aig_Man_t *pAig, int nPref, int nFrames, int nWords, int fCheckMiter)
int Abc_NtkDarSec(Abc_Ntk_t *pNtk1, Abc_Ntk_t *pNtk2, Fra_Sec_t *pSecPar)
int Aig_ManSeqCleanup(Aig_Man_t *p)
Abc_Ntk_t * Abc_NtkDarFrames(Abc_Ntk_t *pNtk, int nPrefix, int nFrames, int fInit, int fVerbose)
int Abc_NtkDarProve(Abc_Ntk_t *pNtk, Fra_Sec_t *pSecPar, int nBmcFramesMax, int nBmcConfMax)
void Abc_NtkInterFast(Abc_Ntk_t *pNtkOn, Abc_Ntk_t *pNtkOff, int fVerbose)
static int Gia_ObjFaninLit0p(Gia_Man_t *p, Gia_Obj_t *pObj)
Aig_Man_t * Saig_ManPhaseAbstract(Aig_Man_t *p, Vec_Int_t *vInits, int nFrames, int nPref, int fIgnore, int fPrint, int fVerbose)
int Saig_ManVerifyCex(Aig_Man_t *pAig, Abc_Cex_t *p)
Hop_Obj_t * Abc_ObjHopFromGia(Hop_Man_t *pHopMan, Gia_Man_t *p, int GiaId, Vec_Ptr_t *vCopies)
static int Abc_ObjFanoutNum(Abc_Obj_t *pObj)
ABC_NAMESPACE_IMPL_END ABC_NAMESPACE_IMPL_START Abc_Ntk_t * Amap_ManProduceNetwork(Abc_Ntk_t *pNtk, Vec_Ptr_t *vMapping)
typedefABC_NAMESPACE_HEADER_START struct Ssw_Pars_t_ Ssw_Pars_t
INCLUDES ///.
static int Abc_NtkBoxNum(Abc_Ntk_t *pNtk)
Aig_Man_t * Fra_FraigLatchCorrespondence(Aig_Man_t *pAig, int nFramesP, int nConfMax, int fProve, int fVerbose, int *pnIter, float TimeLimit)
Aig_Man_t * Saig_ManDupFoldConstrsFunc(Aig_Man_t *pAig, int fCompl, int fVerbose)
int Abc_NtkDarSimSec(Abc_Ntk_t *pNtk1, Abc_Ntk_t *pNtk2, Ssw_Pars_t *pPars)
Abc_Ntk_t * Abc_NtkDarExtWin(Abc_Ntk_t *pNtk, int nObjId, int nDist, int fVerbose)
Abc_Ntk_t * Abc_NtkDarOutdec(Abc_Ntk_t *pNtk, int nLits, int fVerbose)
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
static void Vec_PtrFreeFree(Vec_Ptr_t *p)
static Abc_Obj_t * Abc_NtkFromCellRead(Abc_Ntk_t *p, Vec_Int_t *vCopyLits, int i, int c)
ABC_DLL char * Abc_SopCreateAnd(Mem_Flex_t *pMan, int nVars, int *pfCompl)
static int Abc_Var2Lit(int Var, int fCompl)
Aig_Man_t * Aig_ManStart(int nNodesMax)
DECLARATIONS ///.
Aig_Man_t * Aig_ManDupDfs(Aig_Man_t *p)
static Abc_Obj_t * Abc_ObjChild1Copy(Abc_Obj_t *pObj)
void Aig_ManPrintStats(Aig_Man_t *p)
static int Abc_ObjIsBarBuf(Abc_Obj_t *pObj)
ABC_DLL char * Abc_SopCreateFromIsop(Mem_Flex_t *pMan, int nVars, Vec_Int_t *vCover)
Aig_Man_t * Ssw_SignalCorrespondence(Aig_Man_t *pAig, Ssw_Pars_t *pPars)
abctime timeCnf
DECLARATIONS ///.
int Dar_ManRewrite(Aig_Man_t *pAig, Dar_RwrPar_t *pPars)
int Fra_Clau(Aig_Man_t *pMan, int nIters, int fVerbose, int fVeryVerbose)
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
int Saig_ManBmcSimple(Aig_Man_t *pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int *piFrame, int nCofFanLit)
ABC_DLL Abc_Obj_t * Abc_NtkDupObj(Abc_Ntk_t *pNtkNew, Abc_Obj_t *pObj, int fCopyName)
void Cnf_DataTranformPolarity(Cnf_Dat_t *pCnf, int fTransformPos)
Abc_Ntk_t * Abc_NtkDarAmap(Abc_Ntk_t *pNtk, Amap_Par_t *pPars)
static int Gia_ObjValue(Gia_Obj_t *pObj)
static int Abc_NtkLatchNum(Abc_Ntk_t *pNtk)
ABC_DLL Abc_Obj_t * Abc_NtkCreateNodeConst1(Abc_Ntk_t *pNtk)
Aig_Man_t * Aig_ManRetimeFrontier(Aig_Man_t *p, int nStepsMax)
Abc_Ntk_t * Abc_NtkDarRetime(Abc_Ntk_t *pNtk, int nStepsMax, int fVerbose)
static int Abc_ObjFaninC0(Abc_Obj_t *pObj)
static int Abc_ObjIsPi(Abc_Obj_t *pObj)
ABC_DLL Abc_Ntk_t * Abc_NtkDup(Abc_Ntk_t *pNtk)
Aig_Obj_t * Aig_ObjCreateCi(Aig_Man_t *p)
DECLARATIONS ///.
Abc_Ntk_t * Abc_NtkDarMatch(Abc_Ntk_t *pNtk1, Abc_Ntk_t *pNtk2, int nDist, int fVerbose)
int Saig_ManDemiterDual(Aig_Man_t *p, Aig_Man_t **ppAig0, Aig_Man_t **ppAig1)
Abc_Ntk_t * Abc_NtkDarSynch(Abc_Ntk_t *pNtk1, Abc_Ntk_t *pNtk2, int nWords, int fVerbose)
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
static Aig_Obj_t * Aig_ManConst0(Aig_Man_t *p)
#define Aig_ManForEachCo(p, pObj, i)
int Saig_BmcPerform(Aig_Man_t *pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int *piFrames, int fSilent)
static int Abc_NtkCiNum(Abc_Ntk_t *pNtk)
static int Abc_LatchIsInit0(Abc_Obj_t *pLatch)
Abc_Ntk_t * Abc_NtkBalanceExor(Abc_Ntk_t *pNtk, int fUpdateLevel, int fVerbose)
#define ABC_ALLOC(type, num)
static Aig_Obj_t * Aig_ManObj(Aig_Man_t *p, int i)
#define Abc_NtkForEachCo(pNtk, pCo, i)
Vec_Int_t * Saig_StrSimPerformMatching(Aig_Man_t *p0, Aig_Man_t *p1, int nDist, int fVerbose, Aig_Man_t **ppMiter)
static Abc_Obj_t * Abc_NtkCi(Abc_Ntk_t *pNtk, int i)
int Abc_NtkDarPrintCone(Abc_Ntk_t *pNtk)
static Aig_Obj_t * Aig_Not(Aig_Obj_t *p)
ABC_DLL int Abc_NtkCheck(Abc_Ntk_t *pNtk)
FUNCTION DEFINITIONS ///.
void Prove_ParamsSetDefault(Prove_Params_t *pParams)
FUNCTION DEFINITIONS ///.
typedefABC_NAMESPACE_HEADER_START struct Dch_Pars_t_ Dch_Pars_t
INCLUDES ///.
ABC_DLL char * Abc_ObjAssignName(Abc_Obj_t *pObj, char *pName, char *pSuffix)
ABC_DLL Vec_Ptr_t * Abc_NtkDfs(Abc_Ntk_t *pNtk, int fCollectAll)
static abctime Abc_Clock()
static int Abc_MaxInt(int a, int b)
Hop_Obj_t * Abc_ObjHopFromGia_rec(Hop_Man_t *pHopMan, Gia_Man_t *p, int Id, Vec_Ptr_t *vCopies)
static Abc_Obj_t * Abc_NtkObj(Abc_Ntk_t *pNtk, int i)
static int Vec_PtrSize(Vec_Ptr_t *p)
static Vec_Int_t * Vec_IntStartNatural(int nSize)
Aig_Man_t * Dar_ManChoice(Aig_Man_t *pAig, int fBalance, int fUpdateLevel, int fConstruct, int nConfMax, int nLevelMax, int fVerbose)
Abc_Ntk_t * Abc_NtkDarRetimeMinArea(Abc_Ntk_t *pNtk, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose)
static void * Vec_PtrPop(Vec_Ptr_t *p)
Abc_Ntk_t * Abc_NtkDarInsWin(Abc_Ntk_t *pNtk, Abc_Ntk_t *pCare, int nObjId, int nDist, int fVerbose)
Abc_Ntk_t * Abc_NtkDar(Abc_Ntk_t *pNtk)
static Vec_Int_t * Vec_IntStartFull(int nSize)
Abc_Ntk_t * Abc_NtkDarRetimeStep(Abc_Ntk_t *pNtk, int fVerbose)
static Abc_Obj_t * Abc_ObjFanin0(Abc_Obj_t *pObj)
ABC_DLL int Abc_NtkGetChoiceNum(Abc_Ntk_t *pNtk)
ABC_NAMESPACE_IMPL_START Aig_Man_t * Dar_ManRwsat(Aig_Man_t *pAig, int fBalance, int fVerbose)
DECLARATIONS ///.
static Gia_Obj_t * Gia_ManObj(Gia_Man_t *p, int v)
Abc_Ntk_t * Abc_NtkDarFraigPart(Abc_Ntk_t *pNtk, int nPartSize, int nConfLimit, int nLevelMax, int fVerbose)
static int Abc_NtkCoNum(Abc_Ntk_t *pNtk)
#define Gia_ManForEachLut(p, i)
Aig_Man_t * Saig_ManTempor(Aig_Man_t *pAig, int nFrames, int TimeOut, int nConfLimit, int fUseBmc, int fUseTransSigs, int fVerbose, int fVeryVerbose)
ABC_DLL Abc_Ntk_t * Abc_NtkFraig(Abc_Ntk_t *pNtk, void *pParams, int fAllNodes, int fExdc)
FUNCTION DEFINITIONS ///.
Aig_Man_t * Saig_ManRetimeForward(Aig_Man_t *p, int nMaxIters, int fVerbose)
static int Abc_ObjIsNone(Abc_Obj_t *pObj)
ABC_DLL void Abc_NtkDelete(Abc_Ntk_t *pNtk)
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
int Abc_NtkDarInduction(Abc_Ntk_t *pNtk, int nTimeOut, int nFramesMax, int nConfMax, int fUnique, int fUniqueAll, int fGetCex, int fVerbose, int fVeryVerbose)
Abc_Ntk_t * Abc_NtkFromDarChoices(Abc_Ntk_t *pNtkOld, Aig_Man_t *pMan)
static Abc_Obj_t * Abc_NtkCo(Abc_Ntk_t *pNtk, int i)
Abc_Ntk_t * Abc_NtkInterOne(Abc_Ntk_t *pNtkOn, Abc_Ntk_t *pNtkOff, int fRelation, int fVerbose)
Aig_Man_t * Aig_ManFrames(Aig_Man_t *pAig, int nFs, int fInit, int fOuts, int fRegs, int fEnlarge, Aig_Obj_t ***ppObjMap)
FUNCTION DEFINITIONS ///.
int Abc_NtkDarDemiter(Abc_Ntk_t *pNtk)
ABC_DLL void Abc_ObjAddFanin(Abc_Obj_t *pObj, Abc_Obj_t *pFanin)
ABC_DLL Abc_Ntk_t * Abc_NtkAlloc(Abc_NtkType_t Type, Abc_NtkFunc_t Func, int fUseMemMan)
DECLARATIONS ///.
static void Vec_PtrUniqify(Vec_Ptr_t *p, int(*Vec_PtrSortCompare)()) ___unused
static unsigned * Cnf_CutTruth(Cnf_Cut_t *pCut)
Abc_Ntk_t * Abc_NtkDarSynchOne(Abc_Ntk_t *pNtk, int nWords, int fVerbose)
ABC_DLL void Abc_SopComplementVar(char *pSop, int iVar)
int Saig_ManDemiterSimpleDiff(Aig_Man_t *p, Aig_Man_t **ppAig0, Aig_Man_t **ppAig1)
int Saig_ManPhaseFrameNum(Aig_Man_t *p, Vec_Int_t *vInits)
ABC_DLL Abc_Obj_t * Abc_AigXor(Abc_Aig_t *pMan, Abc_Obj_t *p0, Abc_Obj_t *p1)
static Abc_Obj_t * Abc_NtkCreateBo(Abc_Ntk_t *pNtk)
static Abc_Obj_t * Abc_ObjChild0(Abc_Obj_t *pObj)
Gia_Man_t * Gia_ManFromAig(Aig_Man_t *p)
INCLUDES ///.
void Aig_ManPrintControlFanouts(Aig_Man_t *p)
#define Gia_ManForEachRiRo(p, pObjRi, pObjRo, i)
static void Abc_PrintTime(int level, const char *pStr, abctime time)
static int Aig_ManBufNum(Aig_Man_t *p)
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Abc_Ntk_t * Abc_NtkDarLatchSweep(Abc_Ntk_t *pNtk, int fLatchConst, int fLatchEqual, int fSaveNames, int fUseMvSweep, int nFramesSymb, int nFramesSatur, int fVerbose, int fVeryVerbose)
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
static Vec_Vec_t * Vec_VecDupInt(Vec_Vec_t *p)
static int Abc_ObjIsNode(Abc_Obj_t *pObj)
int Abc_NtkDarDemiterDual(Abc_Ntk_t *pNtk, int fVerbose)
static int Abc_NtkNodeNum(Abc_Ntk_t *pNtk)
static int Aig_ManCoNum(Aig_Man_t *p)
Abc_Cex_t * Fra_SmlGetCounterExample(Fra_Sml_t *p)
Abc_Ntk_t * Abc_NtkDarRetimeF(Abc_Ntk_t *pNtk, int nStepsMax, int fVerbose)
ABC_DLL Abc_Obj_t * Abc_AigAnd(Abc_Aig_t *pMan, Abc_Obj_t *p0, Abc_Obj_t *p1)
static int Aig_ObjIsBuf(Aig_Obj_t *pObj)
ABC_DLL void Abc_NtkAddDummyPoNames(Abc_Ntk_t *pNtk)
static Vec_Int_t * Vec_IntStart(int nSize)
static int Abc_LitIsCompl(int Lit)
void Fra_ParamsDefault(Fra_Par_t *pParams)
DECLARATIONS ///.
static Abc_Obj_t * Abc_ObjChild0Copy(Abc_Obj_t *pObj)
static int Saig_ManConstrNum(Aig_Man_t *p)
ABC_DLL Abc_Ntk_t * Abc_NtkStartFrom(Abc_Ntk_t *pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func)
static int Gia_ObjIsMuxId(Gia_Man_t *p, int iObj)
int Abc_NtkDarSeqSim3(Abc_Ntk_t *pNtk, Ssw_RarPars_t *pPars)
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Aig_Man_t * Abc_NtkToDarChoices(Abc_Ntk_t *pNtk)
ABC_DLL void Abc_NtkDeleteObj(Abc_Obj_t *pObj)
#define Aig_ManForEachNode(p, pObj, i)
int Abc_NtkDarPdr(Abc_Ntk_t *pNtk, Pdr_Par_t *pPars)
Aig_Man_t * Aig_ManReduceLaches(Aig_Man_t *p, int fVerbose)
Aig_Man_t * Saig_Synchronize(Aig_Man_t *pAig1, Aig_Man_t *pAig2, int nWords, int fVerbose)
void Abc_CollectTopOr_rec(Abc_Obj_t *pObj, Vec_Ptr_t *vSuper)
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
static int Gia_ObjLutSize(Gia_Man_t *p, int Id)
void Aig_ObjPatchFanin0(Aig_Man_t *p, Aig_Obj_t *pObj, Aig_Obj_t *pFaninNew)
ABC_DLL int Abc_AigCleanup(Abc_Aig_t *pMan)
int Saig_ManDemiterNew(Aig_Man_t *pMan)
Vec_Int_t * Saig_ManComputeSwitchProbs(Aig_Man_t *pAig, int nFrames, int nPref, int fProbOne)
void Saig_ManPrintCones(Aig_Man_t *p)
FUNCTION DECLARATIONS ///.
int Fra_FraigCecPartitioned(Aig_Man_t *pMan1, Aig_Man_t *pMan2, int nConfLimit, int nPartSize, int fSmart, int fVerbose)
ABC_DLL Abc_Obj_t * Abc_NtkCreateNodeInv(Abc_Ntk_t *pNtk, Abc_Obj_t *pFanin)
int Dar_ManRefactor(Aig_Man_t *pAig, Dar_RefPar_t *pPars)
void Aig_ManSetRegNum(Aig_Man_t *p, int nRegs)
ABC_DLL Abc_Ntk_t * Abc_NtkMiter(Abc_Ntk_t *pNtk1, Abc_Ntk_t *pNtk2, int fComb, int nPartSize, int fImplic, int fMulti)
FUNCTION DEFINITIONS ///.
Abc_Ntk_t * Abc_NtkDrwsat(Abc_Ntk_t *pNtk, int fBalance, int fVerbose)
Abc_Ntk_t * Abc_NtkCSweep(Abc_Ntk_t *pNtk, int nCutsMax, int nLeafMax, int fVerbose)
Aig_Man_t * Aig_ManScl(Aig_Man_t *pAig, int fLatchConst, int fLatchEqual, int fUseMvSweep, int nFramesSymb, int nFramesSatur, int fVerbose, int fVeryVerbose)
static Aig_Obj_t * Aig_ManCi(Aig_Man_t *p, int i)
#define Aig_ManForEachLiLoSeq(p, pObjLi, pObjLo, k)
int Ssw_SecWithSimilarity(Aig_Man_t *p0, Aig_Man_t *p1, Ssw_Pars_t *pPars)
void Cnf_SopConvertToVector(char *pSop, int nCubes, Vec_Int_t *vCover)
Aig_Man_t * Dar_ManCompress2(Aig_Man_t *pAig, int fBalance, int fUpdateLevel, int fFanout, int fPower, int fVerbose)
Fra_Sml_t * Fra_SmlSimulateComb(Aig_Man_t *pAig, int nWords, int fCheckMiter)
int Inter_ManPerformInterpolation(Aig_Man_t *pAig, Inter_ManParams_t *pPars, int *piFrame)
ABC_DLL int Abc_NtkIvyProve(Abc_Ntk_t **ppNtk, void *pPars)
Cnf_Dat_t * Cnf_DeriveFast(Aig_Man_t *p, int nOutputs)
void Ssw_ManSetDefaultParams(Ssw_Pars_t *p)
DECLARATIONS ///.
static int Vec_IntEntry(Vec_Int_t *p, int i)
Aig_Man_t * Aig_ManConstReduce(Aig_Man_t *p, int fUseMvSweep, int nFramesSymb, int nFramesSatur, int fVerbose, int fVeryVerbose)
static int Aig_ManCiNum(Aig_Man_t *p)
int Nm_ManFindIdByNameTwoTypes(Nm_Man_t *p, char *pName, int Type1, int Type2)
static int Abc_Base10Log(unsigned n)
#define ABC_NAMESPACE_IMPL_END
static int Abc_LatchIsInitDc(Abc_Obj_t *pLatch)
#define Cnf_CutForEachLeaf(p, pCut, pLeaf, i)
int Saig_ManDetectConstrTest(Aig_Man_t *p)
ABC_DLL char * Abc_SopCreateXor(Mem_Flex_t *pMan, int nVars)
void Fraig_ParamsSetDefault(Fraig_Params_t *pParams)
static int Aig_ObjIsConst1(Aig_Obj_t *pObj)
ABC_DLL char * Abc_ObjNameDummy(char *pPrefix, int Num, int nDigits)
ABC_DLL Abc_Ntk_t * Abc_NtkCreateCone(Abc_Ntk_t *pNtk, Abc_Obj_t *pNode, char *pNodeName, int fUseAllCis)
static Aig_Obj_t * Aig_ObjEquiv(Aig_Man_t *p, Aig_Obj_t *pObj)
static Aig_Obj_t * Aig_ObjChild1Copy(Aig_Obj_t *pObj)
void Abc_NtkDarTest(Abc_Ntk_t *pNtk, int Num)
Gia_Man_t * Dar_NewChoiceSynthesis(Aig_Man_t *pAig, int fBalance, int fUpdateLevel, int fPower, int fLightSynth, int fVerbose)
static int Gia_ObjIsXor(Gia_Obj_t *pObj)
Abc_Ntk_t * Abc_NtkAfterTrim(Aig_Man_t *pMan, Abc_Ntk_t *pNtkOld)
#define Gia_ManForEachAnd(p, pObj, i)
ABC_DLL void Abc_NtkAddDummyBoxNames(Abc_Ntk_t *pNtk)
Abc_Ntk_t * Abc_NtkDarToCnf(Abc_Ntk_t *pNtk, char *pFileName, int fFastAlgo, int fChangePol, int fVerbose)
static Abc_Obj_t * Abc_NtkCreateLatch(Abc_Ntk_t *pNtk)
Vec_Ptr_t * Aig_ManDfs(Aig_Man_t *p, int fNodesOnly)
STRUCTURE DEFINITIONS ///.
static void Abc_NtkFromCellWrite(Vec_Int_t *vCopyLits, int i, int c, int Id)
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Abc_Ntk_t * Abc_NtkDarSeqSweep(Abc_Ntk_t *pNtk, Fra_Ssw_t *pPars)
ABC_DLL char * Abc_SopCreateMux(Mem_Flex_t *pMan)
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
#define Saig_ManForEachLo(p, pObj, i)
void Gia_ManFillValue(Gia_Man_t *p)
static Aig_Obj_t * Aig_ObjChild0Copy(Aig_Obj_t *pObj)
#define Abc_NtkForEachLatch(pNtk, pObj, i)
static int Abc_LatchIsInit1(Abc_Obj_t *pLatch)
typedefABC_NAMESPACE_HEADER_START struct Cgt_Par_t_ Cgt_Par_t
INCLUDES ///.
static Abc_Obj_t * Abc_NtkCreatePi(Abc_Ntk_t *pNtk)
void Aig_ManSetCioIds(Aig_Man_t *p)
static int Gia_ObjIsCellInv(Gia_Man_t *p, int iLit)
static void Vec_IntFreeP(Vec_Int_t **p)
Abc_Ntk_t * Abc_NtkDarLcorrNew(Abc_Ntk_t *pNtk, int nVarsMax, int nConfMax, int fVerbose)
Aig_Man_t * Cec_ComputeChoices(Gia_Man_t *pGia, Dch_Pars_t *pPars)
#define Gia_ManForEachPi(p, pObj, i)
int Abc_NtkDSat(Abc_Ntk_t *pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose)
Abc_Ntk_t * Abc_NtkDarClockGate(Abc_Ntk_t *pNtk, Abc_Ntk_t *pCare, Cgt_Par_t *pPars)
Fra_Sml_t * Fra_SmlSimulateCombGiven(Aig_Man_t *pAig, char *pFileName, int fCheckMiter, int fVerbose)
Vec_Ptr_t * Abc_NtkCollectCoNames(Abc_Ntk_t *pNtk)
Aig_Man_t * Saig_SynchSequenceApply(Aig_Man_t *pAig, int nWords, int fVerbose)
static void Abc_Print(int level, const char *format,...)
Abc_Ntk_t * Abc_NtkDarTempor(Abc_Ntk_t *pNtk, int nFrames, int TimeOut, int nConfLimit, int fUseBmc, int fUseTransSigs, int fVerbose, int fVeryVerbose)
ABC_NAMESPACE_HEADER_START Aig_Man_t * Csw_Sweep(Aig_Man_t *pAig, int nCutsMax, int nLeafMax, int fVerbose)
INCLUDES ///.
void Ioa_WriteAiger(Aig_Man_t *pMan, char *pFileName, int fWriteSymbols, int fCompact)
static int Vec_PtrCountZero(Vec_Ptr_t *p)
void Llb_ManMinCutTest(Aig_Man_t *pAig, int Num)
static int Aig_ObjFaninC0(Aig_Obj_t *pObj)
void Aig_ManInterFast(Aig_Man_t *pManOn, Aig_Man_t *pManOff, int fVerbose)
FUNCTION DEFINITIONS ///.
int Abc_NtkDarBmc(Abc_Ntk_t *pNtk, int nStart, int nFrames, int nSizeMax, int nNodeDelta, int nTimeOut, int nBTLimit, int nBTLimitAll, int fRewrite, int fNewAlgo, int fOrDecomp, int nCofFanLit, int fVerbose, int *piFrames)
static void Vec_PtrWriteEntry(Vec_Ptr_t *p, int i, void *Entry)
Vec_Int_t * Abc_NtkGetLatchValues(Abc_Ntk_t *pNtk)
static int Aig_ManObjNumMax(Aig_Man_t *p)
int Aig_ManPartitionedSat(Aig_Man_t *p, int nAlgo, int nPartSize, int nConfPart, int nConfTotal, int fAlignPol, int fSynthesize, int fVerbose)
#define Abc_NtkForEachNode(pNtk, pNode, i)
static Abc_Obj_t * Abc_NtkBox(Abc_Ntk_t *pNtk, int i)
static Gia_Obj_t * Gia_ObjFanin2(Gia_Man_t *p, Gia_Obj_t *pObj)
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
static int Gia_ObjIsTravIdCurrentId(Gia_Man_t *p, int Id)
Abc_Ntk_t * Abc_NtkFromCellMappedGia(Gia_Man_t *p)
ABC_DLL Vec_Ptr_t * Abc_AigDfs(Abc_Ntk_t *pNtk, int fCollectAll, int fCollectCos)
static int Abc_NtkConstrNum(Abc_Ntk_t *pNtk)
static int Aig_ObjIsExor(Aig_Obj_t *pObj)
int Fra_FraigSec(Aig_Man_t *p, Fra_Sec_t *pParSec, Aig_Man_t **ppResult)
#define ABC_NAMESPACE_IMPL_START
int Abc_NtkDarBmcInter(Abc_Ntk_t *pNtk, Inter_ManParams_t *pPars, Abc_Ntk_t **ppNtkRes)
Abc_Ntk_t * Abc_NtkDarFraig(Abc_Ntk_t *pNtk, int nConfLimit, int fDoSparse, int fProve, int fTransfer, int fSpeculate, int fChoicing, int fVerbose)
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
static Aig_Obj_t * Aig_ManCo(Aig_Man_t *p, int i)
Aig_Man_t * Aig_ManDupUnsolvedOutputs(Aig_Man_t *p, int fAddRegs)
void Saig_ManDetectConstrFuncTest(Aig_Man_t *p, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose)
ABC_DLL int Abc_NtkLogicMakeSimpleCos(Abc_Ntk_t *pNtk, int fDuplicate)
void Saig_ManBmcSectionsTest(Aig_Man_t *p)
static int Abc_AigNodeIsChoice(Abc_Obj_t *pNode)
static int Aig_ManRegNum(Aig_Man_t *p)
static int Abc_LitNot(int Lit)
int Pdr_ManSolve(Aig_Man_t *p, Pdr_Par_t *pPars)
static Abc_Obj_t * Abc_ObjEquiv(Abc_Obj_t *pObj)
Aig_Man_t * Fra_FraigInduction(Aig_Man_t *p, Fra_Ssw_t *pPars)
Aig_Man_t * Aig_ManInter(Aig_Man_t *pManOn, Aig_Man_t *pManOff, int fRelation, int fVerbose)
static Abc_Obj_t * Abc_ObjRegular(Abc_Obj_t *p)
Aig_Man_t * Saig_ManDecPropertyOutput(Aig_Man_t *pAig, int nLits, int fVerbose)
Abc_Ntk_t * Abc_NtkFromDarSeqSweep(Abc_Ntk_t *pNtkOld, Aig_Man_t *pMan)
void Abc_NtkPrintLatchEquivClasses(Abc_Ntk_t *pNtk, Aig_Man_t *pAig)
Aig_Obj_t * Saig_ManFindPivot(Aig_Man_t *p)
static int Abc_ObjIsBi(Abc_Obj_t *pObj)
Abc_Ntk_t * Abc_NtkDarRetimeMostFwd(Abc_Ntk_t *pNtk, int nMaxIters, int fVerbose)
static int Vec_IntSize(Vec_Int_t *p)
void Dar_BalancePrintStats(Aig_Man_t *p)
ABC_DLL int Abc_NtkMiterIsConstant(Abc_Ntk_t *pMiter)
static int Gia_ManHasMapping(Gia_Man_t *p)
void Abc_NtkDarConstr(Abc_Ntk_t *pNtk, int nFrames, int nConfs, int nProps, int fStruct, int fOldAlgo, int fVerbose)
static Abc_Obj_t * Abc_NtkPo(Abc_Ntk_t *pNtk, int i)
#define Aig_ManForEachObj(p, pObj, i)
#define Abc_NtkForEachCi(pNtk, pCi, i)
int Ssw_ManSetConstrPhases(Aig_Man_t *p, int nFrames, Vec_Int_t **pvInits)
static int Abc_NtkPoNum(Abc_Ntk_t *pNtk)
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Abc_Ntk_t * Abc_NtkInter(Abc_Ntk_t *pNtkOn, Abc_Ntk_t *pNtkOff, int fRelation, int fVerbose)
Aig_Man_t * Saig_ManWindowExtract(Aig_Man_t *p, Aig_Obj_t *pObj, int nDist)
int Abc_NtkDarSeqSim(Abc_Ntk_t *pNtk, int nFrames, int nWords, int TimeOut, int fNew, int fMiter, int fVerbose, char *pFileSim)
int Ssw_SecSpecialMiter(Aig_Man_t *p0, Aig_Man_t *p1, int nFrames, int fVerbose)
static int Saig_ManPiNum(Aig_Man_t *p)
MACRO DEFINITIONS ///.
Aig_Man_t * Aig_ManDupOneOutput(Aig_Man_t *p, int iPoNum, int fAddRegs)
typedefABC_NAMESPACE_HEADER_START struct Fra_Par_t_ Fra_Par_t
INCLUDES ///.
Abc_Ntk_t * Abc_NtkConstructFromCnf(Abc_Ntk_t *pNtk, Cnf_Man_t *p, Vec_Ptr_t *vMapped)
static Hop_Obj_t * Hop_NotCond(Hop_Obj_t *p, int c)
ABC_DLL Abc_Ntk_t * Abc_NtkStartFromNoLatches(Abc_Ntk_t *pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func)
Aig_Man_t * Gia_ManToAigSkip(Gia_Man_t *p, int nOutDelta)
int Saig_ManInduction(Aig_Man_t *p, int nTimeOut, int nFramesMax, int nConfMax, int fUnique, int fUniqueAll, int fGetCex, int fVerbose, int fVeryVerbose)
ABC_DLL Abc_Obj_t * Abc_NtkCreateNodeConst0(Abc_Ntk_t *pNtk)
int Aig_ManCiCleanup(Aig_Man_t *p)
static int Abc_NtkPiNum(Abc_Ntk_t *pNtk)
ABC_DLL char * Abc_ObjName(Abc_Obj_t *pNode)
DECLARATIONS ///.
void Aig_MmFlexStop(Aig_MmFlex_t *p, int fVerbose)
static int Gia_ObjIsAnd(Gia_Obj_t *pObj)
Abc_Ntk_t * Abc_NtkDarUnfold(Abc_Ntk_t *pNtk, int nFrames, int nConfs, int nProps, int fStruct, int fOldAlgo, int fVerbose)
typedefABC_NAMESPACE_HEADER_START struct Dar_RwrPar_t_ Dar_RwrPar_t
INCLUDES ///.
#define Abc_NtkForEachLatchInput(pNtk, pObj, i)
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
void Aig_ManComputeSccs(Aig_Man_t *p)
static Abc_Obj_t * Abc_NtkCreateNode(Abc_Ntk_t *pNtk)
int Abc_NtkDarCec(Abc_Ntk_t *pNtk1, Abc_Ntk_t *pNtk2, int nConfLimit, int fPartition, int fVerbose)
Aig_Man_t * Aig_ManFraigPartitioned(Aig_Man_t *pAig, int nPartSize, int nConfMax, int nLevelMax, int fVerbose)
int Abc_NtkDarBmc3(Abc_Ntk_t *pNtk, Saig_ParBmc_t *pPars, int fOrDecomp)
void Gia_ManSimSetDefaultParams(Gia_ParSim_t *p)
static int Abc_Lit2Var(int Lit)
Aig_Man_t * Fra_FraigPerform(Aig_Man_t *pManAig, Fra_Par_t *pPars)
static int Gia_ObjFaninId0p(Gia_Man_t *p, Gia_Obj_t *pObj)
Abc_Ntk_t * Abc_NtkDRewrite(Abc_Ntk_t *pNtk, Dar_RwrPar_t *pPars)
void Cnf_DataFree(Cnf_Dat_t *p)
static void Abc_ObjXorFaninC(Abc_Obj_t *pObj, int i)
static Gia_Obj_t * Gia_ObjFanin1(Gia_Obj_t *pObj)
Mio_Cell_t * Mio_CollectRootsNewDefault(int nInputs, int *pnGates, int fVerbose)
int Fra_FraigCec(Aig_Man_t **ppAig, int nConfLimit, int fVerbose)
static int Abc_ObjIsPo(Abc_Obj_t *pObj)
#define Gia_ManForEachBuf(p, pObj, i)
int Abc_NtkDarClau(Abc_Ntk_t *pNtk, int nFrames, int nPref, int nClauses, int nLutSize, int nLevels, int nCutsMax, int nBatches, int fStepUp, int fBmc, int fRefs, int fTarget, int fVerbose, int fVeryVerbose)
Abc_Ntk_t * Abc_NtkDChoice(Abc_Ntk_t *pNtk, int fBalance, int fUpdateLevel, int fConstruct, int nConfMax, int nLevelMax, int fVerbose)
#define Saig_ManForEachPo(p, pObj, i)
Aig_Man_t * Abc_NtkToDarBmc(Abc_Ntk_t *pNtk, Vec_Int_t **pvMap)
static Abc_Obj_t * Abc_ObjNotCond(Abc_Obj_t *p, int c)
Abc_Ntk_t * Abc_NtkFromDarSeq(Abc_Ntk_t *pNtkOld, Aig_Man_t *pMan)
void Saig_ManBmcMappingTest(Aig_Man_t *p)
static void Vec_PtrClear(Vec_Ptr_t *p)
Aig_Man_t * Cgt_ClockGating(Aig_Man_t *pAig, Aig_Man_t *pCare, Cgt_Par_t *pPars)
#define Aig_ManForEachLiSeq(p, pObj, i)
Abc_Ntk_t * Abc_NtkDC2(Abc_Ntk_t *pNtk, int fBalance, int fUpdateLevel, int fFanout, int fPower, int fVerbose)
ABC_DLL char * Abc_FrameReadFlag(char *pFlag)
static Abc_Obj_t * Abc_ObjNot(Abc_Obj_t *p)
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
int Abc_NtkDarAbSec(Abc_Ntk_t *pNtk1, Abc_Ntk_t *pNtk2, int nFrames, int fVerbose)
static int Gia_ObjIsLut(Gia_Man_t *p, int Id)
Aig_Man_t * Dch_ComputeChoices(Aig_Man_t *pAig, Dch_Pars_t *pPars)
void Gia_ManIncrementTravId(Gia_Man_t *p)
static Abc_Obj_t * Abc_NtkPi(Abc_Ntk_t *pNtk, int i)
static int Gia_ManHasCellMapping(Gia_Man_t *p)
#define Gia_ManForEachCell(p, i)
Aig_Man_t * Dar_ManBalance(Aig_Man_t *p, int fUpdateLevel)
#define Abc_NtkForEachPo(pNtk, pPo, i)
static Abc_Obj_t * Abc_NtkCreateBi(Abc_Ntk_t *pNtk)
static int Gia_ObjFaninC0(Gia_Obj_t *pObj)
static void Vec_IntFree(Vec_Int_t *p)
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
int Abc_NtkPhaseFrameNum(Abc_Ntk_t *pNtk)
typedefABC_NAMESPACE_HEADER_START struct Cnf_Man_t_ Cnf_Man_t
INCLUDES ///.
static int Gia_ManPiNum(Gia_Man_t *p)
Abc_Ntk_t * Abc_NtkDarCleanupAig(Abc_Ntk_t *pNtk, int fCleanupPis, int fCleanupPos, int fVerbose)
#define Aig_ManForEachPoSeq(p, pObj, i)
static int Abc_ObjIsComplement(Abc_Obj_t *p)
Aig_Man_t * Saig_ManDupUnfoldConstrsFunc(Aig_Man_t *pAig, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose)
static void Gia_ObjSetTravIdCurrentId(Gia_Man_t *p, int Id)
static int Abc_NtkObjNum(Abc_Ntk_t *pNtk)
Abc_Cex_t * Abc_CexCreate(int nRegs, int nPis, int *pArray, int iFrame, int iPo, int fSkipRegs)
ABC_DLL void Abc_NtkAddDummyPiNames(Abc_Ntk_t *pNtk)
char * Abc_UtilStrsav(char *s)
#define Gia_ManForEachPo(p, pObj, i)
Aig_Man_t * Saig_ManTimeframeSimplify(Aig_Man_t *pAig, int nFrames, int nFramesMax, int fInit, int fVerbose)
static int Gia_ObjFaninId1(Gia_Obj_t *pObj, int ObjId)
#define Gia_CellForEachFanin(p, i, iFanLit, k)
ABC_DLL void Abc_NtkOrderCisCos(Abc_Ntk_t *pNtk)
void Aig_ManCleanData(Aig_Man_t *p)
static void Abc_LatchSetInit0(Abc_Obj_t *pLatch)
static Abc_Obj_t * Abc_NtkCreatePo(Abc_Ntk_t *pNtk)
static Abc_Obj_t * Abc_ObjChild1(Abc_Obj_t *pObj)
void Abc_NtkVerifyReportErrorSeq(Abc_Ntk_t *pNtk1, Abc_Ntk_t *pNtk2, int *pModel, int nFrames)
int Ssw_SecGeneralMiter(Aig_Man_t *pMiter, Ssw_Pars_t *pPars)
int Aig_ManCleanup(Aig_Man_t *p)
typedefABC_NAMESPACE_HEADER_START struct Hop_Man_t_ Hop_Man_t
INCLUDES ///.
#define Gia_LutForEachFanin(p, i, iFan, k)
ABC_DLL int Abc_NtkAppend(Abc_Ntk_t *pNtk1, Abc_Ntk_t *pNtk2, int fAddPos)
Hop_Obj_t * Hop_IthVar(Hop_Man_t *p, int i)
FUNCTION DEFINITIONS ///.
Aig_Man_t * Saig_ManWindowInsert(Aig_Man_t *p, Aig_Obj_t *pObj, int nDist, Aig_Man_t *pWnd)
Abc_Ntk_t * Abc_NtkDarSeqSweep2(Abc_Ntk_t *pNtk, Ssw_Pars_t *pPars)
Aig_Man_t * Rtm_ManRetime(Aig_Man_t *p, int fForward, int nStepsMax, int fVerbose)
Abc_Ntk_t * Abc_NtkDRefactor(Abc_Ntk_t *pNtk, Dar_RefPar_t *pPars)
Abc_Ntk_t * Abc_NtkFromAigPhase(Aig_Man_t *pMan)
static int Gia_ManObjNum(Gia_Man_t *p)
static Abc_Obj_t * Abc_ObjFanout0(Abc_Obj_t *pObj)
int Fra_FraigSat(Aig_Man_t *pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose)
ITERATORS ///.
#define Aig_ManForEachPiSeq(p, pObj, i)
SEQUENTIAL ITERATORS ///.
Abc_Ntk_t * Abc_NtkPhaseAbstract(Abc_Ntk_t *pNtk, int nFrames, int nPref, int fIgnore, int fPrint, int fVerbose)
static int Aig_ObjCioId(Aig_Obj_t *pObj)
#define Abc_NtkForEachPi(pNtk, pPi, i)
int Ssw_RarSimulate(Aig_Man_t *pAig, Ssw_RarPars_t *pPars)
Aig_Man_t * Abc_NtkToDar(Abc_Ntk_t *pNtk, int fExors, int fRegisters)
DECLARATIONS ///.
typedefABC_NAMESPACE_HEADER_START struct Inter_ManParams_t_ Inter_ManParams_t
INCLUDES ///.
void Saig_ManBmcSupergateTest(Aig_Man_t *p)
void Fra_SmlStop(Fra_Sml_t *p)
int Aig_ManVerifyUsingBdds(Aig_Man_t *p, Saig_ParBbr_t *pPars)
int Fra_Claus(Aig_Man_t *pAig, int nFrames, int nPref, int nClausesMax, int nLutSize, int nLevels, int nCutsMax, int nBatches, int fStepUp, int fBmc, int fRefs, int fTarget, int fVerbose, int fVeryVerbose)
static void Vec_PtrFree(Vec_Ptr_t *p)
int Ssw_ManProfileConstraints(Aig_Man_t *p, int nWords, int nFrames, int fVerbose)
FUNCTION DEFINITIONS ///.
static int Gia_ObjFaninId0(Gia_Obj_t *pObj, int ObjId)
Abc_Ntk_t * Abc_NtkDarLcorr(Abc_Ntk_t *pNtk, int nFramesP, int nConfMax, int fVerbose)
void Saig_ManBmcTerSimTest(Aig_Man_t *p)
static int Gia_ManRegNum(Gia_Man_t *p)