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

Version abc50915

This commit is contained in:
Alan Mishchenko 2005-09-15 08:01:00 -07:00
parent 0f6eeaea3c
commit 2d782f7bc9
35 changed files with 2103 additions and 809 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
abc.dsp
View File

@ -418,6 +418,10 @@ SOURCE=.\src\base\io\ioWritePla.c
# PROP Default_Filter ""
# Begin Source File
SOURCE=.\src\base\main\libSupport.c
# End Source File
# Begin Source File
SOURCE=.\src\base\main\main.c
# End Source File
# Begin Source File

BIN
abc.opt
View File

Binary file not shown.

1819
abc.plg
View File

File diff suppressed because it is too large Load Diff

2
abc.rc
View File

@ -36,6 +36,7 @@ alias r read
alias ren renode
alias rl read_blif
alias rb read_bench
alias ret retime
alias rp read_pla
alias rv read_verilog
alias rsup read_super mcnc5_old.super
@ -63,4 +64,3 @@ alias sharedsd "b; ren; dsd -g; sw; fx; b"
alias resyn "b; rw; rwz; b; rwz; b"
alias resyn2 "b; rw; rf; b; rw; rwz; b; rfz; rwz; b"
alias thin "rwz; rfz; b; ps"

103
regtest.script Normal file
View File

@ -0,0 +1,103 @@
r examples/apex4.pla
resyn
sharem
fpga
cec
ps
clp
share
resyn
map
cec
ps
r examples/C2670.blif
resyn
fpga
cec
ps
u
map
cec
ps
r examples/frg2.blif
dsd
muxes
cec
clp
share
resyn
map
cec
ps
r examples/pj1.blif
resyn
fpga
cec
ps
u
map
cec
ps
r examples/s38584.bench
resyn
fpga
cec
ps
u
map
cec
ps
r examples/ac.v
resyn
fpga
cec
ps
u
map
cec
ps
r examples/s444.blif
b
esd -v
dsd
cec
ps
r examples/i10.blif
fpga
cec
ps
u
map
cec
ps
r examples/i10.blif
b
fraig_store
resyn
fraig_store
resyn2
fraig_store
fraig_restore
fpga
cec
ps
u
map
cec
ps
time

165
regtest_output.txt Normal file
View File

@ -0,0 +1,165 @@
UC Berkeley, ABC 1.01 (compiled Sep 5 2005 23:36:08)
abc 01> so regtest.script
abc - > r examples/apex4.pla
abc - > resyn
abc - > sharem
abc - > fpga
abc - > cec
Networks are equivalent after fraiging.
abc - > ps
examples/apex4.pla: i/o = 9/ 19 lat = 0 nd = 784 cube = 1985 lev = 5
abc - >
abc - > clp
The shared BDD size is 917 nodes.
abc - > share
abc - > resyn
abc - > map
A simple supergate library is derived from gate library "mcnc_temp.genlib".
Loaded 20 unique 5-input supergates from "mcnc_temp.super". Time = 0.02 sec
abc - > cec
Networks are equivalent after fraiging.
abc - > ps
examples/apex4.pla: i/o = 9/ 19 lat = 0 nd = 1816 area = 4599.00 delay = 11.50 lev = 11
abc - >
abc - > r examples/C2670.blif
abc - > resyn
abc - > fpga
abc - > cec
Networks are equivalent after fraiging.
abc - > ps
C2670.iscas : i/o = 233/ 140 lat = 0 nd = 169 cube = 482 lev = 6
abc - >
abc - > u
abc - > map
abc - > cec
Networks are equivalent after fraiging.
abc - > ps
C2670.iscas : i/o = 233/ 140 lat = 0 nd = 465 area = 1142.00 delay = 15.50 lev = 14
abc - >
abc - > r examples/frg2.blif
abc - > dsd
abc - > muxes
abc - > cec
Networks are equivalent after fraiging.
abc - > clp
The shared BDD size is 1111 nodes.
abc - > share
abc - > resyn
abc - > map
abc - > cec
Networks are equivalent after fraiging.
abc - > ps
frg2 : i/o = 143/ 139 lat = 0 nd = 540 area = 1360.00 delay = 10.10 lev = 9
abc - >
abc - > r examples/pj1.blif
abc - > resyn
abc - > fpga
abc - > cec
Networks are equivalent after fraiging.
abc - > ps
exCombCkt : i/o = 1769/1063 lat = 0 nd = 4730 cube = 10662 lev = 12
abc - >
abc - > u
abc - > map
abc - > cec
Networks are equivalent after fraiging.
abc - > ps
exCombCkt : i/o = 1769/1063 lat = 0 nd = 10396 area = 25170.00 delay = 29.20 lev = 27
abc - >
abc - > r examples/s38584.bench
abc - > resyn
The network has 26 self-feeding latches.
abc - > fpga
abc - > cec
The network has 26 self-feeding latches.
The network has 26 self-feeding latches.
Networks are equivalent after fraiging.
abc - > ps
examples/s38584.bench: i/o = 12/ 278 lat = 1452 nd = 3239 cube = 6769 lev = 7
abc - >
abc - > u
abc - > map
The network has 26 self-feeding latches.
abc - > cec
The network has 26 self-feeding latches.
The network has 26 self-feeding latches.
Networks are equivalent after fraiging.
abc - > ps
examples/s38584.bench: i/o = 12/ 278 lat = 1452 nd = 8522 area = 19305.00 delay = 20.60 lev = 17
abc - >
abc - > r examples/ac.v
abc - > resyn
abc - > fpga
abc - > cec
Networks are equivalent after fraiging.
abc - > ps
ac97_ctrl : i/o = 84/ 48 lat = 2199 nd = 3652 cube = 9391 lev = 3
abc - >
abc - > u
abc - > map
abc - > cec
Networks are equivalent after fraiging.
abc - > ps
ac97_ctrl : i/o = 84/ 48 lat = 2199 nd = 8337 area = 19861.00 delay = 8.10 lev = 8
abc - >
abc - > r examples/s444.blif
abc - > b
abc - > esd -v
The shared BDD size is 181 nodes.
BDD nodes in the transition relation before reordering 557.
BDD nodes in the transition relation after reordering 456.
Reachability analysis completed in 151 iterations.
The number of minterms in the reachable state set = 8865.
BDD nodes in the unreachable states before reordering 124.
BDD nodes in the unreachable states after reordering 113.
abc - > dsd
abc - > cec
Networks are equivalent after fraiging.
abc - > ps
iscas\s444.bench: i/o = 3/ 6 lat = 21 nd = 81 cube = 119 lev = 7
abc - >
abc - > r examples/i10.blif
abc - > fpga
The network was strashed and balanced before FPGA mapping.
abc - > cec
Networks are equivalent after fraiging.
abc - > ps
i10 : i/o = 257/ 224 lat = 0 nd = 741 cube = 1616 lev = 11
abc - > u
abc - > map
The network was strashed and balanced before mapping.
abc - > cec
Networks are equivalent after fraiging.
abc - > ps
i10 : i/o = 257/ 224 lat = 0 nd = 1659 area = 4215.00 delay = 30.80 lev = 27
abc - >
abc - > r examples/i10.blif
abc - > b
abc - > fraig_store
The number of AIG nodes added to storage = 2425.
abc - > resyn
abc - > fraig_store
The number of AIG nodes added to storage = 1678.
abc - > resyn2
abc - > fraig_store
The number of AIG nodes added to storage = 1323.
abc - > fraig_restore
Currently stored 3 networks with 5426 nodes will be fraiged.
abc - > fpga
Performing FPGA mapping with choices.
abc - > cec
Networks are equivalent after fraiging.
abc - > ps
i10 : i/o = 257/ 224 lat = 0 nd = 674 cube = 1498 lev = 10
abc - >
abc - > u
abc - > map
Performing mapping with choices.
abc - > cec
Networks are equivalent after fraiging.
abc - > ps
i10 : i/o = 257/ 224 lat = 0 nd = 1505 area = 3561.00 delay = 25.00 lev = 22
abc - >
abc 109> time
elapse: 77.52 seconds, total: 77.52 seconds
abc 109>

28
src/base/abc/abc.h
View File

@ -249,12 +249,12 @@ static inline int Abc_NtkCiNum( Abc_Ntk_t * pNtk ) { return pN
static inline int Abc_NtkCoNum( Abc_Ntk_t * pNtk ) { return pNtk->vCos->nSize; }
// reading objects
static inline Abc_Obj_t * Abc_NtkObj( Abc_Ntk_t * pNtk, int i ) { assert( i < Vec_PtrSize(pNtk->vObjs) ); return pNtk->vObjs->pArray[i]; }
static inline Abc_Obj_t * Abc_NtkLatch( Abc_Ntk_t * pNtk, int i ) { assert( i < Vec_PtrSize(pNtk->vLats) ); return pNtk->vLats->pArray[i]; }
static inline Abc_Obj_t * Abc_NtkPi( Abc_Ntk_t * pNtk, int i ) { assert( i < Abc_NtkPiNum(pNtk) ); return pNtk->vCis->pArray[i]; }
static inline Abc_Obj_t * Abc_NtkPo( Abc_Ntk_t * pNtk, int i ) { assert( i < Abc_NtkPoNum(pNtk) ); return pNtk->vCos->pArray[i]; }
static inline Abc_Obj_t * Abc_NtkCi( Abc_Ntk_t * pNtk, int i ) { assert( i < Abc_NtkCiNum(pNtk) ); return pNtk->vCis->pArray[i]; }
static inline Abc_Obj_t * Abc_NtkCo( Abc_Ntk_t * pNtk, int i ) { assert( i < Abc_NtkCoNum(pNtk) ); return pNtk->vCos->pArray[i]; }
static inline Abc_Obj_t * Abc_NtkObj( Abc_Ntk_t * pNtk, int i ) { assert( i < Vec_PtrSize(pNtk->vObjs) ); return (Abc_Obj_t *)pNtk->vObjs->pArray[i]; }
static inline Abc_Obj_t * Abc_NtkLatch( Abc_Ntk_t * pNtk, int i ) { assert( i < Vec_PtrSize(pNtk->vLats) ); return (Abc_Obj_t *)pNtk->vLats->pArray[i]; }
static inline Abc_Obj_t * Abc_NtkPi( Abc_Ntk_t * pNtk, int i ) { assert( i < Abc_NtkPiNum(pNtk) ); return (Abc_Obj_t *)pNtk->vCis->pArray[i]; }
static inline Abc_Obj_t * Abc_NtkPo( Abc_Ntk_t * pNtk, int i ) { assert( i < Abc_NtkPoNum(pNtk) ); return (Abc_Obj_t *)pNtk->vCos->pArray[i]; }
static inline Abc_Obj_t * Abc_NtkCi( Abc_Ntk_t * pNtk, int i ) { assert( i < Abc_NtkCiNum(pNtk) ); return (Abc_Obj_t *)pNtk->vCis->pArray[i]; }
static inline Abc_Obj_t * Abc_NtkCo( Abc_Ntk_t * pNtk, int i ) { assert( i < Abc_NtkCoNum(pNtk) ); return (Abc_Obj_t *)pNtk->vCos->pArray[i]; }
// reading data members of the object
static inline unsigned Abc_ObjType( Abc_Obj_t * pObj ) { return pObj->Type; }
@ -293,13 +293,13 @@ static inline int Abc_ObjFanoutNum( Abc_Obj_t * pObj ) { return pO
static inline int Abc_ObjFaninId( Abc_Obj_t * pObj, int i) { return pObj->vFanins.pArray[i].iFan; }
static inline int Abc_ObjFaninId0( Abc_Obj_t * pObj ) { return pObj->vFanins.pArray[0].iFan; }
static inline int Abc_ObjFaninId1( Abc_Obj_t * pObj ) { return pObj->vFanins.pArray[1].iFan; }
static inline Abc_Obj_t * Abc_ObjFanout( Abc_Obj_t * pObj, int i ) { return pObj->pNtk->vObjs->pArray[ pObj->vFanouts.pArray[i].iFan ]; }
static inline Abc_Obj_t * Abc_ObjFanout0( Abc_Obj_t * pObj ) { return pObj->pNtk->vObjs->pArray[ pObj->vFanouts.pArray[0].iFan ]; }
static inline Abc_Obj_t * Abc_ObjFanin( Abc_Obj_t * pObj, int i ) { return pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[i].iFan ]; }
static inline Abc_Obj_t * Abc_ObjFanin0( Abc_Obj_t * pObj ) { return pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[0].iFan ]; }
static inline Abc_Obj_t * Abc_ObjFanin1( Abc_Obj_t * pObj ) { return pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[1].iFan ]; }
static inline Abc_Obj_t * Abc_ObjFanin0Ntk( Abc_Obj_t * pObj ) { return Abc_NtkIsNetlist(pObj->pNtk)? Abc_ObjFanin0(pObj) : pObj; }
static inline Abc_Obj_t * Abc_ObjFanout0Ntk( Abc_Obj_t * pObj ) { return Abc_NtkIsNetlist(pObj->pNtk)? Abc_ObjFanout0(pObj) : pObj; }
static inline Abc_Obj_t * Abc_ObjFanout( Abc_Obj_t * pObj, int i ) { return (Abc_Obj_t *)pObj->pNtk->vObjs->pArray[ pObj->vFanouts.pArray[i].iFan ]; }
static inline Abc_Obj_t * Abc_ObjFanout0( Abc_Obj_t * pObj ) { return (Abc_Obj_t *)pObj->pNtk->vObjs->pArray[ pObj->vFanouts.pArray[0].iFan ]; }
static inline Abc_Obj_t * Abc_ObjFanin( Abc_Obj_t * pObj, int i ) { return (Abc_Obj_t *)pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[i].iFan ]; }
static inline Abc_Obj_t * Abc_ObjFanin0( Abc_Obj_t * pObj ) { return (Abc_Obj_t *)pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[0].iFan ]; }
static inline Abc_Obj_t * Abc_ObjFanin1( Abc_Obj_t * pObj ) { return (Abc_Obj_t *)pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[1].iFan ]; }
static inline Abc_Obj_t * Abc_ObjFanin0Ntk( Abc_Obj_t * pObj ) { return (Abc_Obj_t *)(Abc_NtkIsNetlist(pObj->pNtk)? Abc_ObjFanin0(pObj) : pObj); }
static inline Abc_Obj_t * Abc_ObjFanout0Ntk( Abc_Obj_t * pObj ) { return (Abc_Obj_t *)(Abc_NtkIsNetlist(pObj->pNtk)? Abc_ObjFanout0(pObj) : pObj); }
static inline bool Abc_ObjFaninC( Abc_Obj_t * pObj, int i ) { return pObj->vFanins.pArray[i].fCompl; }
static inline bool Abc_ObjFaninC0( Abc_Obj_t * pObj ) { return pObj->vFanins.pArray[0].fCompl; }
static inline bool Abc_ObjFaninC1( Abc_Obj_t * pObj ) { return pObj->vFanins.pArray[1].fCompl; }
@ -421,6 +421,8 @@ extern bool Abc_AigNodeHasComplFanoutEdge( Abc_Obj_t * pNode );
extern bool Abc_AigNodeHasComplFanoutEdgeTrav( Abc_Obj_t * pNode );
extern void Abc_AigPrintNode( Abc_Obj_t * pNode );
extern bool Abc_AigNodeIsAcyclic( Abc_Obj_t * pNode, Abc_Obj_t * pRoot );
extern void Abc_AigCheckFaninOrder( Abc_Aig_t * pMan );
extern void Abc_AigRehash( Abc_Aig_t * pMan );
/*=== abcAttach.c ==========================================================*/
extern int Abc_NtkAttach( Abc_Ntk_t * pNtk );
/*=== abcBalance.c ==========================================================*/

80
src/base/abc/abcAig.c
View File

@ -409,6 +409,7 @@ Abc_Obj_t * Abc_AigAndCreateFrom( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t *
Key = Abc_HashKey2( p0, p1, pMan->nBins );
pAnd->pNext = pMan->pBins[Key];
pMan->pBins[Key] = pAnd;
pMan->nEntries++;
// create the cuts if defined
// if ( pAnd->pNtk->pManCut )
// Abc_NodeGetCuts( pAnd->pNtk->pManCut, pAnd );
@ -542,6 +543,57 @@ clk = clock();
pMan->nBins = nBinsNew;
}
/**Function*************************************************************
Synopsis [Resizes the hash table of AIG nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_AigRehash( Abc_Aig_t * pMan )
{
Abc_Obj_t ** pBinsNew;
Abc_Obj_t * pEnt, * pEnt2;
Abc_Fan_t * pArray;
unsigned Key;
int Counter, Temp, i;
// allocate a new array
pBinsNew = ALLOC( Abc_Obj_t *, pMan->nBins );
memset( pBinsNew, 0, sizeof(Abc_Obj_t *) * pMan->nBins );
// rehash the entries from the old table
Counter = 0;
for ( i = 0; i < pMan->nBins; i++ )
Abc_AigBinForEachEntrySafe( pMan->pBins[i], pEnt, pEnt2 )
{
// swap the fanins if needed
pArray = pEnt->vFanins.pArray;
if ( pArray[0].iFan > pArray[1].iFan )
{
Temp = pArray[0].iFan;
pArray[0].iFan = pArray[1].iFan;
pArray[1].iFan = Temp;
Temp = pArray[0].fCompl;
pArray[0].fCompl = pArray[1].fCompl;
pArray[1].fCompl = Temp;
}
// rehash the node
Key = Abc_HashKey2( Abc_ObjChild0(pEnt), Abc_ObjChild1(pEnt), pMan->nBins );
pEnt->pNext = pBinsNew[Key];
pBinsNew[Key] = pEnt;
Counter++;
}
assert( Counter == pMan->nEntries );
// replace the table and the parameters
free( pMan->pBins );
pMan->pBins = pBinsNew;
}
@ -1157,6 +1209,34 @@ bool Abc_AigNodeIsAcyclic( Abc_Obj_t * pNode, Abc_Obj_t * pRoot )
return 1;
}
/**Function*************************************************************
Synopsis [Resizes the hash table of AIG nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_AigCheckFaninOrder( Abc_Aig_t * pMan )
{
Abc_Obj_t * pEnt;
int i;
for ( i = 0; i < pMan->nBins; i++ )
Abc_AigBinForEachEntry( pMan->pBins[i], pEnt )
{
if ( Abc_ObjRegular(Abc_ObjChild0(pEnt))->Id > Abc_ObjRegular(Abc_ObjChild1(pEnt))->Id )
{
int i0 = Abc_ObjRegular(Abc_ObjChild0(pEnt))->Id;
int i1 = Abc_ObjRegular(Abc_ObjChild1(pEnt))->Id;
int x = 0;
printf( "Node %d has incorrect ordering of fanins.\n", pEnt->Id );
}
}
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

1
src/base/abc/abcNames.c
View File

@ -283,6 +283,7 @@ void Abc_NtkDupCioNamesTable( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
Abc_NtkLogicStoreName( Abc_NtkPi(pNtkNew,i), Abc_ObjName(pObj) );
Abc_NtkForEachPo( pNtk, pObj, i )
Abc_NtkLogicStoreName( Abc_NtkPo(pNtkNew,i), Abc_ObjName(pObj) );
if ( !Abc_NtkIsSeq(pNtk) )
Abc_NtkForEachLatch( pNtk, pObj, i )
Abc_NtkLogicStoreName( Abc_NtkLatch(pNtkNew,i), Abc_ObjName(pObj) );
}

32
src/base/abc/abcNtk.c
View File

@ -72,7 +72,10 @@ Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func )
else if ( Abc_NtkHasBdd(pNtk) )
pNtk->pManFunc = Cudd_Init( 20, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
else if ( Abc_NtkHasAig(pNtk) )
pNtk->pManFunc = Abc_AigAlloc( pNtk );
{
if ( Abc_NtkIsStrash(pNtk) )
pNtk->pManFunc = Abc_AigAlloc( pNtk );
}
else if ( Abc_NtkHasMapping(pNtk) )
pNtk->pManFunc = Abc_FrameReadLibGen();
else
@ -266,7 +269,7 @@ Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk )
// start the network
pNtkNew = Abc_NtkStartFrom( pNtk, pNtk->ntkType, pNtk->ntkFunc );
// copy the internal nodes
if ( Abc_NtkHasAig(pNtk) )
if ( Abc_NtkIsStrash(pNtk) )
Abc_AigDup( pNtk->pManFunc, pNtkNew->pManFunc );
else
{
@ -278,6 +281,23 @@ Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk )
Abc_NtkForEachObj( pNtk, pObj, i )
Abc_ObjForEachFanin( pObj, pFanin, k )
Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy );
// if it is a sequential networ, transfer attributes on edges
if ( Abc_NtkIsSeq(pNtk) )
{
pNtkNew->vInits = Vec_IntStart( 2 * Abc_NtkObjNumMax(pNtkNew) );
Abc_NtkForEachObj( pNtk, pObj, i )
{
Abc_ObjForEachFanin( pObj, pFanin, k )
{
if ( Abc_ObjFaninC(pObj, k) )
Abc_ObjSetFaninC( pObj->pCopy, k );
if ( Abc_ObjFaninL(pObj, k) > 0 )
Abc_ObjSetFaninL( pObj->pCopy, k, Abc_ObjFaninL(pObj, k) );
}
Vec_IntWriteEntry( pNtkNew->vInits, 2*pObj->pCopy->Id+0, Vec_IntEntry(pNtk->vInits, 2*pObj->Id+0) );
Vec_IntWriteEntry( pNtkNew->vInits, 2*pObj->pCopy->Id+1, Vec_IntEntry(pNtk->vInits, 2*pObj->Id+1) );
}
}
}
// duplicate the EXDC Ntk
if ( pNtk->pExdc )
@ -504,7 +524,8 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
Vec_PtrFree( pNtk->vPtrTemp );
Vec_IntFree( pNtk->vIntTemp );
Vec_StrFree( pNtk->vStrTemp );
if ( pNtk->vInits ) Vec_IntFree( pNtk->vInits );
if ( pNtk->vInits ) Vec_IntFree( pNtk->vInits );
if ( pNtk->pModel ) free( pNtk->pModel );
// free the hash table of Obj name into Obj ID
stmm_free_table( pNtk->tName2Net );
stmm_free_table( pNtk->tObj2Name );
@ -526,7 +547,10 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
else if ( Abc_NtkHasBdd(pNtk) )
Extra_StopManager( pNtk->pManFunc );
else if ( Abc_NtkHasAig(pNtk) )
Abc_AigFree( pNtk->pManFunc );
{
if ( Abc_NtkIsStrash(pNtk) )
Abc_AigFree( pNtk->pManFunc );
}
else if ( !Abc_NtkHasMapping(pNtk) )
assert( 0 );
free( pNtk );

9
src/base/abc/abcObj.c
View File

@ -158,7 +158,7 @@ Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj )
pObjNew->pData = Cudd_bddTransfer(pObj->pNtk->pManFunc, pNtkNew->pManFunc, pObj->pData), Cudd_Ref(pObjNew->pData);
else if ( Abc_NtkHasMapping(pNtkNew) )
pObjNew->pData = pObj->pData;
else if ( Abc_NtkHasAig(pNtkNew) )
else if ( Abc_NtkIsStrash(pNtkNew) )
assert( 0 );
}
}
@ -191,6 +191,13 @@ Abc_Obj_t * Abc_NtkDupConst1( Abc_Ntk_t * pNtkAig, Abc_Ntk_t * pNtkNew )
pConst1 = Abc_AigConst1(pNtkAig->pManFunc);
if ( Abc_ObjFanoutNum(pConst1) > 0 )
pConst1->pCopy = Abc_NodeCreateConst1( pNtkNew );
else
{
// skip the 0-th entry to allow one-to-one match of object IDs
if ( pConst1->Id == 0 && pNtkNew->nNodes == 0 )
Vec_PtrPush( pNtkNew->vObjs, NULL );
}
return pConst1->pCopy;
}

2
src/base/abc/abcShow.c
View File

@ -96,7 +96,7 @@ void Abc_NtkShowAig( Abc_Ntk_t * pNtk )
char FileNameDot[200];
int i;
assert( Abc_NtkIsStrash(pNtk) );
assert( Abc_NtkHasAig(pNtk) );
// create the file name
Abc_ShowGetFileName( pNtk->pName, FileNameDot );
// check that the file can be opened

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

@ -86,6 +86,7 @@ static int Abc_CommandFpga ( Abc_Frame_t * pAbc, int argc, char ** argv
static int Abc_CommandPga ( Abc_Frame_t * pAbc, int argc, char ** argv );
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_CommandCec ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -163,6 +164,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "FPGA mapping", "pga", Abc_CommandPga, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "seq", Abc_CommandSeq, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "unseq", Abc_CommandUnseq, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "retime", Abc_CommandRetime, 1 );
Cmd_CommandAdd( pAbc, "Verification", "cec", Abc_CommandCec, 0 );
@ -949,9 +951,9 @@ int Abc_CommandShowAig( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
if ( !Abc_NtkIsStrash(pNtk) )
if ( !Abc_NtkHasAig(pNtk) )
{
fprintf( pErr, "Visualizing AIG can only be done for AIGs (run \"strash\").\n" );
fprintf( pErr, "Visualizing AIG can only be done for AIGs (run \"strash\" or \"seq\").\n" );
return 1;
}
Abc_NtkShowAig( pNtk );
@ -3906,7 +3908,6 @@ int Abc_CommandSeq( Abc_Frame_t * pAbc, int argc, char ** argv )
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk, * pNtkRes;
int c;
extern Abc_Ntk_t * Abc_NtkSuperChoice( Abc_Ntk_t * pNtk );
pNtk = Abc_FrameReadNet(pAbc);
pOut = Abc_FrameReadOut(pAbc);
@ -3931,8 +3932,8 @@ int Abc_CommandSeq( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
printf( "This command is not yet implemented.\n" );
return 0;
// printf( "This command is not yet implemented.\n" );
// return 0;
if ( !Abc_NtkIsStrash(pNtk) )
{
@ -3959,7 +3960,81 @@ int Abc_CommandSeq( Abc_Frame_t * pAbc, int argc, char ** argv )
usage:
fprintf( pErr, "usage: seq [-h]\n" );
fprintf( pErr, "\t converts AIG into sequential AIG (while sweeping latches)\n" );
fprintf( pErr, "\t converts AIG into sequential AIG\n" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandUnseq( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk, * pNtkRes;
int c;
int fShare;
pNtk = Abc_FrameReadNet(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
fShare = 1;
util_getopt_reset();
while ( ( c = util_getopt( argc, argv, "sh" ) ) != EOF )
{
switch ( c )
{
case 's':
fShare ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pNtk == NULL )
{
fprintf( pErr, "Empty network.\n" );
return 1;
}
if ( !Abc_NtkIsSeq(pNtk) )
{
fprintf( pErr, "Works only for sequential AIG (run \"seq\").\n" );
return 1;
}
// share the latches on the fanout edges
if ( fShare )
Abc_NtkSeqShareFanouts(pNtk);
// get the new network
pNtkRes = Abc_NtkSeqToLogicSop( pNtk );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Converting sequential AIG into an SOP logic network has failed.\n" );
return 1;
}
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
return 0;
usage:
fprintf( pErr, "usage: unseq [-sh]\n" );
fprintf( pErr, "\t converts sequential AIG into an SOP logic network\n" );
fprintf( pErr, "\t-s : toggle sharing latches [default = %s]\n", fShare? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
@ -3991,7 +4066,7 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
pErr = Abc_FrameReadErr(pAbc);
// set defaults
fForward = 0;
fForward = 1;
fBackward = 0;
fInitial = 0;
util_getopt_reset();
@ -4021,10 +4096,6 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
printf( "This command is not yet implemented.\n" );
return 0;
if ( !Abc_NtkIsSeq(pNtk) )
{
fprintf( pErr, "Works only for sequential AIG.\n" );

14
src/base/abci/abcMiter.c
View File

@ -501,7 +501,7 @@ Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial )
pLatch->pCopy = Abc_ObjNotCond( Abc_AigConst1(pNtkFrames->pManFunc), Abc_LatchIsInit0(pLatch) );
}
if ( Counter )
printf( "Warning: %d uninitialized latches are replaced by free variables.\n", Counter );
printf( "Warning: %d uninitialized latches are replaced by free PI variables.\n", Counter );
}
// create the timeframes
@ -521,12 +521,18 @@ Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial )
Abc_NtkForEachLatch( pNtk, pLatch, i )
{
pLatchNew = Abc_NtkLatch(pNtkFrames, i);
Abc_ObjAddFanin( pLatchNew, Abc_ObjFanin0(pLatch)->pCopy );
Abc_ObjAddFanin( pLatchNew, pLatch->pCopy );
Vec_PtrPush( pNtkFrames->vCis, pLatchNew );
Vec_PtrPush( pNtkFrames->vCos, pLatchNew );
Abc_NtkLogicStoreName( pLatchNew, Abc_ObjName(pLatch) );
}
}
Abc_NtkForEachLatch( pNtk, pLatch, i )
pLatch->pNext = NULL;
// remove dangling nodes
Abc_AigCleanup( pNtkFrames->pManFunc );
// make sure that everything is okay
if ( !Abc_NtkCheck( pNtkFrames ) )
{
@ -586,7 +592,9 @@ void Abc_NtkAddFrame( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec_
}
// transfer the implementation of the latch drivers to the latches
Abc_NtkForEachLatch( pNtk, pLatch, i )
pLatch->pCopy = Abc_ObjChild0Copy(pLatch);
pLatch->pNext = Abc_ObjChild0Copy(pLatch);
Abc_NtkForEachLatch( pNtk, pLatch, i )
pLatch->pCopy = pLatch->pNext;
}

2
src/base/abci/abcRefactor.c
View File

@ -144,6 +144,8 @@ pManRef->timeTotal = clock() - clkStart;
Abc_NtkManRefStop( pManRef );
// put the nodes into the DFS order and reassign their IDs
Abc_NtkReassignIds( pNtk );
Abc_AigRehash( pNtk->pManFunc );
// Abc_AigCheckFaninOrder( pNtk->pManFunc );
// fix the levels
if ( fUpdateLevel )
Abc_NtkStopReverseLevels( pNtk );

2
src/base/abci/abcRewrite.c
View File

@ -115,6 +115,8 @@ Rwr_ManAddTimeTotal( pManRwr, clock() - clkStart );
pNtk->pManCut = NULL;
// put the nodes into the DFS order and reassign their IDs
Abc_NtkReassignIds( pNtk );
Abc_AigRehash( pNtk->pManFunc );
// Abc_AigCheckFaninOrder( pNtk->pManFunc );
// fix the levels
if ( fUpdateLevel )
Abc_NtkStopReverseLevels( pNtk );

14
src/base/abci/abcSat.c
View File

@ -52,7 +52,7 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose )
assert( Abc_NtkLatchNum(pNtk) == 0 );
if ( Abc_NtkPoNum(pNtk) > 1 )
fprintf( stdout, "Warning: The miter has more than 1 output. SAT will try to prove all of them.\n" );
fprintf( stdout, "Warning: The miter has %d outputs. SAT will try to prove all of them.\n", Abc_NtkPoNum(pNtk) );
// load clauses into the solver
clk = clock();
@ -65,11 +65,11 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose )
status = solver_simplify(pSat);
// printf( "Simplified the problem to %d variables and %d clauses. ", solver_nvars(pSat), solver_nclauses(pSat) );
// PRT( "Time", clock() - clk );
if ( status == l_False )
if ( status == 0 )
{
solver_delete( pSat );
printf( "The problem is UNSATISFIABLE after simplification.\n" );
return 0;
// printf( "The problem is UNSATISFIABLE after simplification.\n" );
return -1;
}
// solve the miter
@ -146,8 +146,10 @@ solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk )
Abc_NodeAddClauses( pSat, pSop0, pSop1, pNode, vVars );
}
// add clauses for each PO
Abc_NtkForEachPo( pNtk, pNode, i )
Abc_NodeAddClausesTop( pSat, pNode, vVars );
// Abc_NtkForEachPo( pNtk, pNode, i )
// Abc_NodeAddClausesTop( pSat, pNode, vVars );
Abc_NodeAddClausesTop( pSat, Abc_NtkPo(pNtk, Abc_NtkPoNum(pNtk)-1), vVars );
// delete
Vec_StrFree( vCube );

2
src/base/abcs/abcRetImpl.c
View File

@ -224,7 +224,7 @@ void Abc_ObjRetimeForward( Abc_Obj_t * pObj )
Init = ABC_INIT_DC;
// add the init values to the fanouts
Abc_ObjForEachFanout( pObj, pFanout, i )
Abc_ObjFaninLInsertLast( pFanout, Abc_ObjEdgeNum(pFanout, pObj), Init );
Abc_ObjFaninLInsertLast( pFanout, Abc_ObjEdgeNum(pObj, pFanout), Init );
}
/**Function*************************************************************

78
src/base/abcs/abcSeq.c
View File

@ -73,18 +73,21 @@ Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk )
{
Abc_Ntk_t * pNtkNew;
Vec_Ptr_t * vNodes;
Abc_Obj_t * pObj, * pFanin;
int i, Init, nLatches;
Abc_Obj_t * pObj, * pFaninNew;
unsigned Init;
int i, nLatches;
// make sure it is an AIG without self-feeding latches
assert( Abc_NtkIsStrash(pNtk) );
assert( Abc_NtkCountSelfFeedLatches(pNtk) == 0 );
// start the network
Abc_NtkCleanCopy( pNtk );
pNtkNew = Abc_NtkAlloc( ABC_NTK_SEQ, ABC_FUNC_AIG );
// duplicate the name and the spec
pNtkNew->pName = util_strsav(pNtk->pName);
pNtkNew->pSpec = util_strsav(pNtk->pSpec);
// clone const/PIs/POs
Abc_NtkDupObj(pNtkNew, Abc_AigConst1(pNtk->pManFunc) );
pNtkNew->nNodes -= 1;
Abc_NtkForEachPi( pNtk, pObj, i )
Abc_NtkDupObj(pNtkNew, pObj);
Abc_NtkForEachPo( pNtk, pObj, i )
@ -98,8 +101,11 @@ Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk )
vNodes = Abc_AigDfs( pNtk, 0, 0 );
Vec_PtrForEachEntry( vNodes, pObj, i )
{
if ( Abc_ObjFaninNum(pObj) != 2 )
continue;
Abc_NtkDupObj(pNtkNew, pObj);
pObj->pCopy->fPhase = pObj->fPhase; // needed for choices
pObj->pCopy->Level = pObj->Level;
}
// relink the choice nodes
Vec_PtrForEachEntry( vNodes, pObj, i )
@ -114,20 +120,33 @@ Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk )
// skip the constant and the PIs
if ( Abc_ObjFaninNum(pObj) == 0 )
continue;
if ( Abc_ObjIsLatch(pObj) )
continue;
// process the first fanin
pFanin = Abc_NodeAigToSeq( pObj, 0, &nLatches, &Init );
Abc_ObjAddFanin( pObj->pCopy, Abc_ObjGetCopy(pFanin) );
pFaninNew = Abc_NodeAigToSeq( pObj, 0, &nLatches, &Init );
if ( nLatches > ABC_MAX_EDGE_LATCH )
{
printf( "The number of latches on an edge (%d) exceeds the limit (%d).\n", nLatches, ABC_MAX_EDGE_LATCH );
nLatches = ABC_MAX_EDGE_LATCH;
}
Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
Abc_ObjAddFaninL0( pObj->pCopy, nLatches );
Vec_IntWriteEntry( pNtkNew->vInits, 2 * i + 0, Init );
Vec_IntWriteEntry( pNtkNew->vInits, 2 * pObj->pCopy->Id + 0, Init );
if ( Abc_ObjFaninNum(pObj) == 1 )
continue;
// process the second fanin
pFanin = Abc_NodeAigToSeq( pObj, 1, &nLatches, &Init );
Abc_ObjAddFanin( pObj->pCopy, Abc_ObjGetCopy(pFanin) );
pFaninNew = Abc_NodeAigToSeq( pObj, 1, &nLatches, &Init );
if ( nLatches > ABC_MAX_EDGE_LATCH )
{
printf( "The number of latches on an edge (%d) exceeds the limit (%d).\n", nLatches, ABC_MAX_EDGE_LATCH );
nLatches = ABC_MAX_EDGE_LATCH;
}
Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
Abc_ObjAddFaninL1( pObj->pCopy, nLatches );
Vec_IntWriteEntry( pNtkNew->vInits, 2 * i + 1, Init );
Vec_IntWriteEntry( pNtkNew->vInits, 2 * pObj->pCopy->Id + 1, Init );
}
// set the cutset composed of latch drivers
Vec_PtrFree( pNtkNew->vLats );
pNtkNew->vLats = Abc_NtkAigCutsetCopy( pNtk );
// copy EXDC and check correctness
if ( pNtkNew->pExdc )
@ -179,21 +198,24 @@ Vec_Ptr_t * Abc_NtkAigCutsetCopy( Abc_Ntk_t * pNtk )
***********************************************************************/
Abc_Obj_t * Abc_NodeAigToSeq( Abc_Obj_t * pObj, int Num, int * pnLatches, unsigned * pnInit )
{
Abc_Obj_t * pFanin;
Abc_Obj_t * pFanin, * pFaninNew;
Abc_InitType_t Init;
// get the given fanin of the node
pFanin = Abc_ObjFanin( pObj, Num );
// if fanin is the internal node, return its copy in the corresponding polarity
if ( !Abc_ObjIsLatch(pFanin) )
{
*pnLatches = 0;
*pnInit = 0;
return Abc_ObjChild( pObj, Num );
return Abc_ObjNotCond( pFanin->pCopy, Abc_ObjFaninC(pObj, Num) );
}
pFanin = Abc_NodeAigToSeq( pFanin, 0, pnLatches, pnInit );
// get the new initial state
Init = Abc_LatchInit(pObj);
// fanin is a latch
// get the new fanins
pFaninNew = Abc_NodeAigToSeq( pFanin, 0, pnLatches, pnInit );
// get the initial state
Init = Abc_LatchInit(pFanin);
// complement the initial state if the inv is retimed over the latch
if ( Abc_ObjIsComplement(pFanin) )
if ( Abc_ObjIsComplement(pFaninNew) )
{
if ( Init == ABC_INIT_ZERO )
Init = ABC_INIT_ONE;
@ -205,7 +227,7 @@ Abc_Obj_t * Abc_NodeAigToSeq( Abc_Obj_t * pObj, int Num, int * pnLatches, unsign
// update the latch number and initial state
(*pnLatches)++;
(*pnInit) = ((*pnInit) << 2) | Init;
return Abc_ObjNotCond( pFanin, Abc_ObjFaninC(pObj,Num) );
return Abc_ObjNotCond( pFaninNew, Abc_ObjFaninC(pObj, Num) );
}
@ -225,16 +247,24 @@ Abc_Obj_t * Abc_NodeAigToSeq( Abc_Obj_t * pObj, int Num, int * pnLatches, unsign
Abc_Ntk_t * Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk )
{
Abc_Ntk_t * pNtkNew;
Abc_Obj_t * pObj, * pObjNew, * pFaninNew;
Abc_Obj_t * pObj, * pObjNew, * pFaninNew, * pConst1;
int i, nCutNodes, nDigits;
unsigned Init;
int nLatchMax = 0;
assert( Abc_NtkIsSeq(pNtk) );
// start the network without latches
nCutNodes = pNtk->vLats->nSize; pNtk->vLats->nSize = 0;
pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP );
pNtk->vLats->nSize = nCutNodes;
// create the constant node
Abc_NtkDupConst1( pNtk, pNtkNew );
// Abc_NtkDupConst1( pNtk, pNtkNew );
pConst1 = Abc_NtkObj(pNtk,0);
if ( !Abc_ObjIsNode(pConst1) )
pConst1 = NULL;
if ( pConst1 && Abc_ObjFanoutNum(pConst1) > 0 )
pConst1->pCopy = Abc_NodeCreateConst1( pNtkNew );
// duplicate the nodes, create node functions
Abc_NtkForEachNode( pNtk, pObj, i )
{
@ -254,9 +284,12 @@ Abc_Ntk_t * Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk )
// connect the objects
Abc_NtkForEachObj( pNtk, pObj, i )
{
assert( (int)pObj->Id == i );
// skip PIs and the constant
if ( Abc_ObjFaninNum(pObj) == 0 )
continue;
if ( nLatchMax < Abc_ObjFaninL0(pObj) )
nLatchMax = Abc_ObjFaninL0(pObj);
// get the initial states of the latches on the fanin edge of this node
Init = Vec_IntEntry( pNtk->vInits, 2 * pObj->Id );
// create the edge
@ -269,6 +302,8 @@ Abc_Ntk_t * Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk )
Abc_ObjSetFaninC( pObj->pCopy, 0 );
continue;
}
if ( nLatchMax < Abc_ObjFaninL0(pObj) )
nLatchMax = Abc_ObjFaninL0(pObj);
// get the initial states of the latches on the fanin edge of this node
Init = Vec_IntEntry( pNtk->vInits, 2 * pObj->Id + 1 );
// create the edge
@ -276,6 +311,7 @@ Abc_Ntk_t * Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk )
Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
// the complemented edges are subsumed by the node function
}
printf( "The max edge latch num = %d.\n", nLatchMax );
// count the number of digits in the latch names
nDigits = Extra_Base10Log( Abc_NtkLatchNum(pNtkNew) );
// add the latches and their names
@ -289,11 +325,8 @@ Abc_Ntk_t * Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk )
}
// fix the problem with complemented and duplicated CO edges
Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
// duplicate the EXDC network
if ( pNtk->pExdc )
fprintf( stdout, "Warning: EXDC network is not copied.\n" );
if ( !Abc_NtkCheck( pNtkNew ) )
fprintf( stdout, "Abc_NtkSeqToLogic(): Network check has failed.\n" );
fprintf( stdout, "Abc_NtkSeqToLogicSop(): Network check has failed.\n" );
return pNtkNew;
}
@ -313,7 +346,10 @@ Abc_Obj_t * Abc_NodeSeqToLogic( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pFanin, int nLa
{
Abc_Obj_t * pLatch;
if ( nLatches == 0 )
{
assert( pFanin->pCopy );
return pFanin->pCopy;
}
pFanin = Abc_NodeSeqToLogic( pNtkNew, pFanin, nLatches - 1, Init >> 2 );
pLatch = Abc_NtkCreateLatch( pNtkNew );
pLatch->pData = (void *)(Init & 3);

4
src/base/abcs/abcShare.c
View File

@ -25,7 +25,7 @@
////////////////////////////////////////////////////////////////////////
static void Abc_NodeSeqShareFanouts( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes );
static void Abc_NodeSeqShareOne( Abc_Obj_t * pNode, int Init, Vec_Ptr_t * vNodes );
static void Abc_NodeSeqShareOne( Abc_Obj_t * pNode, Abc_InitType_t Init, Vec_Ptr_t * vNodes );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFITIONS ///
@ -124,6 +124,8 @@ void Abc_NodeSeqShareOne( Abc_Obj_t * pNode, Abc_InitType_t Init, Vec_Ptr_t * vN
Vec_PtrClear( vNodes );
Abc_ObjForEachFanout( pNode, pFanout, i )
{
if ( Abc_ObjFanoutL(pNode, pFanout) == 0 )
continue;
Type = Abc_ObjFaninLGetInitLast( pFanout, Abc_ObjEdgeNum(pNode, pFanout) );
if ( Type == Init )
InitNew = Init;

35
src/base/abcs/abcUtils.c
View File

@ -76,6 +76,41 @@ int Abc_NtkSeqLatchNumShared( Abc_Ntk_t * pNtk )
return Counter;
}
/**Function*************************************************************
Synopsis [Generates the printable edge label with the initial state.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
char * Abc_ObjFaninGetInitPrintable( Abc_Obj_t * pObj, int Edge )
{
static char Buffer[ABC_MAX_EDGE_LATCH + 1];
Abc_InitType_t Init;
int nLatches, i;
nLatches = Abc_ObjFaninL( pObj, Edge );
assert( nLatches <= ABC_MAX_EDGE_LATCH );
for ( i = 0; i < nLatches; i++ )
{
Init = Abc_ObjFaninLGetInitOne( pObj, Edge, i );
if ( Init == ABC_INIT_NONE )
Buffer[i] = '_';
else if ( Init == ABC_INIT_ZERO )
Buffer[i] = '0';
else if ( Init == ABC_INIT_ONE )
Buffer[i] = '1';
else if ( Init == ABC_INIT_DC )
Buffer[i] = 'x';
else assert( 0 );
}
Buffer[nLatches] = 0;
return Buffer;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///

47
src/base/abcs/abc_.c
View File

@ -1,47 +0,0 @@
/**CFile****************************************************************
FileName [abc_.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Network and node package.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: abc_.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "abc.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

10
src/base/abcs/abcs.h
View File

@ -164,11 +164,17 @@ static inline void Abc_ObjFaninLSetInit( Abc_Obj_t * pObj, int Edge, unsigned In
Vec_IntWriteEntry( pObj->pNtk->vInits, 2 * pObj->Id + Edge, Init );
}
// getting the init value of the given latch on the edge
static inline Abc_InitType_t Abc_ObjFaninLGetInitOne( Abc_Obj_t * pObj, int Edge, int iLatch )
{
return 0x3 & (Abc_ObjFaninLGetInit(pObj, Edge) >> (2*iLatch));
}
// setting the init value of the given latch on the edge
static inline void Abc_ObjFaninLSetInitOne( Abc_Obj_t * pObj, int Edge, int iLatch, Abc_InitType_t Init )
{
unsigned EntryCur = Abc_ObjFaninLGetInit(pObj, Edge);
unsigned EntryNew = (EntryCur & ~(0x3 << iLatch)) | (Init << iLatch);
unsigned EntryNew = (EntryCur & ~(0x3 << (2*iLatch))) | (Init << (2*iLatch));
assert( iLatch < Abc_ObjFaninL(pObj, Edge) );
Abc_ObjFaninLSetInit( pObj, Edge, EntryNew );
}
@ -305,7 +311,7 @@ extern void Abc_NtkSeqShareFanouts( Abc_Ntk_t * pNtk );
/*=== abcUtil.c ==============================================================*/
extern int Abc_NtkSeqLatchNum( Abc_Ntk_t * pNtk );
extern int Abc_NtkSeqLatchNumShared( Abc_Ntk_t * pNtk );
extern char * Abc_ObjFaninGetInitPrintable( Abc_Obj_t * pObj, int Edge );
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///

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

@ -876,9 +876,9 @@ int IoCommandWriteDot( Abc_Frame_t * pAbc, int argc, char **argv )
return 0;
}
if ( !Abc_NtkIsStrash(pAbc->pNtkCur) )
if ( !Abc_NtkHasAig(pAbc->pNtkCur) )
{
fprintf( stdout, "IoCommandWriteDot(): Currently can only process logic networks with BDDs.\n" );
fprintf( stdout, "IoCommandWriteDot(): Currently can only process AIGs.\n" );
return 0;
}

27
src/base/io/ioWriteDot.c
View File

@ -19,6 +19,7 @@
***********************************************************************/
#include "io.h"
#include "abcs.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@ -191,7 +192,7 @@ void Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow,
fprintf( pFile, " rank = same;\n" );
// the labeling node of this level
fprintf( pFile, " Level%d;\n", LevelMax );
// generat the PO nodes
// generate the PO nodes
Vec_PtrForEachEntry( vNodes, pNode, i )
{
if ( !Abc_ObjIsCo(pNode) )
@ -242,7 +243,19 @@ void Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow,
Vec_PtrForEachEntry( vNodes, pNode, i )
{
if ( !Abc_ObjIsCi(pNode) )
{
// check if the costant node is present
if ( Abc_ObjFaninNum(pNode) == 0 && Abc_ObjFanoutNum(pNode) > 0 )
{
fprintf( pFile, " Node%d [label = \"Const1\"", pNode->Id );
fprintf( pFile, ", shape = ellipse" );
if ( pNode->fMarkB )
fprintf( pFile, ", style = filled" );
fprintf( pFile, ", color = coral, fillcolor = coral" );
fprintf( pFile, "];\n" );
}
continue;
}
fprintf( pFile, " Node%d%s [label = \"%s%s\"", pNode->Id,
(Abc_ObjIsLatch(pNode)? "_out":""), Abc_ObjName(pNode), (Abc_ObjIsLatch(pNode)? "_out":"") );
fprintf( pFile, ", shape = %s", (Abc_ObjIsLatch(pNode)? "box":"triangle") );
@ -277,7 +290,11 @@ void Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow,
fprintf( pFile, "Node%d%s", pNode->Id, (Abc_ObjIsLatch(pNode)? "_in":"") );
fprintf( pFile, " -> " );
fprintf( pFile, "Node%d%s", Abc_ObjFaninId0(pNode), (Abc_ObjIsLatch(Abc_ObjFanin0(pNode))? "_out":"") );
fprintf( pFile, " [style = %s]", Abc_ObjFaninC0(pNode)? "dotted" : "bold" );
fprintf( pFile, " [" );
fprintf( pFile, "style = %s", Abc_ObjFaninC0(pNode)? "dotted" : "bold" );
if ( Abc_ObjFaninL0(pNode) > 0 )
fprintf( pFile, ", label = \"%s\"", Abc_ObjFaninGetInitPrintable(pNode,0) );
fprintf( pFile, "]" );
fprintf( pFile, ";\n" );
}
if ( Abc_ObjFaninNum(pNode) == 1 )
@ -288,7 +305,11 @@ void Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow,
fprintf( pFile, "Node%d", pNode->Id );
fprintf( pFile, " -> " );
fprintf( pFile, "Node%d%s", Abc_ObjFaninId1(pNode), (Abc_ObjIsLatch(Abc_ObjFanin1(pNode))? "_out":"") );
fprintf( pFile, " [style = %s]", Abc_ObjFaninC1(pNode)? "dotted" : "bold" );
fprintf( pFile, " [" );
fprintf( pFile, "style = %s", Abc_ObjFaninC1(pNode)? "dotted" : "bold" );
if ( Abc_ObjFaninL1(pNode) > 0 )
fprintf( pFile, ", label = \"%s\"", Abc_ObjFaninGetInitPrintable(pNode,1) );
fprintf( pFile, "]" );
fprintf( pFile, ";\n" );
}
// generate the edges between the equivalent nodes

164
src/base/main/libSupport.c Normal file
View File

@ -0,0 +1,164 @@
/**CFile****************************************************************
FileName [libSupport.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [The main package.]
Synopsis [Support for external libaries.]
Author [Mike Case]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: libSupport.c,v 1.1 2005/09/06 19:59:51 casem Exp $]
***********************************************************************/
#include "mainInt.h"
#include <stdio.h>
#include <string.h>
#ifndef WIN32
# include <sys/types.h>
# include <dirent.h>
# include <dlfcn.h>
#endif
#define MAX_LIBS 256
static void* libHandles[MAX_LIBS+1]; // will be null terminated
typedef void (*lib_init_end_func) (Abc_Frame_t * pAbc);
////////////////////////////////////////////////////////////////////////////////////////////////////
// This will find all the ABC library extensions in the current directory and load them all.
////////////////////////////////////////////////////////////////////////////////////////////////////
void open_libs() {
int curr_lib = 0;
#ifdef WIN32
printf("Warning: open_libs WIN32 not implemented.\n");
#else
DIR* dirp;
struct dirent* dp;
dirp = opendir(".");
while ((dp = readdir(dirp)) != NULL) {
if ((strncmp("libabc_", dp->d_name, 7) == 0) &&
(strcmp(".so", dp->d_name + strlen(dp->d_name) - 3) == 0)) {
// make sure we don't overflow the handle array
if (curr_lib >= MAX_LIBS) {
printf("Warning: maximum number of ABC libraries (%d) exceeded. Not loading %s.\n",
MAX_LIBS,
dp->d_name);
}
// attempt to load it
else {
char* szPrefixed = malloc((strlen(dp->d_name) + 3) * sizeof(char));
strcpy(szPrefixed, "./");
strcat(szPrefixed, dp->d_name);
libHandles[curr_lib] = dlopen(szPrefixed, RTLD_NOW | RTLD_LOCAL);
// did the load succeed?
if (libHandles[curr_lib] != 0) {
printf("Loaded ABC library: %s (Abc library extension #%d)\n", szPrefixed, curr_lib);
curr_lib++;
} else {
printf("Warning: failed to load ABC library %s:\n\t%s\n", szPrefixed, dlerror());
}
free(szPrefixed);
}
}
}
closedir(dirp);
#endif
// null terminate the list of handles
libHandles[curr_lib] = 0;
}
////////////////////////////////////////////////////////////////////////////////////////////////////
// This will close all open ABC library extensions
////////////////////////////////////////////////////////////////////////////////////////////////////
void close_libs() {
#ifdef WIN32
printf("Warning: close_libs WIN32 not implemented.\n");
#else
int i;
for (i = 0; libHandles[i] != 0; i++) {
if (dlclose(libHandles[i]) != 0) {
printf("Warning: failed to close library %d\n", i);
}
libHandles[i] = 0;
}
#endif
}
////////////////////////////////////////////////////////////////////////////////////////////////////
// This will get a pointer to a function inside of an open library
////////////////////////////////////////////////////////////////////////////////////////////////////
void* get_fnct_ptr(int lib_num, char* sym_name) {
#ifdef WIN32
printf("Warning: get_fnct_ptr WIN32 not implemented.\n");
return 0;
#else
return dlsym(libHandles[lib_num], sym_name);
#endif
}
////////////////////////////////////////////////////////////////////////////////////////////////////
// This will call an initialization function in every open library.
////////////////////////////////////////////////////////////////////////////////////////////////////
void call_inits(Abc_Frame_t* pAbc) {
int i;
lib_init_end_func init_func;
for (i = 0; libHandles[i] != 0; i++) {
init_func = (lib_init_end_func) get_fnct_ptr(i, "abc_init");
if (init_func == 0) {
printf("Warning: Failed to initialize library %d.\n", i);
} else {
(*init_func)(pAbc);
}
}
}
////////////////////////////////////////////////////////////////////////////////////////////////////
// This will call a shutdown function in every open library.
////////////////////////////////////////////////////////////////////////////////////////////////////
void call_ends(Abc_Frame_t* pAbc) {
int i;
lib_init_end_func end_func;
for (i = 0; libHandles[i] != 0; i++) {
end_func = (lib_init_end_func) get_fnct_ptr(i, "abc_end");
if (end_func == 0) {
printf("Warning: Failed to end library %d.\n", i);
} else {
(*end_func)(pAbc);
}
}
}
void Libs_Init(Abc_Frame_t * pAbc)
{
open_libs();
call_inits(pAbc);
}
void Libs_End(Abc_Frame_t * pAbc)
{
call_ends(pAbc);
// It's good practice to close our libraries at this point, but this can mess up any backtrace printed by Valgind.
// close_libs();
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

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

@ -216,7 +216,7 @@ int main( int argc, char * argv[] )
}
// if the memory should be freed, quit packages
if ( fStatus == -2 )
if ( fStatus < 0 )
{
// perform uninitializations
Abc_FrameEnd( pAbc );

6
src/base/main/mainInit.c
View File

@ -14,7 +14,7 @@
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: mainInit.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
Revision [$Id: mainInit.c,v 1.3 2005/09/14 22:53:37 casem Exp $]
***********************************************************************/
@ -38,6 +38,8 @@ extern void Mio_Init( Abc_Frame_t * pAbc );
extern void Mio_End ( Abc_Frame_t * pAbc );
extern void Super_Init( Abc_Frame_t * pAbc );
extern void Super_End ( Abc_Frame_t * pAbc );
extern void Libs_Init(Abc_Frame_t * pAbc);
extern void Libs_End(Abc_Frame_t * pAbc);
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFITIONS ///
@ -63,6 +65,7 @@ void Abc_FrameInit( Abc_Frame_t * pAbc )
Map_Init( pAbc );
Mio_Init( pAbc );
Super_Init( pAbc );
Libs_Init( pAbc );
}
@ -86,6 +89,7 @@ void Abc_FrameEnd( Abc_Frame_t * pAbc )
Map_End( pAbc );
Mio_End( pAbc );
Super_End( pAbc );
Libs_End( pAbc );
}

3
src/base/main/module.make
View File

@ -1,4 +1,5 @@
SRC += src/base/main/main.c \
src/base/main/mainFrame.c \
src/base/main/mainInit.c \
src/base/main/mainUtils.c
src/base/main/mainUtils.c \
src/base/main/libSupport.c

4
src/bdd/dsd/dsdProc.c
View File

@ -1255,7 +1255,7 @@ EXIT:
s_CacheEntries++;
#if 0
/*
if ( dsdKernelVerifyDecomposition(dd, pThis) == 0 )
{
// write the function, for which verification does not work
@ -1277,7 +1277,7 @@ EXIT:
cuddWriteFunctionSop( stdout, dd, zNewFunc, -1, dd->size, "1", s_pVarMask );
Cudd_RecursiveDerefZdd( dd, zNewFunc );
}
#endif
*/
}

1
src/map/pga/pgaMan.c
View File

@ -75,6 +75,7 @@ Pga_Man_t * Pga_ManStart( Pga_Params_t * pParams )
{
printf( "The nodes of the network are not DFS ordered.\n" );
// Abc_NtkReassignIds( pNtk );
// Abc_AigRehash( pNtk->pManFunc );
return NULL;
}
// make sure there are no dangling nodes (unless they are choices)

12
src/misc/vec/vecVec.h
View File

@ -50,13 +50,13 @@ struct Vec_Vec_t_
// iterators through levels
#define Vec_VecForEachLevel( vGlob, vVec, i ) \
for ( i = 0; (i < Vec_VecSize(vGlob)) && (((vVec) = Vec_VecEntry(vGlob, i)), 1); i++ )
for ( i = 0; (i < Vec_VecSize(vGlob)) && (((vVec) = (Vec_Ptr_t*)Vec_VecEntry(vGlob, i)), 1); i++ )
#define Vec_VecForEachLevelStart( vGlob, vVec, i, LevelStart ) \
for ( i = LevelStart; (i < Vec_VecSize(vGlob)) && (((vVec) = Vec_VecEntry(vGlob, i)), 1); i++ )
for ( i = LevelStart; (i < Vec_VecSize(vGlob)) && (((vVec) = (Vec_Ptr_t*)Vec_VecEntry(vGlob, i)), 1); i++ )
#define Vec_VecForEachLevelStartStop( vGlob, vVec, i, LevelStart, LevelStop ) \
for ( i = LevelStart; (i <= LevelStop) && (((vVec) = Vec_VecEntry(vGlob, i)), 1); i++ )
for ( i = LevelStart; (i <= LevelStop) && (((vVec) = (Vec_Ptr_t*)Vec_VecEntry(vGlob, i)), 1); i++ )
#define Vec_VecForEachLevelReverse( vGlob, vVec, i ) \
for ( i = Vec_VecSize(vGlob) - 1; (i >= 0) && (((vVec) = Vec_VecEntry(vGlob, i)), 1); i-- )
for ( i = Vec_VecSize(vGlob) - 1; (i >= 0) && (((vVec) = (Vec_Ptr_t*)Vec_VecEntry(vGlob, i)), 1); i-- )
// iteratores through entries
#define Vec_VecForEachEntry( vGlob, pEntry, i, k ) \
@ -234,7 +234,7 @@ static inline void Vec_VecPush( Vec_Vec_t * p, int Level, void * Entry )
p->pArray[i] = Vec_PtrAlloc( 0 );
p->nSize = Level + 1;
}
Vec_PtrPush( p->pArray[Level], Entry );
Vec_PtrPush( (Vec_Ptr_t*)p->pArray[Level], Entry );
}
/**Function*************************************************************
@ -253,7 +253,7 @@ static inline void Vec_VecPushUnique( Vec_Vec_t * p, int Level, void * Entry )
if ( p->nSize < Level + 1 )
Vec_VecPush( p, Level, Entry );
else
Vec_PtrPushUnique( p->pArray[Level], Entry );
Vec_PtrPushUnique( (Vec_Ptr_t*)p->pArray[Level], Entry );
}
////////////////////////////////////////////////////////////////////////

94
src/sat/asat/solver.c
View File

@ -317,11 +317,11 @@ static void clause_remove(solver* s, clause* c)
vec_remove(solver_read_wlist(s,neg(lits[1])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[0])));
if (clause_learnt(c)){
s->stats.learnts--;
s->stats.learnts_literals -= clause_size(c);
s->solver_stats.learnts--;
s->solver_stats.learnts_literals -= clause_size(c);
}else{
s->stats.clauses--;
s->stats.clauses_literals -= clause_size(c);
s->solver_stats.clauses--;
s->solver_stats.clauses_literals -= clause_size(c);
}
free(c);
@ -409,7 +409,7 @@ static inline bool enqueue(solver* s, lit l, clause* from)
s->trail[s->qtail++] = l;
order_assigned(s, v);
return true;
return 1;
}
}
@ -465,8 +465,8 @@ static void solver_record(solver* s, vec* cls)
if (c != 0) {
vec_push(&s->learnts,(void*)c);
act_clause_bump(s,c);
s->stats.learnts++;
s->stats.learnts_literals += vec_size(cls);
s->solver_stats.learnts++;
s->solver_stats.learnts_literals += vec_size(cls);
}
}
@ -521,7 +521,7 @@ static bool solver_lit_removable(solver* s, lit l, int minl)
for (j = top; j < vec_size(&s->tagged); j++)
tags[tagged[j]] = l_Undef;
vec_resize(&s->tagged,top);
return false;
return 0;
}
}
}else{
@ -541,14 +541,14 @@ static bool solver_lit_removable(solver* s, lit l, int minl)
for (j = top; j < vec_size(&s->tagged); j++)
tags[tagged[j]] = l_Undef;
vec_resize(&s->tagged,top);
return false;
return 0;
}
}
}
}
}
return true;
return 1;
}
static void solver_analyze(solver* s, clause* c, vec* learnt)
@ -627,9 +627,9 @@ static void solver_analyze(solver* s, clause* c, vec* learnt)
}
// update size of learnt + statistics
s->stats.max_literals += vec_size(learnt);
s->solver_stats.max_literals += vec_size(learnt);
vec_resize(learnt,j);
s->stats.tot_literals += j;
s->solver_stats.tot_literals += j;
// clear tags
tagged = (int*)vec_begin(&s->tagged);
@ -684,7 +684,7 @@ clause* solver_propagate(solver* s)
clause **end = begin + vec_size(ws);
clause **i, **j;
s->stats.propagations++;
s->solver_stats.propagations++;
s->simpdb_props--;
//printf("checking lit %d: "L_LIT"\n", vec_size(ws), L_lit(p));
@ -746,7 +746,7 @@ clause* solver_propagate(solver* s)
i++;
}
s->stats.inspects += j - (clause**)vec_begin(ws);
s->solver_stats.inspects += j - (clause**)vec_begin(ws);
vec_resize(ws,j - (clause**)vec_begin(ws));
}
@ -796,7 +796,7 @@ static lbool solver_search(solver* s, int nof_conflicts, int nof_learnts)
assert(s->root_level == solver_dlevel(s));
s->stats.starts++;
s->solver_stats.starts++;
s->var_decay = (float)(1 / var_decay );
s->cla_decay = (float)(1 / clause_decay);
vec_resize(&s->model,0);
@ -811,7 +811,7 @@ static lbool solver_search(solver* s, int nof_conflicts, int nof_learnts)
#ifdef VERBOSEDEBUG
printf(L_IND"**CONFLICT**\n", L_ind);
#endif
s->stats.conflicts++; conflictC++;
s->solver_stats.conflicts++; conflictC++;
if (solver_dlevel(s) == s->root_level){
vec_delete(&learnt_clause);
return l_False;
@ -845,7 +845,7 @@ static lbool solver_search(solver* s, int nof_conflicts, int nof_learnts)
solver_reducedb(s);
// New variable decision:
s->stats.decisions++;
s->solver_stats.decisions++;
next = order_select(s,(float)random_var_freq);
if (next == var_Undef){
@ -910,17 +910,17 @@ solver* solver_new(void)
s->binary->size_learnt = (2 << 1);
s->verbosity = 0;
s->stats.starts = 0;
s->stats.decisions = 0;
s->stats.propagations = 0;
s->stats.inspects = 0;
s->stats.conflicts = 0;
s->stats.clauses = 0;
s->stats.clauses_literals = 0;
s->stats.learnts = 0;
s->stats.learnts_literals = 0;
s->stats.max_literals = 0;
s->stats.tot_literals = 0;
s->solver_stats.starts = 0;
s->solver_stats.decisions = 0;
s->solver_stats.propagations = 0;
s->solver_stats.inspects = 0;
s->solver_stats.conflicts = 0;
s->solver_stats.clauses = 0;
s->solver_stats.clauses_literals = 0;
s->solver_stats.learnts = 0;
s->solver_stats.learnts_literals = 0;
s->solver_stats.max_literals = 0;
s->solver_stats.tot_literals = 0;
return s;
}
@ -973,7 +973,7 @@ bool solver_addclause(solver* s, lit* begin, lit* end)
lbool* values;
lit last;
if (begin == end) return false;
if (begin == end) return 0;
//printlits(begin,end); printf("\n");
// insertion sort
@ -996,7 +996,7 @@ bool solver_addclause(solver* s, lit* begin, lit* end)
//printf("lit: "L_LIT", value = %d\n", L_lit(*i), (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]));
lbool sig = !lit_sign(*i); sig += sig - 1;
if (*i == neg(last) || sig == values[lit_var(*i)])
return true; // tautology
return 1; // tautology
else if (*i != last && values[lit_var(*i)] == l_Undef)
last = *j++ = *i;
}
@ -1004,7 +1004,7 @@ bool solver_addclause(solver* s, lit* begin, lit* end)
//printf("final: "); printlits(begin,j); printf("\n");
if (j == begin) // empty clause
return false;
return 0;
else if (j - begin == 1) // unit clause
return enqueue(s,*begin,(clause*)0);
@ -1012,10 +1012,10 @@ bool solver_addclause(solver* s, lit* begin, lit* end)
vec_push(&s->clauses,clause_new(s,begin,j,0));
s->stats.clauses++;
s->stats.clauses_literals += j - begin;
s->solver_stats.clauses++;
s->solver_stats.clauses_literals += j - begin;
return true;
return 1;
}
@ -1027,10 +1027,10 @@ bool solver_simplify(solver* s)
assert(solver_dlevel(s) == 0);
if (solver_propagate(s) != 0)
return false;
return 0;
if (s->qhead == s->simpdb_assigns || s->simpdb_props > 0)
return true;
return 1;
reasons = s->reasons;
for (type = 0; type < 2; type++){
@ -1050,13 +1050,13 @@ bool solver_simplify(solver* s)
s->simpdb_assigns = s->qhead;
// (shouldn't depend on 'stats' really, but it will do for now)
s->simpdb_props = (int)(s->stats.clauses_literals + s->stats.learnts_literals);
s->simpdb_props = (int)(s->solver_stats.clauses_literals + s->solver_stats.learnts_literals);
return true;
return 1;
}
int solver_solve(solver* s, lit* begin, lit* end, int nSeconds)
bool solver_solve(solver* s, lit* begin, lit* end, int nSeconds)
{
double nof_conflicts = 100;
double nof_learnts = solver_nclauses(s) / 3;
@ -1068,7 +1068,7 @@ int solver_solve(solver* s, lit* begin, lit* end, int nSeconds)
for (i = begin; i < end; i++)
if ((lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]) == l_False || (assume(s,*i), solver_propagate(s) != 0)){
solver_canceluntil(s,0);
return false; }
return l_False; }
s->root_level = solver_dlevel(s);
@ -1080,17 +1080,17 @@ int solver_solve(solver* s, lit* begin, lit* end, int nSeconds)
}
while (status == l_Undef){
double Ratio = (s->stats.learnts == 0)? 0.0 :
s->stats.learnts_literals / (double)s->stats.learnts;
double Ratio = (s->solver_stats.learnts == 0)? 0.0 :
s->solver_stats.learnts_literals / (double)s->solver_stats.learnts;
if (s->verbosity >= 1){
printf("| %9.0f | %7.0f %8.0f | %7.0f %7.0f %8.0f %7.1f | %6.3f %% |\n",
(double)s->stats.conflicts,
(double)s->stats.clauses,
(double)s->stats.clauses_literals,
(double)s->solver_stats.conflicts,
(double)s->solver_stats.clauses,
(double)s->solver_stats.clauses_literals,
(double)nof_learnts,
(double)s->stats.learnts,
(double)s->stats.learnts_literals,
(double)s->solver_stats.learnts,
(double)s->solver_stats.learnts_literals,
Ratio,
s->progress_estimate*100);
fflush(stdout);

9
src/sat/asat/solver.h
View File

@ -36,16 +36,13 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#define bool int
#endif
static const bool true = 1;
static const bool false = 0;
typedef int lit;
typedef char lbool;
#ifdef _WIN32
typedef signed __int64 sint64; // compatible with MS VS 6.0
typedef signed __int64 sint64; // compatible with MS VS 6.0
#else
typedef long long sint64;
typedef long long sint64;
#endif
static const int var_Undef = -1;
@ -132,7 +129,7 @@ struct solver_t
double progress_estimate;
int verbosity; // Verbosity level. 0=silent, 1=some progress report, 2=everything
stats stats;
stats solver_stats;
};
#endif

40
src/sat/fraig/fraigSat.c
View File

@ -123,26 +123,32 @@ void Fraig_ManProveMiter( Fraig_Man_t * p )
int Fraig_ManCheckMiter( Fraig_Man_t * p )
{
Fraig_Node_t * pNode;
int i;
FREE( p->pModel );
// get the output node (it can be complemented!)
pNode = p->vOutputs->pArray[0];
// if the miter is constant 0, the problem is UNSAT
if ( pNode == Fraig_Not(p->pConst1) )
return 1;
// consider the special case when the miter is constant 1
if ( pNode == p->pConst1 )
for ( i = 0; i < p->vOutputs->nSize; i++ )
{
// in this case, any counter example will do to distinquish it from constant 0
// here we pick the counter example composed of all zeros
p->pModel = Fraig_ManAllocCounterExample( p );
return 0;
// get the output node (it can be complemented!)
pNode = p->vOutputs->pArray[i];
// if the miter is constant 0, the problem is UNSAT
if ( pNode == Fraig_Not(p->pConst1) )
continue;
// consider the special case when the miter is constant 1
if ( pNode == p->pConst1 )
{
// in this case, any counter example will do to distinquish it from constant 0
// here we pick the counter example composed of all zeros
p->pModel = Fraig_ManAllocCounterExample( p );
return 0;
}
// save the counter example
p->pModel = Fraig_ManSaveCounterExample( p, pNode );
// if the model is not found, return undecided
if ( p->pModel == NULL )
return -1;
else
return 0;
}
// save the counter example
p->pModel = Fraig_ManSaveCounterExample( p, pNode );
// if the model is not found, return undecided
if ( p->pModel == NULL )
return -1;
return 0;
return 1;
}