From 24f2a120f2203acc8038ccce4e8dd141564a7a04 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 24 Aug 2015 21:09:50 -0700 Subject: Changes to be able to compile ABC without CUDD. --- src/proof/llb/llb2Driver.c | 222 --------------------------------------------- 1 file changed, 222 deletions(-) delete mode 100644 src/proof/llb/llb2Driver.c (limited to 'src/proof/llb/llb2Driver.c') diff --git a/src/proof/llb/llb2Driver.c b/src/proof/llb/llb2Driver.c deleted file mode 100644 index 1471f377..00000000 --- a/src/proof/llb/llb2Driver.c +++ /dev/null @@ -1,222 +0,0 @@ -/**CFile**************************************************************** - - FileName [llb2Driver.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [BDD based reachability.] - - Synopsis [Procedures working with flop drivers.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: llb2Driver.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "llbInt.h" - -ABC_NAMESPACE_IMPL_START - - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -// driver issue:arises when creating -// - driver ref-counter array -// - Ns2Glo maps -// - final partition -// - change-phase cube - -// LI variable is used when -// - driver drives more than one LI -// - driver is a PI -// - driver is a constant - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Returns the array of times each flop driver is referenced.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Llb_DriverCountRefs( Aig_Man_t * p ) -{ - Vec_Int_t * vCounts; - Aig_Obj_t * pObj; - int i; - vCounts = Vec_IntStart( Aig_ManObjNumMax(p) ); - Saig_ManForEachLi( p, pObj, i ) - Vec_IntAddToEntry( vCounts, Aig_ObjFaninId0(pObj), 1 ); - return vCounts; -} - -/**Function************************************************************* - - Synopsis [Returns array of NS variables.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Llb_DriverCollectNs( Aig_Man_t * pAig, Vec_Int_t * vDriRefs ) -{ - Vec_Int_t * vVars; - Aig_Obj_t * pObj, * pDri; - int i; - vVars = Vec_IntAlloc( Aig_ManRegNum(pAig) ); - Saig_ManForEachLi( pAig, pObj, i ) - { - pDri = Aig_ObjFanin0(pObj); - if ( Vec_IntEntry( vDriRefs, Aig_ObjId(pDri) ) != 1 || Saig_ObjIsPi(pAig, pDri) || Aig_ObjIsConst1(pDri) ) - Vec_IntPush( vVars, Aig_ObjId(pObj) ); - else - Vec_IntPush( vVars, Aig_ObjId(pDri) ); - } - return vVars; -} - -/**Function************************************************************* - - Synopsis [Returns array of CS variables.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Llb_DriverCollectCs( Aig_Man_t * pAig ) -{ - Vec_Int_t * vVars; - Aig_Obj_t * pObj; - int i; - vVars = Vec_IntAlloc( Aig_ManRegNum(pAig) ); - Saig_ManForEachLo( pAig, pObj, i ) - Vec_IntPush( vVars, Aig_ObjId(pObj) ); - return vVars; -} - -/**Function************************************************************* - - Synopsis [Create cube for phase swapping.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -DdNode * Llb_DriverPhaseCube( Aig_Man_t * pAig, Vec_Int_t * vDriRefs, DdManager * dd ) -{ - DdNode * bCube, * bVar, * bTemp; - Aig_Obj_t * pObj; - int i; - abctime TimeStop; - TimeStop = dd->TimeStop; dd->TimeStop = 0; - bCube = Cudd_ReadOne( dd ); Cudd_Ref( bCube ); - Saig_ManForEachLi( pAig, pObj, i ) - { - assert( Vec_IntEntry( vDriRefs, Aig_ObjFaninId0(pObj) ) >= 1 ); - if ( Vec_IntEntry( vDriRefs, Aig_ObjFaninId0(pObj) ) != 1 ) - continue; - if ( !Aig_ObjFaninC0(pObj) ) - continue; - bVar = Cudd_bddIthVar( dd, Aig_ObjFaninId0(pObj) ); - bCube = Cudd_bddAnd( dd, bTemp = bCube, bVar ); Cudd_Ref( bCube ); - Cudd_RecursiveDeref( dd, bTemp ); - } - Cudd_Deref( bCube ); - dd->TimeStop = TimeStop; - return bCube; -} - -/**Function************************************************************* - - Synopsis [Compute the last partition.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -DdManager * Llb_DriverLastPartition( Aig_Man_t * p, Vec_Int_t * vVarsNs, abctime TimeTarget ) -{ -// int fVerbose = 1; - DdManager * dd; - DdNode * bVar1, * bVar2, * bProd, * bRes, * bTemp; - Aig_Obj_t * pObj; - int i; - dd = Cudd_Init( Aig_ManObjNumMax(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); - Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT ); - dd->TimeStop = TimeTarget; - bRes = Cudd_ReadOne(dd); Cudd_Ref( bRes ); - - // mark the duplicated flop inputs - Aig_ManForEachObjVec( vVarsNs, p, pObj, i ) - { - if ( !Saig_ObjIsLi(p, pObj) ) - continue; - bVar1 = Cudd_bddIthVar( dd, Aig_ObjId(pObj) ); - bVar2 = Cudd_bddIthVar( dd, Aig_ObjFaninId0(pObj) ); - if ( Aig_ObjIsConst1(Aig_ObjFanin0(pObj)) ) - bVar2 = Cudd_ReadOne(dd); - bVar2 = Cudd_NotCond( bVar2, Aig_ObjFaninC0(pObj) ); - bProd = Cudd_bddXnor( dd, bVar1, bVar2 ); Cudd_Ref( bProd ); -// bRes = Cudd_bddAnd( dd, bTemp = bRes, bProd ); Cudd_Ref( bRes ); -// bRes = Extra_bddAndTime( dd, bTemp = bRes, bProd, TimeTarget ); - bRes = Cudd_bddAnd( dd, bTemp = bRes, bProd ); - if ( bRes == NULL ) - { - Cudd_RecursiveDeref( dd, bTemp ); - Cudd_RecursiveDeref( dd, bProd ); - return NULL; - } - Cudd_Ref( bRes ); - Cudd_RecursiveDeref( dd, bTemp ); - Cudd_RecursiveDeref( dd, bProd ); - } - -/* - Saig_ManForEachLi( p, pObj, i ) - printf( "%d ", Aig_ObjId(pObj) ); - printf( "\n" ); - Saig_ManForEachLi( p, pObj, i ) - printf( "%c%d ", Aig_ObjFaninC0(pObj)? '-':'+', Aig_ObjFaninId0(pObj) ); - printf( "\n" ); -*/ - Cudd_AutodynDisable( dd ); -// Cudd_RecursiveDeref( dd, bRes ); -// Extra_StopManager( dd ); - dd->bFunc = bRes; - dd->TimeStop = 0; - return dd; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - -ABC_NAMESPACE_IMPL_END - -- cgit v1.2.3