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

1014 lines
35 KiB
C
Raw Blame History

/**CFile****************************************************************
FileName [saigConstr2.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Sequential AIG package.]
Synopsis [Functional constraint detection.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: saigConstr2.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "saig.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satSolver.h"
#include "bool/kit/kit.h"
#include "misc/bar/bar.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static inline Aig_Obj_t * Aig_ObjFrames( Aig_Obj_t ** pObjMap, int nFs, Aig_Obj_t * pObj, int i ) { return pObjMap[nFs*pObj->Id + i]; }
static inline void Aig_ObjSetFrames( Aig_Obj_t ** pObjMap, int nFs, Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { pObjMap[nFs*pObj->Id + i] = pNode; }
static inline Aig_Obj_t * Aig_ObjChild0Frames( Aig_Obj_t ** pObjMap, int nFs, Aig_Obj_t * pObj, int i ) { return Aig_ObjFanin0(pObj)? Aig_NotCond(Aig_ObjFrames(pObjMap,nFs,Aig_ObjFanin0(pObj),i), Aig_ObjFaninC0(pObj)) : NULL; }
static inline Aig_Obj_t * Aig_ObjChild1Frames( Aig_Obj_t ** pObjMap, int nFs, Aig_Obj_t * pObj, int i ) { return Aig_ObjFanin1(pObj)? Aig_NotCond(Aig_ObjFrames(pObjMap,nFs,Aig_ObjFanin1(pObj),i), Aig_ObjFaninC1(pObj)) : NULL; }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Returns the probability of POs being 1 under rand seq sim.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_ManProfileConstraints( Aig_Man_t * p, int nWords, int nFrames, int fVerbose )
{
Vec_Ptr_t * vInfo;
Vec_Int_t * vProbs, * vProbs2;
Aig_Obj_t * pObj, * pObjLi;
unsigned * pInfo, * pInfo0, * pInfo1, * pInfoMask, * pInfoMask2;
int i, w, f, RetValue = 1;
abctime clk = Abc_Clock();
if ( fVerbose )
printf( "Simulating %d nodes and %d flops for %d frames with %d words... ",
Aig_ManNodeNum(p), Aig_ManRegNum(p), nFrames, nWords );
Aig_ManRandom( 1 );
vInfo = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p)+2, nWords );
Vec_PtrCleanSimInfo( vInfo, 0, nWords );
vProbs = Vec_IntStart( Saig_ManPoNum(p) );
vProbs2 = Vec_IntStart( Saig_ManPoNum(p) );
// start the constant
pInfo = (unsigned *)Vec_PtrEntry( vInfo, Aig_ObjId(Aig_ManConst1(p)) );
for ( w = 0; w < nWords; w++ )
pInfo[w] = ~0;
// start the flop inputs
Saig_ManForEachLi( p, pObj, i )
{
pInfo = (unsigned *)Vec_PtrEntry( vInfo, Aig_ObjId(pObj) );
for ( w = 0; w < nWords; w++ )
pInfo[w] = 0;
}
// get the info mask
pInfoMask = (unsigned *)Vec_PtrEntry( vInfo, Aig_ManObjNumMax(p) ); // PO failed
pInfoMask2 = (unsigned *)Vec_PtrEntry( vInfo, Aig_ManObjNumMax(p)+1 ); // constr failed
for ( f = 0; f < nFrames; f++ )
{
// assign primary inputs
Saig_ManForEachPi( p, pObj, i )
{
pInfo = (unsigned *)Vec_PtrEntry( vInfo, Aig_ObjId(pObj) );
for ( w = 0; w < nWords; w++ )
pInfo[w] = Aig_ManRandom( 0 );
}
// move the flop values
Saig_ManForEachLiLo( p, pObjLi, pObj, i )
{
pInfo = (unsigned *)Vec_PtrEntry( vInfo, Aig_ObjId(pObj) );
pInfo0 = (unsigned *)Vec_PtrEntry( vInfo, Aig_ObjId(pObjLi) );
for ( w = 0; w < nWords; w++ )
pInfo[w] = pInfo0[w];
}
// simulate the nodes
Aig_ManForEachNode( p, pObj, i )
{
pInfo = (unsigned *)Vec_PtrEntry( vInfo, Aig_ObjId(pObj) );
pInfo0 = (unsigned *)Vec_PtrEntry( vInfo, Aig_ObjFaninId0(pObj) );
pInfo1 = (unsigned *)Vec_PtrEntry( vInfo, Aig_ObjFaninId1(pObj) );
if ( Aig_ObjFaninC0(pObj) )
{
if ( Aig_ObjFaninC1(pObj) )
for ( w = 0; w < nWords; w++ )
pInfo[w] = ~(pInfo0[w] | pInfo1[w]);
else
for ( w = 0; w < nWords; w++ )
pInfo[w] = ~pInfo0[w] & pInfo1[w];
}
else
{
if ( Aig_ObjFaninC1(pObj) )
for ( w = 0; w < nWords; w++ )
pInfo[w] = pInfo0[w] & ~pInfo1[w];
else
for ( w = 0; w < nWords; w++ )
pInfo[w] = pInfo0[w] & pInfo1[w];
}
}
// clean the mask
for ( w = 0; w < nWords; w++ )
pInfoMask[w] = pInfoMask2[w] = 0;
// simulate the primary outputs
Aig_ManForEachCo( p, pObj, i )
{
pInfo = (unsigned *)Vec_PtrEntry( vInfo, Aig_ObjId(pObj) );
pInfo0 = (unsigned *)Vec_PtrEntry( vInfo, Aig_ObjFaninId0(pObj) );
if ( i < Saig_ManPoNum(p)-Saig_ManConstrNum(p) || i >= Saig_ManPoNum(p) )
{
if ( Aig_ObjFaninC0(pObj) )
{
for ( w = 0; w < nWords; w++ )
pInfo[w] = ~pInfo0[w];
}
else
{
for ( w = 0; w < nWords; w++ )
pInfo[w] = pInfo0[w];
}
}
else
{
if ( Aig_ObjFaninC0(pObj) )
{
for ( w = 0; w < nWords; w++ )
pInfo[w] |= ~pInfo0[w];
}
else
{
for ( w = 0; w < nWords; w++ )
pInfo[w] |= pInfo0[w];
}
}
// collect patterns when one of the outputs fails
if ( i < Saig_ManPoNum(p)-Saig_ManConstrNum(p) )
{
for ( w = 0; w < nWords; w++ )
pInfoMask[w] |= pInfo[w];
}
else if ( i < Saig_ManPoNum(p) )
{
for ( w = 0; w < nWords; w++ )
pInfoMask2[w] |= pInfo[w];
}
}
// compare the PO values (mask=1 => out=0) or UNSAT(mask=1 & out=1)
Saig_ManForEachPo( p, pObj, i )
{
pInfo = (unsigned *)Vec_PtrEntry( vInfo, Aig_ObjId(pObj) );
for ( w = 0; w < nWords; w++ )
Vec_IntAddToEntry( vProbs, i, Aig_WordCountOnes(pInfo[w]) );
if ( i < Saig_ManPoNum(p)-Saig_ManConstrNum(p) )
{
// chek the output
for ( w = 0; w < nWords; w++ )
if ( pInfo[w] & ~pInfoMask2[w] )
break;
if ( w == nWords )
continue;
printf( "Primary output %d fails on some input patterns.\n", i );
}
else
{
// collect patterns that block the POs
for ( w = 0; w < nWords; w++ )
Vec_IntAddToEntry( vProbs2, i, Aig_WordCountOnes(pInfo[w] & pInfoMask[w]) );
}
}
}
if ( fVerbose )
Abc_PrintTime( 1, "T", Abc_Clock() - clk );
// print the state
if ( fVerbose )
{
Saig_ManForEachPo( p, pObj, i )
{
if ( i < Saig_ManPoNum(p) - Saig_ManConstrNum(p) )
printf( "Primary output : " );
else
printf( "Constraint %3d : ", i-(Saig_ManPoNum(p) - Saig_ManConstrNum(p)) );
printf( "ProbOne = %f ", (float)Vec_IntEntry(vProbs, i)/(32*nWords*nFrames) );
printf( "ProbOneC = %f ", (float)Vec_IntEntry(vProbs2, i)/(32*nWords*nFrames) );
printf( "AllZeroValue = %d ", Aig_ObjPhase(pObj) );
printf( "\n" );
}
}
// print the states
Vec_PtrFree( vInfo );
Vec_IntFree( vProbs );
Vec_IntFree( vProbs2 );
return RetValue;
}
/**Function*************************************************************
Synopsis [Creates COI of the property output.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Saig_ManCreateIndMiter( Aig_Man_t * pAig, Vec_Vec_t * vCands )
{
int nFrames = 2;
Vec_Ptr_t * vNodes;
Aig_Man_t * pFrames;
Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew;
Aig_Obj_t ** pObjMap;
int i, f, k;
// create mapping for the frames nodes
pObjMap = ABC_CALLOC( Aig_Obj_t *, nFrames * Aig_ManObjNumMax(pAig) );
// start the fraig package
pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) * nFrames );
pFrames->pName = Abc_UtilStrsav( pAig->pName );
pFrames->pSpec = Abc_UtilStrsav( pAig->pSpec );
// map constant nodes
for ( f = 0; f < nFrames; f++ )
Aig_ObjSetFrames( pObjMap, nFrames, Aig_ManConst1(pAig), f, Aig_ManConst1(pFrames) );
// create PI nodes for the frames
for ( f = 0; f < nFrames; f++ )
Aig_ManForEachPiSeq( pAig, pObj, i )
Aig_ObjSetFrames( pObjMap, nFrames, pObj, f, Aig_ObjCreateCi(pFrames) );
// set initial state for the latches
Aig_ManForEachLoSeq( pAig, pObj, i )
Aig_ObjSetFrames( pObjMap, nFrames, pObj, 0, Aig_ObjCreateCi(pFrames) );
// add timeframes
for ( f = 0; f < nFrames; f++ )
{
// add internal nodes of this frame
Aig_ManForEachNode( pAig, pObj, i )
{
pObjNew = Aig_And( pFrames, Aig_ObjChild0Frames(pObjMap,nFrames,pObj,f), Aig_ObjChild1Frames(pObjMap,nFrames,pObj,f) );
Aig_ObjSetFrames( pObjMap, nFrames, pObj, f, pObjNew );
}
// set the latch inputs and copy them into the latch outputs of the next frame
Aig_ManForEachLiLoSeq( pAig, pObjLi, pObjLo, i )
{
pObjNew = Aig_ObjChild0Frames(pObjMap,nFrames,pObjLi,f);
if ( f < nFrames - 1 )
Aig_ObjSetFrames( pObjMap, nFrames, pObjLo, f+1, pObjNew );
}
}
// go through the candidates
Vec_VecForEachLevel( vCands, vNodes, i )
{
Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, k )
{
Aig_Obj_t * pObjR = Aig_Regular(pObj);
Aig_Obj_t * pNode0 = pObjMap[nFrames*Aig_ObjId(pObjR)+0];
Aig_Obj_t * pNode1 = pObjMap[nFrames*Aig_ObjId(pObjR)+1];
Aig_Obj_t * pFan0 = Aig_NotCond( pNode0, Aig_IsComplement(pObj) );
Aig_Obj_t * pFan1 = Aig_NotCond( pNode1, !Aig_IsComplement(pObj) );
Aig_Obj_t * pMiter = Aig_And( pFrames, pFan0, pFan1 );
Aig_ObjCreateCo( pFrames, pMiter );
}
}
Aig_ManCleanup( pFrames );
ABC_FREE( pObjMap );
//Aig_ManShow( pAig, 0, NULL );
//Aig_ManShow( pFrames, 0, NULL );
return pFrames;
}
/**Function*************************************************************
Synopsis [Performs inductive check for one of the constraints.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Saig_ManFilterUsingIndOne_new( Aig_Man_t * p, Aig_Man_t * pFrame, sat_solver * pSat, Cnf_Dat_t * pCnf, int nConfs, int nProps, int Counter )
{
Aig_Obj_t * pObj;
int Lit, status;
pObj = Aig_ManCo( pFrame, Counter );
Lit = toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], 0 );
status = sat_solver_solve( pSat, &Lit, &Lit + 1, (ABC_INT64_T)nConfs, 0, 0, 0 );
if ( status == l_False )
return 1;
if ( status == l_Undef )
{
// printf( "Solver returned undecided.\n" );
return 0;
}
assert( status == l_True );
return 0;
}
/**Function*************************************************************
Synopsis [Detects constraints functionally.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Saig_ManFilterUsingInd( Aig_Man_t * p, Vec_Vec_t * vCands, int nConfs, int nProps, int fVerbose )
{
Vec_Ptr_t * vNodes;
Aig_Man_t * pFrames;
sat_solver * pSat;
Cnf_Dat_t * pCnf;
Aig_Obj_t * pObj;
int i, k, k2, Counter;
/*
Vec_VecForEachLevel( vCands, vNodes, i )
Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, k )
printf( "%d ", Aig_ObjId(Aig_Regular(pObj)) );
printf( "\n" );
*/
// create timeframes
// pFrames = Saig_ManUnrollInd( p );
pFrames = Saig_ManCreateIndMiter( p, vCands );
assert( Aig_ManCoNum(pFrames) == Vec_VecSizeSize(vCands) );
// start the SAT solver
pCnf = Cnf_DeriveSimple( pFrames, Aig_ManCoNum(pFrames) );
pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
// check candidates
if ( fVerbose )
printf( "Filtered cands: " );
Counter = 0;
Vec_VecForEachLevel( vCands, vNodes, i )
{
k2 = 0;
Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, k )
{
if ( Saig_ManFilterUsingIndOne_new( p, pFrames, pSat, pCnf, nConfs, nProps, Counter++ ) )
// if ( Saig_ManFilterUsingIndOne_old( p, pSat, pCnf, nConfs, pObj ) )
{
Vec_PtrWriteEntry( vNodes, k2++, pObj );
if ( fVerbose )
printf( "%d:%s%d ", i, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
}
}
Vec_PtrShrink( vNodes, k2 );
}
if ( fVerbose )
printf( "\n" );
// clean up
Cnf_DataFree( pCnf );
sat_solver_delete( pSat );
if ( fVerbose )
Aig_ManPrintStats( pFrames );
Aig_ManStop( pFrames );
}
/**Function*************************************************************
Synopsis [Creates COI of the property output.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Saig_ManUnrollCOI_( Aig_Man_t * p, int nFrames )
{
Aig_Man_t * pFrames;
Aig_Obj_t ** pObjMap;
int i;
//Aig_Man_t * Aig_ManFrames( Aig_Man_t * pAig, int nFrames, int fInit, int fOuts, int fRegs, int fEnlarge, Aig_Obj_t *** ppObjMap )
pFrames = Aig_ManFrames( p, nFrames, 0, 1, 1, 0, &pObjMap );
for ( i = 0; i < nFrames * Aig_ManObjNumMax(p); i++ )
if ( pObjMap[i] && Aig_ObjIsNone( Aig_Regular(pObjMap[i]) ) )
pObjMap[i] = NULL;
assert( p->pObjCopies == NULL );
p->pObjCopies = pObjMap;
return pFrames;
}
/**Function*************************************************************
Synopsis [Creates COI of the property output.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Saig_ManUnrollCOI( Aig_Man_t * pAig, int nFrames )
{
Aig_Man_t * pFrames;
Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew;
Aig_Obj_t ** pObjMap;
int i, f;
// create mapping for the frames nodes
pObjMap = ABC_CALLOC( Aig_Obj_t *, nFrames * Aig_ManObjNumMax(pAig) );
// start the fraig package
pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) * nFrames );
pFrames->pName = Abc_UtilStrsav( pAig->pName );
pFrames->pSpec = Abc_UtilStrsav( pAig->pSpec );
// map constant nodes
for ( f = 0; f < nFrames; f++ )
Aig_ObjSetFrames( pObjMap, nFrames, Aig_ManConst1(pAig), f, Aig_ManConst1(pFrames) );
// create PI nodes for the frames
for ( f = 0; f < nFrames; f++ )
Aig_ManForEachPiSeq( pAig, pObj, i )
Aig_ObjSetFrames( pObjMap, nFrames, pObj, f, Aig_ObjCreateCi(pFrames) );
// set initial state for the latches
Aig_ManForEachLoSeq( pAig, pObj, i )
Aig_ObjSetFrames( pObjMap, nFrames, pObj, 0, Aig_ObjCreateCi(pFrames) );
// add timeframes
for ( f = 0; f < nFrames; f++ )
{
Aig_ManForEachNode( pAig, pObj, i )
{
pObjNew = Aig_And( pFrames, Aig_ObjChild0Frames(pObjMap,nFrames,pObj,f), Aig_ObjChild1Frames(pObjMap,nFrames,pObj,f) );
Aig_ObjSetFrames( pObjMap, nFrames, pObj, f, pObjNew );
}
// set the latch inputs and copy them into the latch outputs of the next frame
Aig_ManForEachLiLoSeq( pAig, pObjLi, pObjLo, i )
{
pObjNew = Aig_ObjChild0Frames(pObjMap,nFrames,pObjLi,f);
if ( f < nFrames - 1 )
Aig_ObjSetFrames( pObjMap, nFrames, pObjLo, f+1, pObjNew );
}
}
// create the only output
for ( f = nFrames-1; f < nFrames; f++ )
{
Aig_ManForEachPoSeq( pAig, pObj, i )
{
pObjNew = Aig_ObjCreateCo( pFrames, Aig_ObjChild0Frames(pObjMap,nFrames,pObj,f) );
Aig_ObjSetFrames( pObjMap, nFrames, pObj, f, pObjNew );
}
}
// created lots of dangling nodes - no sweeping!
//Aig_ManCleanup( pFrames );
assert( pAig->pObjCopies == NULL );
pAig->pObjCopies = pObjMap;
return pFrames;
}
/**Function*************************************************************
Synopsis [Collects and saves values of the SAT variables.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Saig_CollectSatValues( sat_solver * pSat, Cnf_Dat_t * pCnf, Vec_Ptr_t * vInfo, int * piPat )
{
Aig_Obj_t * pObj;
unsigned * pInfo;
int i;
Aig_ManForEachObj( pCnf->pMan, pObj, i )
{
if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
continue;
assert( pCnf->pVarNums[i] > 0 );
pInfo = (unsigned *)Vec_PtrEntry( vInfo, i );
if ( Abc_InfoHasBit(pInfo, *piPat) != sat_solver_var_value(pSat, pCnf->pVarNums[i]) )
Abc_InfoXorBit(pInfo, *piPat);
}
}
/**Function*************************************************************
Synopsis [Runs the SAT test for the node in one polarity.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Saig_DetectTryPolarity( sat_solver * pSat, int nConfs, int nProps, Cnf_Dat_t * pCnf, Aig_Obj_t * pObj, int iPol, Vec_Ptr_t * vInfo, int * piPat, int fVerbose )
{
Aig_Obj_t * pOut = Aig_ManCo( pCnf->pMan, 0 );
int status, Lits[2];
// ABC_INT64_T nOldConfs = pSat->stats.conflicts;
// ABC_INT64_T nOldImps = pSat->stats.propagations;
Lits[0] = toLitCond( pCnf->pVarNums[Aig_ObjId(pOut)], 0 );
Lits[1] = toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], !iPol );
status = sat_solver_solve( pSat, Lits, Lits + 2, (ABC_INT64_T)nConfs, (ABC_INT64_T)nProps, 0, 0 );
if ( status == l_False )
{
// printf( "u%d(%d) ", (int)(pSat->stats.conflicts-nOldConfs), (int)(pSat->stats.propagations-nOldImps) );
return 1;
}
if ( status == l_Undef )
{
// printf( "Solver returned undecided.\n" );
return 0;
}
// printf( "s%d(%d) ", (int)(pSat->stats.conflicts-nOldConfs), (int)(pSat->stats.propagations-nOldImps) );
assert( status == l_True );
Saig_CollectSatValues( pSat, pCnf, vInfo, piPat );
(*piPat)++;
if ( *piPat == Vec_PtrReadWordsSimInfo(vInfo) * 32 )
{
if ( fVerbose )
printf( "Warning: Reached the limit on the number of patterns.\n" );
*piPat = 0;
}
return 0;
}
/**Function*************************************************************
Synopsis [Returns the number of variables implied by the output.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Vec_t * Ssw_ManFindDirectImplications( Aig_Man_t * p, int nFrames, int nConfs, int nProps, int fVerbose )
{
Vec_Vec_t * vCands = NULL;
Vec_Ptr_t * vNodes;
Cnf_Dat_t * pCnf;
sat_solver * pSat;
Aig_Man_t * pFrames;
Aig_Obj_t * pObj, * pRepr, * pReprR;
int i, f, k, value;
vCands = Vec_VecAlloc( nFrames );
// perform unrolling
pFrames = Saig_ManUnrollCOI( p, nFrames );
assert( Aig_ManCoNum(pFrames) == 1 );
// start the SAT solver
pCnf = Cnf_DeriveSimple( pFrames, 0 );
pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
if ( pSat != NULL )
{
Aig_ManIncrementTravId( p );
for ( f = 0; f < nFrames; f++ )
{
Aig_ManForEachObj( p, pObj, i )
{
if ( !Aig_ObjIsCand(pObj) )
continue;
if ( Aig_ObjIsTravIdCurrent(p, pObj) )
continue;
// get the node from timeframes
pRepr = p->pObjCopies[nFrames*i + nFrames-1-f];
pReprR = Aig_Regular(pRepr);
if ( pCnf->pVarNums[Aig_ObjId(pReprR)] < 0 )
continue;
// value = pSat->assigns[ pCnf->pVarNums[Aig_ObjId(pReprR)] ];
value = sat_solver_get_var_value( pSat, pCnf->pVarNums[Aig_ObjId(pReprR)] );
if ( value == l_Undef )
continue;
// label this node as taken
Aig_ObjSetTravIdCurrent(p, pObj);
if ( Saig_ObjIsLo(p, pObj) )
Aig_ObjSetTravIdCurrent( p, Aig_ObjFanin0(Saig_ObjLoToLi(p, pObj)) );
// remember the node
Vec_VecPush( vCands, f, Aig_NotCond( pObj, (value == l_True) ^ Aig_IsComplement(pRepr) ) );
// printf( "%s%d ", (value == l_False)? "":"!", i );
}
}
// printf( "\n" );
sat_solver_delete( pSat );
}
Aig_ManStop( pFrames );
Cnf_DataFree( pCnf );
if ( fVerbose )
{
printf( "Found %3d candidates.\n", Vec_VecSizeSize(vCands) );
Vec_VecForEachLevel( vCands, vNodes, k )
{
printf( "Level %d. Cands =%d ", k, Vec_PtrSize(vNodes) );
// Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
// printf( "%d:%s%d ", k, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
printf( "\n" );
}
}
ABC_FREE( p->pObjCopies );
Saig_ManFilterUsingInd( p, vCands, nConfs, nProps, fVerbose );
if ( Vec_VecSizeSize(vCands) )
printf( "Found %3d constraints after filtering.\n", Vec_VecSizeSize(vCands) );
if ( fVerbose )
{
Vec_VecForEachLevel( vCands, vNodes, k )
{
printf( "Level %d. Constr =%d ", k, Vec_PtrSize(vNodes) );
// Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
// printf( "%d:%s%d ", k, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
printf( "\n" );
}
}
return vCands;
}
/**Function*************************************************************
Synopsis [Detects constraints functionally.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Vec_t * Saig_ManDetectConstrFunc( Aig_Man_t * p, int nFrames, int nConfs, int nProps, int fVerbose )
{
int iPat = 0, nWordsAlloc = 16;
Bar_Progress_t * pProgress = NULL;
Vec_Vec_t * vCands = NULL;
Vec_Ptr_t * vInfo, * vNodes;
Aig_Obj_t * pObj, * pRepr, * pObjNew;
Aig_Man_t * pFrames;
sat_solver * pSat;
Cnf_Dat_t * pCnf;
unsigned * pInfo;
int i, j, k, Lit, status, nCands = 0;
assert( Saig_ManPoNum(p) == 1 );
if ( Saig_ManPoNum(p) != 1 )
{
printf( "The number of outputs is different from 1.\n" );
return NULL;
}
//printf( "Implications = %d.\n", Ssw_ManCountImplications(p, nFrames) );
// perform unrolling
pFrames = Saig_ManUnrollCOI( p, nFrames );
assert( Aig_ManCoNum(pFrames) == 1 );
if ( fVerbose )
{
printf( "Detecting constraints with %d frames, %d conflicts, and %d propagations.\n", nFrames, nConfs, nProps );
printf( "Frames: " );
Aig_ManPrintStats( pFrames );
}
// Aig_ManShow( pFrames, 0, NULL );
// start the SAT solver
pCnf = Cnf_DeriveSimple( pFrames, Aig_ManCoNum(pFrames) );
pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
//printf( "Implications = %d.\n", pSat->qhead );
// solve the original problem
Lit = toLitCond( pCnf->pVarNums[Aig_ObjId(Aig_ManCo(pFrames,0))], 0 );
status = sat_solver_solve( pSat, &Lit, &Lit + 1, (ABC_INT64_T)nConfs, 0, 0, 0 );
if ( status == l_False )
{
printf( "The problem is trivially UNSAT (inductive with k=%d).\n", nFrames-1 );
Cnf_DataFree( pCnf );
sat_solver_delete( pSat );
Aig_ManStop( pFrames );
return NULL;
}
if ( status == l_Undef )
{
printf( "Solver could not solve the original problem.\n" );
Cnf_DataFree( pCnf );
sat_solver_delete( pSat );
Aig_ManStop( pFrames );
return NULL;
}
assert( status == l_True );
// create simulation info
vInfo = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(pFrames), nWordsAlloc );
Vec_PtrCleanSimInfo( vInfo, 0, nWordsAlloc );
Saig_CollectSatValues( pSat, pCnf, vInfo, &iPat );
Aig_ManForEachObj( pFrames, pObj, i )
{
pInfo = (unsigned *)Vec_PtrEntry( vInfo, i );
if ( pInfo[0] & 1 )
memset( (char*)pInfo, 0xff, 4*nWordsAlloc );
}
// Aig_ManShow( pFrames, 0, NULL );
// Aig_ManShow( p, 0, NULL );
// consider the nodes for ci=>!Out and label when it holds
pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(pFrames) );
Aig_ManCleanMarkAB( pFrames );
Aig_ManForEachObj( pFrames, pObj, i )
{
if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
continue;
Bar_ProgressUpdate( pProgress, i, NULL );
// check if the node is available in both polarities
pInfo = (unsigned *)Vec_PtrEntry( vInfo, i );
for ( k = 0; k < nWordsAlloc; k++ )
if ( pInfo[k] != ~0 )
break;
if ( k == nWordsAlloc )
{
if ( Saig_DetectTryPolarity(pSat, nConfs, nProps, pCnf, pObj, 0, vInfo, &iPat, fVerbose) ) // !pObj is a constr
{
pObj->fMarkA = 1, nCands++;
// printf( "!%d ", Aig_ObjId(pObj) );
}
continue;
}
for ( k = 0; k < nWordsAlloc; k++ )
if ( pInfo[k] != 0 )
break;
if ( k == nWordsAlloc )
{
if ( Saig_DetectTryPolarity(pSat, nConfs, nProps, pCnf, pObj, 1, vInfo, &iPat, fVerbose) ) // pObj is a constr
{
pObj->fMarkB = 1, nCands++;
// printf( "%d ", Aig_ObjId(pObj) );
}
continue;
}
}
Bar_ProgressStop( pProgress );
if ( nCands )
{
// printf( "\n" );
if ( fVerbose )
printf( "Found %3d classes of candidates.\n", nCands );
vCands = Vec_VecAlloc( nFrames );
for ( k = 0; k < nFrames; k++ )
{
Aig_ManForEachObj( p, pObj, i )
{
if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
continue;
pRepr = p->pObjCopies[nFrames*i + nFrames-1-k];
// pRepr = p->pObjCopies[nFrames*i + k];
if ( pRepr == NULL )
continue;
if ( Aig_Regular(pRepr)->fMarkA ) // !pObj is a constr
{
pObjNew = Aig_NotCond(pObj, !Aig_IsComplement(pRepr));
for ( j = 0; j < k; j++ )
if ( Vec_PtrFind( Vec_VecEntry(vCands, j), pObjNew ) >= 0 )
break;
if ( j == k )
Vec_VecPush( vCands, k, pObjNew );
// printf( "%d->!%d ", Aig_ObjId(Aig_Regular(pRepr)), Aig_ObjId(pObj) );
}
else if ( Aig_Regular(pRepr)->fMarkB ) // pObj is a constr
{
pObjNew = Aig_NotCond(pObj, Aig_IsComplement(pRepr));
for ( j = 0; j < k; j++ )
if ( Vec_PtrFind( Vec_VecEntry(vCands, j), pObjNew ) >= 0 )
break;
if ( j == k )
Vec_VecPush( vCands, k, pObjNew );
// printf( "%d->%d ", Aig_ObjId(Aig_Regular(pRepr)), Aig_ObjId(pObj) );
}
}
}
// printf( "\n" );
if ( fVerbose )
{
printf( "Found %3d candidates.\n", Vec_VecSizeSize(vCands) );
Vec_VecForEachLevel( vCands, vNodes, k )
{
printf( "Level %d. Cands =%d ", k, Vec_PtrSize(vNodes) );
// Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
// printf( "%d:%s%d ", k, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
printf( "\n" );
}
}
ABC_FREE( p->pObjCopies );
Saig_ManFilterUsingInd( p, vCands, nConfs, nProps, fVerbose );
if ( Vec_VecSizeSize(vCands) )
printf( "Found %3d constraints after filtering.\n", Vec_VecSizeSize(vCands) );
if ( fVerbose )
{
Vec_VecForEachLevel( vCands, vNodes, k )
{
printf( "Level %d. Constr =%d ", k, Vec_PtrSize(vNodes) );
// Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
// printf( "%d:%s%d ", k, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
printf( "\n" );
}
}
}
Vec_PtrFree( vInfo );
Cnf_DataFree( pCnf );
sat_solver_delete( pSat );
Aig_ManCleanMarkAB( pFrames );
Aig_ManStop( pFrames );
return vCands;
}
/**Function*************************************************************
Synopsis [Experimental procedure.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Saig_ManDetectConstrFuncTest( Aig_Man_t * p, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose )
{
Vec_Vec_t * vCands;
if ( fOldAlgo )
vCands = Saig_ManDetectConstrFunc( p, nFrames, nConfs, nProps, fVerbose );
else
vCands = Ssw_ManFindDirectImplications( p, nFrames, nConfs, nProps, fVerbose );
Vec_VecFreeP( &vCands );
}
/**Function*************************************************************
Synopsis [Duplicates the AIG while unfolding constraints.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Saig_ManDupUnfoldConstrsFunc( Aig_Man_t * pAig, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose )
{
Aig_Man_t * pNew;
Vec_Vec_t * vCands;
Vec_Ptr_t * vNodes, * vNewFlops;
Aig_Obj_t * pObj;
int i, j, k, nNewFlops;
if ( fOldAlgo )
vCands = Saig_ManDetectConstrFunc( pAig, nFrames, nConfs, nProps, fVerbose );
else
vCands = Ssw_ManFindDirectImplications( pAig, nFrames, nConfs, nProps, fVerbose );
if ( vCands == NULL || Vec_VecSizeSize(vCands) == 0 )
{
Vec_VecFreeP( &vCands );
return Aig_ManDupDfs( pAig );
}
// create new manager
pNew = Aig_ManDupWithoutPos( pAig );
pNew->nConstrs = pAig->nConstrs + Vec_VecSizeSize(vCands);
// add normal POs
Saig_ManForEachPo( pAig, pObj, i )
Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
// create constraint outputs
vNewFlops = Vec_PtrAlloc( 100 );
Vec_VecForEachLevel( vCands, vNodes, i )
{
Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, k )
{
Vec_PtrPush( vNewFlops, Aig_ObjRealCopy(pObj) );
for ( j = 0; j < i; j++ )
Vec_PtrPush( vNewFlops, Aig_ObjCreateCi(pNew) );
Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Vec_PtrPop(vNewFlops) );
}
}
// add latch outputs
Saig_ManForEachLi( pAig, pObj, i )
Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
// add new latch outputs
nNewFlops = 0;
Vec_VecForEachLevel( vCands, vNodes, i )
{
Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, k )
{
for ( j = 0; j < i; j++ )
Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Vec_PtrEntry(vNewFlops, nNewFlops++) );
}
}
assert( nNewFlops == Vec_PtrSize(vNewFlops) );
Aig_ManSetRegNum( pNew, Aig_ManRegNum(pAig) + nNewFlops );
Vec_VecFreeP( &vCands );
Vec_PtrFree( vNewFlops );
return pNew;
}
/**Function*************************************************************
Synopsis [Duplicates the AIG while unfolding constraints.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Saig_ManDupFoldConstrsFunc( Aig_Man_t * pAig, int fCompl, int fVerbose )
{
Aig_Man_t * pAigNew;
Aig_Obj_t * pMiter, * pFlopOut, * pFlopIn, * pObj;
int i;
if ( Aig_ManConstrNum(pAig) == 0 )
return Aig_ManDupDfs( pAig );
assert( Aig_ManConstrNum(pAig) < Saig_ManPoNum(pAig) );
// start the new manager
pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
pAigNew->pName = Abc_UtilStrsav( pAig->pName );
pAigNew->pSpec = Abc_UtilStrsav( pAig->pSpec );
// map the constant node
Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
// create variables for PIs
Aig_ManForEachCi( pAig, pObj, i )
pObj->pData = Aig_ObjCreateCi( pAigNew );
// add internal nodes of this frame
Aig_ManForEachNode( pAig, pObj, i )
pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
// OR the constraint outputs
pMiter = Aig_ManConst0( pAigNew );
Saig_ManForEachPo( pAig, pObj, i )
{
if ( i < Saig_ManPoNum(pAig)-Aig_ManConstrNum(pAig) )
continue;
pMiter = Aig_Or( pAigNew, pMiter, Aig_NotCond( Aig_ObjChild0Copy(pObj), fCompl ) );
}
// create additional flop
if ( Saig_ManRegNum(pAig) > 0 )
{
pFlopOut = Aig_ObjCreateCi( pAigNew );
pFlopIn = Aig_Or( pAigNew, pMiter, pFlopOut );
}
else
pFlopIn = pMiter;
// create primary output
Saig_ManForEachPo( pAig, pObj, i )
{
if ( i >= Saig_ManPoNum(pAig)-Aig_ManConstrNum(pAig) )
continue;
pMiter = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_Not(pFlopIn) );
Aig_ObjCreateCo( pAigNew, pMiter );
}
// transfer to register outputs
Saig_ManForEachLi( pAig, pObj, i )
Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
// create additional flop
if ( Saig_ManRegNum(pAig) > 0 )
{
Aig_ObjCreateCo( pAigNew, pFlopIn );
Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig)+1 );
}
// perform cleanup
Aig_ManCleanup( pAigNew );
Aig_ManSeqCleanup( pAigNew );
return pAigNew;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
#include "saigUnfold2.c"
ABC_NAMESPACE_IMPL_END
Reference in New Issue View Git Blame Copy Permalink