Skip to content

A
abc
Commit 457e243e by Alan Mishchenko
Options

Version abc51222

parent 37f19d8d
Showing with 1837 additions and 429 deletions
Makefile
......@@ -10,7 +10,7 @@ MODULES := src/base/abc src/base/abci src/base/seq src/base/cmd src/base/io src/
src/bdd/cudd src/bdd/dsd src/bdd/epd src/bdd/mtr src/bdd/parse src/bdd/reo \
src/map/fpga src/map/pga src/map/mapper src/map/mio src/map/super \
src/misc/extra src/misc/mvc src/misc/st src/misc/util src/misc/vec \
src/opt/cut src/opt/dec src/opt/fxu src/opt/rwr src/opt/sim \
src/opt/cut src/opt/dec src/opt/fxu src/opt/rwr src/opt/sim src/opt/xyz \
src/sat/asat src/sat/csat src/sat/msat src/sat/fraig
default: $(PROG)
......
abc.dsp
......@@ -460,6 +460,10 @@ SOURCE=.\src\base\io\ioWriteList.c
SOURCE=.\src\base\io\ioWritePla.c
# End Source File
# Begin Source File
SOURCE=.\src\base\io\ioWriteVerilog.c
# End Source File
# End Group
# Begin Group "main"
......@@ -934,7 +938,7 @@ SOURCE=.\src\sat\msat\msatMem.c
# End Source File
# Begin Source File
SOURCE=.\src\sat\msat\msatOrderH.c
SOURCE=.\src\sat\msat\msatOrderJ.c
# End Source File
# Begin Source File
......@@ -1265,6 +1269,50 @@ SOURCE=.\src\opt\sim\simSymStr.c
SOURCE=.\src\opt\sim\simUtils.c
# End Source File
# End Group
# Begin Group "xyz"
# PROP Default_Filter ""
# Begin Source File
SOURCE=.\src\opt\xyz\xyz.h
# End Source File
# Begin Source File
SOURCE=.\src\opt\xyz\xyzBuild.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\xyz\xyzCore.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\xyz\xyzInt.h
# End Source File
# Begin Source File
SOURCE=.\src\opt\xyz\xyzMan.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\xyz\xyzMinEsop.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\xyz\xyzMinMan.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\xyz\xyzMinSop.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\xyz\xyzMinUtil.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\xyz\xyzTest.c
# End Source File
# End Group
# End Group
# Begin Group "map"
......
abc.opt
No preview for this file type
abc.rc
......@@ -59,6 +59,7 @@ alias u undo
alias wb write_blif
alias wl write_blif
alias wp write_pla
alias wv write_verilog
# standard scripts
alias cnf "st; ren -c; write_cnf"
......@@ -72,4 +73,5 @@ alias resyn2 "b; rw; rf; b; rw; rwz; b; rfz; rwz; b"
alias compress "b; rw -l; rwz -l; b; rwz -l; b"
alias compress2 "b; rw -l; rf -l; b; rw -l; rwz -l; b; rfz -l; rwz -l; b"
alias choice "fraig_store; resyn; fraig_store; resyn2; fraig_store; fraig_restore"
alias choice2 "fraig_store; balance; fraig_store; resyn; fraig_store; resyn2; fraig_store; resyn2; fraig_store; fraig_restore"
examples/ac.v deleted 100644 → 0
This source diff could not be displayed because it is too large. You can view the blob instead.
examples/pj1.blif deleted 100644 → 0
This source diff could not be displayed because it is too large. You can view the blob instead.
examples/s38417.blif deleted 100644 → 0
This source diff could not be displayed because it is too large. You can view the blob instead.
examples/s38584.bench deleted 100644 → 0
This source diff could not be displayed because it is too large. You can view the blob instead.
examples/s444.blif deleted 100644 → 0
.model s444
.inputs G0 G1 G2
.outputs G118 G167 G107 G119 G168 G108
.latch G11_in G11 0
.latch G12_in G12 0
.latch G13_in G13 0
.latch G14_in G14 0
.latch G15_in G15 0
.latch G16_in G16 0
.latch G17_in G17 0
.latch G18_in G18 0
.latch G19_in G19 0
.latch G20_in G20 0
.latch G21_in G21 0
.latch G22_in G22 0
.latch G23_in G23 0
.latch G24_in G24 0
.latch G25_in G25 0
.latch G26_in G26 0
.latch G27_in G27 0
.latch G28_in G28 0
.latch G29_in G29 0
.latch G30_in G30 0
.latch G31_in G31 0
.names G12 G13 [25]
00 1
.names G11 [25] [26]
01 1
.names G14 [26] [27]
10 1
.names G0 G11 [28]
00 1
.names [27] [28] G11_in
01 1
.names G11 G12 [30]
11 1
.names G12 [30] [31]
10 1
.names G11 [30] [32]
10 1
.names [31] [32] [33]
00 1
.names G0 [33] [34]
00 1
.names [27] [34] G12_in
01 1
.names G13 [30] [36]
11 1
.names G13 [36] [37]
10 1
.names [30] [36] [38]
10 1
.names [37] [38] [39]
00 1
.names G0 [39] [40]
00 1
.names [27] [40] G13_in
01 1
.names G12 G13 [42]
11 1
.names G11 [42] [43]
11 1
.names G14 [43] [44]
11 1
.names G14 [44] [45]
10 1
.names [43] [44] [46]
10 1
.names [45] [46] [47]
00 1
.names G0 [47] [48]
00 1
.names [27] [48] G14_in
01 1
.names G31 [27] [50]
00 1
.names G16 G17 [51]
00 1
.names G15 [51] [52]
01 1
.names [50] [52] [53]
00 1
.names G18 [53] [54]
11 1
.names G15 [50] [55]
10 1
.names G15 [55] [56]
10 1
.names [50] [55] [57]
00 1
.names [56] [57] [58]
00 1
.names G0 [58] [59]
00 1
.names [54] [59] G15_in
01 1
.names G16 [55] [61]
11 1
.names G16 [61] [62]
10 1
.names [55] [61] [63]
10 1
.names [62] [63] [64]
00 1
.names G0 [64] [65]
00 1
.names [54] [65] G16_in
01 1
.names G16 [50] [67]
10 1
.names G15 [67] [68]
11 1
.names G17 [68] [69]
11 1
.names G17 [69] [70]
10 1
.names [68] [69] [71]
10 1
.names [70] [71] [72]
00 1
.names G0 [72] [73]
00 1
.names [54] [73] G17_in
01 1
.names G15 G16 [75]
11 1
.names G17 [50] [76]
10 1
.names [75] [76] [77]
11 1
.names G18 [77] [78]
11 1
.names G18 [78] [79]
10 1
.names [77] [78] [80]
10 1
.names [79] [80] [81]
00 1
.names G0 [81] [82]
00 1
.names [54] [82] G18_in
01 1
.names G20 G21 [84]
00 1
.names G19 [84] [85]
01 1
.names [54] [85] [86]
10 1
.names G22 [86] [87]
11 1
.names G19 [54] [88]
11 1
.names G19 [88] [89]
10 1
.names [54] [88] [90]
10 1
.names [89] [90] [91]
00 1
.names G0 [91] [92]
00 1
.names [87] [92] G19_in
01 1
.names G20 [88] [94]
11 1
.names G20 [94] [95]
10 1
.names [88] [94] [96]
10 1
.names [95] [96] [97]
00 1
.names G0 [97] [98]
00 1
.names [87] [98] G20_in
01 1
.names G20 [54] [100]
11 1
.names G19 [100] [101]
11 1
.names G21 [101] [102]
11 1
.names G21 [102] [103]
10 1
.names [101] [102] [104]
10 1
.names [103] [104] [105]
00 1
.names G0 [105] [106]
00 1
.names [87] [106] G21_in
01 1
.names G19 G20 [108]
11 1
.names G21 [54] [109]
11 1
.names [108] [109] [110]
11 1
.names G22 [110] [111]
11 1
.names G22 [111] [112]
10 1
.names [110] [111] [113]
10 1
.names [112] [113] [114]
00 1
.names G0 [114] [115]
00 1
.names [87] [115] G22_in
01 1
.names G2 G23 [117]
00 1
.names G2 G23 [118]
11 1
.names [117] [118] [119]
00 1
.names G0 [119] G23_in
01 1
.names G20 G21 [121]
01 1
.names G0 G23 [122]
01 1
.names [121] [122] [123]
11 1
.names G19 [123] [124]
01 1
.names G21 G22 [126]
10 1
.names G19 G20 [125]
10 1
.names G23 [125] [127]
01 1
.names [126] [127] [128]
11 1
.names G0 G24 [129]
01 1
.names [128] [129] [130]
01 1
.names [124] [130] [131]
00 1
.names G22 G23 [132]
00 1
.names [125] [132] [133]
11 1
.names G24 [133] [134]
10 1
.names G19 G20 [135]
00 1
.names G23 [135] [136]
11 1
.names G22 G23 [137]
11 1
.names [136] [137] [138]
00 1
.names G0 G21 [139]
01 1
.names [138] [139] [140]
11 1
.names [134] [140] G25_in
01 1
.names G19 G22 [142]
01 1
.names G0 [142] [143]
01 1
.names G0 [108] [144]
01 1
.names [143] [144] [145]
00 1
.names [129] [139] [146]
00 1
.names [145] [146] G26_in
11 1
.names G21 G24 [148]
00 1
.names [125] [148] [149]
11 1
.names G21 G22 [150]
00 1
.names G24 [150] [151]
01 1
.names G0 [151] [152]
00 1
.names [149] [152] [153]
01 1
.names G0 G22 [154]
01 1
.names [135] [154] [155]
11 1
.names [146] [155] [156]
10 1
.names [131] [156] [157]
00 1
.names G17 [157] [158]
01 1
.names [131] [156] [159]
10 1
.names [158] [159] G28_in
00 1
.names [122] [126] [161]
11 1
.names G21 G22 [162]
01 1
.names G0 [162] [163]
01 1
.names [161] [163] [164]
00 1
.names G20 [164] [165]
00 1
.names G19 [165] [166]
01 1
.names [130] [166] [167]
00 1
.names [131] [167] [168]
00 1
.names G17 [168] [169]
01 1
.names [131] [167] [170]
10 1
.names [169] [170] G29_in
00 1
.names G20 G21 [172]
10 1
.names G0 G24 [173]
00 1
.names [172] [173] [174]
11 1
.names G19 [174] G30_in
11 1
.names G1 G31 [176]
00 1
.names G1 G31 [177]
11 1
.names [176] [177] [178]
00 1
.names G0 [178] G31_in
01 1
.names [131] G24_in
0 1
.names [153] G27_in
0 1
.names G27 G118
1 1
.names G29 G167
0 1
.names G25 G107
1 1
.names G28 G119
0 1
.names G30 G168
1 1
.names G26 G108
1 1
.end
examples/s6669.blif deleted 100644 → 0
This source diff could not be displayed because it is too large. You can view the blob instead.
regtest_output.txt
......@@ -87,4 +87,4 @@ The network was strashed and balanced before mapping.
s5378 : i/o = 35/ 49 lat = 364 nd = 1084 area = 2453.00 delay = 11.70 lev = 11
Networks are equivalent after fraiging.
abc - > time
elapse: 42.05 seconds, total: 42.05 secondsabc - >abc - > r examples/s38584.benchabc - > resynThe network has 26 self-feeding latches.abc - > fpgaabc - > cecThe network has 26 self-feeding latches.The network has 26 self-feeding latches.Networks are equivalent after fraiging.abc - > psexamples/s38584.bench: i/o = 12/ 278 lat = 1452 nd = 3239 cube = 6769 lev = 7abc - >abc - > uabc - > mapThe network has 26 self-feeding latches.abc - > cecThe network has 26 self-feeding latches.The network has 26 self-feeding latches.Networks are equivalent after fraiging.abc - > psexamples/s38584.bench: i/o = 12/ 278 lat = 1452 nd = 8522 area = 19305.00 delay = 20.60 lev = 17abc - >abc - > r examples/ac.vabc - > resynabc - > fpgaabc - > cecNetworks are equivalent after fraiging.abc - > psac97_ctrl : i/o = 84/ 48 lat = 2199 nd = 3652 cube = 9391 lev = 3abc - >abc - > uabc - > mapabc - > cecNetworks are equivalent after fraiging.abc - > psac97_ctrl : i/o = 84/ 48 lat = 2199 nd = 8337 area = 19861.00 delay = 8.10 lev = 8abc - >abc - > r examples/s444.blifabc - > babc - > esd -vThe 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 - > dsdabc - > cecNetworks are equivalent after fraiging.abc - > psiscas\s444.bench: i/o = 3/ 6 lat = 21 nd = 81 cube = 119 lev = 7abc - >abc - > r examples/i10.blifabc - > fpgaThe network was strashed and balanced before FPGA mapping.abc - > cecNetworks are equivalent after fraiging.abc - > psi10 : i/o = 257/ 224 lat = 0 nd = 741 cube = 1616 lev = 11abc - > uabc - > mapThe network was strashed and balanced before mapping.abc - > cecNetworks are equivalent after fraiging.abc - > psi10 : i/o = 257/ 224 lat = 0 nd = 1659 area = 4215.00 delay = 30.80 lev = 27abc - >abc - > r examples/i10.blifabc - > babc - > fraig_storeThe number of AIG nodes added to storage = 2425.abc - > resynabc - > fraig_storeThe number of AIG nodes added to storage = 1678.abc - > resyn2abc - > fraig_storeThe number of AIG nodes added to storage = 1323.abc - > fraig_restoreCurrently stored 3 networks with 5426 nodes will be fraiged.abc - > fpgaPerforming FPGA mapping with choices.abc - > cecNetworks are equivalent after fraiging.abc - > psi10 : i/o = 257/ 224 lat = 0 nd = 674 cube = 1498 lev = 10abc - >abc - > uabc - > mapPerforming mapping with choices.abc - > cecNetworks are equivalent after fraiging.abc - > psi10 : i/o = 257/ 224 lat = 0 nd = 1505 area = 3561.00 delay = 25.00 lev = 22abc - >abc 109> timeelapse: 77.52 seconds, total: 77.52 secondsabc 109>
\ No newline at end of file
elapse: 42.05 seconds, total: 42.05 seconds
\ No newline at end of file
src/base/abc/abc.h
......@@ -209,8 +209,9 @@ struct Abc_Ntk_t_
#define ABC_INFINITY (10000000)
// transforming floats into ints and back
static inline int Abc_Float2Int( float Val ) { return *((int *)&Val); }
static inline float Abc_Int2Float( int Num ) { return *((float *)&Num); }
static inline int Abc_Float2Int( float Val ) { return *((int *)&Val); }
static inline float Abc_Int2Float( int Num ) { return *((float *)&Num); }
static inline int Abc_BitWordNum( int nBits ) { return nBits/32 + ((nBits%32) > 0); }
// checking the network type
static inline bool Abc_NtkIsNetlist( Abc_Ntk_t * pNtk ) { return pNtk->ntkType == ABC_NTK_NETLIST; }
......@@ -570,7 +571,7 @@ extern void Abc_NtkPrintFanio( FILE * pFile, Abc_Ntk_t * pNtk );
extern void Abc_NodePrintFanio( FILE * pFile, Abc_Obj_t * pNode );
extern void Abc_NtkPrintFactor( FILE * pFile, Abc_Ntk_t * pNtk, int fUseRealNames );
extern void Abc_NodePrintFactor( FILE * pFile, Abc_Obj_t * pNode, int fUseRealNames );
extern void Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile );
extern void Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile, int fListNodes );
extern void Abc_NodePrintLevel( FILE * pFile, Abc_Obj_t * pNode );
/*=== abcReconv.c ==========================================================*/
extern Abc_ManCut_t * Abc_NtkManCutStart( int nNodeSizeMax, int nConeSizeMax, int nNodeFanStop, int nConeFanStop );
......@@ -600,12 +601,13 @@ extern char * Abc_SopStart( Extra_MmFlex_t * pMan, int nCubes, int n
extern char * Abc_SopCreateConst0( Extra_MmFlex_t * pMan );
extern char * Abc_SopCreateConst1( Extra_MmFlex_t * pMan );
extern char * Abc_SopCreateAnd2( Extra_MmFlex_t * pMan, int fCompl0, int fCompl1 );
extern char * Abc_SopCreateAnd( Extra_MmFlex_t * pMan, int nVars );
extern char * Abc_SopCreateAnd( Extra_MmFlex_t * pMan, int nVars, int * pfCompl );
extern char * Abc_SopCreateNand( Extra_MmFlex_t * pMan, int nVars );
extern char * Abc_SopCreateOr( Extra_MmFlex_t * pMan, int nVars, int * pfCompl );
extern char * Abc_SopCreateOrMultiCube( Extra_MmFlex_t * pMan, int nVars, int * pfCompl );
extern char * Abc_SopCreateNor( Extra_MmFlex_t * pMan, int nVars );
extern char * Abc_SopCreateXor( Extra_MmFlex_t * pMan, int nVars );
extern char * Abc_SopCreateXorSpecial( Extra_MmFlex_t * pMan, int nVars );
extern char * Abc_SopCreateNxor( Extra_MmFlex_t * pMan, int nVars );
extern char * Abc_SopCreateInv( Extra_MmFlex_t * pMan );
extern char * Abc_SopCreateBuf( Extra_MmFlex_t * pMan );
......
src/base/abc/abcFunc.c
......@@ -93,27 +93,41 @@ DdNode * Abc_ConvertSopToBdd( DdManager * dd, char * pSop )
DdNode * bSum, * bCube, * bTemp, * bVar;
char * pCube;
int nVars, Value, v;
extern int Abc_SopIsExorType( char * pSop );
// start the cover
nVars = Abc_SopGetVarNum(pSop);
// check the logic function of the node
bSum = Cudd_ReadLogicZero(dd); Cudd_Ref( bSum );
Abc_SopForEachCube( pSop, nVars, pCube )
if ( Abc_SopIsExorType(pSop) )
{
for ( v = 0; v < nVars; v++ )
{
bSum = Cudd_bddXor( dd, bTemp = bSum, Cudd_bddIthVar(dd, v) ); Cudd_Ref( bSum );
Cudd_RecursiveDeref( dd, bTemp );
}
}
else
{
bCube = Cudd_ReadOne(dd); Cudd_Ref( bCube );
Abc_CubeForEachVar( pCube, Value, v )
// check the logic function of the node
Abc_SopForEachCube( pSop, nVars, pCube )
{
if ( Value == '0' )
bVar = Cudd_Not( Cudd_bddIthVar( dd, v ) );
else if ( Value == '1' )
bVar = Cudd_bddIthVar( dd, v );
else
continue;
bCube = Cudd_bddAnd( dd, bTemp = bCube, bVar ); Cudd_Ref( bCube );
bCube = Cudd_ReadOne(dd); Cudd_Ref( bCube );
Abc_CubeForEachVar( pCube, Value, v )
{
if ( Value == '0' )
bVar = Cudd_Not( Cudd_bddIthVar( dd, v ) );
else if ( Value == '1' )
bVar = Cudd_bddIthVar( dd, v );
else
continue;
bCube = Cudd_bddAnd( dd, bTemp = bCube, bVar ); Cudd_Ref( bCube );
Cudd_RecursiveDeref( dd, bTemp );
}
bSum = Cudd_bddOr( dd, bTemp = bSum, bCube );
Cudd_Ref( bSum );
Cudd_RecursiveDeref( dd, bTemp );
Cudd_RecursiveDeref( dd, bCube );
}
bSum = Cudd_bddOr( dd, bTemp = bSum, bCube ); Cudd_Ref( bSum );
Cudd_RecursiveDeref( dd, bTemp );
Cudd_RecursiveDeref( dd, bCube );
}
// complement the result if necessary
bSum = Cudd_NotCond( bSum, !Abc_SopGetPhase(pSop) );
......@@ -246,16 +260,18 @@ char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFun
assert( bFuncOn == bFuncOnDc || Cudd_bddLeq( dd, bFuncOn, bFuncOnDc ) );
if ( Cudd_IsConstant(bFuncOn) || Cudd_IsConstant(bFuncOnDc) )
{
if ( fMode == -1 ) // if the phase is not known, write constant 1
fMode = 1;
Vec_StrFill( vCube, nFanins, '-' );
Vec_StrPush( vCube, '\0' );
if ( pMan )
pSop = Extra_MmFlexEntryFetch( pMan, nFanins + 4 );
else
pSop = ALLOC( char, nFanins + 4 );
if ( bFuncOn == Cudd_ReadLogicZero(dd) )
sprintf( pSop, "%s 0\n", vCube->pArray );
if ( bFuncOn == Cudd_ReadOne(dd) )
sprintf( pSop, "%s %d\n", vCube->pArray, fMode );
else
sprintf( pSop, "%s 1\n", vCube->pArray );
sprintf( pSop, "%s %d\n", vCube->pArray, !fMode );
return pSop;
}
......
src/base/abc/abcNetlist.c
......@@ -342,7 +342,7 @@ Abc_Ntk_t * Abc_NtkAigToLogicSopBench( Abc_Ntk_t * pNtk )
if ( !Abc_NodeIsConst(pObj) )
{
Abc_NtkDupObj( pNtkNew, pObj );
pObj->pCopy->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, 2 );
pObj->pCopy->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, 2, NULL );
}
if ( Abc_AigNodeHasComplFanoutEdgeTrav(pObj) )
pObj->pCopy->pCopy = Abc_NodeCreateInv( pNtkNew, pObj->pCopy );
......
src/base/abc/abcSop.c
......@@ -156,13 +156,14 @@ char * Abc_SopCreateAnd2( Extra_MmFlex_t * pMan, int fCompl0, int fCompl1 )
SeeAlso []
***********************************************************************/
char * Abc_SopCreateAnd( Extra_MmFlex_t * pMan, int nVars )
char * Abc_SopCreateAnd( Extra_MmFlex_t * pMan, int nVars, int * pfCompl )
{
char * pSop;
int i;
pSop = Abc_SopStart( pMan, 1, nVars );
for ( i = 0; i < nVars; i++ )
pSop[i] = '1';
pSop[i] = '1' - (pfCompl? pfCompl[i] : 0);
pSop[nVars + 1] = '1';
return pSop;
}
......@@ -275,6 +276,26 @@ char * Abc_SopCreateXor( Extra_MmFlex_t * pMan, int nVars )
/**Function*************************************************************
Synopsis [Starts the multi-input XOR cover (special case).]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
char * Abc_SopCreateXorSpecial( Extra_MmFlex_t * pMan, int nVars )
{
char * pSop;
pSop = Abc_SopCreateAnd( pMan, nVars, NULL );
pSop[nVars+1] = 'x';
assert( pSop[nVars+2] == '\n' );
return pSop;
}
/**Function*************************************************************
Synopsis [Starts the multi-input XNOR cover.]
Description []
......@@ -402,9 +423,9 @@ int Abc_SopGetVarNum( char * pSop )
int Abc_SopGetPhase( char * pSop )
{
int nVars = Abc_SopGetVarNum( pSop );
if ( pSop[nVars+1] == '0' )
if ( pSop[nVars+1] == '0' || pSop[nVars+1] == 'n' )
return 0;
if ( pSop[nVars+1] == '1' )
if ( pSop[nVars+1] == '1' || pSop[nVars+1] == 'x' )
return 1;
assert( 0 );
return -1;
......@@ -453,6 +474,10 @@ void Abc_SopComplement( char * pSop )
*(pCur - 1) = '1';
else if ( *(pCur - 1) == '1' )
*(pCur - 1) = '0';
else if ( *(pCur - 1) == 'x' )
*(pCur - 1) = 'n';
else if ( *(pCur - 1) == 'n' )
*(pCur - 1) = 'x';
else
assert( 0 );
}
......@@ -474,7 +499,7 @@ bool Abc_SopIsComplement( char * pSop )
char * pCur;
for ( pCur = pSop; *pCur; pCur++ )
if ( *pCur == '\n' )
return (int)(*(pCur - 1) == '0');
return (int)(*(pCur - 1) == '0' || *(pCur - 1) == 'n');
assert( 0 );
return 0;
}
......@@ -616,6 +641,27 @@ bool Abc_SopIsOrType( char * pSop )
SeeAlso []
***********************************************************************/
int Abc_SopIsExorType( char * pSop )
{
char * pCur;
for ( pCur = pSop; *pCur; pCur++ )
if ( *pCur == '\n' )
return (int)(*(pCur - 1) == 'x' || *(pCur - 1) == 'n');
assert( 0 );
return 0;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
bool Abc_SopCheck( char * pSop, int nFanins )
{
char * pCubes, * pCubesOld;
......@@ -638,7 +684,7 @@ bool Abc_SopCheck( char * pSop, int nFanins )
fFound0 = 1;
else if ( *pCubes == '1' )
fFound1 = 1;
else
else if ( *pCubes != 'x' && *pCubes != 'n' )
{
fprintf( stdout, "Abc_SopCheck: SOP has a strange character in the output part of its cube.\n" );
return 0;
......
src/base/abc/abcUtil.c
......@@ -76,6 +76,8 @@ int Abc_NtkGetCubeNum( Abc_Ntk_t * pNtk )
assert( Abc_NtkHasSop(pNtk) );
Abc_NtkForEachNode( pNtk, pNode, i )
{
if ( Abc_NodeIsConst(pNode) )
continue;
assert( pNode->pData );
nCubes += Abc_SopGetCubeNum( pNode->pData );
}
......@@ -153,6 +155,8 @@ int Abc_NtkGetBddNodeNum( Abc_Ntk_t * pNtk )
assert( Abc_NtkIsBddLogic(pNtk) );
Abc_NtkForEachNode( pNtk, pNode, i )
{
if ( Abc_NodeIsConst(pNode) )
continue;
assert( pNode->pData );
nNodes += pNode->pData? Cudd_DagSize( pNode->pData ) : 0;
}
......
src/base/abci/abc.c
......@@ -77,6 +77,7 @@ static int Abc_CommandExdcFree ( Abc_Frame_t * pAbc, int argc, char ** argv
static int Abc_CommandExdcGet ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandExdcSet ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandCut ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandXyz ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTest ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandFraig ( Abc_Frame_t * pAbc, int argc, char ** argv );
......@@ -173,6 +174,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Various", "exdc_get", Abc_CommandExdcGet, 1 );
Cmd_CommandAdd( pAbc, "Various", "exdc_set", Abc_CommandExdcSet, 1 );
Cmd_CommandAdd( pAbc, "Various", "cut", Abc_CommandCut, 0 );
Cmd_CommandAdd( pAbc, "Various", "xyz", Abc_CommandXyz, 1 );
Cmd_CommandAdd( pAbc, "Various", "test", Abc_CommandTest, 0 );
Cmd_CommandAdd( pAbc, "Fraiging", "fraig", Abc_CommandFraig, 1 );
......@@ -648,6 +650,7 @@ int Abc_CommandPrintLevel( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Ntk_t * pNtk;
Abc_Obj_t * pNode;
int c;
int fListNodes;
int fProfile;
pNtk = Abc_FrameReadNet(pAbc);
......@@ -655,12 +658,16 @@ int Abc_CommandPrintLevel( Abc_Frame_t * pAbc, int argc, char ** argv )
pErr = Abc_FrameReadErr(pAbc);
// set defaults
fProfile = 1;
fListNodes = 0;
fProfile = 1;
util_getopt_reset();
while ( ( c = util_getopt( argc, argv, "ph" ) ) != EOF )
while ( ( c = util_getopt( argc, argv, "nph" ) ) != EOF )
{
switch ( c )
{
case 'n':
fListNodes ^= 1;
break;
case 'p':
fProfile ^= 1;
break;
......@@ -701,12 +708,13 @@ int Abc_CommandPrintLevel( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
}
// process all COs
Abc_NtkPrintLevel( pOut, pNtk, fProfile );
Abc_NtkPrintLevel( pOut, pNtk, fProfile, fListNodes );
return 0;
usage:
fprintf( pErr, "usage: print_level [-ph] <node>\n" );
fprintf( pErr, "usage: print_level [-nph] <node>\n" );
fprintf( pErr, "\t prints information about node level and cone size\n" );
fprintf( pErr, "\t-n : toggles printing nodes by levels [default = %s]\n", fListNodes? "yes": "no" );
fprintf( pErr, "\t-p : toggles printing level profile [default = %s]\n", fProfile? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
fprintf( pErr, "\tnode : (optional) one node to consider\n");
......@@ -732,6 +740,7 @@ int Abc_CommandPrintSupport( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
int fVerbose;
extern Vec_Ptr_t * Sim_ComputeFunSupp( Abc_Ntk_t * pNtk, int fVerbose );
extern void Abc_NtkPrintStrSupports( Abc_Ntk_t * pNtk );
pNtk = Abc_FrameReadNet(pAbc);
pOut = Abc_FrameReadOut(pAbc);
......@@ -759,6 +768,11 @@ int Abc_CommandPrintSupport( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Empty network.\n" );
return 1;
}
// print support information
Abc_NtkPrintStrSupports( pNtk );
return 0;
if ( !Abc_NtkIsComb(pNtk) )
{
fprintf( pErr, "This command works only for combinational networks.\n" );
......@@ -3649,11 +3663,102 @@ usage:
SeeAlso []
***********************************************************************/
int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk, * pNtkRes;
int c;
int fVerbose;
int fUseInvs;
int nFaninMax;
extern Abc_Ntk_t * Abc_NtkXyz( Abc_Ntk_t * pNtk, int nFaninMax, bool fUseEsop, bool fUseSop, bool fUseInvs, bool fVerbose );
pNtk = Abc_FrameReadNet(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
fVerbose = 0;
fUseInvs = 1;
nFaninMax = 128;
util_getopt_reset();
while ( ( c = util_getopt( argc, argv, "Nivh" ) ) != EOF )
{
switch ( c )
{
case 'N':
if ( util_optind >= argc )
{
fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" );
goto usage;
}
nFaninMax = atoi(argv[util_optind]);
util_optind++;
if ( nFaninMax < 0 )
goto usage;
break;
case 'i':
fUseInvs ^= 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_NtkIsStrash(pNtk) )
{
fprintf( pErr, "Only works for strashed networks.\n" );
return 1;
}
// run the command
pNtkRes = Abc_NtkXyz( pNtk, nFaninMax, 0, 0, fUseInvs, fVerbose );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Command has failed.\n" );
return 1;
}
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
return 0;
usage:
fprintf( pErr, "usage: xyz [-N num] [-ivh]\n" );
fprintf( pErr, "\t specilized AND/OR/EXOR decomposition\n" );
fprintf( pErr, "\t-N num : maximum number of inputs [default = %d]\n", nFaninMax );
fprintf( pErr, "\t-i : toggle the use of interters [default = %s]\n", fUseInvs? "yes": "no" );
fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk;//, * pNtkRes;
int c;
pNtk = Abc_FrameReadNet(pAbc);
pOut = Abc_FrameReadOut(pAbc);
......@@ -3676,6 +3781,18 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Empty network.\n" );
return 1;
}
if ( !Abc_NtkIsStrash(pNtk) )
{
fprintf( pErr, "Only works for strashed networks.\n" );
return 1;
}
// Abc_NtkDeriveEsops( pNtk );
// Abc_NtkXyz( pNtk, 128, 0, 0, 0 );
printf( "This command is currently not used.\n" );
/*
// run the command
pNtkRes = Abc_NtkMiterForCofactors( pNtk, 0, 0, -1 );
if ( pNtkRes == NULL )
......@@ -3685,6 +3802,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
*/
return 0;
usage:
......@@ -3696,7 +3814,6 @@ usage:
/**Function*************************************************************
Synopsis []
......
src/base/abci/abcBalance.c
......@@ -102,6 +102,42 @@ void Abc_NtkBalancePerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fDuplica
/**Function*************************************************************
Synopsis [Randomizes the node positions.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NodeBalanceRandomize( Vec_Ptr_t * vSuper )
{
Abc_Obj_t * pNode1, * pNode2;
int i, Signature;
if ( Vec_PtrSize(vSuper) < 3 )
return;
pNode1 = Vec_PtrEntry( vSuper, Vec_PtrSize(vSuper)-2 );
pNode2 = Vec_PtrEntry( vSuper, Vec_PtrSize(vSuper)-3 );
if ( Abc_ObjRegular(pNode1)->Level != Abc_ObjRegular(pNode2)->Level )
return;
// some reordering will be performed
Signature = rand();
for ( i = Vec_PtrSize(vSuper)-2; i > 0; i-- )
{
pNode1 = Vec_PtrEntry( vSuper, i );
pNode2 = Vec_PtrEntry( vSuper, i-1 );
if ( Abc_ObjRegular(pNode1)->Level != Abc_ObjRegular(pNode2)->Level )
return;
if ( Signature & (1 << (i % 10)) )
continue;
Vec_PtrWriteEntry( vSuper, i, pNode2 );
Vec_PtrWriteEntry( vSuper, i-1, pNode1 );
}
}
/**Function*************************************************************
Synopsis [Rebalances the multi-input node rooted at pNodeOld.]
Description []
......@@ -143,6 +179,9 @@ Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_
assert( vSuper->nSize > 1 );
while ( vSuper->nSize > 1 )
{
// randomize the node positions
// Abc_NodeBalanceRandomize( vSuper );
// pull out the last two nodes
pNode1 = Vec_PtrPop(vSuper);
pNode2 = Vec_PtrPop(vSuper);
Abc_VecObjPushUniqueOrderByLevel( vSuper, Abc_AigAnd(pMan, pNode1, pNode2) );
......
src/base/abci/abcFraig.c
......@@ -56,7 +56,7 @@ Abc_Ntk_t * Abc_NtkFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes, int f
{
Fraig_Params_t * pPars = pParams;
Abc_Ntk_t * pNtkNew;
Fraig_Man_t * pMan;
Fraig_Man_t * pMan;
// check if EXDC is present
if ( fExdc && pNtk->pExdc == NULL )
fExdc = 0, printf( "Warning: Networks has no EXDC.\n" );
......
src/base/abci/abcPrint.c
......@@ -79,7 +79,7 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
fprintf( pFile, " lit(fac) = %5d", Abc_NtkGetLitFactNum(pNtk) );
}
else if ( Abc_NtkHasBdd(pNtk) )
fprintf( pFile, " bdd = %5d", Abc_NtkGetBddNodeNum(pNtk) );
fprintf( pFile, " bdd = %5d", Abc_NtkGetBddNodeNum(pNtk) );
else if ( Abc_NtkHasMapping(pNtk) )
{
fprintf( pFile, " area = %5.2f", Abc_NtkGetMappedArea(pNtk) );
......@@ -423,10 +423,26 @@ void Abc_NodePrintFactor( FILE * pFile, Abc_Obj_t * pNode, int fUseRealNames )
SeeAlso []
***********************************************************************/
void Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile )
void Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile, int fListNodes )
{
Abc_Obj_t * pNode;
int i, Length;
int i, k, Length;
if ( fListNodes )
{
int nLevels;
nLevels = Abc_NtkGetLevelNum(pNtk);
printf( "Nodes by level:\n" );
for ( i = 0; i <= nLevels; i++ )
{
printf( "%2d : ", i );
Abc_NtkForEachNode( pNtk, pNode, k )
if ( (int)pNode->Level == i )
printf( " %s", Abc_ObjName(pNode) );
printf( "\n" );
}
return;
}
// print the delay profile
if ( fProfile && Abc_NtkHasMapping(pNtk) )
......@@ -716,6 +732,34 @@ void Abc_NtkPrintSharing( Abc_Ntk_t * pNtk )
printf( "\n" );
}
/**Function*************************************************************
Synopsis [Prints info for each output cone.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkPrintStrSupports( Abc_Ntk_t * pNtk )
{
Vec_Ptr_t * vSupp, * vNodes;
Abc_Obj_t * pObj;
int i;
printf( "Structural support info:\n" );
Abc_NtkForEachCo( pNtk, pObj, i )
{
vSupp = Abc_NtkNodeSupport( pNtk, &pObj, 1 );
vNodes = Abc_NtkDfsNodes( pNtk, &pObj, 1 );
printf( "%20s : Cone = %5d. Supp = %5d.\n",
Abc_ObjName(pObj), vNodes->nSize, vSupp->nSize );
Vec_PtrFree( vNodes );
Vec_PtrFree( vSupp );
}
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
src/base/abci/abcRewrite.c
......@@ -109,6 +109,7 @@ Rwr_ManAddTimeTotal( pManRwr, clock() - clkStart );
// print stats
if ( fVerbose )
Rwr_ManPrintStats( pManRwr );
// Rwr_ManPrintStatsFile( pManRwr );
// delete the managers
Rwr_ManStop( pManRwr );
Cut_ManStop( pManCut );
......
src/base/abci/abcSat.c
......@@ -24,8 +24,8 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static void Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * pNode, Vec_Int_t * vVars );
static void Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars );
static int Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * pNode, Vec_Int_t * vVars );
static int Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
......@@ -57,6 +57,8 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose )
// load clauses into the solver
clk = clock();
pSat = Abc_NtkMiterSatCreate( pNtk );
if ( pSat == NULL )
return 1;
// printf( "Created SAT problem with %d variable and %d clauses. ", solver_nvars(pSat), solver_nclauses(pSat) );
// PRT( "Time", clock() - clk );
......@@ -69,7 +71,7 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose )
{
solver_delete( pSat );
// printf( "The problem is UNSATISFIABLE after simplification.\n" );
return -1;
return 1;
}
// solve the miter
......@@ -143,13 +145,19 @@ solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk )
// derive SOPs for both phases of the node
Abc_NodeBddToCnf( pNode, pMmFlex, vCube, &pSop0, &pSop1 );
// add the clauses to the solver
Abc_NodeAddClauses( pSat, pSop0, pSop1, pNode, vVars );
if ( !Abc_NodeAddClauses( pSat, pSop0, pSop1, pNode, vVars ) )
{
solver_delete( pSat );
return NULL;
}
}
// add clauses for each PO
// Abc_NtkForEachPo( pNtk, pNode, i )
// Abc_NodeAddClausesTop( pSat, pNode, vVars );
Abc_NodeAddClausesTop( pSat, Abc_NtkPo(pNtk, Abc_NtkPoNum(pNtk)-1), vVars );
// add clauses for the POs
if ( !Abc_NodeAddClausesTop( pSat, Abc_NtkPo(pNtk, Abc_NtkPoNum(pNtk)-1), vVars ) )
{
solver_delete( pSat );
return NULL;
}
// Asat_SolverWriteDimacs( pSat, "test.cnf", NULL, NULL, 0 );
// delete
Vec_StrFree( vCube );
......@@ -169,7 +177,7 @@ solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk )
SeeAlso []
***********************************************************************/
void Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * pNode, Vec_Int_t * vVars )
int Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * pNode, Vec_Int_t * vVars )
{
Abc_Obj_t * pFanin;
int i, c, nFanins;
......@@ -177,6 +185,16 @@ void Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t *
nFanins = Abc_ObjFaninNum( pNode );
assert( nFanins == Abc_SopGetVarNum( pSop0 ) );
if ( nFanins == 0 )
{
vVars->nSize = 0;
if ( Abc_SopIsConst1(pSop1) )
Vec_IntPush( vVars, toLit(pNode->Id) );
else
Vec_IntPush( vVars, neg(toLit(pNode->Id)) );
return solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
}
// add clauses for the negative phase
for ( c = 0; ; c++ )
......@@ -195,7 +213,8 @@ void Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t *
Vec_IntPush( vVars, neg(toLit(pFanin->Id)) );
}
Vec_IntPush( vVars, neg(toLit(pNode->Id)) );
solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
return 0;
}
// add clauses for the positive phase
......@@ -215,8 +234,10 @@ void Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t *
Vec_IntPush( vVars, neg(toLit(pFanin->Id)) );
}
Vec_IntPush( vVars, toLit(pNode->Id) );
solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
return 0;
}
return 1;
}
/**Function*************************************************************
......@@ -230,7 +251,7 @@ void Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t *
SeeAlso []
***********************************************************************/
void Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars )
int Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars )
{
Abc_Obj_t * pFanin;
......@@ -240,29 +261,33 @@ void Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars
vVars->nSize = 0;
Vec_IntPush( vVars, toLit(pFanin->Id) );
Vec_IntPush( vVars, toLit(pNode->Id) );
solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
return 0;
vVars->nSize = 0;
Vec_IntPush( vVars, neg(toLit(pFanin->Id)) );
Vec_IntPush( vVars, neg(toLit(pNode->Id)) );
solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
return 0;
}
else
{
vVars->nSize = 0;
Vec_IntPush( vVars, neg(toLit(pFanin->Id)) );
Vec_IntPush( vVars, toLit(pNode->Id) );
solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
return 0;
vVars->nSize = 0;
Vec_IntPush( vVars, toLit(pFanin->Id) );
Vec_IntPush( vVars, neg(toLit(pNode->Id)) );
solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
return 0;
}
vVars->nSize = 0;
Vec_IntPush( vVars, toLit(pNode->Id) );
solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
return solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
}
......
src/base/abci/abcStrash.c
......@@ -29,6 +29,7 @@
// static functions
static void Abc_NtkStrashPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fAllNodes );
static Abc_Obj_t * Abc_NodeStrashSop( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, char * pSop );
static Abc_Obj_t * Abc_NodeStrashExor( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, char * pSop );
static Abc_Obj_t * Abc_NodeStrashFactor( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, char * pSop );
extern char * Mio_GateReadSop( void * pGate );
......@@ -182,6 +183,7 @@ Abc_Obj_t * Abc_NodeStrash( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode )
{
int fUseFactor = 1;
char * pSop;
extern int Abc_SopIsExorType( char * pSop );
assert( Abc_ObjIsNode(pNode) );
......@@ -203,6 +205,10 @@ Abc_Obj_t * Abc_NodeStrash( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode )
if ( Abc_NodeIsConst(pNode) )
return Abc_ObjNotCond( Abc_NtkConst1(pNtkNew), Abc_SopIsConst0(pSop) );
// consider the special case of EXOR function
if ( Abc_SopIsExorType(pSop) )
return Abc_NodeStrashExor( pNtkNew, pNode, pSop );
// decide when to use factoring
if ( fUseFactor && Abc_ObjFaninNum(pNode) > 2 && Abc_SopGetCubeNum(pSop) > 1 )
return Abc_NodeStrashFactor( pNtkNew, pNode, pSop );
......@@ -254,6 +260,37 @@ Abc_Obj_t * Abc_NodeStrashSop( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, char * pS
/**Function*************************************************************
Synopsis [Strashed n-input XOR function.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Obj_t * Abc_NodeStrashExor( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, char * pSop )
{
Abc_Aig_t * pMan = pNtkNew->pManFunc;
Abc_Obj_t * pFanin, * pSum;
int i, nFanins;
// get the number of node's fanins
nFanins = Abc_ObjFaninNum( pNode );
assert( nFanins == Abc_SopGetVarNum(pSop) );
// go through the cubes of the node's SOP
pSum = Abc_ObjNot( Abc_NtkConst1(pNtkNew) );
for ( i = 0; i < nFanins; i++ )
{
pFanin = Abc_ObjFanin( pNode, i );
pSum = Abc_AigXor( pMan, pSum, pFanin->pCopy );
}
if ( Abc_SopIsComplement(pSop) )
pSum = Abc_ObjNot(pSum);
return pSum;
}
/**Function*************************************************************
Synopsis [Strashes one logic node using its SOP.]
Description []
......
src/base/cmd/cmd.c
......@@ -1245,6 +1245,12 @@ int CmdCommandSis( Abc_Frame_t * pAbc, int argc, char **argv )
}
fclose( pFile );
if ( Abc_NtkIsMappedLogic(pNtk) )
{
Abc_NtkUnmap(pNtk);
printf( "The current network is unmapped before calling SIS.\n" );
}
// write out the current network
pNetlist = Abc_NtkLogicToNetlist(pNtk);
Io_WriteBlif( pNetlist, "_sis_in.blif", 1 );
......@@ -1375,6 +1381,11 @@ int CmdCommandMvsis( Abc_Frame_t * pAbc, int argc, char **argv )
}
fclose( pFile );
if ( Abc_NtkIsMappedLogic(pNtk) )
{
Abc_NtkUnmap(pNtk);
printf( "The current network is unmapped before calling MVSIS.\n" );
}
// write out the current network
pNetlist = Abc_NtkLogicToNetlist(pNtk);
......
src/base/cmd/cmdUtils.c
......@@ -245,7 +245,7 @@ int CmdApplyAlias( Abc_Frame_t * pAbc, int *argcp, char ***argvp, int *loop )
argc = *argcp;
argv = *argvp;
stopit = 0;
for ( ; *loop < 20; ( *loop )++ )
for ( ; *loop < 200; ( *loop )++ )
{
if ( argc == 0 )
return 0;
......
src/base/io/io.c
......@@ -44,6 +44,7 @@ static int IoCommandWriteEqn ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteGml ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteList ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWritePla ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
......@@ -81,6 +82,7 @@ void Io_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "I/O", "write_gml", IoCommandWriteGml, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_list", IoCommandWriteList, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_pla", IoCommandWritePla, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_verilog", IoCommandWriteVerilog, 0 );
}
/**Function*************************************************************
......@@ -1383,6 +1385,69 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv )
{
Abc_Ntk_t * pNtk, * pNtkTemp;
char * FileName;
int c;
util_getopt_reset();
while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
{
switch ( c )
{
case 'h':
goto usage;
default:
goto usage;
}
}
pNtk = pAbc->pNtkCur;
if ( pNtk == NULL )
{
fprintf( pAbc->Out, "Empty network.\n" );
return 0;
}
if ( argc != util_optind + 1 )
{
goto usage;
}
// get the input file name
FileName = argv[util_optind];
// derive the netlist
pNtkTemp = Abc_NtkLogicToNetlist(pNtk);
if ( pNtkTemp == NULL )
{
fprintf( pAbc->Out, "Writing PLA has failed.\n" );
return 0;
}
Io_WriteVerilog( pNtkTemp, FileName );
Abc_NtkDelete( pNtkTemp );
return 0;
usage:
fprintf( pAbc->Err, "usage: write_verilog [-h] <file>\n" );
fprintf( pAbc->Err, "\t write a very special subset of Verilog\n" );
fprintf( pAbc->Err, "\t-h : print the help massage\n" );
fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
return 1;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
src/base/io/io.h
......@@ -90,6 +90,8 @@ extern void Io_WriteGml( Abc_Ntk_t * pNtk, char * pFileName );
extern void Io_WriteList( Abc_Ntk_t * pNtk, char * pFileName, int fUseHost );
/*=== abcWritePla.c ==========================================================*/
extern int Io_WritePla( Abc_Ntk_t * pNtk, char * FileName );
/*=== abcWriteVerilog.c ==========================================================*/
extern void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * FileName );
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
......
src/base/io/ioReadBench.c
......@@ -127,7 +127,7 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p )
pNode = Io_ReadCreateNode( pNtk, vTokens->pArray[0], ppNames, nNames );
// assign the cover
if ( strcmp(pType, "AND") == 0 )
Abc_ObjSetData( pNode, Abc_SopCreateAnd(pNtk->pManFunc, nNames) );
Abc_ObjSetData( pNode, Abc_SopCreateAnd(pNtk->pManFunc, nNames, NULL) );
else if ( strcmp(pType, "OR") == 0 )
Abc_ObjSetData( pNode, Abc_SopCreateOr(pNtk->pManFunc, nNames, NULL) );
else if ( strcmp(pType, "NAND") == 0 )
......
src/base/io/ioReadBlif.c
......@@ -504,7 +504,7 @@ int Io_ReadBlifNetworkNames( Io_ReadBlif_t * p, Vec_Ptr_t ** pvTokens )
Vec_StrAppend( p->vCubes, vTokens->pArray[0] );
// check the char
Char = ((char *)vTokens->pArray[1])[0];
if ( Char != '0' && Char != '1' )
if ( Char != '0' && Char != '1' && Char != 'x' && Char != 'n' )
{
p->LineCur = Extra_FileReaderGetLineNumber(p->pReader, 0);
sprintf( p->sError, "The output character in the constant cube is wrong." );
......
src/base/io/ioReadEdif.c
......@@ -191,7 +191,7 @@ Abc_Ntk_t * Io_ReadEdifNetwork( Extra_FileReader_t * p )
Abc_NtkForEachNode( pNtk, pObj, i )
{
if ( strncmp( pObj->pData, "And", 3 ) == 0 )
Abc_ObjSetData( pObj, Abc_SopCreateAnd(pNtk->pManFunc, Abc_ObjFaninNum(pObj)) );
Abc_ObjSetData( pObj, Abc_SopCreateAnd(pNtk->pManFunc, Abc_ObjFaninNum(pObj), NULL) );
else if ( strncmp( pObj->pData, "Or", 2 ) == 0 )
Abc_ObjSetData( pObj, Abc_SopCreateOr(pNtk->pManFunc, Abc_ObjFaninNum(pObj), NULL) );
else if ( strncmp( pObj->pData, "Nand", 4 ) == 0 )
......
src/map/fpga/fpgaUtils.c
......@@ -51,11 +51,11 @@ static Fpga_Man_t * s_pMan = NULL;
***********************************************************************/
Fpga_NodeVec_t * Fpga_MappingDfs( Fpga_Man_t * pMan, int fCollectEquiv )
{
Fpga_NodeVec_t * vNodes, * vNodesCo;
Fpga_NodeVec_t * vNodes;//, * vNodesCo;
Fpga_Node_t * pNode;
int i;
// collect the CO nodes by level
vNodesCo = Fpga_MappingOrderCosByLevel( pMan );
// vNodesCo = Fpga_MappingOrderCosByLevel( pMan );
// start the array
vNodes = Fpga_NodeVecAlloc( 100 );
// collect the PIs
......@@ -66,17 +66,17 @@ Fpga_NodeVec_t * Fpga_MappingDfs( Fpga_Man_t * pMan, int fCollectEquiv )
pNode->fMark0 = 1;
}
// perform the traversal
// for ( i = 0; i < pMan->nOutputs; i++ )
// Fpga_MappingDfs_rec( Fpga_Regular(pMan->pOutputs[i]), vNodes, fCollectEquiv );
for ( i = 0; i < vNodesCo->nSize; i++ )
for ( pNode = vNodesCo->pArray[i]; pNode; pNode = (Fpga_Node_t *)pNode->pData0 )
Fpga_MappingDfs_rec( pNode, vNodes, fCollectEquiv );
for ( i = 0; i < pMan->nOutputs; i++ )
Fpga_MappingDfs_rec( Fpga_Regular(pMan->pOutputs[i]), vNodes, fCollectEquiv );
// for ( i = vNodesCo->nSize - 1; i >= 0 ; i-- )
// for ( pNode = vNodesCo->pArray[i]; pNode; pNode = (Fpga_Node_t *)pNode->pData0 )
// Fpga_MappingDfs_rec( pNode, vNodes, fCollectEquiv );
// clean the node marks
for ( i = 0; i < vNodes->nSize; i++ )
vNodes->pArray[i]->fMark0 = 0;
// for ( i = 0; i < pMan->nOutputs; i++ )
// Fpga_MappingUnmark_rec( Fpga_Regular(pMan->pOutputs[i]) );
Fpga_NodeVecFree( vNodesCo );
// Fpga_NodeVecFree( vNodesCo );
return vNodes;
}
......@@ -954,7 +954,7 @@ Fpga_NodeVec_t * Fpga_MappingOrderCosByLevel( Fpga_Man_t * pMan )
Fpga_Node_t * pNode;
Fpga_NodeVec_t * vNodes;
int i, nLevels;
// get the largest node
// get the largest level of a CO
nLevels = Fpga_MappingMaxLevel( pMan );
// allocate the array of nodes
vNodes = Fpga_NodeVecAlloc( nLevels + 1 );
......
src/opt/rwr/rwr.h
......@@ -129,6 +129,7 @@ extern void Rwr_ManIncTravId( Rwr_Man_t * p );
extern Rwr_Man_t * Rwr_ManStart( bool fPrecompute );
extern void Rwr_ManStop( Rwr_Man_t * p );
extern void Rwr_ManPrintStats( Rwr_Man_t * p );
extern void Rwr_ManPrintStatsFile( Rwr_Man_t * p );
extern void * Rwr_ManReadDecs( Rwr_Man_t * p );
extern int Rwr_ManReadCompl( Rwr_Man_t * p );
extern void Rwr_ManAddTimeCuts( Rwr_Man_t * p, int Time );
......
src/opt/rwr/rwrMan.c
......@@ -179,6 +179,29 @@ void Rwr_ManPrintStats( Rwr_Man_t * p )
SeeAlso []
***********************************************************************/
void Rwr_ManPrintStatsFile( Rwr_Man_t * p )
{
FILE * pTable;
pTable = fopen( "stats.txt", "a+" );
fprintf( pTable, "%d ", p->nCutsGood );
fprintf( pTable, "%d ", p->nSubgraphs );
fprintf( pTable, "%d ", p->nNodesRewritten );
fprintf( pTable, "%d", p->nNodesGained );
fprintf( pTable, "\n" );
fclose( pTable );
}
/**Function*************************************************************
Synopsis [Stops the resynthesis manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void * Rwr_ManReadDecs( Rwr_Man_t * p )
{
return p->pGraph;
......
src/opt/xyz/module.make 0 → 100644
SRC += src/opt/xyz/xyzBuild.c \
src/opt/xyz/xyzCore.c \
src/opt/xyz/xyzMan.c \
src/opt/xyz/xyzMinEsop.c \
src/opt/xyz/xyzMinMan.c \
src/opt/xyz/xyzMinSop.c \
src/opt/xyz/xyzMinUtil.c \
src/opt/xyz/xyzTest.c
src/opt/xyz/xyz.h 0 → 100644
/**CFile****************************************************************
FileName [xyz.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Cover manipulation package.]
Synopsis [External declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: xyz.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "abc.h"
#include "xyzInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
typedef struct Xyz_Man_t_ Xyz_Man_t;
typedef struct Xyz_Obj_t_ Xyz_Obj_t;
// storage for node information
struct Xyz_Obj_t_
{
Min_Cube_t * pCover[3]; // pos/neg/esop
Vec_Int_t * vSupp; // computed support (all nodes except CIs)
};
// storage for additional information
struct Xyz_Man_t_
{
// general characteristics
int nFaninMax; // the number of vars
int nCubesMax; // the limit on the number of cubes in the intermediate covers
int nWords; // the number of words
Vec_Int_t * vFanCounts; // fanout counts
Vec_Ptr_t * vObjStrs; // object structures
void * pMemory; // memory for the internal data strctures
Min_Man_t * pManMin; // the cub manager
// arrays to map local variables
Vec_Int_t * vComTo0; // mapping of common variables into first fanin
Vec_Int_t * vComTo1; // mapping of common variables into second fanin
Vec_Int_t * vPairs0; // the first var in each pair of common vars
Vec_Int_t * vPairs1; // the second var in each pair of common vars
Vec_Int_t * vTriv0; // trival support of the first node
Vec_Int_t * vTriv1; // trival support of the second node
// statistics
int nSupps; // supports created
int nSuppsMax; // the maximum number of supports
int nBoundary; // the boundary size
int nNodes; // the number of nodes processed
};
static inline Xyz_Obj_t * Abc_ObjGetStr( Abc_Obj_t * pObj ) { return Vec_PtrEntry(((Xyz_Man_t *)pObj->pNtk->pManCut)->vObjStrs, pObj->Id); }
static inline void Abc_ObjSetSupp( Abc_Obj_t * pObj, Vec_Int_t * vVec ) { Abc_ObjGetStr(pObj)->vSupp = vVec; }
static inline Vec_Int_t * Abc_ObjGetSupp( Abc_Obj_t * pObj ) { return Abc_ObjGetStr(pObj)->vSupp; }
static inline void Abc_ObjSetCover2( Abc_Obj_t * pObj, Min_Cube_t * pCov ) { Abc_ObjGetStr(pObj)->pCover[2] = pCov; }
static inline Min_Cube_t * Abc_ObjGetCover2( Abc_Obj_t * pObj ) { return Abc_ObjGetStr(pObj)->pCover[2]; }
static inline void Abc_ObjSetCover( Abc_Obj_t * pObj, Min_Cube_t * pCov, int Pol ) { Abc_ObjGetStr(pObj)->pCover[Pol] = pCov; }
static inline Min_Cube_t * Abc_ObjGetCover( Abc_Obj_t * pObj, int Pol ) { return Abc_ObjGetStr(pObj)->pCover[Pol]; }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/*=== xyzBuild.c ==========================================================*/
extern Abc_Ntk_t * Abc_NtkXyzDerive( Xyz_Man_t * p, Abc_Ntk_t * pNtk );
extern Abc_Ntk_t * Abc_NtkXyzDeriveClean( Xyz_Man_t * p, Abc_Ntk_t * pNtk );
/*=== xyzCore.c ===========================================================*/
extern Abc_Ntk_t * Abc_NtkXyz( Abc_Ntk_t * pNtk, int nFaninMax, bool fUseEsop, bool fUseSop, bool fUseInvs, bool fVerbose );
/*=== xyzMan.c ============================================================*/
extern Xyz_Man_t * Xyz_ManAlloc( Abc_Ntk_t * pNtk, int nFaninMax );
extern void Xyz_ManFree( Xyz_Man_t * p );
extern void Abc_NodeXyzDropData( Xyz_Man_t * p, Abc_Obj_t * pObj );
/*=== xyzTest.c ===========================================================*/
extern Abc_Ntk_t * Abc_NtkXyzTestSop( Abc_Ntk_t * pNtk );
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/opt/xyz/xyzMan.c 0 → 100644
/**CFile****************************************************************
FileName [xyzMan.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Cover manipulation package.]
Synopsis [Decomposition manager.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: xyzMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "xyz.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Xyz_Man_t * Xyz_ManAlloc( Abc_Ntk_t * pNtk, int nFaninMax )
{
Xyz_Man_t * pMan;
Xyz_Obj_t * pMem;
Abc_Obj_t * pObj;
int i;
assert( pNtk->pManCut == NULL );
// start the manager
pMan = ALLOC( Xyz_Man_t, 1 );
memset( pMan, 0, sizeof(Xyz_Man_t) );
pMan->nFaninMax = nFaninMax;
pMan->nCubesMax = 2 * pMan->nFaninMax;
pMan->nWords = Abc_BitWordNum( nFaninMax * 2 );
// get the cubes
pMan->vComTo0 = Vec_IntAlloc( 2*nFaninMax );
pMan->vComTo1 = Vec_IntAlloc( 2*nFaninMax );
pMan->vPairs0 = Vec_IntAlloc( nFaninMax );
pMan->vPairs1 = Vec_IntAlloc( nFaninMax );
pMan->vTriv0 = Vec_IntAlloc( 1 ); Vec_IntPush( pMan->vTriv0, -1 );
pMan->vTriv1 = Vec_IntAlloc( 1 ); Vec_IntPush( pMan->vTriv1, -1 );
// allocate memory for object structures
pMan->pMemory = pMem = ALLOC( Xyz_Obj_t, sizeof(Xyz_Obj_t) * Abc_NtkObjNumMax(pNtk) );
memset( pMem, 0, sizeof(Xyz_Obj_t) * Abc_NtkObjNumMax(pNtk) );
// allocate storage for the pointers to the memory
pMan->vObjStrs = Vec_PtrAlloc( Abc_NtkObjNumMax(pNtk) );
Vec_PtrFill( pMan->vObjStrs, Abc_NtkObjNumMax(pNtk), NULL );
Abc_NtkForEachObj( pNtk, pObj, i )
Vec_PtrWriteEntry( pMan->vObjStrs, i, pMem + i );
// create the cube manager
pMan->pManMin = Min_ManAlloc( nFaninMax );
return pMan;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Xyz_ManFree( Xyz_Man_t * p )
{
Vec_Int_t * vSupp;
int i;
for ( i = 0; i < p->vObjStrs->nSize; i++ )
{
vSupp = ((Xyz_Obj_t *)p->vObjStrs->pArray[i])->vSupp;
if ( vSupp ) Vec_IntFree( vSupp );
}
Min_ManFree( p->pManMin );
Vec_PtrFree( p->vObjStrs );
Vec_IntFree( p->vFanCounts );
Vec_IntFree( p->vTriv0 );
Vec_IntFree( p->vTriv1 );
Vec_IntFree( p->vComTo0 );
Vec_IntFree( p->vComTo1 );
Vec_IntFree( p->vPairs0 );
Vec_IntFree( p->vPairs1 );
free( p->pMemory );
free( p );
}
/**Function*************************************************************
Synopsis [Drop the covers at the node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NodeXyzDropData( Xyz_Man_t * p, Abc_Obj_t * pObj )
{
int nFanouts;
assert( p->vFanCounts );
nFanouts = Vec_IntEntry( p->vFanCounts, pObj->Id );
assert( nFanouts > 0 );
if ( --nFanouts == 0 )
{
Vec_IntFree( Abc_ObjGetSupp(pObj) );
Abc_ObjSetSupp( pObj, NULL );
Min_CoverRecycle( p->pManMin, Abc_ObjGetCover2(pObj) );
Abc_ObjSetCover2( pObj, NULL );
p->nSupps--;
}
Vec_IntWriteEntry( p->vFanCounts, pObj->Id, nFanouts );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/opt/xyz/xyzMinEsop.c 0 → 100644
/**CFile****************************************************************
FileName [xyzMinEsop.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Cover manipulation package.]
Synopsis [ESOP manipulation.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: xyzMinEsop.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "xyzInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static void Min_EsopRewrite( Min_Man_t * p );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Min_EsopMinimize( Min_Man_t * p )
{
int nCubesInit, nCubesOld, nIter;
if ( p->nCubes < 3 )
return;
nIter = 0;
nCubesInit = p->nCubes;
do {
nCubesOld = p->nCubes;
Min_EsopRewrite( p );
nIter++;
}
while ( 100.0*(nCubesOld - p->nCubes)/nCubesOld > 3.0 );
// printf( "%d:%d->%d ", nIter, nCubesInit, p->nCubes );
}
/**Function*************************************************************
Synopsis [Performs one round of rewriting using distance 2 cubes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Min_EsopRewrite( Min_Man_t * p )
{
Min_Cube_t * pCube, ** ppPrev;
Min_Cube_t * pThis, ** ppPrevT;
int v00, v01, v10, v11, Var0, Var1, Index, nCubesOld;
int nPairs = 0;
// insert the bubble before the first cube
p->pBubble->pNext = p->ppStore[0];
p->ppStore[0] = p->pBubble;
p->pBubble->nLits = 0;
// go through the cubes
while ( 1 )
{
// get the index of the bubble
Index = p->pBubble->nLits;
// find the bubble
Min_CoverForEachCubePrev( p->ppStore[Index], pCube, ppPrev )
if ( pCube == p->pBubble )
break;
assert( pCube == p->pBubble );
// remove the bubble, get the next cube after the bubble
*ppPrev = p->pBubble->pNext;
pCube = p->pBubble->pNext;
if ( pCube == NULL )
for ( Index++; Index <= p->nVars; Index++ )
if ( p->ppStore[Index] )
{
ppPrev = &(p->ppStore[Index]);
pCube = p->ppStore[Index];
break;
}
// stop if there is no more cubes
if ( pCube == NULL )
break;
// find the first dist2 cube
Min_CoverForEachCubePrev( pCube->pNext, pThis, ppPrevT )
if ( Min_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) )
break;
if ( pThis == NULL && Index < p->nVars )
Min_CoverForEachCubePrev( p->ppStore[Index+1], pThis, ppPrevT )
if ( Min_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) )
break;
if ( pThis == NULL && Index < p->nVars - 1 )
Min_CoverForEachCubePrev( p->ppStore[Index+2], pThis, ppPrevT )
if ( Min_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) )
break;
// continue if there is no dist2 cube
if ( pThis == NULL )
{
// insert the bubble after the cube
p->pBubble->pNext = pCube->pNext;
pCube->pNext = p->pBubble;
p->pBubble->nLits = pCube->nLits;
continue;
}
nPairs++;
// remove the cubes, insert the bubble instead of pCube
*ppPrevT = pThis->pNext;
*ppPrev = p->pBubble;
p->pBubble->pNext = pCube->pNext;
p->pBubble->nLits = pCube->nLits;
p->nCubes -= 2;
// Exorlink-2:
// A{v00} B{v01} + A{v10} B{v11} =
// A{v00+v10} B{v01} + A{v10} B{v01+v11} =
// A{v00} B{v01+v11} + A{v00+v10} B{v11}
// save the dist2 parameters
v00 = Min_CubeGetVar( pCube, Var0 );
v01 = Min_CubeGetVar( pCube, Var1 );
v10 = Min_CubeGetVar( pThis, Var0 );
v11 = Min_CubeGetVar( pThis, Var1 );
//printf( "\n" );
//Min_CubeWrite( stdout, pCube );
//Min_CubeWrite( stdout, pThis );
// derive the first pair of resulting cubes
Min_CubeXorVar( pCube, Var0, v10 );
pCube->nLits -= (v00 != 3);
pCube->nLits += ((v00 ^ v10) != 3);
Min_CubeXorVar( pThis, Var1, v01 );
pThis->nLits -= (v11 != 3);
pThis->nLits += ((v01 ^ v11) != 3);
// add the cubes
nCubesOld = p->nCubes;
while ( Min_EsopAddCube( p, pCube ) );
while ( Min_EsopAddCube( p, pThis ) );
// check if the cubes were absorbed
if ( p->nCubes < nCubesOld + 2 )
continue;
// pull out both cubes
assert( pThis == p->ppStore[pThis->nLits] );
p->ppStore[pThis->nLits] = pThis->pNext;
assert( pCube == p->ppStore[pCube->nLits] );
p->ppStore[pCube->nLits] = pCube->pNext;
p->nCubes -= 2;
// derive the second pair of resulting cubes
Min_CubeXorVar( pCube, Var0, v10 );
pCube->nLits -= ((v00 ^ v10) != 3);
pCube->nLits += (v00 != 3);
Min_CubeXorVar( pCube, Var1, v11 );
pCube->nLits -= (v01 != 3);
pCube->nLits += ((v01 ^ v11) != 3);
Min_CubeXorVar( pThis, Var0, v00 );
pThis->nLits -= (v10 != 3);
pThis->nLits += ((v00 ^ v10) != 3);
Min_CubeXorVar( pThis, Var1, v01 );
pThis->nLits -= ((v01 ^ v11) != 3);
pThis->nLits += (v11 != 3);
// add them anyhow
while ( Min_EsopAddCube( p, pCube ) );
while ( Min_EsopAddCube( p, pThis ) );
}
// printf( "Pairs = %d ", nPairs );
}
/**Function*************************************************************
Synopsis [Adds the cube to storage.]
Description [If the distance one cube is found, returns the transformed
cube. If there is no distance one, adds the given cube to storage.
Do not forget to clean the storage!]
SideEffects []
SeeAlso []
***********************************************************************/
int Min_EsopAddCube( Min_Man_t * p, Min_Cube_t * pCube )
{
Min_Cube_t * pThis, ** ppPrev;
// try to find the identical cube
Min_CoverForEachCubePrev( p->ppStore[pCube->nLits], pThis, ppPrev )
{
if ( Min_CubesAreEqual( pCube, pThis ) )
{
*ppPrev = pThis->pNext;
Min_CubeRecycle( p, pCube );
Min_CubeRecycle( p, pThis );
p->nCubes--;
return 0;
}
}
// find a distance-1 cube if it exists
if ( pCube->nLits < pCube->nVars )
Min_CoverForEachCubePrev( p->ppStore[pCube->nLits+1], pThis, ppPrev )
{
if ( Min_CubesDistOne( pCube, pThis, p->pTemp ) )
{
*ppPrev = pThis->pNext;
Min_CubesTransform( pCube, pThis, p->pTemp );
pCube->nLits++;
Min_CubeRecycle( p, pThis );
p->nCubes--;
return 1;
}
}
Min_CoverForEachCubePrev( p->ppStore[pCube->nLits], pThis, ppPrev )
{
if ( Min_CubesDistOne( pCube, pThis, p->pTemp ) )
{
*ppPrev = pThis->pNext;
Min_CubesTransform( pCube, pThis, p->pTemp );
pCube->nLits--;
Min_CubeRecycle( p, pThis );
p->nCubes--;
return 1;
}
}
if ( pCube->nLits > 0 )
Min_CoverForEachCubePrev( p->ppStore[pCube->nLits-1], pThis, ppPrev )
{
if ( Min_CubesDistOne( pCube, pThis, p->pTemp ) )
{
*ppPrev = pThis->pNext;
Min_CubesTransform( pCube, pThis, p->pTemp );
Min_CubeRecycle( p, pThis );
p->nCubes--;
return 1;
}
}
// add the cube
pCube->pNext = p->ppStore[pCube->nLits];
p->ppStore[pCube->nLits] = pCube;
p->nCubes++;
return 0;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/opt/xyz/xyzMinMan.c 0 → 100644
/**CFile****************************************************************
FileName [xyzMinMan.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Cover manipulation package.]
Synopsis [SOP manipulation.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: xyzMinMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "xyzInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Starts the minimization manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Min_Man_t * Min_ManAlloc( int nVars )
{
Min_Man_t * pMan;
// start the manager
pMan = ALLOC( Min_Man_t, 1 );
memset( pMan, 0, sizeof(Min_Man_t) );
pMan->nVars = nVars;
pMan->nWords = Abc_BitWordNum( nVars * 2 );
pMan->pMemMan = Extra_MmFixedStart( sizeof(Min_Cube_t) + sizeof(unsigned) * (pMan->nWords - 1) );
// allocate storage for the temporary cover
pMan->ppStore = ALLOC( Min_Cube_t *, pMan->nVars + 1 );
// create tautology cubes
Min_ManClean( pMan, nVars );
pMan->pOne0 = Min_CubeAlloc( pMan );
pMan->pOne1 = Min_CubeAlloc( pMan );
pMan->pTemp = Min_CubeAlloc( pMan );
pMan->pBubble = Min_CubeAlloc( pMan ); pMan->pBubble->uData[0] = 0;
// create trivial cubes
Min_ManClean( pMan, 1 );
pMan->pTriv0[0] = Min_CubeAllocVar( pMan, 0, 0 );
pMan->pTriv0[1] = Min_CubeAllocVar( pMan, 0, 1 );
pMan->pTriv1[0] = Min_CubeAllocVar( pMan, 0, 0 );
pMan->pTriv1[1] = Min_CubeAllocVar( pMan, 0, 1 );
return pMan;
}
/**Function*************************************************************
Synopsis [Cleans the minimization manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Min_ManClean( Min_Man_t * p, int nSupp )
{
// set the size of the cube manager
p->nVars = nSupp;
p->nWords = Abc_BitWordNum(2*nSupp);
// clean the storage
memset( p->ppStore, 0, sizeof(Min_Cube_t *) * (nSupp + 1) );
p->nCubes = 0;
}
/**Function*************************************************************
Synopsis [Stops the minimization manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Min_ManFree( Min_Man_t * p )
{
Extra_MmFixedStop ( p->pMemMan, 0 );
free( p->ppStore );
free( p );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/opt/xyz/xyzMinSop.c 0 → 100644
/**CFile****************************************************************
FileName [xyzMinSop.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Cover manipulation package.]
Synopsis [SOP manipulation.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: xyzMinSop.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "xyzInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static void Min_SopRewrite( Min_Man_t * p );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Min_SopMinimize( Min_Man_t * p )
{
int nCubesInit, nCubesOld, nIter;
if ( p->nCubes < 3 )
return;
nIter = 0;
nCubesInit = p->nCubes;
do {
nCubesOld = p->nCubes;
Min_SopRewrite( p );
nIter++;
}
while ( 100.0*(nCubesOld - p->nCubes)/nCubesOld > 3.0 );
// printf( "%d:%d->%d ", nIter, nCubesInit, p->nCubes );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Min_SopRewrite( Min_Man_t * p )
{
Min_Cube_t * pCube, ** ppPrev;
Min_Cube_t * pThis, ** ppPrevT;
Min_Cube_t * pTemp;
int v00, v01, v10, v11, Var0, Var1, Index;
int nPairs = 0;
// insert the bubble before the first cube
p->pBubble->pNext = p->ppStore[0];
p->ppStore[0] = p->pBubble;
p->pBubble->nLits = 0;
// go through the cubes
while ( 1 )
{
// get the index of the bubble
Index = p->pBubble->nLits;
// find the bubble
Min_CoverForEachCubePrev( p->ppStore[Index], pCube, ppPrev )
if ( pCube == p->pBubble )
break;
assert( pCube == p->pBubble );
// remove the bubble, get the next cube after the bubble
*ppPrev = p->pBubble->pNext;
pCube = p->pBubble->pNext;
if ( pCube == NULL )
for ( Index++; Index <= p->nVars; Index++ )
if ( p->ppStore[Index] )
{
ppPrev = &(p->ppStore[Index]);
pCube = p->ppStore[Index];
break;
}
// stop if there is no more cubes
if ( pCube == NULL )
break;
// find the first dist2 cube
Min_CoverForEachCubePrev( pCube->pNext, pThis, ppPrevT )
if ( Min_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) )
break;
if ( pThis == NULL && Index < p->nVars )
Min_CoverForEachCubePrev( p->ppStore[Index+1], pThis, ppPrevT )
if ( Min_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) )
break;
// continue if there is no dist2 cube
if ( pThis == NULL )
{
// insert the bubble after the cube
p->pBubble->pNext = pCube->pNext;
pCube->pNext = p->pBubble;
p->pBubble->nLits = pCube->nLits;
continue;
}
nPairs++;
// remove the cubes, insert the bubble instead of pCube
*ppPrevT = pThis->pNext;
*ppPrev = p->pBubble;
p->pBubble->pNext = pCube->pNext;
p->pBubble->nLits = pCube->nLits;
p->nCubes -= 2;
// save the dist2 parameters
v00 = Min_CubeGetVar( pCube, Var0 );
v01 = Min_CubeGetVar( pCube, Var1 );
v10 = Min_CubeGetVar( pThis, Var0 );
v11 = Min_CubeGetVar( pThis, Var1 );
assert( v00 != v10 && v01 != v11 );
assert( v00 != 3 || v01 != 3 );
assert( v10 != 3 || v11 != 3 );
// skip the case when rewriting is impossible
if ( v00 != 3 && v01 != 3 && v10 != 3 && v11 != 3 )
continue;
// if one of them does not have DC lit, move it
if ( v00 != 3 && v01 != 3 )
{
pTemp = pCube; pCube = pThis; pThis = pTemp;
Index = v00; v00 = v10; v10 = Index;
Index = v01; v01 = v11; v11 = Index;
}
//printf( "\n" );
//Min_CubeWrite( stdout, pCube );
//Min_CubeWrite( stdout, pThis );
// make sure the first cube has first var DC
if ( v00 != 3 )
{
assert( v01 == 3 );
Index = Var0; Var0 = Var1; Var1 = Index;
Index = v00; v00 = v01; v01 = Index;
Index = v10; v10 = v11; v11 = Index;
}
// consider both cases: both have DC lit
if ( v00 == 3 && v11 == 3 )
{
assert( v01 != 3 && v10 != 3 );
// try two reduced cubes
}
else // the first cube has DC lit
{
assert( v01 != 3 && v10 != 3 && v11 != 3 );
// try reduced and expanded cube
}
}
// printf( "Pairs = %d ", nPairs );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Min_SopAddCube( Min_Man_t * p, Min_Cube_t * pCube )
{
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Min_SopDist1Merge( Min_Man_t * p )
{
Min_Cube_t * pCube, * pCube2, * pCubeNew;
int i;
for ( i = p->nVars; i >= 0; i-- )
{
Min_CoverForEachCube( p->ppStore[i], pCube )
Min_CoverForEachCube( pCube->pNext, pCube2 )
{
assert( pCube->nLits == pCube2->nLits );
if ( !Min_CubesDistOne( pCube, pCube2, NULL ) )
continue;
pCubeNew = Min_CubesXor( p, pCube, pCube2 );
assert( pCubeNew->nLits == pCube->nLits - 1 );
pCubeNew->pNext = p->ppStore[pCubeNew->nLits];
p->ppStore[pCubeNew->nLits] = pCubeNew;
p->nCubes++;
}
}
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Min_SopContain( Min_Man_t * p )
{
Min_Cube_t * pCube, * pCube2, ** ppPrev;
int i, k;
for ( i = 0; i <= p->nVars; i++ )
{
Min_CoverForEachCube( p->ppStore[i], pCube )
Min_CoverForEachCubePrev( pCube->pNext, pCube2, ppPrev )
{
if ( !Min_CubesAreEqual( pCube, pCube2 ) )
continue;
*ppPrev = pCube2->pNext;
Min_CubeRecycle( p, pCube2 );
p->nCubes--;
}
for ( k = i + 1; k <= p->nVars; k++ )
Min_CoverForEachCubePrev( p->ppStore[k], pCube2, ppPrev )
{
if ( !Min_CubeIsContained( pCube, pCube2 ) )
continue;
*ppPrev = pCube2->pNext;
Min_CubeRecycle( p, pCube2 );
p->nCubes--;
}
}
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Min_Cube_t * Min_SopComplement( Min_Man_t * p, Min_Cube_t * pSharp )
{
Vec_Int_t * vVars;
Min_Cube_t * pCover, * pCube, * pNext, * pReady, * pThis, ** ppPrev;
int Num, Value, i;
// get the variables
vVars = Vec_IntAlloc( 100 );
// create the tautology cube
pCover = Min_CubeAlloc( p );
// sharp it with all cubes
Min_CoverForEachCube( pSharp, pCube )
Min_CoverForEachCubePrev( pCover, pThis, ppPrev )
{
if ( Min_CubesDisjoint( pThis, pCube ) )
continue;
// remember the next pointer
pNext = pThis->pNext;
// get the variables, in which pThis is '-' while pCube is fixed
Min_CoverGetDisjVars( pThis, pCube, vVars );
// generate the disjoint cubes
pReady = pThis;
Vec_IntForEachEntryReverse( vVars, Num, i )
{
// correct the literal
Min_CubeXorVar( pReady, vVars->pArray[i], 3 );
if ( i == 0 )
break;
// create the new cube and clean this value
Value = Min_CubeGetVar( pReady, vVars->pArray[i] );
pReady = Min_CubeDup( p, pReady );
Min_CubeXorVar( pReady, vVars->pArray[i], 3 ^ Value );
// add to the cover
*ppPrev = pReady;
ppPrev = &pReady->pNext;
}
pThis = pReady;
pThis->pNext = pNext;
}
Vec_IntFree( vVars );
// perform dist-1 merge and contain
Min_CoverExpandRemoveEqual( p, pCover );
Min_SopDist1Merge( p );
Min_SopContain( p );
return Min_CoverCollect( p, p->nVars );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/opt/xyz/xyzMinUtil.c 0 → 100644
/**CFile****************************************************************
FileName [xyzMinUtil.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Cover manipulation package.]
Synopsis [Utilities.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: xyzMinUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "xyzInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Min_CubeWrite( FILE * pFile, Min_Cube_t * pCube )
{
int i;
assert( (int)pCube->nLits == Min_CubeCountLits(pCube) );
for ( i = 0; i < (int)pCube->nVars; i++ )
if ( Min_CubeHasBit(pCube, i*2) )
{
if ( Min_CubeHasBit(pCube, i*2+1) )
fprintf( pFile, "-" );
else
fprintf( pFile, "0" );
}
else
{
if ( Min_CubeHasBit(pCube, i*2+1) )
fprintf( pFile, "1" );
else
fprintf( pFile, "?" );
}
fprintf( pFile, " 1\n" );
// fprintf( pFile, " %d\n", pCube->nLits );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Min_CoverWrite( FILE * pFile, Min_Cube_t * pCover )
{
Min_Cube_t * pCube;
Min_CoverForEachCube( pCover, pCube )
Min_CubeWrite( pFile, pCube );
printf( "\n" );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Min_CoverWriteFile( Min_Cube_t * pCover, char * pName, int fEsop )
{
char Buffer[1000];
Min_Cube_t * pCube;
FILE * pFile;
int i;
sprintf( Buffer, "%s.esop", pName );
for ( i = strlen(Buffer) - 1; i >= 0; i-- )
if ( Buffer[i] == '<' || Buffer[i] == '>' )
Buffer[i] = '_';
pFile = fopen( Buffer, "w" );
fprintf( pFile, "# %s cover for output %s generated by ABC on %s\n", fEsop? "ESOP":"SOP", pName, Extra_TimeStamp() );
fprintf( pFile, ".i %d\n", pCover? pCover->nVars : 0 );
fprintf( pFile, ".o %d\n", 1 );
fprintf( pFile, ".p %d\n", Min_CoverCountCubes(pCover) );
if ( fEsop ) fprintf( pFile, ".type esop\n" );
Min_CoverForEachCube( pCover, pCube )
Min_CubeWrite( pFile, pCube );
fprintf( pFile, ".e\n" );
fclose( pFile );
}
/**Function*************************************************************
Synopsis [Performs one round of rewriting using distance 2 cubes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Min_CoverCheck( Min_Man_t * p )
{
Min_Cube_t * pCube;
int i;
for ( i = 0; i <= p->nVars; i++ )
Min_CoverForEachCube( p->ppStore[i], pCube )
assert( i == (int)pCube->nLits );
}
/**Function*************************************************************
Synopsis [Converts the cover from the sorted structure.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Min_Cube_t * Min_CoverCollect( Min_Man_t * p, int nSuppSize )
{
Min_Cube_t * pCov = NULL, ** ppTail = &pCov;
Min_Cube_t * pCube, * pCube2;
int i;
for ( i = 0; i <= nSuppSize; i++ )
{
Min_CoverForEachCubeSafe( p->ppStore[i], pCube, pCube2 )
{
assert( i == (int)pCube->nLits );
*ppTail = pCube;
ppTail = &pCube->pNext;
}
}
*ppTail = NULL;
return pCov;
}
/**Function*************************************************************
Synopsis [Sorts the cover in the increasing number of literals.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Min_CoverExpand( Min_Man_t * p, Min_Cube_t * pCover )
{
Min_Cube_t * pCube, * pCube2;
Min_ManClean( p, p->nVars );
Min_CoverForEachCubeSafe( pCover, pCube, pCube2 )
{
pCube->pNext = p->ppStore[pCube->nLits];
p->ppStore[pCube->nLits] = pCube;
p->nCubes++;
}
}
/**Function*************************************************************
Synopsis [Sorts the cover in the increasing number of literals.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Min_CoverSuppVarNum( Min_Man_t * p, Min_Cube_t * pCover )
{
Min_Cube_t * pCube;
int i, Counter;
if ( pCover == NULL )
return 0;
// clean the cube
for ( i = 0; i < (int)pCover->nWords; i++ )
p->pTemp->uData[i] = ~((unsigned)0);
// add the bit data
Min_CoverForEachCube( pCover, pCube )
for ( i = 0; i < (int)pCover->nWords; i++ )
p->pTemp->uData[i] &= pCube->uData[i];
// count the vars
Counter = 0;
for ( i = 0; i < (int)pCover->nVars; i++ )
Counter += ( Min_CubeGetVar(p->pTemp, i) != 3 );
return Counter;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/opt/xyz/xyzTest.c 0 → 100644
/**CFile****************************************************************
FileName [xyzTest.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Cover manipulation package.]
Synopsis [Testing procedures.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: xyzTest.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "xyz.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkXyzTestSop( Abc_Ntk_t * pNtk )
{
return NULL;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/sat/asat/added.c
......@@ -71,6 +71,11 @@ void Asat_SolverWriteDimacs( solver * p, char * pFileName, lit* assumptionsBegin
// start the file
pFile = fopen( pFileName, "wb" );
if ( pFile == NULL )
{
printf( "Asat_SolverWriteDimacs(): Cannot open the ouput file.\n" );
return;
}
fprintf( pFile, "c CNF generated by ABC on %s\n", Extra_TimeStamp() );
fprintf( pFile, "p cnf %d %d\n", p->size, nClauses );
......
src/sat/csat/csat_apis.c
......@@ -188,7 +188,7 @@ int CSAT_AddGate( CSAT_Manager mng, enum GateType type, char * name, int nofi, c
case CSAT_BAND:
if ( nofi < 1 )
{ printf( "CSAT_AddGate: The AND gate \"%s\" no fanins.\n", name ); return 0; }
pSop = Abc_SopCreateAnd( mng->pNtk->pManFunc, nofi );
pSop = Abc_SopCreateAnd( mng->pNtk->pManFunc, nofi, NULL );
break;
case CSAT_BNAND:
if ( nofi < 1 )
......
src/sat/fraig/fraigMan.c
......@@ -104,7 +104,8 @@ Fraig_Man_t * Fraig_ManCreate( Fraig_Params_t * pParams )
Fraig_Man_t * p;
// set the random seed for simulation
srand( 0xFEEDDEAF );
// srand( 0xFEEDDEAF );
srand( 0xDEADCAFE );
// set parameters for equivalence checking
if ( pParams == NULL )
......
src/sat/fraig/fraigSat.c
......@@ -1049,6 +1049,26 @@ void Fraig_SupergateAddClausesMux( Fraig_Man_t * p, Fraig_Node_t * pNode )
Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarF, 1) );
RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
assert( RetValue );
// two additional clauses
// t' & e' -> f'
// t & e -> f
// t + e + f'
// t' + e' + f
Msat_IntVecClear( p->vProj );
Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarT, 0^fCompT) );
Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarE, 0^fCompE) );
Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarF, 1) );
RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
assert( RetValue );
Msat_IntVecClear( p->vProj );
Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarT, 1^fCompT) );
Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarE, 1^fCompE) );
Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarF, 0) );
RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
assert( RetValue );
}
......
src/sat/msat/msatSolverCore.c
......@@ -176,7 +176,7 @@ bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTra
if ( nBackTrackLimit > 0 )
break;
// if the runtime limit is exceeded, quit the restart loop
if ( clock() - timeStart >= nTimeLimit * CLOCKS_PER_SEC )
if ( nTimeLimit > 0 && clock() - timeStart >= nTimeLimit * CLOCKS_PER_SEC )
break;
}
Msat_SolverCancelUntil( p, 0 );
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment