From 6e774ef541114d1cff4926192dc5221c4f43c52e Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 23 Sep 2012 12:01:59 -0700 Subject: Cleaing AIG manager by removing pointers to HAIG. --- src/aig/saig/module.make | 1 - src/aig/saig/saigHaig.c | 733 ----------------------------------------------- 2 files changed, 734 deletions(-) delete mode 100644 src/aig/saig/saigHaig.c (limited to 'src/aig/saig') diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make index edf5798e..a3231929 100644 --- a/src/aig/saig/module.make +++ b/src/aig/saig/module.make @@ -7,7 +7,6 @@ SRC += src/aig/saig/saigBmc.c \ src/aig/saig/saigConstr2.c \ src/aig/saig/saigDual.c \ src/aig/saig/saigDup.c \ - src/aig/saig/saigHaig.c \ src/aig/saig/saigInd.c \ src/aig/saig/saigIoa.c \ src/aig/saig/saigIso.c \ diff --git a/src/aig/saig/saigHaig.c b/src/aig/saig/saigHaig.c deleted file mode 100644 index 7cb34c5d..00000000 --- a/src/aig/saig/saigHaig.c +++ /dev/null @@ -1,733 +0,0 @@ -/**CFile**************************************************************** - - FileName [saigHaig.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Sequential AIG package.] - - Synopsis [Experiments with history AIG recording.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - April 28, 2007.] - - Revision [$Id: saigHaig.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "saig.h" -#include "sat/bsat/satSolver.h" -#include "sat/cnf/cnf.h" - -ABC_NAMESPACE_IMPL_START - - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Prepares the inductive case with speculative reduction.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Aig_ManHaigSpeculate( Aig_Man_t * pFrames, Aig_Obj_t * pObj ) -{ - Aig_Obj_t * pObjNew, * pObjNew2, * pObjRepr, * pObjReprNew;//, * pMiter; - Aig_Obj_t * pPo; - // skip nodes without representative - pObjRepr = pObj->pHaig; - if ( pObjRepr == NULL ) - return; -// assert( pObjRepr->Id < pObj->Id ); - // get the new node - pObjNew = (Aig_Obj_t *)pObj->pData; - // get the new node of the representative - pObjReprNew = (Aig_Obj_t *)pObjRepr->pData; - // if this is the same node, no need to add constraints - assert( pObjNew != NULL && pObjReprNew != NULL ); - if ( Aig_Regular(pObjNew) == Aig_Regular(pObjReprNew) ) - return; - // these are different nodes - perform speculative reduction - pObjNew2 = Aig_NotCond( pObjReprNew, pObj->fPhase ^ pObjRepr->fPhase ); - // set the new node - pObj->pData = pObjNew2; - // add the constraint - if ( pObj->fMarkA ) - return; -// pMiter = Aig_Exor( pFrames, pObjNew, pObjReprNew ); -// pMiter = Aig_NotCond( pMiter, !Aig_ObjPhaseReal(pMiter) ); -// assert( Aig_ObjPhaseReal(pMiter) == 1 ); -// Aig_ObjCreateCo( pFrames, pMiter ); - if ( Aig_ObjPhaseReal(pObjNew) != Aig_ObjPhaseReal(pObjReprNew) ) - pObjReprNew = Aig_Not(pObjReprNew); - pPo = Aig_ObjCreateCo( pFrames, pObjNew ); - Aig_ObjCreateCo( pFrames, pObjReprNew ); - - // remember the node corresponding to this PO - pPo->pData = pObj; -} - -/**Function************************************************************* - - Synopsis [Prepares the inductive case with speculative reduction.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Man_t * Aig_ManHaigFrames( Aig_Man_t * pHaig, int nFrames ) -{ - Aig_Man_t * pFrames; - Aig_Obj_t * pObj, * pObjLi, * pObjLo; - int i, f, nAssumptions = 0; - assert( nFrames == 1 || nFrames == 2 ); - assert( nFrames == 1 || Saig_ManRegNum(pHaig) > 0 ); - // start AIG manager for timeframes - pFrames = Aig_ManStart( Aig_ManNodeNum(pHaig) * nFrames ); - pFrames->pName = Abc_UtilStrsav( pHaig->pName ); - pFrames->pSpec = Abc_UtilStrsav( pHaig->pSpec ); - // map the constant node - Aig_ManConst1(pHaig)->pData = Aig_ManConst1( pFrames ); - // create variables for register outputs - Saig_ManForEachLo( pHaig, pObj, i ) - pObj->pData = Aig_ObjCreateCi( pFrames ); - // add timeframes - Aig_ManSetCioIds( pHaig ); - for ( f = 0; f < nFrames; f++ ) - { - // create primary inputs - Saig_ManForEachPi( pHaig, pObj, i ) - pObj->pData = Aig_ObjCreateCi( pFrames ); - // create internal nodes - Aig_ManForEachNode( pHaig, pObj, i ) - { - pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); - Aig_ManHaigSpeculate( pFrames, pObj ); - } - if ( f == nFrames - 2 ) - nAssumptions = Aig_ManCoNum(pFrames); - if ( f == nFrames - 1 ) - break; - // save register inputs - Saig_ManForEachLi( pHaig, pObj, i ) - pObj->pData = Aig_ObjChild0Copy(pObj); - // transfer to register outputs - Saig_ManForEachLiLo( pHaig, pObjLi, pObjLo, i ) - pObjLo->pData = pObjLi->pData; - } - Aig_ManCleanup( pFrames ); - pFrames->nAsserts = Aig_ManCoNum(pFrames) - nAssumptions; - Aig_ManSetRegNum( pFrames, 0 ); - return pFrames; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Aig_ManMapHaigNodes( Aig_Man_t * pHaig ) -{ - Aig_Obj_t * pObj1, * pObj2; - int Id1, Id2, i, Counter = 0; - Aig_ManForEachObj( pHaig, pObj1, i ) - pObj1->pHaig = NULL; - Vec_IntForEachEntry( pHaig->vEquPairs, Id1, i ) - { - Id2 = Vec_IntEntry( pHaig->vEquPairs, ++i ); - pObj1 = Aig_ManObj( pHaig, Id1 ); - pObj2 = Aig_ManObj( pHaig, Id2 ); - assert( pObj1 != pObj2 ); - assert( !Aig_ObjIsCi(pObj1) || !Aig_ObjIsCi(pObj2) ); - if ( Aig_ObjIsCi(pObj1) ) - { - Counter += (int)(pObj2->pHaig != NULL); - pObj2->pHaig = pObj1; - } - else if ( Aig_ObjIsCi(pObj2) ) - { - Counter += (int)(pObj1->pHaig != NULL); - pObj1->pHaig = pObj2; - } - else if ( pObj1->Id < pObj2->Id ) - { - Counter += (int)(pObj2->pHaig != NULL); - pObj2->pHaig = pObj1; - } - else - { - Counter += (int)(pObj1->pHaig != NULL); - pObj1->pHaig = pObj2; - } - } -// printf( "Overwrites %d out of %d.\n", Counter, Vec_IntSize(pHaig->vEquPairs)/2 ); - return Counter; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Aig_ManHaigVerify( Aig_Man_t * p, Aig_Man_t * pAig, Aig_Man_t * pHaig, int nFrames, clock_t clkSynth ) -{ - int nBTLimit = 0; - Aig_Man_t * pFrames, * pTemp; - Cnf_Dat_t * pCnf; - sat_solver * pSat; - Aig_Obj_t * pObj1, * pObj2; - int i, RetValue1, RetValue2, Counter, Lits[2], nOvers; - clock_t clk = clock(), clkVerif; - - nOvers = Aig_ManMapHaigNodes( pHaig ); - - // create time frames with speculative reduction and convert them into CNF -clk = clock(); - pFrames = Aig_ManHaigFrames( pHaig, nFrames ); - Aig_ManCleanMarkA( pHaig ); - - printf( "Frames: " ); - Aig_ManPrintStats( pFrames ); - - pFrames = Dar_ManRwsat( pTemp = pFrames, 1, 0 ); - Aig_ManStop( pTemp ); - - printf( "Frames synt:" ); - Aig_ManPrintStats( pFrames ); - - printf( "Additional frames stats: Assumptions = %d. Assertions = %d. Pairs = %d. Over = %d.\n", - Aig_ManCoNum(pFrames)/2 - pFrames->nAsserts/2, pFrames->nAsserts/2, Vec_IntSize(pHaig->vEquPairs)/2, nOvers ); -// pCnf = Cnf_DeriveSimple( pFrames, Aig_ManCoNum(pFrames) ); - pCnf = Cnf_Derive( pFrames, Aig_ManCoNum(pFrames) ); - - - -// pCnf = Cnf_Derive( pFrames, Aig_ManCoNum(pFrames) - pFrames->nAsserts ); -//Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 ); -// Saig_ManDumpBlif( pHaig, "haig_temp.blif" ); -// Saig_ManDumpBlif( pFrames, "haig_temp_frames.blif" ); - // create the SAT solver to be used for this problem - pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); - if ( pSat == NULL ) - { - printf( "Aig_ManHaigVerify(): Computed CNF is not valid.\n" ); - return 0; - } - - if ( nFrames == 2 ) - { - // add clauses for the first frame - Aig_ManForEachCo( pFrames, pObj1, i ) - { - if ( i >= Aig_ManCoNum(pFrames) - pFrames->nAsserts ) - break; - - pObj2 = Aig_ManCo( pFrames, ++i ); - assert( pObj1->fPhase == pObj2->fPhase ); - - Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id], 0 ); - Lits[1] = toLitCond( pCnf->pVarNums[pObj2->Id], 1 ); - if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) ) - { - sat_solver_delete( pSat ); - return 0; - } - Lits[0]++; - Lits[1]--; - if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) ) - { - sat_solver_delete( pSat ); - return 0; - } - } - - if ( !sat_solver_simplify(pSat) ) - { - sat_solver_delete( pSat ); - return 0; - } - } -ABC_PRT( "Preparation", clock() - clk ); - - - // check in the second timeframe -clk = clock(); - Counter = 0; - printf( "Started solving ...\r" ); - Aig_ManForEachCo( pFrames, pObj1, i ) - { - if ( i < Aig_ManCoNum(pFrames) - pFrames->nAsserts ) - continue; - - pObj2 = Aig_ManCo( pFrames, ++i ); - assert( pObj1->fPhase == pObj2->fPhase ); - - Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id], 0 ); - Lits[1] = toLitCond( pCnf->pVarNums[pObj2->Id], 1 ); - - RetValue1 = sat_solver_solve( pSat, Lits, Lits + 2, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); - if ( RetValue1 == l_False ) - { - Lits[0] = lit_neg( Lits[0] ); - Lits[1] = lit_neg( Lits[1] ); -// RetValue = sat_solver_addclause( pSat, Lits, Lits + 2 ); -// assert( RetValue ); - } - - Lits[0]++; - Lits[1]--; - - RetValue2 = sat_solver_solve( pSat, Lits, Lits + 2, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); - if ( RetValue2 == l_False ) - { - Lits[0] = lit_neg( Lits[0] ); - Lits[1] = lit_neg( Lits[1] ); -// RetValue = sat_solver_addclause( pSat, Lits, Lits + 2 ); -// assert( RetValue ); - } - - if ( RetValue1 != l_False || RetValue2 != l_False ) - Counter++; - - if ( i % 50 == 1 ) - printf( "Solving assertion %6d out of %6d.\r", - (i - (Aig_ManCoNum(pFrames) - pFrames->nAsserts))/2, - pFrames->nAsserts/2 ); -// if ( nClasses == 1000 ) -// break; - } - printf( " \r" ); -ABC_PRT( "Solving ", clock() - clk ); -clkVerif = clock() - clk; - if ( Counter ) - printf( "Verification failed for %d out of %d assertions.\n", Counter, pFrames->nAsserts/2 ); - else - printf( "Verification is successful for all %d assertions.\n", pFrames->nAsserts/2 ); - - // print the statistic into a file - { - FILE * pTable; - Aig_Man_t * pTemp, * pHaig2; - - pHaig2 = pAig->pManHaig; - pAig->pManHaig = NULL; - pTemp = Aig_ManDupDfs( pAig ); - pAig->pManHaig = pHaig2; - - Aig_ManSeqCleanup( pTemp ); - - pTable = fopen( "stats.txt", "a+" ); - fprintf( pTable, "%s ", p->pName ); - fprintf( pTable, "%d ", Saig_ManPiNum(p) ); - fprintf( pTable, "%d ", Saig_ManPoNum(p) ); - - fprintf( pTable, "%d ", Saig_ManRegNum(p) ); - fprintf( pTable, "%d ", Aig_ManNodeNum(p) ); - fprintf( pTable, "%d ", Aig_ManLevelNum(p) ); - - fprintf( pTable, "%d ", Saig_ManRegNum(pTemp) ); - fprintf( pTable, "%d ", Aig_ManNodeNum(pTemp) ); - fprintf( pTable, "%d ", Aig_ManLevelNum(pTemp) ); - - fprintf( pTable, "%d ", Saig_ManRegNum(pHaig) ); - fprintf( pTable, "%d ", Aig_ManNodeNum(pHaig) ); - fprintf( pTable, "%d ", Aig_ManLevelNum(pHaig) ); - - fprintf( pTable, "%.2f", (float)(clkSynth)/(float)(CLOCKS_PER_SEC) ); - fprintf( pTable, "\n" ); - fclose( pTable ); - - - pTable = fopen( "stats2.txt", "a+" ); - fprintf( pTable, "%s ", p->pName ); - fprintf( pTable, "%d ", Aig_ManNodeNum(pFrames) ); - fprintf( pTable, "%d ", Aig_ManLevelNum(pFrames) ); - - fprintf( pTable, "%d ", pCnf->nVars ); - fprintf( pTable, "%d ", pCnf->nClauses ); - fprintf( pTable, "%d ", pCnf->nLiterals ); - - fprintf( pTable, "%d ", Aig_ManCoNum(pFrames)/2 - pFrames->nAsserts/2 ); - fprintf( pTable, "%d ", pFrames->nAsserts/2 ); - fprintf( pTable, "%d ", Vec_IntSize(pHaig->vEquPairs)/2 ); - - fprintf( pTable, "%.2f", (float)(clkVerif)/(float)(CLOCKS_PER_SEC) ); - fprintf( pTable, "\n" ); - fclose( pTable ); - - Aig_ManStop( pTemp ); - } - - // clean up - Aig_ManStop( pFrames ); - Cnf_DataFree( pCnf ); - sat_solver_delete( pSat ); - return 1; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Aig_ManHaigVerify2( Aig_Man_t * p, Aig_Man_t * pAig, Aig_Man_t * pHaig, int nFrames ) -{ - int nBTLimit = 0; - Cnf_Dat_t * pCnf; - sat_solver * pSat; - Aig_Obj_t * pObj1, * pObj2; - int i, RetValue1, RetValue2, Counter, Lits[2]; - clock_t clk = clock(); - int Delta; - int Id1, Id2; - - assert( nFrames == 1 || nFrames == 2 ); - -clk = clock(); - pCnf = Cnf_DeriveSimple( pHaig, Aig_ManCoNum(pHaig) ); -// Aig_ManForEachObj( pHaig, pObj, i ) -// printf( "%d=%d ", pObj->Id, pCnf->pVarNums[pObj->Id] ); -// printf( "\n" ); - - // create the SAT solver to be used for this problem - pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, nFrames, 0 ); -//Sat_SolverWriteDimacs( pSat, "1.cnf", NULL, NULL, 0 ); - if ( pSat == NULL ) - { - printf( "Aig_ManHaigVerify(): Computed CNF is not valid.\n" ); - return -1; - } - - if ( nFrames == 2 ) - { - Vec_IntForEachEntry( pHaig->vEquPairs, Id1, i ) - { - Id2 = Vec_IntEntry( pHaig->vEquPairs, ++i ); - pObj1 = Aig_ManObj( pHaig, Id1 ); - pObj2 = Aig_ManObj( pHaig, Id2 ); - if ( pObj1->fPhase ^ pObj2->fPhase ) - { - Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id], 0 ); - Lits[1] = toLitCond( pCnf->pVarNums[pObj2->Id], 0 ); - if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) ) - { - sat_solver_delete( pSat ); - return 0; - } - Lits[0]++; - Lits[1]++; - if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) ) - { - sat_solver_delete( pSat ); - return 0; - } - } - else - { - Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id], 0 ); - Lits[1] = toLitCond( pCnf->pVarNums[pObj2->Id], 1 ); - if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) ) - { - sat_solver_delete( pSat ); - return 0; - } - Lits[0]++; - Lits[1]--; - if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) ) - { - sat_solver_delete( pSat ); - return 0; - } - } - } - - if ( !sat_solver_simplify(pSat) ) - { - sat_solver_delete( pSat ); - return 0; - } - } -ABC_PRT( "Preparation", clock() - clk ); - - - // check in the second timeframe -clk = clock(); - Counter = 0; - Delta = (nFrames == 2)? pCnf->nVars : 0; - Vec_IntForEachEntry( pHaig->vEquPairs, Id1, i ) - { - Id2 = Vec_IntEntry( pHaig->vEquPairs, ++i ); - pObj1 = Aig_ManObj( pHaig, Id1 ); - pObj2 = Aig_ManObj( pHaig, Id2 ); - if ( pObj1->fPhase ^ pObj2->fPhase ) - { - Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id]+Delta, 0 ); - Lits[1] = toLitCond( pCnf->pVarNums[pObj2->Id]+Delta, 0 ); - - RetValue1 = sat_solver_solve( pSat, Lits, Lits + 2, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); - - Lits[0]++; - Lits[1]++; - - RetValue2 = sat_solver_solve( pSat, Lits, Lits + 2, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); - - if ( RetValue1 != l_False || RetValue2 != l_False ) - Counter++; - } - else - { - Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id]+Delta, 0 ); - Lits[1] = toLitCond( pCnf->pVarNums[pObj2->Id]+Delta, 1 ); - - RetValue1 = sat_solver_solve( pSat, Lits, Lits + 2, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); - - Lits[0]++; - Lits[1]--; - - RetValue2 = sat_solver_solve( pSat, Lits, Lits + 2, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); - - if ( RetValue1 != l_False || RetValue2 != l_False ) - Counter++; - } - if ( i % 50 == 1 ) - printf( "Solving assertion %6d out of %6d.\r", i/2, Vec_IntSize(pHaig->vEquPairs)/2 ); - -// if ( i / 2 > 1000 ) -// break; - } -ABC_PRT( "Solving ", clock() - clk ); - if ( Counter ) - printf( "Verification failed for %d out of %d classes.\n", Counter, Vec_IntSize(pHaig->vEquPairs)/2 ); - else - printf( "Verification is successful for all %d classes.\n", Vec_IntSize(pHaig->vEquPairs)/2 ); - - Cnf_DataFree( pCnf ); - sat_solver_delete( pSat ); - return 1; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Man_t * Saig_ManHaigDump( Aig_Man_t * pHaig ) -{ - Vec_Ptr_t * vTemp; - Aig_Obj_t * pObj, * pObj1, * pObj2, * pMiter; - int Id1, Id2, i; - // remove regular POs - Aig_ManSetCioIds( pHaig ); - vTemp = Vec_PtrAlloc( Saig_ManRegNum(pHaig) ); - Aig_ManForEachCo( pHaig, pObj, i ) - { - if ( Saig_ObjIsPo(pHaig, pObj) ) - { - Aig_ObjDisconnect( pHaig, pObj ); - Vec_PtrWriteEntry( pHaig->vObjs, pObj->Id, NULL ); - } - else - { - Vec_PtrPush( vTemp, pObj ); - } - } - Vec_PtrShrink( pHaig->vCos, 0 ); - pHaig->nObjs[AIG_OBJ_CO] = Vec_PtrSize( vTemp ); - // add new POs - Vec_IntForEachEntry( pHaig->vEquPairs, Id1, i ) - { - Id2 = Vec_IntEntry( pHaig->vEquPairs, ++i ); - pObj1 = Aig_ManObj( pHaig, Id1 ); - pObj2 = Aig_ManObj( pHaig, Id2 ); - assert( pObj1 != pObj2 ); - assert( !Aig_ObjIsCi(pObj1) || !Aig_ObjIsCi(pObj2) ); - pMiter = Aig_Exor( pHaig, pObj1, pObj2 ); - pMiter = Aig_NotCond( pMiter, Aig_ObjPhaseReal(pMiter) ); - assert( Aig_ObjPhaseReal(pMiter) == 0 ); - Aig_ObjCreateCo( pHaig, pMiter ); - } - printf( "Added %d property outputs.\n", Vec_IntSize(pHaig->vEquPairs)/2 ); - // add the registers - Vec_PtrForEachEntry( Aig_Obj_t *, vTemp, pObj, i ) - Vec_PtrPush( pHaig->vCos, pObj ); - Vec_PtrFree( vTemp ); - assert( pHaig->nObjs[AIG_OBJ_CO] == Vec_PtrSize(pHaig->vCos) ); - Aig_ManCleanup( pHaig ); - Aig_ManSetRegNum( pHaig, pHaig->nRegs ); -// return pHaig; - - printf( "HAIG: " ); - Aig_ManPrintStats( pHaig ); - printf( "HAIG is written into file \"haig.blif\".\n" ); - Saig_ManDumpBlif( pHaig, "haig.blif" ); - - Vec_IntFree( pHaig->vEquPairs ); - Aig_ManStop( pHaig ); - return NULL; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Man_t * Saig_ManHaigRecord( Aig_Man_t * p, int nIters, int nSteps, int fRetimingOnly, int fAddBugs, int fUseCnf, int fVerbose ) -{ - int fSeqHaig = (int)( Aig_ManRegNum(p) > 0 ); - Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr; - Aig_Man_t * pNew, * pTemp; - Aig_Obj_t * pObj; - int i, k, nStepsReal; - clock_t clk = clock(), clkSynth; - Dar_ManDefaultRwrParams( pParsRwr ); - -clk = clock(); - // duplicate this manager - pNew = Aig_ManDupSimple( p ); - // create its history AIG - pNew->pManHaig = Aig_ManDupSimple( pNew ); - Aig_ManForEachObj( pNew, pObj, i ) - pObj->pHaig = (Aig_Obj_t *)pObj->pData; - // remove structural hashing table - Aig_TableClear( pNew->pManHaig ); - pNew->pManHaig->vEquPairs = Vec_IntAlloc( 10000 ); -ABC_PRT( "HAIG setup time", clock() - clk ); - -clk = clock(); - if ( fSeqHaig ) - { - if ( fRetimingOnly ) - { - // perform retiming - nStepsReal = Saig_ManRetimeSteps( pNew, nSteps, 1, fAddBugs ); - pNew = Aig_ManDupSimpleDfs( pTemp = pNew ); - Aig_ManStop( pTemp ); - printf( "Performed %d retiming moves.\n", nStepsReal ); - } - else - { - for ( k = 0; k < nIters; k++ ) - { - // perform balancing - pNew = Dar_ManBalance( pTemp = pNew, 0 ); - Aig_ManStop( pTemp ); - - // perform rewriting - Dar_ManRewrite( pNew, pParsRwr ); - pNew = Aig_ManDupDfs( pTemp = pNew ); - Aig_ManStop( pTemp ); - - // perform retiming - nStepsReal = Saig_ManRetimeSteps( pNew, nSteps, 1, fAddBugs ); - pNew = Aig_ManDupSimpleDfs( pTemp = pNew ); - Aig_ManStop( pTemp ); - printf( "Performed %d retiming moves.\n", nStepsReal ); - } - } - } - else - { - for ( k = 0; k < nIters; k++ ) - { - // perform balancing - pNew = Dar_ManBalance( pTemp = pNew, 0 ); - Aig_ManStop( pTemp ); - - // perform rewriting - Dar_ManRewrite( pNew, pParsRwr ); - pNew = Aig_ManDupDfs( pTemp = pNew ); - Aig_ManStop( pTemp ); - } - } -ABC_PRT( "Synthesis time ", clock() - clk ); -clkSynth = clock() - clk; - - // use the haig for verification -// Aig_ManAntiCleanup( pNew->pManHaig ); - Aig_ManSetRegNum( pNew->pManHaig, pNew->pManHaig->nRegs ); -//Aig_ManShow( pNew->pManHaig, 0, NULL ); - - printf( "AIG before: " ); - Aig_ManPrintStats( p ); - printf( "AIG after: " ); - Aig_ManPrintStats( pNew ); - printf( "HAIG: " ); - Aig_ManPrintStats( pNew->pManHaig ); - - if ( fUseCnf ) - { - if ( !Aig_ManHaigVerify2( p, pNew, pNew->pManHaig, 1+fSeqHaig ) ) - printf( "Constructing SAT solver has failed.\n" ); - } - else - { - if ( !Aig_ManHaigVerify( p, pNew, pNew->pManHaig, 1+fSeqHaig, clkSynth ) ) - printf( "Constructing SAT solver has failed.\n" ); - } - - Saig_ManHaigDump( pNew->pManHaig ); - pNew->pManHaig = NULL; - return pNew; -/* - // cleanup - Vec_IntFree( pNew->pManHaig->vEquPairs ); - Aig_ManStop( pNew->pManHaig ); - pNew->pManHaig = NULL; - return pNew; -*/ -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - -ABC_NAMESPACE_IMPL_END - -- cgit v1.2.3