mirror of https://github.com/YosysHQ/abc.git
Improvements to ternary simulation.
This commit is contained in:
Alan Mishchenko
parent
6a997172df
commit
d877074d8f
|
|
@ -4659,6 +4659,10 @@ SOURCE=.\src\aig\gia\giaRex.c
|
|||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\aig\gia\giaSat3.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\aig\gia\giaSatEdge.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
|
|
|||
|
|
@ -6,4 +6,5 @@ SRC += src/proof/pdr/pdrCnf.c \
|
|||
src/proof/pdr/pdrSat.c \
|
||||
src/proof/pdr/pdrTsim.c \
|
||||
src/proof/pdr/pdrTsim2.c \
|
||||
src/proof/pdr/pdrTsim3.c \
|
||||
src/proof/pdr/pdrUtil.c
|
||||
|
|
|
|||
|
|
@ -43,7 +43,8 @@ ABC_NAMESPACE_HEADER_START
|
|||
/// BASIC TYPES ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
typedef struct Txs_Man_t_ Txs_Man_t;
|
||||
typedef struct Txs_Man_t_ Txs_Man_t;
|
||||
typedef struct Txs3_Man_t_ Txs3_Man_t;
|
||||
|
||||
typedef struct Pdr_Set_t_ Pdr_Set_t;
|
||||
struct Pdr_Set_t_
|
||||
|
|
@ -99,7 +100,7 @@ struct Pdr_Man_t_
|
|||
int nCexes;
|
||||
int nCexesTotal;
|
||||
// terminary simulation
|
||||
Txs_Man_t * pTxs;
|
||||
Txs3_Man_t * pTxs3;
|
||||
// internal use
|
||||
Vec_Int_t * vPrio; // priority flops
|
||||
Vec_Int_t * vLits; // array of literals
|
||||
|
|
@ -206,6 +207,10 @@ extern Pdr_Set_t * Pdr_ManTernarySim( Pdr_Man_t * p, int k, Pdr_Set_t * pCub
|
|||
extern Txs_Man_t * Txs_ManStart( Pdr_Man_t * pMan, Aig_Man_t * pAig, Vec_Int_t * vPrio );
|
||||
extern void Txs_ManStop( Txs_Man_t * );
|
||||
extern Pdr_Set_t * Txs_ManTernarySim( Txs_Man_t * p, int k, Pdr_Set_t * pCube );
|
||||
/*=== pdrTsim3.c ==========================================================*/
|
||||
extern Txs3_Man_t * Txs3_ManStart( Pdr_Man_t * pMan, Aig_Man_t * pAig, Vec_Int_t * vPrio );
|
||||
extern void Txs3_ManStop( Txs3_Man_t * );
|
||||
extern Pdr_Set_t * Txs3_ManTernarySim( Txs3_Man_t * p, int k, Pdr_Set_t * pCube );
|
||||
/*=== pdrUtil.c ==========================================================*/
|
||||
extern Pdr_Set_t * Pdr_SetAlloc( int nSize );
|
||||
extern Pdr_Set_t * Pdr_SetCreate( Vec_Int_t * vLits, Vec_Int_t * vPiLits );
|
||||
|
|
|
|||
|
|
@ -265,8 +265,8 @@ Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrio
|
|||
p->vPrio = vPrioInit;
|
||||
else if ( pPars->fFlopPrio )
|
||||
p->vPrio = Pdr_ManDeriveFlopPriorities2(p->pGia, 1);
|
||||
else if ( p->pPars->fNewXSim )
|
||||
p->vPrio = Vec_IntStartNatural( Aig_ManRegNum(pAig) );
|
||||
// else if ( p->pPars->fNewXSim )
|
||||
// p->vPrio = Vec_IntStartNatural( Aig_ManRegNum(pAig) );
|
||||
else
|
||||
p->vPrio = Vec_IntStart( Aig_ManRegNum(pAig) );
|
||||
p->vLits = Vec_IntAlloc( 100 ); // array of literals
|
||||
|
|
@ -281,7 +281,7 @@ Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrio
|
|||
p->vRes = Vec_IntAlloc( 100 ); // final result
|
||||
p->pCnfMan = Cnf_ManStart();
|
||||
// ternary simulation
|
||||
p->pTxs = pPars->fNewXSim ? Txs_ManStart( p, pAig, p->vPrio ) : NULL;
|
||||
p->pTxs3 = pPars->fNewXSim ? Txs3_ManStart( p, pAig, p->vPrio ) : NULL;
|
||||
// additional AIG data-members
|
||||
if ( pAig->pFanData == NULL )
|
||||
Aig_ManFanoutStart( pAig );
|
||||
|
|
@ -369,7 +369,7 @@ void Pdr_ManStop( Pdr_Man_t * p )
|
|||
Vec_IntFreeP( &p->vMapPpi2Ff );
|
||||
// terminary simulation
|
||||
if ( p->pPars->fNewXSim )
|
||||
Txs_ManStop( p->pTxs );
|
||||
Txs3_ManStop( p->pTxs3 );
|
||||
// internal use
|
||||
Vec_IntFreeP( &p->vPrio ); // priority flops
|
||||
Vec_IntFree( p->vLits ); // array of literals
|
||||
|
|
|
|||
|
|
@ -147,7 +147,7 @@ Vec_Int_t * Pdr_ManCubeToLits( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, int fCom
|
|||
int i, iVar, iVarMax = 0;
|
||||
abctime clk = Abc_Clock();
|
||||
Vec_IntClear( p->vLits );
|
||||
assert( !(fNext && fCompl) );
|
||||
// assert( !(fNext && fCompl) );
|
||||
for ( i = 0; i < pCube->nLits; i++ )
|
||||
{
|
||||
if ( pCube->Lits[i] == -1 )
|
||||
|
|
@ -362,7 +362,7 @@ int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPr
|
|||
{
|
||||
abctime clk = Abc_Clock();
|
||||
if ( p->pPars->fNewXSim )
|
||||
*ppPred = Txs_ManTernarySim( p->pTxs, k, pCube );
|
||||
*ppPred = Txs3_ManTernarySim( p->pTxs3, k, pCube );
|
||||
else
|
||||
*ppPred = Pdr_ManTernarySim( p, k, pCube );
|
||||
p->tTsim += Abc_Clock() - clk;
|
||||
|
|
|
|||
|
|
@ -0,0 +1,361 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [pdrTsim3.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Property driven reachability.]
|
||||
|
||||
Synopsis [Improved ternary simulation.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - November 20, 2010.]
|
||||
|
||||
Revision [$Id: pdrTsim3.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "pdrInt.h"
|
||||
#include "aig/gia/giaAig.h"
|
||||
|
||||
ABC_NAMESPACE_IMPL_START
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
struct Txs3_Man_t_
|
||||
{
|
||||
Gia_Man_t * pGia; // user's AIG
|
||||
Vec_Int_t * vPrio; // priority of each flop
|
||||
Vec_Int_t * vCiObjs; // cone leaves (CI obj IDs)
|
||||
Vec_Int_t * vFosPre; // cone leaves (CI obj IDs)
|
||||
Vec_Int_t * vFosAbs; // cone leaves (CI obj IDs)
|
||||
Vec_Int_t * vCoObjs; // cone roots (CO obj IDs)
|
||||
Vec_Int_t * vCiVals; // cone leaf values (0/1 CI values)
|
||||
Vec_Int_t * vCoVals; // cone root values (0/1 CO values)
|
||||
Vec_Int_t * vNodes; // cone nodes (node obj IDs)
|
||||
Vec_Int_t * vTemp; // cone nodes (node obj IDs)
|
||||
Vec_Int_t * vPiLits; // resulting array of PI literals
|
||||
Vec_Int_t * vFfLits; // resulting array of flop literals
|
||||
Pdr_Man_t * pMan; // calling manager
|
||||
int nPiLits; // the number of PI literals
|
||||
};
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Start and stop the ternary simulation engine.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Txs3_Man_t * Txs3_ManStart( Pdr_Man_t * pMan, Aig_Man_t * pAig, Vec_Int_t * vPrio )
|
||||
{
|
||||
Txs3_Man_t * p;
|
||||
// Aig_Obj_t * pObj;
|
||||
// int i;
|
||||
assert( Vec_IntSize(vPrio) == Aig_ManRegNum(pAig) );
|
||||
p = ABC_CALLOC( Txs3_Man_t, 1 );
|
||||
p->pGia = Gia_ManFromAigSimple(pAig); // user's AIG
|
||||
// Aig_ManForEachObj( pAig, pObj, i )
|
||||
// assert( i == 0 || pObj->iData == Abc_Var2Lit(i, 0) );
|
||||
p->vPrio = vPrio; // priority of each flop
|
||||
p->vCiObjs = Vec_IntAlloc( 100 ); // cone leaves (CI obj IDs)
|
||||
p->vFosPre = Vec_IntAlloc( 100 ); // present flop outputs
|
||||
p->vFosAbs = Vec_IntAlloc( 100 ); // absracted flop outputs
|
||||
p->vCoObjs = Vec_IntAlloc( 100 ); // cone roots (CO obj IDs)
|
||||
p->vCiVals = Vec_IntAlloc( 100 ); // cone leaf values (0/1 CI values)
|
||||
p->vCoVals = Vec_IntAlloc( 100 ); // cone root values (0/1 CO values)
|
||||
p->vNodes = Vec_IntAlloc( 100 ); // cone nodes (node obj IDs)
|
||||
p->vTemp = Vec_IntAlloc( 100 ); // cone nodes (node obj IDs)
|
||||
p->vPiLits = Vec_IntAlloc( 100 ); // resulting array of PI literals
|
||||
p->vFfLits = Vec_IntAlloc( 100 ); // resulting array of flop literals
|
||||
p->pMan = pMan; // calling manager
|
||||
return p;
|
||||
}
|
||||
void Txs3_ManStop( Txs3_Man_t * p )
|
||||
{
|
||||
Gia_ManStop( p->pGia );
|
||||
Vec_IntFree( p->vCiObjs );
|
||||
Vec_IntFree( p->vFosPre );
|
||||
Vec_IntFree( p->vFosAbs );
|
||||
Vec_IntFree( p->vCoObjs );
|
||||
Vec_IntFree( p->vCiVals );
|
||||
Vec_IntFree( p->vCoVals );
|
||||
Vec_IntFree( p->vNodes );
|
||||
Vec_IntFree( p->vTemp );
|
||||
Vec_IntFree( p->vPiLits );
|
||||
Vec_IntFree( p->vFfLits );
|
||||
ABC_FREE( p );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Marks the TFI cone and collects CIs and nodes.]
|
||||
|
||||
Description [For this procedure to work Value should not be ~0
|
||||
at the beginning.]
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Txs3_ManCollectCone_rec( Txs3_Man_t * p, Gia_Obj_t * pObj )
|
||||
{
|
||||
if ( !~pObj->Value )
|
||||
return;
|
||||
pObj->Value = ~0;
|
||||
if ( Gia_ObjIsCi(pObj) )
|
||||
{
|
||||
int Entry;
|
||||
if ( Gia_ObjIsPi(p->pGia, pObj) )
|
||||
{
|
||||
Vec_IntPush( p->vCiObjs, Gia_ObjId(p->pGia, pObj) );
|
||||
return;
|
||||
}
|
||||
Entry = Gia_ObjCioId(pObj) - Gia_ManPiNum(p->pGia);
|
||||
if ( Vec_IntEntry(p->vPrio, Entry) ) // present flop
|
||||
Vec_IntPush( p->vFosPre, Gia_ObjId(p->pGia, pObj) );
|
||||
else // asbstracted flop
|
||||
Vec_IntPush( p->vFosAbs, Gia_ObjId(p->pGia, pObj) );
|
||||
return;
|
||||
}
|
||||
assert( Gia_ObjIsAnd(pObj) );
|
||||
Txs3_ManCollectCone_rec( p, Gia_ObjFanin0(pObj) );
|
||||
Txs3_ManCollectCone_rec( p, Gia_ObjFanin1(pObj) );
|
||||
Vec_IntPush( p->vNodes, Gia_ObjId(p->pGia, pObj) );
|
||||
}
|
||||
void Txs3_ManCollectCone( Txs3_Man_t * p, int fVerbose )
|
||||
{
|
||||
Gia_Obj_t * pObj; int i, Entry;
|
||||
// printf( "Collecting cones for clause with %d literals.\n", Vec_IntSize(vCoObjs) );
|
||||
Vec_IntClear( p->vCiObjs );
|
||||
Vec_IntClear( p->vFosPre );
|
||||
Vec_IntClear( p->vFosAbs );
|
||||
Vec_IntClear( p->vNodes );
|
||||
Gia_ManConst0(p->pGia)->Value = ~0;
|
||||
Gia_ManForEachObjVec( p->vCoObjs, p->pGia, pObj, i )
|
||||
Txs3_ManCollectCone_rec( p, Gia_ObjFanin0(pObj) );
|
||||
if ( fVerbose )
|
||||
printf( "%d %d %d \n", Vec_IntSize(p->vCiObjs), Vec_IntSize(p->vFosPre), Vec_IntSize(p->vFosAbs) );
|
||||
p->nPiLits = Vec_IntSize(p->vCiObjs);
|
||||
// sort primary inputs
|
||||
Vec_IntSelectSort( Vec_IntArray(p->vCiObjs), Vec_IntSize(p->vCiObjs) );
|
||||
// sort and add present flop variables
|
||||
Vec_IntSelectSortReverse( Vec_IntArray(p->vFosPre), Vec_IntSize(p->vFosPre) );
|
||||
Vec_IntForEachEntry( p->vFosPre, Entry, i )
|
||||
Vec_IntPush( p->vCiObjs, Entry );
|
||||
// sort and add absent flop variables
|
||||
Vec_IntSelectSortReverse( Vec_IntArray(p->vFosAbs), Vec_IntSize(p->vFosAbs) );
|
||||
Vec_IntForEachEntry( p->vFosAbs, Entry, i )
|
||||
Vec_IntPush( p->vCiObjs, Entry );
|
||||
// cleanup
|
||||
Gia_ManForEachObjVec( p->vCiObjs, p->pGia, pObj, i )
|
||||
pObj->Value = 0;
|
||||
Gia_ManForEachObjVec( p->vNodes, p->pGia, pObj, i )
|
||||
pObj->Value = 0;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Shrinks values using ternary simulation.]
|
||||
|
||||
Description [The cube contains the set of flop index literals which,
|
||||
when converted into a clause and applied to the combinational outputs,
|
||||
led to a satisfiable SAT run in frame k (values stored in the SAT solver).
|
||||
If the cube is NULL, it is assumed that the first property output was
|
||||
asserted and failed.
|
||||
The resulting array is a set of flop index literals that asserts the COs.
|
||||
Priority contains 0 for i-th entry if the i-th FF is desirable to remove.]
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Pdr_Set_t * Txs3_ManTernarySim( Txs3_Man_t * p, int k, Pdr_Set_t * pCube )
|
||||
{
|
||||
int fTryNew = 1;
|
||||
int fUseLit = 1;
|
||||
int fVerbose = 0;
|
||||
sat_solver * pSat;
|
||||
Pdr_Set_t * pRes;
|
||||
Gia_Obj_t * pObj;
|
||||
Vec_Int_t * vVar2Ids, * vLits;
|
||||
int i, Lit, LitAux, Var, Value, RetValue, nCoreLits, * pCoreLits, nLits;
|
||||
// if ( k == 0 )
|
||||
// fVerbose = 1;
|
||||
// collect CO objects
|
||||
Vec_IntClear( p->vCoObjs );
|
||||
if ( pCube == NULL ) // the target is the property output
|
||||
{
|
||||
pObj = Gia_ManCo(p->pGia, p->pMan->iOutCur);
|
||||
Vec_IntPush( p->vCoObjs, Gia_ObjId(p->pGia, pObj) );
|
||||
}
|
||||
else // the target is the cube
|
||||
{
|
||||
int i;
|
||||
for ( i = 0; i < pCube->nLits; i++ )
|
||||
{
|
||||
if ( pCube->Lits[i] == -1 )
|
||||
continue;
|
||||
pObj = Gia_ManCo(p->pGia, Gia_ManPoNum(p->pGia) + Abc_Lit2Var(pCube->Lits[i]));
|
||||
Vec_IntPush( p->vCoObjs, Gia_ObjId(p->pGia, pObj) );
|
||||
}
|
||||
}
|
||||
if ( 0 )
|
||||
{
|
||||
Abc_Print( 1, "Trying to justify cube " );
|
||||
if ( pCube )
|
||||
Pdr_SetPrint( stdout, pCube, Gia_ManRegNum(p->pGia), NULL );
|
||||
else
|
||||
Abc_Print( 1, "<prop=fail>" );
|
||||
Abc_Print( 1, " in frame %d.\n", k );
|
||||
}
|
||||
|
||||
// collect CI objects
|
||||
Txs3_ManCollectCone( p, fVerbose );
|
||||
// collect values
|
||||
Pdr_ManCollectValues( p->pMan, k, p->vCiObjs, p->vCiVals );
|
||||
Pdr_ManCollectValues( p->pMan, k, p->vCoObjs, p->vCoVals );
|
||||
|
||||
// read solver
|
||||
pSat = Pdr_ManFetchSolver( p->pMan, k );
|
||||
LitAux = toLit( Pdr_ManFreeVar(p->pMan, k) );
|
||||
// add the clause (complemented cube) in terms of next state variables
|
||||
if ( pCube == NULL ) // the target is the property output
|
||||
{
|
||||
vLits = p->pMan->vLits;
|
||||
Lit = Abc_Var2Lit( Pdr_ObjSatVar(p->pMan, k, 2, Aig_ManCo(p->pMan->pAig, p->pMan->iOutCur)), 1 ); // neg literal (property holds)
|
||||
Vec_IntFill( vLits, 1, Lit );
|
||||
}
|
||||
else
|
||||
vLits = Pdr_ManCubeToLits( p->pMan, k, pCube, 1, 1 );
|
||||
// add activation literal
|
||||
Vec_IntPush( vLits, LitAux );
|
||||
RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
|
||||
assert( RetValue == 1 );
|
||||
sat_solver_compress( pSat );
|
||||
|
||||
// collect assumptions
|
||||
Vec_IntClear( p->vTemp );
|
||||
Vec_IntPush( p->vTemp, Abc_LitNot(LitAux) );
|
||||
// iterate through the values of the CI variables
|
||||
Vec_IntForEachEntryTwo( p->vCiObjs, p->vCiVals, Var, Value, i )
|
||||
{
|
||||
Aig_Obj_t * pObj = Aig_ManObj( p->pMan->pAig, Var );
|
||||
// iVar = Pdr_ObjSatVar( p->pMan, k, fNext ? 2 - lit_sign(pCube->Lits[i]) : 3, pObj ); assert( iVar >= 0 );
|
||||
int iVar = Pdr_ObjSatVar( p->pMan, k, 3, pObj ); assert( iVar >= 0 );
|
||||
assert( Aig_ObjIsCi(pObj) );
|
||||
Vec_IntPush( p->vTemp, Abc_Var2Lit(iVar, !Value) );
|
||||
}
|
||||
if ( fVerbose )
|
||||
{
|
||||
printf( "Clause with %d lits on lev %d\n", pCube ? pCube->nLits : 0, k );
|
||||
Vec_IntPrint( p->vTemp );
|
||||
}
|
||||
|
||||
/*
|
||||
// solve with assumptions
|
||||
//printf( "%d -> ", Vec_IntSize(p->vTemp) );
|
||||
{
|
||||
abctime clk = Abc_Clock();
|
||||
// assume all except flops
|
||||
Vec_IntForEachEntryStop( p->vTemp, Lit, i, p->nPiLits + 1 )
|
||||
if ( !sat_solver_push(pSat, Lit) )
|
||||
{
|
||||
assert( 0 );
|
||||
}
|
||||
nLits = sat_solver_minimize_assumptions( pSat, Vec_IntArray(p->vTemp) + p->nPiLits + 1, Vec_IntSize(p->vTemp) - p->nPiLits - 1, p->pMan->pPars->nConfLimit );
|
||||
Vec_IntShrink( p->vTemp, p->nPiLits + 1 + nLits );
|
||||
|
||||
p->pMan->tAbs += Abc_Clock() - clk;
|
||||
for ( i = 0; i <= p->nPiLits; i++ )
|
||||
sat_solver_pop(pSat);
|
||||
}
|
||||
//printf( "%d ", nLits );
|
||||
*/
|
||||
|
||||
|
||||
//check one last time
|
||||
RetValue = sat_solver_solve( pSat, Vec_IntArray(p->vTemp), Vec_IntLimit(p->vTemp), 0, 0, 0, 0 );
|
||||
assert( RetValue == l_False );
|
||||
|
||||
// use analyze final
|
||||
nCoreLits = sat_solver_final(pSat, &pCoreLits);
|
||||
//assert( Vec_IntSize(p->vTemp) <= nCoreLits );
|
||||
|
||||
Vec_IntClear( p->vTemp );
|
||||
for ( i = 0; i < nCoreLits; i++ )
|
||||
Vec_IntPush( p->vTemp, Abc_LitNot(pCoreLits[i]) );
|
||||
Vec_IntSelectSort( Vec_IntArray(p->vTemp), Vec_IntSize(p->vTemp) );
|
||||
|
||||
if ( fVerbose )
|
||||
Vec_IntPrint( p->vTemp );
|
||||
|
||||
// collect the resulting sets
|
||||
Vec_IntClear( p->vPiLits );
|
||||
Vec_IntClear( p->vFfLits );
|
||||
vVar2Ids = (Vec_Int_t *)Vec_PtrGetEntry( &p->pMan->vVar2Ids, k );
|
||||
Vec_IntForEachEntry( p->vTemp, Lit, i )
|
||||
{
|
||||
if ( Lit != Abc_LitNot(LitAux) )
|
||||
{
|
||||
int Id = Vec_IntEntry( vVar2Ids, Abc_Lit2Var(Lit) );
|
||||
Aig_Obj_t * pObj = Aig_ManObj( p->pMan->pAig, Id );
|
||||
assert( Aig_ObjIsCi(pObj) );
|
||||
if ( Saig_ObjIsPi(p->pMan->pAig, pObj) )
|
||||
Vec_IntPush( p->vPiLits, Abc_Var2Lit(Aig_ObjCioId(pObj), Abc_LitIsCompl(Lit)) );
|
||||
else
|
||||
Vec_IntPush( p->vFfLits, Abc_Var2Lit(Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pMan->pAig), Abc_LitIsCompl(Lit)) );
|
||||
}
|
||||
}
|
||||
assert( Vec_IntSize(p->vTemp) == Vec_IntSize(p->vPiLits) + Vec_IntSize(p->vFfLits) + 1 );
|
||||
|
||||
// move abstracted literals from flops to inputs
|
||||
if ( p->pMan->pPars->fUseAbs && p->pMan->vAbsFlops )
|
||||
{
|
||||
int i, iLit, k = 0;
|
||||
Vec_IntForEachEntry( p->vFfLits, iLit, i )
|
||||
{
|
||||
if ( Vec_IntEntry(p->pMan->vAbsFlops, Abc_Lit2Var(iLit)) ) // used flop
|
||||
Vec_IntWriteEntry( p->vFfLits, k++, iLit );
|
||||
else
|
||||
Vec_IntPush( p->vPiLits, 2*Saig_ManPiNum(p->pMan->pAig) + iLit );
|
||||
}
|
||||
Vec_IntShrink( p->vFfLits, k );
|
||||
}
|
||||
|
||||
if ( fVerbose )
|
||||
Vec_IntPrint( p->vPiLits );
|
||||
if ( fVerbose )
|
||||
Vec_IntPrint( p->vFfLits );
|
||||
if ( fVerbose )
|
||||
printf( "\n" );
|
||||
|
||||
// derive the final set
|
||||
pRes = Pdr_SetCreate( p->vFfLits, p->vPiLits );
|
||||
//ZH: Disabled assertion because this invariant doesn't hold with down
|
||||
//because of the join operation which can bring in initial states
|
||||
assert( k == 0 || !Pdr_SetIsInit(pRes, -1) );
|
||||
return pRes;
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
ABC_NAMESPACE_IMPL_END
|
||||
Loading…
Reference in New Issue