mirror of https://github.com/YosysHQ/abc.git
Improvements to the interpolation command 'int'; change of default switch -t (forgot to add new file).
This commit is contained in:
Alan Mishchenko
parent
937979d9dd
commit
24f0da1475
|
|
@ -0,0 +1,301 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [intCheck.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Interpolation engine.]
|
||||
|
||||
Synopsis [Procedures to perform incremental inductive check.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - June 24, 2008.]
|
||||
|
||||
Revision [$Id: intCheck.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "intInt.h"
|
||||
|
||||
ABC_NAMESPACE_IMPL_START
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
// checking manager
|
||||
struct Inter_Check_t_
|
||||
{
|
||||
int nFramesK; // the number of timeframes (K=1 for simple induction)
|
||||
int nVars; // the current number of variables in the solver
|
||||
Aig_Man_t * pFrames; // unrolled timeframes
|
||||
Cnf_Dat_t * pCnf; // CNF of unrolled timeframes
|
||||
sat_solver * pSat; // SAT solver
|
||||
Vec_Int_t * vOrLits; // OR vars in each time frame (total number is the number nFrames)
|
||||
Vec_Int_t * vAndLits; // AND vars in the last timeframe (total number is the number of interpolants)
|
||||
Vec_Int_t * vAssLits; // assumptions (the union of the two)
|
||||
};
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Create timeframes of the manager for interpolation.]
|
||||
|
||||
Description [The resulting manager is combinational. The primary inputs
|
||||
corresponding to register outputs are ordered first.]
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Aig_Man_t * Inter_ManUnrollFrames( Aig_Man_t * pAig, int nFrames )
|
||||
{
|
||||
Aig_Man_t * pFrames;
|
||||
Aig_Obj_t * pObj, * pObjLi, * pObjLo;
|
||||
int i, f;
|
||||
assert( Saig_ManRegNum(pAig) > 0 );
|
||||
pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFrames );
|
||||
// map the constant node
|
||||
Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames );
|
||||
// create variables for register outputs
|
||||
Saig_ManForEachLo( pAig, pObj, i )
|
||||
pObj->pData = Aig_ObjCreatePi( pFrames );
|
||||
// add timeframes
|
||||
for ( f = 0; f < nFrames; f++ )
|
||||
{
|
||||
// create PI nodes for this frame
|
||||
Saig_ManForEachPi( pAig, pObj, i )
|
||||
pObj->pData = Aig_ObjCreatePi( pFrames );
|
||||
// add internal nodes of this frame
|
||||
Aig_ManForEachNode( pAig, pObj, i )
|
||||
pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
|
||||
// save register inputs
|
||||
Saig_ManForEachLi( pAig, pObj, i )
|
||||
pObj->pData = Aig_ObjChild0Copy(pObj);
|
||||
// transfer to register outputs
|
||||
Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
|
||||
{
|
||||
pObjLo->pData = pObjLi->pData;
|
||||
Aig_ObjCreatePo( pFrames, pObjLo->pData );
|
||||
}
|
||||
}
|
||||
Aig_ManCleanup( pFrames );
|
||||
return pFrames;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [This procedure sets default values of interpolation parameters.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Inter_Check_t * Inter_CheckStart( Aig_Man_t * pTrans, int nFramesK )
|
||||
{
|
||||
Inter_Check_t * p;
|
||||
// create solver
|
||||
p = ABC_CALLOC( Inter_Check_t, 1 );
|
||||
p->vOrLits = Vec_IntAlloc( 100 );
|
||||
p->vAndLits = Vec_IntAlloc( 100 );
|
||||
p->vAssLits = Vec_IntAlloc( 100 );
|
||||
// generate the timeframes
|
||||
p->pFrames = Inter_ManUnrollFrames( pTrans, nFramesK );
|
||||
assert( Aig_ManPiNum(p->pFrames) == nFramesK * Saig_ManPiNum(pTrans) + Saig_ManRegNum(pTrans) );
|
||||
assert( Aig_ManPoNum(p->pFrames) == nFramesK * Saig_ManRegNum(pTrans) );
|
||||
// convert to CNF
|
||||
p->pCnf = Cnf_Derive( p->pFrames, Aig_ManPoNum(p->pFrames) );
|
||||
p->pSat = (sat_solver *)Cnf_DataWriteIntoSolver( p->pCnf, 1, 0 );
|
||||
// assign parameters
|
||||
p->nFramesK = nFramesK;
|
||||
p->nVars = p->pCnf->nVars;
|
||||
return p;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [This procedure sets default values of interpolation parameters.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Inter_CheckStop( Inter_Check_t * p )
|
||||
{
|
||||
if ( p == NULL )
|
||||
return;
|
||||
Vec_IntFree( p->vOrLits );
|
||||
Vec_IntFree( p->vAndLits );
|
||||
Vec_IntFree( p->vAssLits );
|
||||
Cnf_DataFree( p->pCnf );
|
||||
Aig_ManStop( p->pFrames );
|
||||
sat_solver_delete( p->pSat );
|
||||
ABC_FREE( p );
|
||||
}
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Creates one OR-gate: A + B = C.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Inter_CheckAddOrGate( Inter_Check_t * p, int iVarA, int iVarB, int iVarC )
|
||||
{
|
||||
int RetValue, pLits[3];
|
||||
// add A => C or !A + C
|
||||
pLits[0] = toLitCond(iVarA, 1);
|
||||
pLits[1] = toLitCond(iVarC, 0);
|
||||
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
|
||||
assert( RetValue );
|
||||
// add B => C or !B + C
|
||||
pLits[0] = toLitCond(iVarB, 1);
|
||||
pLits[1] = toLitCond(iVarC, 0);
|
||||
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
|
||||
assert( RetValue );
|
||||
// add !A & !B => !C or A + B + !C
|
||||
pLits[0] = toLitCond(iVarA, 0);
|
||||
pLits[1] = toLitCond(iVarB, 0);
|
||||
pLits[2] = toLitCond(iVarC, 1);
|
||||
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
|
||||
assert( RetValue );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Creates equality: A = B.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Inter_CheckAddEqual( Inter_Check_t * p, int iVarA, int iVarB )
|
||||
{
|
||||
int RetValue, pLits[3];
|
||||
// add A => B or !A + B
|
||||
pLits[0] = toLitCond(iVarA, 1);
|
||||
pLits[1] = toLitCond(iVarB, 0);
|
||||
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
|
||||
assert( RetValue );
|
||||
// add B => A or !B + A
|
||||
pLits[0] = toLitCond(iVarB, 1);
|
||||
pLits[1] = toLitCond(iVarA, 0);
|
||||
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
|
||||
assert( RetValue );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Perform the checking.]
|
||||
|
||||
Description [Returns 1 if the check has passed.]
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnfInt )
|
||||
{
|
||||
Aig_Obj_t * pObj, * pObj2;
|
||||
int i, f, VarA, VarB, RetValue, Entry, status;
|
||||
int nRegs = Aig_ManPiNum(pCnfInt->pMan);
|
||||
assert( Aig_ManPoNum(p->pCnf->pMan) == p->nFramesK * nRegs );
|
||||
assert( Aig_ManPoNum(pCnfInt->pMan) == 1 );
|
||||
|
||||
// add clauses to the SAT solver
|
||||
Cnf_DataLift( pCnfInt, p->nVars );
|
||||
for ( f = 0; f <= p->nFramesK; f++ )
|
||||
{
|
||||
// add clauses to the solver
|
||||
for ( i = 0; i < pCnfInt->nClauses; i++ )
|
||||
{
|
||||
RetValue = sat_solver_addclause( p->pSat, pCnfInt->pClauses[i], pCnfInt->pClauses[i+1] );
|
||||
assert( RetValue );
|
||||
}
|
||||
// add equality clauses for the flop variables
|
||||
Aig_ManForEachPi( pCnfInt->pMan, pObj, i )
|
||||
{
|
||||
pObj2 = f ? Aig_ManPo(p->pFrames, i + (f-1) * nRegs) : Aig_ManPi(p->pFrames, i);
|
||||
Inter_CheckAddEqual( p, pCnfInt->pVarNums[pObj->Id], p->pCnf->pVarNums[pObj2->Id] );
|
||||
}
|
||||
// add final clauses
|
||||
if ( f < p->nFramesK )
|
||||
{
|
||||
if ( f == Vec_IntSize(p->vOrLits) ) // find time here
|
||||
{
|
||||
// add literal to this frame
|
||||
VarB = pCnfInt->pVarNums[ Aig_ManPo(pCnfInt->pMan, 0)->Id ];
|
||||
Vec_IntPush( p->vOrLits, VarB );
|
||||
}
|
||||
else
|
||||
{
|
||||
// add OR gate for this frame
|
||||
VarA = Vec_IntEntry( p->vOrLits, f );
|
||||
VarB = pCnfInt->pVarNums[ Aig_ManPo(pCnfInt->pMan, 0)->Id ];
|
||||
Inter_CheckAddOrGate( p, VarA, VarB, p->nVars + pCnfInt->nVars );
|
||||
Vec_IntWriteEntry( p->vOrLits, f, p->nVars + pCnfInt->nVars ); // using var ID!
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
// add AND gate for this frame
|
||||
VarB = pCnfInt->pVarNums[ Aig_ManPo(pCnfInt->pMan, 0)->Id ];
|
||||
Vec_IntPush( p->vAndLits, VarB );
|
||||
}
|
||||
// update variable IDs
|
||||
Cnf_DataLift( pCnfInt, pCnfInt->nVars + 1 );
|
||||
p->nVars += pCnfInt->nVars + 1;
|
||||
}
|
||||
Cnf_DataLift( pCnfInt, -p->nVars );
|
||||
assert( Vec_IntSize(p->vOrLits) == p->nFramesK );
|
||||
|
||||
// collect the assumption literals
|
||||
Vec_IntClear( p->vAssLits );
|
||||
Vec_IntForEachEntry( p->vOrLits, Entry, i )
|
||||
Vec_IntPush( p->vAssLits, toLitCond(Entry, 0) );
|
||||
Vec_IntForEachEntry( p->vAndLits, Entry, i )
|
||||
Vec_IntPush( p->vAssLits, toLitCond(Entry, 1) );
|
||||
/*
|
||||
if ( pCnfInt->nLiterals == 3635 )
|
||||
{
|
||||
int s = 0;
|
||||
}
|
||||
*/
|
||||
// call the SAT solver
|
||||
status = sat_solver_solve( p->pSat, Vec_IntArray(p->vAssLits),
|
||||
Vec_IntArray(p->vAssLits) + Vec_IntSize(p->vAssLits),
|
||||
(ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
|
||||
|
||||
return status == l_False;
|
||||
}
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
ABC_NAMESPACE_IMPL_END
|
||||
|
||||
Loading…
Reference in New Issue