luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity
abc/src/proof/cec/cecSplit.c

417 lines
13 KiB
C
Raw Blame History

/**CFile****************************************************************
FileName [cecSplit.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Combinational equivalence checking.]
Synopsis [Cofactoring for combinational miters.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: cecSplit.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include <math.h>
#include "aig/gia/gia.h"
#include "aig/gia/giaAig.h"
//#include "bdd/cudd/cuddInt.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satSolver.h"
#include "misc/util/utilTruth.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
#if 0 // BDD code
/**Function*************************************************************
Synopsis [Permute primary inputs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
DdManager * Gia_ManBuildBdd( Gia_Man_t * p, Vec_Ptr_t ** pvNodes, int nSkip )
{
abctime clk = Abc_Clock();
DdManager * dd;
DdNode * bBdd, * bBdd0, * bBdd1;
Vec_Ptr_t * vNodes;
Gia_Obj_t * pObj;
int i;
vNodes = Vec_PtrStart( Gia_ManObjNum(p) );
dd = Cudd_Init( Gia_ManPiNum(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
// Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
bBdd = Cudd_ReadLogicZero(dd); Cudd_Ref( bBdd );
Vec_PtrWriteEntry( vNodes, 0, bBdd );
Gia_ManForEachPi( p, pObj, i )
{
bBdd = i > nSkip ? Cudd_bddIthVar(dd, i) : Cudd_ReadLogicZero(dd); Cudd_Ref( bBdd );
Vec_PtrWriteEntry( vNodes, Gia_ObjId(p, pObj), bBdd );
}
Gia_ManForEachAnd( p, pObj, i )
{
bBdd0 = Cudd_NotCond( (DdNode *)Vec_PtrEntry(vNodes, Gia_ObjFaninId0(pObj, i)), Gia_ObjFaninC0(pObj) );
bBdd1 = Cudd_NotCond( (DdNode *)Vec_PtrEntry(vNodes, Gia_ObjFaninId1(pObj, i)), Gia_ObjFaninC1(pObj) );
bBdd = Cudd_bddAnd( dd, bBdd0, bBdd1 ); Cudd_Ref( bBdd );
Vec_PtrWriteEntry( vNodes, Gia_ObjId(p, pObj), bBdd );
if ( i % 10 == 0 )
printf( "%d ", i );
// if ( i == 3000 )
// break;
}
printf( "\n" );
Gia_ManForEachPo( p, pObj, i )
{
bBdd = Cudd_NotCond( (DdNode *)Vec_PtrEntry(vNodes, Gia_ObjFaninId0(pObj, Gia_ObjId(p, pObj))), Gia_ObjFaninC0(pObj) ); Cudd_Ref( bBdd );
Vec_PtrWriteEntry( vNodes, Gia_ObjId(p, pObj), bBdd );
}
if ( bBdd == Cudd_ReadLogicZero(dd) )
printf( "Equivalent!\n" );
else
printf( "Not tquivalent!\n" );
if ( pvNodes )
*pvNodes = vNodes;
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
return dd;
}
void Gia_ManDerefBdd( DdManager * dd, Vec_Ptr_t * vNodes )
{
DdNode * bBdd;
int i;
Vec_PtrForEachEntry( DdNode *, vNodes, bBdd, i )
if ( bBdd )
Cudd_RecursiveDeref( dd, bBdd );
if ( Cudd_CheckZeroRef(dd) > 0 )
printf( "The number of referenced nodes = %d\n", Cudd_CheckZeroRef(dd) );
Cudd_PrintInfo( dd, stdout );
Cudd_Quit( dd );
}
void Gia_ManBuildBddTest( Gia_Man_t * p )
{
Vec_Ptr_t * vNodes;
DdManager * dd = Gia_ManBuildBdd( p, &vNodes, 50 );
Gia_ManDerefBdd( dd, vNodes );
}
#endif // BDD code
/**Function*************************************************************
Synopsis [Permute primary inputs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int * Gia_PermuteSpecialOrder( Gia_Man_t * p )
{
Vec_Int_t * vPerm;
Gia_Obj_t * pObj;
int i, * pOrder;
Gia_ManCreateRefs( p );
vPerm = Vec_IntAlloc( Gia_ManPiNum(p) );
Gia_ManForEachPi( p, pObj, i )
Vec_IntPush( vPerm, Gia_ObjRefNum(p, pObj) );
pOrder = Abc_QuickSortCost( Vec_IntArray(vPerm), Vec_IntSize(vPerm), 1 );
Vec_IntFree( vPerm );
return pOrder;
}
Gia_Man_t * Gia_PermuteSpecial( Gia_Man_t * p )
{
Gia_Man_t * pNew;
Vec_Int_t * vPerm;
int * pOrder = Gia_PermuteSpecialOrder( p );
vPerm = Vec_IntAllocArray( pOrder, Gia_ManPiNum(p) );
pNew = Gia_ManDupPerm( p, vPerm );
Vec_IntFree( vPerm );
return pNew;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cec_GiaSplitExplore( Gia_Man_t * p )
{
Gia_Obj_t * pObj, * pFan0, * pFan1;
int i, Counter = 0;
assert( p->pMuxes == NULL );
ABC_FREE( p->pRefs );
Gia_ManCreateRefs( p );
Gia_ManForEachAnd( p, pObj, i )
{
if ( !Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1) )
continue;
if ( Gia_ObjRefNum(p, Gia_ObjFanin0(pObj)) > 1 &&
Gia_ObjRefNum(p, Gia_ObjFanin1(pObj)) > 1 )
continue;
printf( "%5d : ", Counter++ );
printf( "%2d %2d ", Gia_ObjRefNum(p, Gia_Regular(pFan0)), Gia_ObjRefNum(p, Gia_Regular(pFan1)) );
printf( "%2d %2d \n", Gia_ObjRefNum(p, Gia_ObjFanin0(pObj)), Gia_ObjRefNum(p, Gia_ObjFanin1(pObj)) );
}
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Cnf_Dat_t * Cec_GiaDeriveGiaRemapped( Gia_Man_t * p )
{
Cnf_Dat_t * pCnf;
Aig_Man_t * pAig = Gia_ManToAigSimple( p );
pAig->nRegs = 0;
pCnf = Cnf_Derive( pAig, 0 );//Aig_ManCoNum(pAig) );
Aig_ManStop( pAig );
return pCnf;
}
static inline sat_solver * Cec_GiaDeriveSolver( Gia_Man_t * p, int nTimeOut )
{
sat_solver * pSat;
Cnf_Dat_t * pCnf;
int i;
pCnf = Cec_GiaDeriveGiaRemapped( p );
pSat = sat_solver_new();
sat_solver_setnvars( pSat, pCnf->nVars );
for ( i = 0; i < pCnf->nClauses; i++ )
if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
assert( 0 );
sat_solver_set_runtime_limit( pSat, nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 );
Cnf_DataFree( pCnf );
return pSat;
}
static inline int Cnf_GiaSolveOne( Gia_Man_t * p, int nTimeOut, int fVerbose, int * pnVars, int * pnConfs )
{
static int Counter = 0;
sat_solver * pSat = Cec_GiaDeriveSolver( p, nTimeOut );
int status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
*pnVars = sat_solver_nvars( pSat );
*pnConfs = sat_solver_nconflicts( pSat );
sat_solver_delete( pSat );
if ( status == l_Undef )
return -1;
if ( status == l_False )
return 1;
return 0;
/*
// get pattern
Vec_IntClear( vLits );
for ( i = 0; i < nFuncVars; i++ )
Vec_IntPush( vLits, Vec_IntEntry(vTests, Iter*nFuncVars + i) );
Gia_ManFaultAddOne( pM, pCnf, pSat, vLits, nFuncVars );
if ( pPars->fVerbose )
{
printf( "Iter%6d : ", Iter );
printf( "Var =%10d ", sat_solver_nvars(pSat) );
printf( "Clause =%10d ", sat_solver_nclauses(pSat) );
printf( "Conflict =%10d ", sat_solver_nconflicts(pSat) );
//Abc_PrintTime( 1, "Time", clkSat );
ABC_PRTr( "Solver time", clkSat );
}
*/
}
static inline int Cnf_GiaCheckOne( Vec_Ptr_t * vStack, Gia_Man_t * p, int nTimeOut, int fVerbose, int * pnVars, int * pnConfs )
{
int status = Cnf_GiaSolveOne( p, nTimeOut, fVerbose, pnVars, pnConfs );
if ( status == -1 )
{
Vec_PtrPush( vStack, p );
return 1;
}
Gia_ManStop( p );
if ( status == 1 )
return 1;
// satisfiable
return 0;
}
static inline void Cec_GiaSplitClean( Vec_Ptr_t * vStack )
{
Gia_Man_t * pNew;
int i;
Vec_PtrForEachEntry( Gia_Man_t *, vStack, pNew, i )
Gia_ManStop( pNew );
Vec_PtrFree( vStack );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cec_GiaSplitPrint( int nIter, int Depth, int nVars, int nConfs, int fSatUnsat, double Prog, abctime clk )
{
printf( "%6d : ", nIter );
printf( "Depth =%3d ", Depth );
printf( "SatVar =%10d ", nVars );
printf( "SatConf =%7d ", nConfs );
printf( "%s ", fSatUnsat ? "UNSAT " : "UNDECIDED" );
printf( "Progress = %.9f ", Prog );
Abc_PrintTime( 1, "Time", clk );
//ABC_PRTr( "Time", Abc_Clock()-clk );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int fVerbose )
{
abctime clk, clkTotal = Abc_Clock();
Gia_Man_t * pPart0, * pPart1, * pLast;
Gia_Obj_t * pObj;
Vec_Ptr_t * vStack;
int * pOrder, RetValue = -1;
int nSatVars, nSatConfs, fSatUnsat;
int i, nIter, iVar, Depth;
double Progress = 0;
// create local copy
p = Gia_ManDup( p );
// reorder variables
pOrder = Gia_PermuteSpecialOrder( p );
if ( fVerbose )
{
Gia_ManForEachPi( p, pObj, i )
printf( "%d ", Gia_ObjRefNum(p, pObj) );
printf( "\n" );
Gia_ManForEachPi( p, pObj, i )
printf( "%d ", Gia_ObjRefNum(p, Gia_ManPi(p, pOrder[i])) );
printf( "\n" );
}
// start cofactored variables
assert( p->vCofVars == NULL );
p->vCofVars = Vec_IntAlloc( 100 );
// start with the current problem
vStack = Vec_PtrAlloc( 1000 );
clk = Abc_Clock();
if ( !Cnf_GiaCheckOne(vStack, p, nTimeOut, fVerbose, &nSatVars, &nSatConfs) )
RetValue = 0;
else
{
if ( fVerbose )
Cec_GiaSplitPrint( 0, 0, nSatVars, nSatConfs, 0, 0, Abc_Clock() - clk );
for ( nIter = 1; Vec_PtrSize(vStack) > 0; nIter++ )
{
// get the last AIG
pLast = (Gia_Man_t *)Vec_PtrPop( vStack );
// determine cofactoring variable
Depth = Vec_IntSize(pLast->vCofVars);
iVar = pOrder[Depth];
// cofactor
pPart0 = Gia_ManDupCofactor( pLast, iVar, 0 );
// create variable
pPart0->vCofVars = Vec_IntAlloc( Vec_IntSize(pLast->vCofVars) + 1 );
Vec_IntAppend( pPart0->vCofVars, pLast->vCofVars );
Vec_IntPush( pPart0->vCofVars, Abc_Var2Lit(iVar, 1) );
// check this AIG
fSatUnsat = Vec_PtrSize(vStack);
clk = Abc_Clock();
if ( !Cnf_GiaCheckOne(vStack, pPart0, nTimeOut, fVerbose, &nSatVars, &nSatConfs) )
{
Gia_ManStop( pLast );
RetValue = 0;
break;
}
fSatUnsat = (fSatUnsat == Vec_PtrSize(vStack));
if ( fSatUnsat )
Progress += 1.0 / pow(2, Depth + 1);
if ( fVerbose )
Cec_GiaSplitPrint( nIter, Depth, nSatVars, nSatConfs, fSatUnsat, Progress, Abc_Clock() - clk );
// cofactor
pPart1 = Gia_ManDupCofactor( pLast, iVar, 1 );
// create variable
pPart1->vCofVars = Vec_IntAlloc( Vec_IntSize(pLast->vCofVars) + 1 );
Vec_IntAppend( pPart1->vCofVars, pLast->vCofVars );
Vec_IntPush( pPart1->vCofVars, Abc_Var2Lit(iVar, 0) );
Gia_ManStop( pLast );
// check this AIG
fSatUnsat = Vec_PtrSize(vStack);
clk = Abc_Clock();
if ( !Cnf_GiaCheckOne(vStack, pPart1, nTimeOut, fVerbose, &nSatVars, &nSatConfs) )
{
RetValue = 0;
break;
}
fSatUnsat = (fSatUnsat == Vec_PtrSize(vStack));
if ( fSatUnsat )
Progress += 1.0 / (Depth + 1);
if ( fVerbose )
Cec_GiaSplitPrint( nIter, Depth, nSatVars, nSatConfs, fSatUnsat, Progress, Abc_Clock() - clk );
// if ( Vec_PtrSize(vStack) > 2 )
// break;
}
if ( Vec_PtrSize(vStack) == 0 )
RetValue = 1;
}
Cec_GiaSplitClean( vStack );
if ( RetValue == 0 )
printf( "Problem is SAT " );
else if ( RetValue == 1 )
printf( "Problem is UNSAT " );
else if ( RetValue == -1 )
printf( "Problem is UNDECIDED " );
else assert( 0 );
ABC_FREE( pOrder );
Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
return RetValue;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END
Reference in New Issue View Git Blame Copy Permalink