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

Version abc71130

This commit is contained in:
Alan Mishchenko 2007-11-30 08:01:00 -08:00
parent 765a212408
commit 369f008e69
24 changed files with 1885 additions and 31 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
abc.dsp
View File

@ -2622,6 +2622,10 @@ SOURCE=.\src\aig\fra\fraClass.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\fra\fraClau.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\fra\fraCnf.c
# End Source File
# Begin Source File
@ -2830,6 +2834,14 @@ SOURCE=.\src\aig\aig\aigFanout.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\aig\aigFrames.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\aig\aigHaig.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\aig\aigMan.c
# End Source File
# Begin Source File
@ -2866,6 +2878,10 @@ SOURCE=.\src\aig\aig\aigRet.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\aig\aigRetF.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\aig\aigScl.c
# End Source File
# Begin Source File

4
abc.rc
View File

@ -52,6 +52,7 @@ alias rh read_hie
alias rl read_blif
alias rb read_bench
alias ret retime
alias dret dretime
alias rp read_pla
alias rt read_truth
alias rv read_verilog
@ -121,4 +122,7 @@ alias trec "rec_start; r c.blif; st; rec_add; rec_use"
alias trec4 "rec_start -K 4; r i10.blif; st; rec_add; rec_use"
alias bmc2 "frames -i -F 10; orpos; iprove"
alias t0 "r test/mc1.blif; st; test"
alias t1 "r s27mc2.blif; st; test"
alias t2 "r i/intel_001.aig; ps; test"

14
src/aig/aig/aig.h
View File

@ -71,6 +71,7 @@ struct Aig_Obj_t_ // 8 words
Aig_Obj_t * pNext; // strashing table
Aig_Obj_t * pFanin0; // fanin
Aig_Obj_t * pFanin1; // fanin
Aig_Obj_t * pHaig; // pointer to the HAIG node
unsigned int Type : 3; // object type
unsigned int fPhase : 1; // value under 000...0 pattern
unsigned int fMarkA : 1; // multipurpose mask
@ -140,6 +141,7 @@ struct Aig_Man_t_
Vec_Ptr_t * vMapped;
Vec_Int_t * vFlopNums;
void * pSeqModel;
Aig_Man_t * pManHaig;
// timing statistics
int time1;
int time2;
@ -251,11 +253,14 @@ static inline Aig_Obj_t * Aig_ObjChild0( Aig_Obj_t * pObj ) { return pObj-
static inline Aig_Obj_t * Aig_ObjChild1( Aig_Obj_t * pObj ) { return pObj->pFanin1; }
static inline Aig_Obj_t * Aig_ObjChild0Copy( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj)) : NULL; }
static inline Aig_Obj_t * Aig_ObjChild1Copy( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj)) : NULL; }
static inline void Aig_ObjChild0Flip( Aig_Obj_t * pObj ) { pObj->pFanin0 = Aig_Not(pObj->pFanin0); }
static inline void Aig_ObjChild1Flip( Aig_Obj_t * pObj ) { pObj->pFanin1 = Aig_Not(pObj->pFanin1); }
static inline int Aig_ObjLevel( Aig_Obj_t * pObj ) { return pObj->Level; }
static inline int Aig_ObjLevelNew( Aig_Obj_t * pObj ) { return Aig_ObjFanin1(pObj)? 1 + Aig_ObjIsExor(pObj) + AIG_MAX(Aig_ObjFanin0(pObj)->Level, Aig_ObjFanin1(pObj)->Level) : Aig_ObjFanin0(pObj)->Level; }
static inline void Aig_ObjClean( Aig_Obj_t * pObj ) { memset( pObj, 0, sizeof(Aig_Obj_t) ); }
static inline Aig_Obj_t * Aig_ObjFanout0( Aig_Man_t * p, Aig_Obj_t * pObj ) { assert(p->pFanData && pObj->Id < p->nFansAlloc); return Aig_ManObj(p, p->pFanData[5*pObj->Id] >> 1); }
static inline Aig_Obj_t * Aig_ObjEquiv( Aig_Man_t * p, Aig_Obj_t * pObj ) { return p->pEquivs? p->pEquivs[pObj->Id] : NULL; }
static inline Aig_Obj_t * Aig_ObjEquiv( Aig_Man_t * p, Aig_Obj_t * pObj ) { return p->pEquivs? p->pEquivs[pObj->Id] : NULL; }
static inline Aig_Obj_t * Aig_ObjHaig( Aig_Obj_t * pObj ) { assert( Aig_Regular(pObj)->pHaig ); return Aig_NotCond( Aig_Regular(pObj)->pHaig, Aig_IsComplement(pObj) ); }
static inline int Aig_ObjWhatFanin( Aig_Obj_t * pObj, Aig_Obj_t * pFanin )
{
if ( Aig_ObjFanin0(pObj) == pFanin ) return 0;
@ -398,6 +403,10 @@ extern void Aig_ObjAddFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Ob
extern void Aig_ObjRemoveFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout );
extern void Aig_ManFanoutStart( Aig_Man_t * p );
extern void Aig_ManFanoutStop( Aig_Man_t * p );
/*=== aigFrames.c ==========================================================*/
extern Aig_Man_t * Aig_ManFrames( Aig_Man_t * pAig, int nFs, int fInit, int fOuts, int fRegs, Aig_Obj_t *** ppObjMap );
/*=== aigHaig.c ==========================================================*/
extern void Aig_ManHaigRecord( Aig_Man_t * p );
/*=== aigMan.c ==========================================================*/
extern Aig_Man_t * Aig_ManStart( int nNodesMax );
extern Aig_Man_t * Aig_ManStartFrom( Aig_Man_t * p );
@ -463,6 +472,8 @@ extern Aig_Man_t * Aig_ManRehash( Aig_Man_t * p );
extern void Aig_ManMarkValidChoices( Aig_Man_t * p );
/*=== aigRet.c ========================================================*/
extern Aig_Man_t * Rtm_ManRetime( Aig_Man_t * p, int fForward, int nStepsMax, int fVerbose );
/*=== aigRetF.c ========================================================*/
extern Aig_Man_t * Aig_ManRetimeFrontier( Aig_Man_t * p, int nStepsMax );
/*=== aigScl.c ==========================================================*/
extern Aig_Man_t * Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap );
extern int Aig_ManSeqCleanup( Aig_Man_t * p );
@ -479,6 +490,7 @@ extern void Aig_TableInsert( Aig_Man_t * p, Aig_Obj_t * pObj );
extern void Aig_TableDelete( Aig_Man_t * p, Aig_Obj_t * pObj );
extern int Aig_TableCountEntries( Aig_Man_t * p );
extern void Aig_TableProfile( Aig_Man_t * p );
extern void Aig_TableClear( Aig_Man_t * p );
/*=== aigTiming.c ========================================================*/
extern void Aig_ObjClearReverseLevel( Aig_Man_t * p, Aig_Obj_t * pObj );
extern int Aig_ObjRequiredLevel( Aig_Man_t * p, Aig_Obj_t * pObj );

133
src/aig/aig/aigFrames.c Normal file
View File

@ -0,0 +1,133 @@
/**CFile****************************************************************
FileName [aigFrames.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [AIG package.]
Synopsis [Performs timeframe expansion of the AIG.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - April 28, 2007.]
Revision [$Id: aigFrames.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
***********************************************************************/
#include "aig.h"
////////////////////////////////////////////////////////////////////////
/// 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 [Performs timeframe expansion of the AIG.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Aig_ManFrames( Aig_Man_t * pAig, int nFs, int fInit, int fOuts, int fRegs, Aig_Obj_t *** ppObjMap )
{
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 = ALLOC( Aig_Obj_t *, nFs * Aig_ManObjNumMax(pAig) );
memset( pObjMap, 0, sizeof(Aig_Obj_t *) * nFs * Aig_ManObjNumMax(pAig) );
// start the fraig package
pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) * nFs );
pFrames->pName = Aig_UtilStrsav( pAig->pName );
// map constant nodes
for ( f = 0; f < nFs; f++ )
Aig_ObjSetFrames( pObjMap, nFs, Aig_ManConst1(pAig), f, Aig_ManConst1(pFrames) );
// create PI nodes for the frames
for ( f = 0; f < nFs; f++ )
Aig_ManForEachPiSeq( pAig, pObj, i )
Aig_ObjSetFrames( pObjMap, nFs, pObj, f, Aig_ObjCreatePi(pFrames) );
// set initial state for the latches
if ( fInit )
{
Aig_ManForEachLoSeq( pAig, pObj, i )
Aig_ObjSetFrames( pObjMap, nFs, pObj, 0, Aig_ManConst0(pFrames) );
}
else
{
Aig_ManForEachLoSeq( pAig, pObj, i )
Aig_ObjSetFrames( pObjMap, nFs, pObj, 0, Aig_ObjCreatePi(pFrames) );
}
// add timeframes
for ( f = 0; f < nFs; f++ )
{
// printf( "Frame = %d.\n", f );
// add internal nodes of this frame
Aig_ManForEachNode( pAig, pObj, i )
{
// Aig_Obj_t * pFanin0 = Aig_ObjChild0Frames(pObjMap,nFs,pObj,f);
// Aig_Obj_t * pFanin1 = Aig_ObjChild1Frames(pObjMap,nFs,pObj,f);
// printf( "Node = %3d. Fanin0 = %3d. Fanin1 = %3d.\n", pObj->Id, Aig_Regular(pFanin0)->Id, Aig_Regular(pFanin1)->Id );
pObjNew = Aig_And( pFrames, Aig_ObjChild0Frames(pObjMap,nFs,pObj,f), Aig_ObjChild1Frames(pObjMap,nFs,pObj,f) );
Aig_ObjSetFrames( pObjMap, nFs, 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,nFs,pObjLi,f);
if ( f < nFs - 1 )
Aig_ObjSetFrames( pObjMap, nFs, pObjLo, f+1, pObjNew );
}
}
if ( fOuts )
{
for ( f = 0; f < nFs; f++ )
Aig_ManForEachPoSeq( pAig, pObj, i )
{
pObjNew = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Frames(pObjMap,nFs,pObj,f) );
Aig_ObjSetFrames( pObjMap, nFs, pObj, f, pObjNew );
}
}
if ( fRegs )
{
pFrames->nRegs = pAig->nRegs;
Aig_ManForEachLiSeq( pAig, pObj, i )
{
pObjNew = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Frames(pObjMap,nFs,pObj,nFs-1) );
Aig_ObjSetFrames( pObjMap, nFs, pObj, nFs-1, pObjNew );
}
}
Aig_ManCleanup( pFrames );
// return the new manager
if ( ppObjMap )
*ppObjMap = pObjMap;
else
free( pObjMap );
return pFrames;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

270
src/aig/aig/aigHaig.c Normal file
View File

@ -0,0 +1,270 @@
/**CFile****************************************************************
FileName [aigHaig.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [AIG package.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - April 28, 2007.]
Revision [$Id: aigHaig.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
***********************************************************************/
#include "aig.h"
#include "satSolver.h"
#include "cnf.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static inline Aig_Obj_t * Aig_HaigObjFrames( Aig_Obj_t ** ppMap, int nFrames, Aig_Obj_t * pObj, int f ) { return ppMap[nFrames*pObj->Id + f]; }
static inline void Aig_HaigObjSetFrames( Aig_Obj_t ** ppMap, int nFrames, Aig_Obj_t * pObj, int f, Aig_Obj_t * pNode ) { ppMap[nFrames*pObj->Id + f] = pNode; }
static inline Aig_Obj_t * Aig_HaigObjChild0Frames( Aig_Obj_t ** ppMap, int nFrames, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Aig_HaigObjFrames(ppMap,nFrames,Aig_ObjFanin0(pObj),i), Aig_ObjFaninC0(pObj)) : NULL; }
static inline Aig_Obj_t * Aig_HaigObjChild1Frames( Aig_Obj_t ** ppMap, int nFrames, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Aig_HaigObjFrames(ppMap,nFrames,Aig_ObjFanin1(pObj),i), Aig_ObjFaninC1(pObj)) : NULL; }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Performs speculative reduction for one node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Aig_ManHaigFramesNode( Aig_Obj_t ** ppMap, int nFrames, Aig_Man_t * pFrames, Aig_Obj_t * pObj, int iFrame )
{
Aig_Obj_t * pObjNew, * pObjNew2, * pObjRepr, * pObjReprNew, * pMiter;
// skip nodes without representative
pObjRepr = pObj->pHaig;
if ( pObjRepr == NULL )
return;
assert( !Aig_IsComplement(pObjRepr) );
assert( pObjRepr->Id < pObj->Id );
// get the new node
pObjNew = Aig_HaigObjFrames( ppMap, nFrames, pObj, iFrame );
// get the new node of the representative
pObjReprNew = Aig_HaigObjFrames( ppMap, nFrames, pObjRepr, iFrame );
// if this is the same node, no need to add constraints
if ( Aig_Regular(pObjNew) == Aig_Regular(pObjReprNew) )
return;
// these are different nodes - perform speculative reduction
pObjNew2 = Aig_NotCond( pObjReprNew, pObj->fPhase ^ pObjRepr->fPhase );
// set the new node
Aig_HaigObjSetFrames( ppMap, nFrames, pObj, iFrame, pObjNew2 );
// add the constraint
pMiter = Aig_Exor( pFrames, Aig_Regular(pObjNew), Aig_Regular(pObjReprNew) );
pMiter = Aig_NotCond( pMiter, Aig_Regular(pMiter)->fPhase ^ Aig_IsComplement(pMiter) );
pMiter = Aig_Not( pMiter );
Aig_ObjCreatePo( pFrames, pMiter );
}
/**Function*************************************************************
Synopsis [Prepares the inductive case with speculative reduction.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Aig_ManHaigFrames( Aig_Man_t * pHaig, int nFrames )
{
Aig_Man_t * pFrames;
Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew;
Aig_Obj_t ** ppMap;
int i, k, f;
assert( nFrames >= 2 );
assert( Aig_ManRegNum(pHaig) > 0 );
assert( Aig_ManRegNum(pHaig) < Aig_ManPiNum(pHaig) );
// create node mapping
ppMap = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pHaig) * nFrames );
memset( ppMap, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(pHaig) * nFrames );
// start the frames
pFrames = Aig_ManStart( Aig_ManObjNumMax(pHaig) * nFrames );
pFrames->pName = Aig_UtilStrsav( pHaig->pName );
pFrames->nRegs = pHaig->nRegs;
// create PI nodes for the frames
for ( f = 0; f < nFrames; f++ )
Aig_HaigObjSetFrames( ppMap, nFrames, Aig_ManConst1(pHaig), f, Aig_ManConst1(pFrames) );
for ( f = 0; f < nFrames; f++ )
Aig_ManForEachPiSeq( pHaig, pObj, i )
Aig_HaigObjSetFrames( ppMap, nFrames, pObj, f, Aig_ObjCreatePi(pFrames) );
// create latches for the first frame
Aig_ManForEachLoSeq( pHaig, pObj, i )
Aig_HaigObjSetFrames( ppMap, nFrames, pObj, 0, Aig_ObjCreatePi(pFrames) );
// add timeframes
for ( f = 0; f < nFrames; f++ )
{
// mark the asserts
if ( f == nFrames - 1 )
pFrames->nAsserts = Aig_ManPoNum(pFrames);
// constrain latch outputs and internal nodes
Aig_ManForEachObj( pHaig, pObj, i )
{
if ( Aig_ObjIsPi(pObj) && Aig_HaigObjFrames(ppMap, nFrames, pObj, f) == NULL )
{
Aig_ManHaigFramesNode( ppMap, nFrames, pFrames, pObj, f );
}
else if ( Aig_ObjIsNode(pObj) )
{
pObjNew = Aig_And( pFrames,
Aig_HaigObjChild0Frames(ppMap,nFrames,pObj,f),
Aig_HaigObjChild1Frames(ppMap,nFrames,pObj,f) );
Aig_HaigObjSetFrames( ppMap, nFrames, pObj, f, pObjNew );
Aig_ManHaigFramesNode( ppMap, nFrames, pFrames, pObj, f );
}
}
/*
// set the constraints on the latch outputs
Aig_ManForEachLoSeq( pHaig, pObj, i )
Aig_ManHaigFramesNode( ppMap, nFrames, pFrames, pObj, f );
// add internal nodes of this frame
Aig_ManForEachNode( pHaig, pObj, i )
{
pObjNew = Aig_And( pFrames,
Aig_HaigObjChild0Frames(ppMap,nFrames,pObj,f),
Aig_HaigObjChild1Frames(ppMap,nFrames,pObj,f) );
Aig_HaigObjSetFrames( ppMap, nFrames, pObj, f, pObjNew );
Aig_ManHaigFramesNode( ppMap, nFrames, pFrames, pObj, f );
}
*/
// transfer latch inputs to the latch outputs
Aig_ManForEachLiLoSeq( pHaig, pObjLi, pObjLo, k )
{
pObjNew = Aig_HaigObjChild0Frames(ppMap,nFrames,pObjLi,f);
Aig_HaigObjSetFrames( ppMap, nFrames, pObjLo, f+1, pObjNew );
}
}
// remove dangling nodes
Aig_ManCleanup( pFrames );
free( ppMap );
return pFrames;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Aig_ManHaigVerify( Aig_Man_t * pHaig )
{
int nBTLimit = 0;
Aig_Man_t * pFrames;
Cnf_Dat_t * pCnf;
sat_solver * pSat;
Aig_Obj_t * pObj;
int i, Lit, RetValue, Counter;
int clk = clock();
// create time frames with speculative reduction and convert them into CNF
clk = clock();
pFrames = Aig_ManHaigFrames( pHaig, 2 );
pCnf = Cnf_DeriveSimple( pFrames, Aig_ManPoNum(pFrames) - pFrames->nAsserts );
// pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) - pFrames->nAsserts );
//Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 );
// create the SAT solver to be used for this problem
pSat = Cnf_DataWriteIntoSolver( pCnf );
printf( "HAIG regs = %d. HAIG nodes = %d. Outputs = %d.\n",
Aig_ManRegNum(pHaig), Aig_ManNodeNum(pHaig), Aig_ManPoNum(pHaig) );
printf( "Frames regs = %d. Frames nodes = %d. Outputs = %d. Assumptions = %d. Asserts = %d.\n",
Aig_ManRegNum(pFrames), Aig_ManNodeNum(pFrames), Aig_ManPoNum(pFrames),
pFrames->nAsserts, Aig_ManPoNum(pFrames) - pFrames->nAsserts );
PRT( "Preparation", clock() - clk );
if ( pSat == NULL )
{
printf( "Aig_ManHaigVerify(): Computed CNF is not valid.\n" );
return -1;
}
// solve each output
clk = clock();
Counter = 0;
Aig_ManForEachPo( pFrames, pObj, i )
{
if ( i < pFrames->nAsserts )
continue;
Lit = toLitCond( pCnf->pVarNums[pObj->Id], pObj->fPhase );
RetValue = sat_solver_solve( pSat, &Lit, &Lit + 1, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
if ( RetValue != l_False )
Counter++;
}
PRT( "Solving ", clock() - clk );
if ( Counter )
printf( "Verification failed for %d classes.\n", Counter );
else
printf( "Verification is successful.\n" );
// clean up
Aig_ManStop( pFrames );
Cnf_DataFree( pCnf );
sat_solver_delete( pSat );
return Counter;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ManHaigRecord( Aig_Man_t * p )
{
Aig_Man_t * pNew;
Aig_Obj_t * pObj;
int i;
// start the HAIG
p->pManHaig = Aig_ManDup( p, 1 );
// set the pointers to the HAIG nodes
Aig_ManForEachObj( p, pObj, i )
pObj->pHaig = pObj->pData;
// remove structural hashing table
Aig_TableClear( p->pManHaig );
// perform a sequence of synthesis steps
pNew = Aig_ManRetimeFrontier( p, 10000 );
// use the haig for verification
Aig_ManDumpBlif( pNew->pManHaig, "haig_temp.blif" );
Aig_ManHaigVerify( pNew->pManHaig );
Aig_ManStop( pNew );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

53
src/aig/aig/aigMan.c
View File

@ -115,7 +115,14 @@ Aig_Obj_t * Aig_ManDup_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
if ( Aig_ObjIsBuf(pObj) )
return pObj->pData = Aig_ObjChild0Copy(pObj);
Aig_ManDup_rec( pNew, p, Aig_ObjFanin1(pObj) );
return pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
if ( pNew->pManHaig == NULL )
return pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
else
{
Aig_Obj_t * pObjNew = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
Aig_Regular(pObjNew->pHaig)->pHaig = Aig_Regular(pObj->pHaig);
return pObj->pData = pObjNew;
}
}
/**Function*************************************************************
@ -132,28 +139,52 @@ Aig_Obj_t * Aig_ManDup_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
{
Aig_Man_t * pNew;
Aig_Obj_t * pObj;
Aig_Obj_t * pObj, * pObjNew;
int i;
// create the new manager
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->nRegs = p->nRegs;
pNew->nAsserts = p->nAsserts;
pNew->pManHaig = p->pManHaig;
if ( p->vFlopNums )
pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
// create the PIs
Aig_ManCleanData( p );
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
Aig_ManForEachPi( p, pObj, i )
pObj->pData = Aig_ObjCreatePi(pNew);
{
pObjNew = Aig_ObjCreatePi( pNew );
pObjNew->pHaig = pObj->pHaig;
pObj->pData = pObjNew;
}
// duplicate internal nodes
if ( fOrdered )
{
Aig_ManForEachObj( p, pObj, i )
if ( Aig_ObjIsBuf(pObj) )
pObj->pData = Aig_ObjChild0Copy(pObj);
{
if ( pNew->pManHaig == NULL )
pObj->pData = Aig_ObjChild0Copy(pObj);
else
{
Aig_Obj_t * pObjNew = Aig_ObjChild0Copy(pObj);
Aig_Regular(pObjNew->pHaig)->pHaig = Aig_Regular(pObj->pHaig);
pObj->pData = pObjNew;
}
}
else if ( Aig_ObjIsNode(pObj) )
pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
{
if ( pNew->pManHaig == NULL )
pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
else
{
Aig_Obj_t * pObjNew = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
Aig_Regular(pObjNew->pHaig)->pHaig = Aig_Regular(pObj->pHaig);
pObj->pData = pObjNew;
}
}
}
else
{
@ -166,8 +197,16 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
}
// add the POs
Aig_ManForEachPo( p, pObj, i )
Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
{
pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
pObjNew->pHaig = pObj->pHaig;
pObj->pData = pObjNew;
}
assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
// pass the HAIG to the new AIG
p->pManHaig = NULL;
Aig_ManForEachObj( p, pObj, i )
pObj->pHaig = NULL;
// check the resulting network
if ( !Aig_ManCheck(pNew) )
printf( "Aig_ManDup(): The check has failed.\n" );
@ -228,6 +267,8 @@ void Aig_ManStop( Aig_Man_t * p )
{
Aig_Obj_t * pObj;
int i;
if ( p->pManHaig )
Aig_ManStop( p->pManHaig );
if ( p->vMapped )
Vec_PtrFree( p->vMapped );
// print time

17
src/aig/aig/aigObj.c
View File

@ -88,7 +88,7 @@ Aig_Obj_t * Aig_ObjCreate( Aig_Man_t * p, Aig_Obj_t * pGhost )
Aig_Obj_t * pObj;
assert( !Aig_IsComplement(pGhost) );
assert( Aig_ObjIsHash(pGhost) );
assert( pGhost == &p->Ghost );
// assert( pGhost == &p->Ghost );
// get memory for the new object
pObj = Aig_ManFetchMemory( p );
pObj->Type = pGhost->Type;
@ -97,6 +97,12 @@ Aig_Obj_t * Aig_ObjCreate( Aig_Man_t * p, Aig_Obj_t * pGhost )
// update node counters of the manager
p->nObjs[Aig_ObjType(pObj)]++;
assert( pObj->pData == NULL );
if ( p->pManHaig )
{
pGhost->pFanin0 = Aig_ObjHaig( pGhost->pFanin0 );
pGhost->pFanin1 = Aig_ObjHaig( pGhost->pFanin1 );
pObj->pHaig = Aig_ObjCreate( p->pManHaig, pGhost );
}
return pObj;
}
@ -365,6 +371,13 @@ void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, in
// make sure object is not pointing to itself
assert( pObjOld != Aig_ObjFanin0(pObjNewR) );
assert( pObjOld != Aig_ObjFanin1(pObjNewR) );
// map the HAIG nodes
if ( p->pManHaig != NULL )
{
assert( pObjNewR->pHaig != NULL );
assert( pObjNewR->pHaig->pHaig == NULL );
pObjNewR->pHaig->pHaig = pObjOld->pHaig;
}
// recursively delete the old node - but leave the object there
pObjNewR->nRefs++;
Aig_ObjDelete_rec( p, pObjOld, 0 );
@ -385,6 +398,8 @@ void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, in
pObjOld->Type = pObjNew->Type;
Aig_ObjDisconnect( p, pObjNew );
Aig_ObjConnect( p, pObjOld, pFanin0, pFanin1 );
// update the haig node
pObjOld->pHaig = pObjNew->pHaig;
// delete the new object
Aig_ObjDelete( p, pObjNew );
// update levels

9
src/aig/aig/aigOper.c
View File

@ -139,6 +139,15 @@ Aig_Obj_t * Aig_And( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 )
{
Aig_Obj_t * pGhost, * pResult;
// Aig_Obj_t * pFan0, * pFan1;
if ( p->pTable == NULL )
{
// pGhost = Aig_ObjCreateGhost( p, p0, p1, AIG_OBJ_AND );
pGhost = Aig_ManGhost(p);
pGhost->Type = AIG_OBJ_AND;
pGhost->pFanin0 = p0;
pGhost->pFanin1 = p1;
return Aig_ObjCreate( p, pGhost );
}
// check trivial cases
if ( p0 == p1 )
return p0;

219
src/aig/aig/aigRetF.c Normal file
View File

@ -0,0 +1,219 @@
/**CFile****************************************************************
FileName [aigRetF.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [AIG package.]
Synopsis [Retiming frontier.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - April 28, 2007.]
Revision [$Id: aigRetF.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
***********************************************************************/
#include "aig.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Mark the nodes reachable from the PIs in the reverse order.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Aig_ManRetimeMark_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
{
if ( pObj->fMarkB )
return 1;
if ( Aig_ObjIsPi(pObj) || Aig_ObjIsConst1(pObj) )
return 0;
if ( Aig_ObjIsTravIdCurrent(p, pObj) )
return pObj->fMarkB;
Aig_ObjSetTravIdCurrent(p, pObj);
if ( Aig_ManRetimeMark_rec( p, Aig_ObjFanin0(pObj) ) )
return pObj->fMarkB = 1;
if ( Aig_ObjIsNode(pObj) && Aig_ManRetimeMark_rec( p, Aig_ObjFanin1(pObj) ) )
return pObj->fMarkB = 1;
assert( pObj->fMarkB == 0 );
return 0;
}
/**Function*************************************************************
Synopsis [Mark the nodes reachable from the true PIs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ManRetimeMark( Aig_Man_t * p )
{
Aig_Obj_t * pObj, * pObjLi, * pObjLo;
int fChange, i;
// mark the PIs
Aig_ManForEachObj( p, pObj, i )
assert( pObj->fMarkB == 0 );
Aig_ManForEachPiSeq( p, pObj, i )
pObj->fMarkB = 1;
// map registers into each other
Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
{
assert( pObjLo->pNext == NULL );
assert( pObjLi->pNext == NULL );
pObjLo->pNext = pObjLi;
pObjLi->pNext = pObjLo;
}
// iterativively mark the logic reachable from PIs
fChange = 1;
while ( fChange )
{
fChange = 0;
Aig_ManIncrementTravId( p );
Aig_ManForEachPo( p, pObj, i )
{
if ( pObj->fMarkB )
continue;
if ( Aig_ManRetimeMark_rec( p, pObj ) )
{
if ( pObj->pNext )
pObj->pNext->fMarkB = 1;
fChange = 1;
}
}
}
// clean register mapping
Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
pObjLo->pNext = pObjLi->pNext = NULL;
}
/**Function*************************************************************
Synopsis [Performs forward retiming.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Aig_ManRetimeFrontier( Aig_Man_t * p, int nStepsMax )
{
Aig_Obj_t * pObj, * pObjNew, * pObjLo, * pObjLo0, * pObjLo1, * pObjLi, * pObjLi0, * pObjLi1;//, * pObjLi0_, * pObjLi1_, * pObjLi0__, * pObjLi1__;
int i, Counter, fCompl, fChange;
assert( Aig_ManRegNum(p) > 0 );
// remove structural hashing table
Aig_TableClear( p );
// mark the retimable nodes
Aig_ManRetimeMark( p );
// mark the register outputs
Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
{
pObjLo->fMarkA = 1;
pObjLo->pNext = pObjLi;
pObjLi->pNext = pObjLo;
}
// go through the nodes and find retimable ones
Counter = 0;
fChange = 1;
while ( fChange )
{
fChange = 0;
Aig_ManForEachNode( p, pObj, i )
{
if ( !pObj->fMarkB )
continue;
if ( Aig_ObjIsBuf(pObj) )
continue;
// get the real inputs of the node (skipping the buffers)
pObjLo0 = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
pObjLo1 = Aig_ObjReal_rec( Aig_ObjChild1(pObj) );
if ( !Aig_Regular(pObjLo0)->fMarkA || !Aig_Regular(pObjLo1)->fMarkA )
continue;
// remember complemented attribute
fCompl = Aig_IsComplement(pObjLo0) & Aig_IsComplement(pObjLo1);
// get the register inputs
// pObjLi0_ = Aig_Regular(pObjLo0)->pNext;
// pObjLi1_ = Aig_Regular(pObjLo1)->pNext;
// pObjLi0__ = Aig_ObjChild0(Aig_Regular(pObjLo0)->pNext);
// pObjLi1__ = Aig_ObjChild0(Aig_Regular(pObjLo1)->pNext);
pObjLi0 = Aig_NotCond( Aig_ObjChild0(Aig_Regular(pObjLo0)->pNext), Aig_IsComplement(pObjLo0) );
pObjLi1 = Aig_NotCond( Aig_ObjChild0(Aig_Regular(pObjLo1)->pNext), Aig_IsComplement(pObjLo1) );
// create new node
pObjNew = Aig_And( p, pObjLi0, pObjLi1 );
pObjNew->fMarkB = 1;
// create new register
pObjLo = Aig_ObjCreatePi(p);
pObjLo->fMarkA = 1;
pObjLi = Aig_ObjCreatePo( p, Aig_NotCond(pObjNew, fCompl) );
p->nRegs++;
pObjLo->pNext = pObjLi;
pObjLi->pNext = pObjLo;
// add the buffer
Aig_ObjDisconnect( p, pObj );
pObj->Type = AIG_OBJ_BUF;
p->nObjs[AIG_OBJ_AND]--;
p->nObjs[AIG_OBJ_BUF]++;
Aig_ObjConnect( p, pObj, Aig_NotCond(pObjLo, fCompl), NULL );
// create HAIG if defined
if ( p->pManHaig )
{
// create HAIG latch
pObjLo->pHaig = Aig_ObjCreatePi( p->pManHaig );
pObjLi->pHaig = Aig_ObjCreatePo( p->pManHaig, Aig_ObjHaig( Aig_ObjChild0(pObjLi) ) );
// create equivalence class
assert( pObjLo->pHaig != NULL );
assert( pObjLo->pHaig->pHaig == NULL );
pObjLo->pHaig->pHaig = Aig_Regular(pObj->pHaig);
}
// mark the change
fChange = 1;
// check the limit
if ( ++Counter >= nStepsMax )
{
fChange = 0;
break;
}
}
}
// clean the markings
Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
{
pObjLo->fMarkA = 0;
pObjLo->pNext = pObjLi->pNext = NULL;
}
Aig_ManForEachObj( p, pObj, i )
pObj->fMarkB = 0;
// remove useless registers
Aig_ManSeqCleanup( p );
// rehash the nodes
return Aig_ManDup( p, 1 );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

6
src/aig/aig/aigScl.c
View File

@ -32,7 +32,7 @@
Synopsis [Remaps the manager.]
Description [Map in the array specifies for each CI nodes the node that
Description [Map in the array specifies for each CI node the node that
should be used after remapping.]
SideEffects []
@ -101,7 +101,7 @@ void Aig_ManSeqCleanup_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes
Vec_PtrPush( vNodes, pObj->pNext );
return;
}
if ( Aig_ObjIsPo(pObj) )
if ( Aig_ObjIsPo(pObj) || Aig_ObjIsBuf(pObj) )
{
Aig_ManSeqCleanup_rec( p, Aig_ObjFanin0(pObj), vNodes );
return;
@ -127,7 +127,7 @@ int Aig_ManSeqCleanup( Aig_Man_t * p )
Vec_Ptr_t * vNodes, * vCis, * vCos;
Aig_Obj_t * pObj, * pObjLi, * pObjLo;
int i, nTruePis, nTruePos;
assert( Aig_ManBufNum(p) == 0 );
// assert( Aig_ManBufNum(p) == 0 );
// mark the PIs
Aig_ManIncrementTravId( p );

21
src/aig/aig/aigTable.c
View File

@ -184,6 +184,8 @@ Aig_Obj_t * Aig_TableLookupTwo( Aig_Man_t * p, Aig_Obj_t * pFanin0, Aig_Obj_t *
void Aig_TableInsert( Aig_Man_t * p, Aig_Obj_t * pObj )
{
Aig_Obj_t ** ppPlace;
if ( p->pTable == NULL )
return;
assert( !Aig_IsComplement(pObj) );
assert( Aig_TableLookup(p, pObj) == NULL );
if ( (pObj->Id & 0xFF) == 0 && 2 * p->nTableSize < Aig_ManNodeNum(p) )
@ -207,6 +209,8 @@ void Aig_TableInsert( Aig_Man_t * p, Aig_Obj_t * pObj )
void Aig_TableDelete( Aig_Man_t * p, Aig_Obj_t * pObj )
{
Aig_Obj_t ** ppPlace;
if ( p->pTable == NULL )
return;
assert( !Aig_IsComplement(pObj) );
ppPlace = Aig_TableFind( p, pObj );
assert( *ppPlace == pObj ); // node should be in the table
@ -261,6 +265,23 @@ void Aig_TableProfile( Aig_Man_t * p )
}
}
/**Function********************************************************************
Synopsis [Profiles the hash table.]
Description []
SideEffects []
SeeAlso []
******************************************************************************/
void Aig_TableClear( Aig_Man_t * p )
{
FREE( p->pTable );
p->nTableSize = 0;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

8
src/aig/aig/aigUtil.c
View File

@ -649,7 +649,7 @@ void Aig_ManDump( Aig_Man_t * p )
/**Function*************************************************************
Synopsis [Writes the AIG into the BLIF file.]
Synopsis [Writes the AIG into a BLIF file.]
Description []
@ -680,7 +680,7 @@ void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName )
Vec_PtrForEachEntry( vNodes, pObj, i )
pObj->iData = Counter++;
nDigits = Aig_Base10Log( Counter );
// write the file
// write the file
pFile = fopen( pFileName, "w" );
fprintf( pFile, "# BLIF file written by procedure Aig_ManDumpBlif()\n" );
// fprintf( pFile, "# http://www.eecs.berkeley.edu/~alanmi/abc/\n" );
@ -702,7 +702,7 @@ void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName )
Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
fprintf( pFile, ".latch n%0*d n%0*d 0\n", nDigits, pObjLi->iData, nDigits, pObjLo->iData );
fprintf( pFile, "\n" );
}
}
// write nodes
Vec_PtrForEachEntry( vNodes, pObj, i )
{
@ -731,7 +731,7 @@ void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName )
/**Function*************************************************************
Synopsis [Writes the AIG into the BLIF file.]
Synopsis [Writes the AIG into a Verilog file.]
Description []

737
src/aig/fra/fraClau.c Normal file
View File

@ -0,0 +1,737 @@
/**CFile****************************************************************
FileName [fraClau.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [New FRAIG package.]
Synopsis [Induction with clause strengthening.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 30, 2007.]
Revision [$Id: fraClau.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
***********************************************************************/
#include "fra.h"
#include "cnf.h"
#include "satSolver.h"
/*
This code is inspired by the paper: Aaron Bradley and Zohar Manna,
"Checking safety by inductive generalization of counterexamples to
induction", FMCAD '07.
*/
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
typedef struct Cla_Man_t_ Cla_Man_t;
struct Cla_Man_t_
{
// SAT solvers
sat_solver * pSatMain;
sat_solver * pSatTest;
sat_solver * pSatBmc;
// CNF for the test solver
// Cnf_Dat_t * pCnfTest;
// SAT variables
Vec_Int_t * vSatVarsMainCs;
Vec_Int_t * vSatVarsTestCs;
Vec_Int_t * vSatVarsTestNs;
Vec_Int_t * vSatVarsBmcNs;
// helper variables
int nSatVarsTestBeg;
int nSatVarsTestCur;
// counter-examples
Vec_Int_t * vCexMain0;
Vec_Int_t * vCexMain;
Vec_Int_t * vCexTest;
Vec_Int_t * vCexBase;
Vec_Int_t * vCexAssm;
Vec_Int_t * vCexBmc;
// mapping of CS into NS var numbers
int * pMapCsMainToCsTest;
int * pMapCsTestToCsMain;
int * pMapCsTestToNsTest;
int * pMapCsTestToNsBmc;
};
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Saves variables corresponding to latch outputs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Fra_ClauSaveLatchVars( Aig_Man_t * pMan, Cnf_Dat_t * pCnf, int fCsVars )
{
Vec_Int_t * vVars;
Aig_Obj_t * pObjLo, * pObjLi;
int i;
vVars = Vec_IntAlloc( Aig_ManRegNum(pMan) );
Aig_ManForEachLiLoSeq( pMan, pObjLi, pObjLo, i )
Vec_IntPush( vVars, pCnf->pVarNums[fCsVars? pObjLo->Id : pObjLi->Id] );
return vVars;
}
/**Function*************************************************************
Synopsis [Saves variables corresponding to latch outputs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Fra_ClauSaveOutputVars( Aig_Man_t * pMan, Cnf_Dat_t * pCnf )
{
Vec_Int_t * vVars;
Aig_Obj_t * pObj;
int i;
vVars = Vec_IntAlloc( Aig_ManPoNum(pMan) );
Aig_ManForEachPo( pMan, pObj, i )
Vec_IntPush( vVars, pCnf->pVarNums[pObj->Id] );
return vVars;
}
/**Function*************************************************************
Synopsis [Saves variables corresponding to latch outputs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Fra_ClauSaveInputVars( Aig_Man_t * pMan, Cnf_Dat_t * pCnf, int nStarting )
{
Vec_Int_t * vVars;
Aig_Obj_t * pObj;
int i;
vVars = Vec_IntAlloc( Aig_ManPiNum(pMan) - nStarting );
Aig_ManForEachPi( pMan, pObj, i )
{
if ( i < nStarting )
continue;
Vec_IntPush( vVars, pCnf->pVarNums[pObj->Id] );
}
return vVars;
}
/**Function*************************************************************
Synopsis [Saves variables corresponding to latch outputs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int * Fra_ClauCreateMapping( Vec_Int_t * vSatVarsFrom, Vec_Int_t * vSatVarsTo, int nVarsMax )
{
int * pMapping, Var, i;
assert( Vec_IntSize(vSatVarsFrom) == Vec_IntSize(vSatVarsTo) );
pMapping = ALLOC( int, nVarsMax );
for ( i = 0; i < nVarsMax; i++ )
pMapping[i] = -1;
Vec_IntForEachEntry( vSatVarsFrom, Var, i )
pMapping[Var] = Vec_IntEntry(vSatVarsTo,i);
return pMapping;
}
/**Function*************************************************************
Synopsis [Deletes the manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_ClauStop( Cla_Man_t * p )
{
free( p->pMapCsMainToCsTest );
free( p->pMapCsTestToCsMain );
free( p->pMapCsTestToNsTest );
free( p->pMapCsTestToNsBmc );
Vec_IntFree( p->vSatVarsMainCs );
Vec_IntFree( p->vSatVarsTestCs );
Vec_IntFree( p->vSatVarsTestNs );
Vec_IntFree( p->vSatVarsBmcNs );
Vec_IntFree( p->vCexMain0 );
Vec_IntFree( p->vCexMain );
Vec_IntFree( p->vCexTest );
Vec_IntFree( p->vCexBase );
Vec_IntFree( p->vCexAssm );
Vec_IntFree( p->vCexBmc );
if ( p->pSatMain ) sat_solver_delete( p->pSatMain );
if ( p->pSatTest ) sat_solver_delete( p->pSatTest );
if ( p->pSatBmc ) sat_solver_delete( p->pSatBmc );
free( p );
}
/**Function*************************************************************
Synopsis [Takes the AIG with the single output to be checked.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Cla_Man_t * Fra_ClauStart( Aig_Man_t * pMan )
{
Cla_Man_t * p;
Cnf_Dat_t * pCnfMain;
Cnf_Dat_t * pCnfTest;
Cnf_Dat_t * pCnfBmc;
Aig_Man_t * pFramesMain;
Aig_Man_t * pFramesTest;
Aig_Man_t * pFramesBmc;
assert( Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan) == 1 );
// start the manager
p = ALLOC( Cla_Man_t, 1 );
memset( p, 0, sizeof(Cla_Man_t) );
p->vCexMain0 = Vec_IntAlloc( Aig_ManRegNum(pMan) );
p->vCexMain = Vec_IntAlloc( Aig_ManRegNum(pMan) );
p->vCexTest = Vec_IntAlloc( Aig_ManRegNum(pMan) );
p->vCexBase = Vec_IntAlloc( Aig_ManRegNum(pMan) );
p->vCexAssm = Vec_IntAlloc( Aig_ManRegNum(pMan) );
p->vCexBmc = Vec_IntAlloc( Aig_ManRegNum(pMan) );
// derive two timeframes to be checked
pFramesMain = Aig_ManFrames( pMan, 2, 0, 1, 0, NULL ); // nFrames, fInit, fOuts, fRegs
//Aig_ManShow( pFramesMain, 0, NULL );
assert( Aig_ManPoNum(pFramesMain) == 2 );
Aig_ObjChild0Flip( Aig_ManPo(pFramesMain, 0) ); // complement the first output
pCnfMain = Cnf_DeriveSimple( pFramesMain, 0 );
//Cnf_DataWriteIntoFile( pCnfMain, "temp.cnf", 1 );
p->pSatMain = Cnf_DataWriteIntoSolver( pCnfMain );
/*
{
int i;
Aig_Obj_t * pObj;
Aig_ManForEachObj( pFramesMain, pObj, i )
printf( "%d -> %d \n", pObj->Id, pCnfMain->pVarNums[pObj->Id] );
printf( "\n" );
}
*/
// derive one timeframe to be checked
pFramesTest = Aig_ManFrames( pMan, 1, 0, 0, 1, NULL );
assert( Aig_ManPoNum(pFramesTest) == Aig_ManRegNum(pMan) );
pCnfTest = Cnf_DeriveSimple( pFramesTest, Aig_ManRegNum(pMan) );
p->pSatTest = Cnf_DataWriteIntoSolver( pCnfTest );
p->nSatVarsTestBeg = p->nSatVarsTestCur = sat_solver_nvars( p->pSatTest );
// derive one timeframe to be checked for BMC
pFramesBmc = Aig_ManFrames( pMan, 1, 1, 0, 1, NULL );
//Aig_ManShow( pFramesBmc, 0, NULL );
assert( Aig_ManPoNum(pFramesBmc) == Aig_ManRegNum(pMan) );
pCnfBmc = Cnf_DeriveSimple( pFramesBmc, Aig_ManRegNum(pMan) );
p->pSatBmc = Cnf_DataWriteIntoSolver( pCnfBmc );
// create variable sets
p->vSatVarsMainCs = Fra_ClauSaveInputVars( pFramesMain, pCnfMain, 2 * (Aig_ManPiNum(pMan)-Aig_ManRegNum(pMan)) );
p->vSatVarsTestCs = Fra_ClauSaveLatchVars( pFramesTest, pCnfTest, 1 );
p->vSatVarsTestNs = Fra_ClauSaveLatchVars( pFramesTest, pCnfTest, 0 );
p->vSatVarsBmcNs = Fra_ClauSaveOutputVars( pFramesBmc, pCnfBmc );
assert( Vec_IntSize(p->vSatVarsTestCs) == Vec_IntSize(p->vSatVarsMainCs) );
assert( Vec_IntSize(p->vSatVarsTestCs) == Vec_IntSize(p->vSatVarsBmcNs) );
// create mapping of CS into NS vars
p->pMapCsMainToCsTest = Fra_ClauCreateMapping( p->vSatVarsMainCs, p->vSatVarsTestCs, Aig_ManObjNumMax(pFramesMain) );
p->pMapCsTestToCsMain = Fra_ClauCreateMapping( p->vSatVarsTestCs, p->vSatVarsMainCs, Aig_ManObjNumMax(pFramesTest) );
p->pMapCsTestToNsTest = Fra_ClauCreateMapping( p->vSatVarsTestCs, p->vSatVarsTestNs, Aig_ManObjNumMax(pFramesTest) );
p->pMapCsTestToNsBmc = Fra_ClauCreateMapping( p->vSatVarsTestCs, p->vSatVarsBmcNs, Aig_ManObjNumMax(pFramesTest) );
// cleanup
Cnf_DataFree( pCnfMain );
Cnf_DataFree( pCnfTest );
Cnf_DataFree( pCnfBmc );
Aig_ManStop( pFramesMain );
Aig_ManStop( pFramesTest );
Aig_ManStop( pFramesBmc );
if ( p->pSatMain == NULL || p->pSatTest == NULL || p->pSatBmc == NULL )
{
Fra_ClauStop( p );
return NULL;
}
return p;
}
/**Function*************************************************************
Synopsis [Splits off second half and returns it as a new vector.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static Vec_Int_t * Vec_IntSplitHalf( Vec_Int_t * vVec )
{
Vec_Int_t * vPart;
int Entry, i;
assert( Vec_IntSize(vVec) > 1 );
vPart = Vec_IntAlloc( Vec_IntSize(vVec) / 2 + 1 );
Vec_IntForEachEntryStart( vVec, Entry, i, Vec_IntSize(vVec) / 2 )
Vec_IntPush( vPart, Entry );
Vec_IntShrink( vVec, Vec_IntSize(vVec) / 2 );
return vPart;
}
/**Function*************************************************************
Synopsis [Appends the contents of the second vector.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static void Vec_IntAppend( Vec_Int_t * vVec1, Vec_Int_t * vVec2 )
{
int Entry, i;
Vec_IntForEachEntry( vVec2, Entry, i )
Vec_IntPush( vVec1, Entry );
}
/**Function*************************************************************
Synopsis [Complements all literals in the clause.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static void Vec_IntComplement( Vec_Int_t * vVec )
{
int i;
for ( i = 0; i < Vec_IntSize(vVec); i++ )
vVec->pArray[i] = lit_neg( vVec->pArray[i] );
}
/**Function*************************************************************
Synopsis [Checks if the property holds. Returns counter-example if not.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_ClauCheckProperty( Cla_Man_t * p, Vec_Int_t * vCex )
{
int nBTLimit = 0;
int RetValue, iVar, i;
sat_solver_act_var_clear( p->pSatMain );
RetValue = sat_solver_solve( p->pSatMain, NULL, NULL, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
Vec_IntClear( vCex );
if ( RetValue == l_False )
return 1;
assert( RetValue == l_True );
Vec_IntForEachEntry( p->vSatVarsMainCs, iVar, i )
Vec_IntPush( vCex, sat_solver_var_literal(p->pSatMain, iVar) );
/*
{
int i;
for (i = 0; i < p->pSatMain->size; i++)
printf( "%d=%d ", i, p->pSatMain->model.ptr[i] == l_True );
printf( "\n" );
}
*/
return 0;
}
/**Function*************************************************************
Synopsis [Checks if the clause holds using BMC.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_ClauCheckBmc( Cla_Man_t * p, Vec_Int_t * vClause )
{
int nBTLimit = 0;
int RetValue;
RetValue = sat_solver_solve( p->pSatBmc, Vec_IntArray(vClause), Vec_IntArray(vClause) + Vec_IntSize(vClause),
(sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
if ( RetValue == l_False )
return 1;
assert( RetValue == l_True );
return 0;
}
/**Function*************************************************************
Synopsis [Lifts the clause to depend on NS variables.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_ClauRemapClause( int * pMap, Vec_Int_t * vClause, Vec_Int_t * vRemapped, int fInv )
{
int iLit, i;
Vec_IntClear( vRemapped );
Vec_IntForEachEntry( vClause, iLit, i )
{
assert( pMap[lit_var(iLit)] >= 0 );
iLit = toLitCond( pMap[lit_var(iLit)], lit_sign(iLit) ^ fInv );
Vec_IntPush( vRemapped, iLit );
}
}
/**Function*************************************************************
Synopsis [Checks if the clause holds. Returns counter example if not.]
Description [Uses test SAT solver.]
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_ClauCheckClause( Cla_Man_t * p, Vec_Int_t * vClause, Vec_Int_t * vCex )
{
int nBTLimit = 0;
int RetValue, iVar, i;
int nClauseSize = Vec_IntSize( vClause );
// complement literals
Vec_IntPush( vClause, toLit( p->nSatVarsTestCur++ ) ); // helper positive
Vec_IntComplement( vClause ); // helper negative (the clause is C v h')
// add the clause
RetValue = sat_solver_addclause( p->pSatTest, Vec_IntArray(vClause), Vec_IntArray(vClause) + Vec_IntSize(vClause) );
assert( RetValue == 1 );
// complement all literals
Vec_IntPop( vClause ); // helper removed
Vec_IntComplement( vClause );
// create the assumption in terms of NS variables
Fra_ClauRemapClause( p->pMapCsTestToNsTest, vClause, p->vCexAssm, 0 );
// add helper literals
for ( i = p->nSatVarsTestBeg; i < p->nSatVarsTestCur - 1; i++ )
Vec_IntPush( p->vCexAssm, toLitCond(i,1) ); // other helpers negative
Vec_IntPush( p->vCexAssm, toLitCond(i,0) ); // positive helper
// try to solve
RetValue = sat_solver_solve( p->pSatTest, Vec_IntArray(p->vCexAssm), Vec_IntArray(p->vCexAssm) + Vec_IntSize(p->vCexAssm),
(sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
if ( vCex )
Vec_IntClear( vCex );
if ( RetValue == l_False )
return 1;
assert( RetValue == l_True );
if ( vCex )
{
Vec_IntForEachEntry( p->vSatVarsTestCs, iVar, i )
Vec_IntPush( vCex, sat_solver_var_literal(p->pSatTest, iVar) );
}
return 0;
}
/**Function*************************************************************
Synopsis [Reduces the counter-example by removing complemented literals.]
Description [Removes literals from vMain that differ from those in the
counter-example (vNew). Relies on the fact that the PI variables are
assigned in the increasing order.]
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_ClauReduceClause( Vec_Int_t * vMain, Vec_Int_t * vNew )
{
int LitM, LitN, VarM, VarN, i, j, k;
assert( Vec_IntSize(vMain) <= Vec_IntSize(vNew) );
for ( i = j = k = 0; i < Vec_IntSize(vMain) && j < Vec_IntSize(vNew); )
{
LitM = Vec_IntEntry( vMain, i );
LitN = Vec_IntEntry( vNew, j );
VarM = lit_var( LitM );
VarN = lit_var( LitN );
if ( VarM > VarN )
{
assert( 0 );
}
else if ( VarM < VarN )
{
j++;
}
else // if ( VarM == VarN )
{
i++;
j++;
if ( LitM == LitN )
Vec_IntWriteEntry( vMain, k++, LitM );
}
}
assert( i == Vec_IntSize(vMain) );
Vec_IntShrink( vMain, k );
}
/**Function*************************************************************
Synopsis [Computes the minimal invariant that holds.]
Description [On entrace, vBasis does not hold, vBasis+vExtra holds but
is not minimal. On exit, vBasis is unchanged, vBasis+vExtra is minimal.]
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_ClauMinimizeClause_rec( Cla_Man_t * p, Vec_Int_t * vBasis, Vec_Int_t * vExtra )
{
Vec_Int_t * vExtra2;
int nSizeOld;
if ( Vec_IntSize(vExtra) == 1 )
return;
nSizeOld = Vec_IntSize( vBasis );
vExtra2 = Vec_IntSplitHalf( vExtra );
// try the first half
Vec_IntAppend( vBasis, vExtra );
if ( Fra_ClauCheckClause( p, vBasis, NULL ) )
{
Vec_IntShrink( vBasis, nSizeOld );
Fra_ClauMinimizeClause_rec( p, vBasis, vExtra );
return;
}
Vec_IntShrink( vBasis, nSizeOld );
// try the second half
Vec_IntAppend( vBasis, vExtra2 );
if ( Fra_ClauCheckClause( p, vBasis, NULL ) )
{
Vec_IntShrink( vBasis, nSizeOld );
Fra_ClauMinimizeClause_rec( p, vBasis, vExtra2 );
return;
}
// Vec_IntShrink( vBasis, nSizeOld );
// find the smallest with the second half added
Fra_ClauMinimizeClause_rec( p, vBasis, vExtra );
Vec_IntShrink( vBasis, nSizeOld );
Vec_IntAppend( vBasis, vExtra );
// find the smallest with the second half added
Fra_ClauMinimizeClause_rec( p, vBasis, vExtra2 );
Vec_IntShrink( vBasis, nSizeOld );
Vec_IntAppend( vExtra, vExtra2 );
Vec_IntFree( vExtra2 );
}
/**Function*************************************************************
Synopsis [Minimizes the clauses using a simple method.]
Description [The input and output clause are in vExtra.]
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_ClauMinimizeClause( Cla_Man_t * p, Vec_Int_t * vBasis, Vec_Int_t * vExtra )
{
int iLit, iLit2, i, k;
Vec_IntForEachEntryReverse( vExtra, iLit, i )
{
// copy literals without the given one
Vec_IntClear( vBasis );
Vec_IntForEachEntry( vExtra, iLit2, k )
if ( iLit2 != iLit )
Vec_IntPush( vBasis, iLit2 );
// try whether it is inductive
if ( !Fra_ClauCheckClause( p, vBasis, NULL ) )
continue;
// the clause is inductive
// remove the literal
for ( k = iLit; k < Vec_IntSize(vExtra)-1; k++ )
Vec_IntWriteEntry( vExtra, k, Vec_IntEntry(vExtra,k+1) );
Vec_IntShrink( vExtra, Vec_IntSize(vExtra)-1 );
}
}
/**Function*************************************************************
Synopsis [Prints the clause.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_ClauPrintClause( Vec_Int_t * vSatCsVars, Vec_Int_t * vCex )
{
int LitM, VarM, VarN, i, j, k;
assert( Vec_IntSize(vCex) <= Vec_IntSize(vSatCsVars) );
for ( i = j = k = 0; i < Vec_IntSize(vCex) && j < Vec_IntSize(vSatCsVars); )
{
LitM = Vec_IntEntry( vCex, i );
VarM = lit_var( LitM );
VarN = Vec_IntEntry( vSatCsVars, j );
if ( VarM > VarN )
{
assert( 0 );
}
else if ( VarM < VarN )
{
j++;
printf( "-" );
}
else // if ( VarM == VarN )
{
i++;
j++;
printf( "%d", !lit_sign(LitM) );
}
}
assert( i == Vec_IntSize(vCex) );
}
/**Function*************************************************************
Synopsis [Takes the AIG with the single output to be checked.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_Clau( Aig_Man_t * pMan, int nIters, int fVerbose )
{
Cla_Man_t * p;
int Iter, RetValue, fFailed, i;
assert( Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan) == 1 );
// create the manager
p = Fra_ClauStart( pMan );
if ( p == NULL )
{
printf( "The property is trivially inductive.\n" );
return 1;
}
// generate counter-examples and expand them
for ( Iter = 0; !Fra_ClauCheckProperty( p, p->vCexMain0 ) && Iter < nIters; Iter++ )
{
if ( fVerbose )
printf( "%4d : ", Iter );
// remap clause into the test manager
Fra_ClauRemapClause( p->pMapCsMainToCsTest, p->vCexMain0, p->vCexMain, 0 );
if ( fVerbose )
Fra_ClauPrintClause( p->vSatVarsTestCs, p->vCexMain );
// the main counter-example is in p->vCexMain
// intermediate counter-examples are in p->vCexTest
// generate the reduced counter-example to the inductive property
fFailed = 0;
for ( i = 0; !Fra_ClauCheckClause( p, p->vCexMain, p->vCexTest ); i++ )
{
Fra_ClauReduceClause( p->vCexMain, p->vCexTest );
Fra_ClauRemapClause( p->pMapCsTestToNsBmc, p->vCexMain, p->vCexBmc, 0 );
if ( !Fra_ClauCheckBmc(p, p->vCexBmc) )
{
fFailed = 1;
break;
}
}
if ( fFailed )
{
if ( fVerbose )
printf( " Reducing failed after %d iterations (BMC failed).\n", i );
continue;
}
if ( Vec_IntSize(p->vCexMain) == 0 )
{
if ( fVerbose )
printf( " Reducing failed after %d iterations (nothing left).\n", i );
continue;
}
if ( fVerbose )
printf( " LitsAfterRed = %3d. ", Vec_IntSize(p->vCexMain) );
// minimize the inductive property
Vec_IntClear( p->vCexBase );
// Fra_ClauMinimizeClause_rec( p, p->vCexBase, p->vCexMain );
// Fra_ClauMinimizeClause( p, p->vCexBase, p->vCexMain );
assert( Vec_IntSize(p->vCexMain) > 0 );
if ( fVerbose )
printf( " LitsAfterMin = %3d. ", Vec_IntSize(p->vCexMain) );
if ( fVerbose )
printf( "\n" );
// add the clause to the solver
Fra_ClauRemapClause( p->pMapCsTestToCsMain, p->vCexMain, p->vCexAssm, 1 );
RetValue = sat_solver_addclause( p->pSatMain, Vec_IntArray(p->vCexAssm), Vec_IntArray(p->vCexAssm) + Vec_IntSize(p->vCexAssm) );
if ( RetValue == 0 )
{
Iter++;
break;
}
}
// report the results
if ( Iter == nIters )
{
printf( "Property is not proved after %d iterations.\n", nIters );
return 0;
}
printf( "Property is proved after %d iterations.\n", Iter );
Fra_ClauStop( p );
return 1;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

2
src/aig/fra/fraCore.c
View File

@ -280,6 +280,8 @@ static inline void Fra_FraigNode( Fra_Man_t * p, Aig_Obj_t * pObj )
// Fra_FraigVerifyCounterEx( p, p->vCex );
// simulate the counter-example and return the Fraig node
Fra_SmlResimulate( p );
if ( p->pManFraig->pData )
return;
if ( !p->pPars->nFramesK && Fra_ClassObjRepr(pObj) == pObjRepr )
printf( "Fra_FraigNode(): Error in class refinement!\n" );
assert( p->pPars->nFramesK || Fra_ClassObjRepr(pObj) != pObjRepr );

9
src/aig/fra/fraInd.c
View File

@ -402,16 +402,21 @@ p->timeTrav += clock() - clk2;
Fra_ClassesCountLits(p->pCla), p->pManFraig->nAsserts );
if ( p->pCla->vImps )
printf( "I = %6d. ", Vec_IntSize(p->pCla->vImps) );
printf( "NR = %6d.\n", Aig_ManNodeNum(p->pManFraig) );
printf( "NR = %6d. ", Aig_ManNodeNum(p->pManFraig) );
printf( "\n" );
}
// perform sweeping
p->nSatCallsRecent = 0;
p->nSatCallsSkipped = 0;
clk2 = clock();
Fra_FraigSweep( p );
if ( fVerbose )
{
// PRT( "t", clock() - clk2 );
}
// Sat_SolverPrintStats( stdout, p->pSat );
// remove FRAIG and SAT solver
Aig_ManStop( p->pManFraig ); p->pManFraig = NULL;
sat_solver_delete( p->pSat ); p->pSat = NULL;

5
src/aig/fra/fraSec.c
View File

@ -228,9 +228,11 @@ PRT( "Time", clock() - clk );
}
if ( pNew->nRegs )
pNew = Aig_ManConstReduce( pNew, 0 );
pNew = Aig_ManConstReduce( pNew, 0 );
// perform sequential simulation
if ( pNew->nRegs )
{
clk = clock();
pSml = Fra_SmlSimulateSeq( pNew, 0, 128 * nFrames, 1 + 16/(1+Aig_ManNodeNum(pNew)/1000) );
if ( fVerbose )
@ -250,6 +252,7 @@ PRT( "Time", clock() - clkTotal );
return RetValue;
}
Fra_SmlStop( pSml );
}
}
// get the miter status

8
src/base/abc/abcCheck.c
View File

@ -913,7 +913,7 @@ int Abc_NtkCheckUniqueCoNames( Abc_Ntk_t * pNtk )
***********************************************************************/
int Abc_NtkCheckUniqueCioNames( Abc_Ntk_t * pNtk )
{
Abc_Obj_t * pObj, * pObjCi;
Abc_Obj_t * pObj, * pObjCi, * pFanin;
int i, nCiId, fRetValue = 1;
assert( !Abc_NtkIsNetlist(pNtk) );
Abc_NtkForEachCo( pNtk, pObj, i )
@ -923,9 +923,11 @@ int Abc_NtkCheckUniqueCioNames( Abc_Ntk_t * pNtk )
continue;
pObjCi = Abc_NtkObj( pNtk, nCiId );
assert( !strcmp( Abc_ObjName(pObj), Abc_ObjName(pObjCi) ) );
if ( Abc_ObjFanin0(pObj) != pObjCi )
pFanin = Abc_ObjFanin0(pObj);
if ( pFanin != pObjCi )
{
printf( "Abc_NtkCheck: A CI/CO pair share the name (%s) but do not link directly.\n", Abc_ObjName(pObj) );
printf( "Abc_NtkCheck: A CI/CO pair share the name (%s) but do not link directly. The name of the CO fanin is %s.\n",
Abc_ObjName(pObj), Abc_ObjName(Abc_ObjFanin0(pObj)) );
fRetValue = 0;
}
}

118
src/base/abci/abc.c
View File

@ -164,6 +164,7 @@ static int Abc_CommandPipe ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandSeq ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandUnseq ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandRetime ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDRetime ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandSeqFpga ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandSeqMap ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandSeqSweep ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -333,6 +334,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Sequential", "undc", Abc_CommandUndc, 1 );
// Cmd_CommandAdd( pAbc, "Sequential", "pipe", Abc_CommandPipe, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "retime", Abc_CommandRetime, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "dretime", Abc_CommandDRetime, 1 );
// Cmd_CommandAdd( pAbc, "Sequential", "sfpga", Abc_CommandSeqFpga, 1 );
// Cmd_CommandAdd( pAbc, "Sequential", "smap", Abc_CommandSeqMap, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "ssweep", Abc_CommandSeqSweep, 1 );
@ -6189,7 +6191,7 @@ usage:
int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk, * pNtkRes;
Abc_Ntk_t * pNtk;//, * pNtkRes;
int c;
int nLevels;
int fVerbose;
@ -6204,14 +6206,16 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
extern Abc_Ntk_t * Abc_NtkFilter( Abc_Ntk_t * pNtk );
extern Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose );
extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fVerbose );
extern Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk );
extern int Abc_NtkDarClau( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
fVerbose = 0;
nLevels = 1000;
fVerbose = 1;
nLevels = 1000;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Nvh" ) ) != EOF )
{
@ -6324,13 +6328,14 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
*/
/*
if ( !Abc_NtkIsStrash(pNtk) )
{
fprintf( stdout, "Currently only works for structurally hashed circuits.\n" );
return 0;
}
*/
/*
if ( Abc_NtkIsStrash(pNtk) )
{
fprintf( stdout, "Currently only works for logic circuits.\n" );
@ -6348,6 +6353,9 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
*/
// Abc_NtkDarHaigRecord( pNtk );
Abc_NtkDarClau( pNtk, 1000, fVerbose );
return 0;
usage:
fprintf( pErr, "usage: test [-h]\n" );
@ -10807,6 +10815,106 @@ usage:
// fprintf( pErr, "\t-i : toggle computation of initial state [default = %s]\n", fInitial? "yes": "no" );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandDRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk, * pNtkRes;
int nStepsMax;
int fFastAlgo;
int fVerbose;
int c;
extern Abc_Ntk_t * Abc_NtkDarRetimeF( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
nStepsMax = 100000;
fFastAlgo = 0;
fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Savh" ) ) != EOF )
{
switch ( c )
{
case 'S':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-S\" should be followed by a positive integer.\n" );
goto usage;
}
nStepsMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nStepsMax < 0 )
goto usage;
break;
case 'a':
fFastAlgo ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pNtk == NULL )
{
fprintf( pErr, "Empty network.\n" );
return 1;
}
if ( !Abc_NtkLatchNum(pNtk) )
{
fprintf( pErr, "The network has no latches. Retiming is not performed.\n" );
return 0;
}
if ( !Abc_NtkIsStrash(pNtk) )
{
printf( "This command works only for structrally hashed networks. Run \"st\".\n" );
return 0;
}
// perform the retiming
if ( fFastAlgo )
pNtkRes = Abc_NtkDarRetime( pNtk, nStepsMax, fVerbose );
else
pNtkRes = Abc_NtkDarRetimeF( pNtk, nStepsMax, fVerbose );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Retiming has failed.\n" );
return 1;
}
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
return 0;
usage:
fprintf( pErr, "usage: dretime [-S num] [-avh]\n" );
fprintf( pErr, "\t retimes the current network forward\n" );
fprintf( pErr, "\t-S num : the max number of retiming steps to perform [default = %d]\n", nStepsMax );
fprintf( pErr, "\t-a : enables a fast algorithm [default = %s]\n", fFastAlgo? "yes": "no" );
fprintf( pErr, "\t-v : enables verbose output [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []

107
src/base/abci/abcDar.c
View File

@ -87,7 +87,8 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters )
if ( fRegisters )
{
pMan->nRegs = Abc_NtkLatchNum(pNtk);
pMan->vFlopNums = Vec_IntStartNatural( pMan->nRegs );
// pMan->vFlopNums = Vec_IntStartNatural( pMan->nRegs );
pMan->vFlopNums = NULL;
}
// transfer the pointers to the basic nodes
Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Aig_ManConst1(pMan);
@ -198,7 +199,7 @@ Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
Abc_Ntk_t * pNtkNew;
Abc_Obj_t * pObjNew, * pLatch;
Aig_Obj_t * pObj, * pObjLo, * pObjLi;
int i;
int i, iNodeId;
// assert( Aig_ManRegNum(pMan) != Abc_NtkLatchNum(pNtkOld) );
// perform strashing
pNtkNew = Abc_NtkStartFromNoLatches( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
@ -242,7 +243,12 @@ Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
{
if ( pMan->nAsserts && i == Aig_ManPoNum(pMan) - pMan->nAsserts )
break;
Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) );
iNodeId = Nm_ManFindIdByNameTwoTypes( pNtkNew->pManName, Abc_ObjName(Abc_NtkCo(pNtkNew, i)), ABC_OBJ_PI, ABC_OBJ_BO );
if ( iNodeId >= 0 )
pObjNew = Abc_NtkObj( pNtkNew, iNodeId );
else
pObjNew = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), pObjNew );
}
// if there are assertions, add them
if ( pMan->nAsserts > 0 )
@ -1270,6 +1276,9 @@ Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
if ( pMan == NULL )
return NULL;
// Aig_ManReduceLachesCount( pMan );
if ( pMan->vFlopNums )
Vec_IntFree( pMan->vFlopNums );
pMan->vFlopNums = NULL;
pMan = Rtm_ManRetime( pTemp = pMan, 1, nStepsMax, 0 );
Aig_ManStop( pTemp );
@ -1282,6 +1291,65 @@ Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
return pNtkAig;
}
/**Function*************************************************************
Synopsis [Gives the current ABC network to AIG manager for processing.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkDarRetimeF( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
{
Abc_Ntk_t * pNtkAig;
Aig_Man_t * pMan, * pTemp;
pMan = Abc_NtkToDar( pNtk, 1 );
if ( pMan == NULL )
return NULL;
// Aig_ManReduceLachesCount( pMan );
if ( pMan->vFlopNums )
Vec_IntFree( pMan->vFlopNums );
pMan->vFlopNums = NULL;
pMan = Aig_ManRetimeFrontier( pTemp = pMan, nStepsMax );
Aig_ManStop( pTemp );
// pMan = Aig_ManReduceLaches( pMan, 1 );
// pMan = Aig_ManConstReduce( pMan, 1 );
pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
Aig_ManStop( pMan );
return pNtkAig;
}
/**Function*************************************************************
Synopsis [Gives the current ABC network to AIG manager for processing.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk )
{
Aig_Man_t * pMan;
pMan = Abc_NtkToDar( pNtk, 1 );
if ( pMan == NULL )
return;
// Aig_ManReduceLachesCount( pMan );
if ( pMan->vFlopNums )
Vec_IntFree( pMan->vFlopNums );
pMan->vFlopNums = NULL;
Aig_ManHaigRecord( pMan );
Aig_ManStop( pMan );
}
/**Function*************************************************************
Synopsis [Performs random simulation.]
@ -1322,6 +1390,39 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int fVerbose )
return RetValue;
}
/**Function*************************************************************
Synopsis [Gives the current ABC network to AIG manager for processing.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NtkDarClau( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
{
extern int Fra_Clau( Aig_Man_t * pMan, int nIters, int fVerbose );
Aig_Man_t * pMan;
if ( Abc_NtkPoNum(pNtk) != 1 )
{
printf( "The number of outputs should be 1.\n" );
return 1;
}
pMan = Abc_NtkToDar( pNtk, 1 );
if ( pMan == NULL )
return 1;
// Aig_ManReduceLachesCount( pMan );
if ( pMan->vFlopNums )
Vec_IntFree( pMan->vFlopNums );
pMan->vFlopNums = NULL;
Fra_Clau( pMan, nStepsMax, fVerbose );
Aig_ManStop( pMan );
return 1;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

2
src/base/io/io.c
View File

@ -348,6 +348,8 @@ int IoCommandReadBlif( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pTemp;
pNtk = Io_ReadBlif( pFileName, fCheck );
if ( pNtk == NULL )
return 1;
pNtk = Abc_NtkToLogic( pTemp = pNtk );
Abc_NtkDelete( pTemp );
}

109
src/base/ver/verCore.c
View File

@ -58,6 +58,7 @@ static int Ver_ParseAlways( Ver_Man_t * p, Abc_Ntk_t * pNtk );
static int Ver_ParseInitial( Ver_Man_t * p, Abc_Ntk_t * pNtk );
static int Ver_ParseAssign( Ver_Man_t * p, Abc_Ntk_t * pNtk );
static int Ver_ParseGateStandard( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_GateType_t GateType );
static int Ver_ParseFlopStandard( Ver_Man_t * pMan, Abc_Ntk_t * pNtk );
static int Ver_ParseGate( Ver_Man_t * p, Abc_Ntk_t * pNtk, Mio_Gate_t * pGate );
static int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox );
static int Ver_ParseConnectBox( Ver_Man_t * pMan, Abc_Obj_t * pBox );
@ -472,6 +473,9 @@ int Ver_ParseModule( Ver_Man_t * pMan )
else if ( !strcmp( pWord, "not" ) )
RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_NOT );
else if ( !strcmp( pWord, "dff" ) )
RetValue = Ver_ParseFlopStandard( pMan, pNtk );
else if ( !strcmp( pWord, "assign" ) )
RetValue = Ver_ParseAssign( pMan, pNtk );
else if ( !strcmp( pWord, "always" ) )
@ -1364,6 +1368,105 @@ int Ver_ParseGateStandard( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_GateType_t Ga
return 1;
}
/**Function*************************************************************
Synopsis [Parses one directive.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ver_ParseFlopStandard( Ver_Man_t * pMan, Abc_Ntk_t * pNtk )
{
Ver_Stream_t * p = pMan->pReader;
Abc_Obj_t * pNetLi, * pNetLo, * pLatch;
char * pWord, Symbol;
// convert from the blackbox into the network with local functions representated by AIGs
if ( !Ver_ParseConvertNetwork( pMan, pNtk, pMan->fMapped ) )
return 0;
// this is gate name - throw it away
if ( Ver_StreamPopChar(p) != '(' )
{
sprintf( pMan->sError, "Cannot parse a standard gate (expected opening paranthesis)." );
Ver_ParsePrintErrorMessage( pMan );
return 0;
}
Ver_ParseSkipComments( pMan );
// parse the output name
pWord = Ver_ParseGetName( pMan );
if ( pWord == NULL )
return 0;
// get the net corresponding to this output
pNetLo = Ver_ParseFindNet( pNtk, pWord );
if ( pNetLo == NULL )
{
sprintf( pMan->sError, "Net is missing in gate %s.", pWord );
Ver_ParsePrintErrorMessage( pMan );
return 0;
}
// check if it is the end of gate
Ver_ParseSkipComments( pMan );
Symbol = Ver_StreamPopChar(p);
if ( Symbol == ')' )
{
sprintf( pMan->sError, "Cannot parse the flop." );
Ver_ParsePrintErrorMessage( pMan );
return 0;
}
// skip comma
if ( Symbol != ',' )
{
sprintf( pMan->sError, "Cannot parse the flop." );
Ver_ParsePrintErrorMessage( pMan );
return 0;
}
Ver_ParseSkipComments( pMan );
// parse the output name
pWord = Ver_ParseGetName( pMan );
if ( pWord == NULL )
return 0;
// get the net corresponding to this output
pNetLi = Ver_ParseFindNet( pNtk, pWord );
if ( pNetLi == NULL )
{
sprintf( pMan->sError, "Net is missing in gate %s.", pWord );
Ver_ParsePrintErrorMessage( pMan );
return 0;
}
// check if it is the end of gate
Ver_ParseSkipComments( pMan );
Symbol = Ver_StreamPopChar(p);
if ( Symbol != ')' )
{
sprintf( pMan->sError, "Cannot parse the flop." );
Ver_ParsePrintErrorMessage( pMan );
return 0;
}
// check if it is the end of gate
Ver_ParseSkipComments( pMan );
if ( Ver_StreamPopChar(p) != ';' )
{
sprintf( pMan->sError, "Cannot parse the flop." );
Ver_ParsePrintErrorMessage( pMan );
return 0;
}
// create the latch
pLatch = Ver_ParseCreateLatch( pNtk, pNetLi, pNetLo );
Abc_LatchSetInit0( pLatch );
return 1;
}
/**Function*************************************************************
Synopsis [Returns the index of the given pin the gate.]
@ -1606,6 +1709,12 @@ int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox )
pNode->pCopy = (Abc_Obj_t *)vBundles;
while ( 1 )
{
/*
if ( Ver_StreamGetLineNumber(pMan->pReader) == 5967 )
{
int x = 0;
}
*/
// allocate the bundle (formal name + array of actual nets)
pBundle = ALLOC( Ver_Bundle_t, 1 );
pBundle->pNameFormal = NULL;

3
src/map/fpga/fpgaLib.c
View File

@ -113,10 +113,11 @@ Fpga_LutLib_t * Fpga_LutLibCreate( char * FileName, int fVerbose )
i++;
}
p->LutMax = i-1;
if ( p->LutMax > FPGA_MAX_LEAVES )
{
p->LutMax = FPGA_MAX_LEAVES;
printf( "Warning: LUTs with more than %d input will not be used.\n", FPGA_MAX_LEAVES );
printf( "Warning: LUTs with more than %d inputs will not be used.\n", FPGA_MAX_LEAVES );
}
// check the library

28
src/misc/extra/extraUtilUtil.c
View File

@ -193,7 +193,7 @@ char * Extra_UtilStrsav( char *s )
Synopsis [util_tilde_expand()]
Description []
Description [The code contributed by Niklas Sorensson.]
SideEffects []
@ -203,6 +203,32 @@ char * Extra_UtilStrsav( char *s )
char * Extra_UtilTildeExpand( char *fname )
{
return Extra_UtilStrsav( fname );
/*
int n_tildes = 0;
const char* home;
char* expanded;
int length;
int i, j, k;
for (i = 0; i < (int)strlen(fname); i++)
if (fname[i] == '~') n_tildes++;
home = getenv("HOME");
length = n_tildes * strlen(home) + strlen(fname);
expanded = ALLOC(char, length + 1);
j = 0;
for (i = 0; i < (int)strlen(fname); i++){
if (fname[i] == '~'){
for (k = 0; k < (int)strlen(home); k++)
expanded[j++] = home[k];
}else
expanded[j++] = fname[i];
}
expanded[j] = '\0';
return expanded;
*/
}
/**Function*************************************************************

18
src/sat/bsat/satSolver.h
View File

@ -188,4 +188,22 @@ struct sat_solver_t
int nRoots;
};
static int sat_solver_var_value( sat_solver* s, int v )
{
assert( s->model.ptr != NULL && v < s->size );
return (int)(s->model.ptr[v] == l_True);
}
static int sat_solver_var_literal( sat_solver* s, int v )
{
assert( s->model.ptr != NULL && v < s->size );
return toLitCond( v, s->model.ptr[v] != l_True );
}
static void sat_solver_act_var_clear(sat_solver* s)
{
int i;
for (i = 0; i < s->size; i++)
s->activity[i] = 0.0;
s->var_inc = 1.0;
}
#endif