summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/base/cba/cbaSimple.c100
-rw-r--r--src/sat/bmc/bmcChain.c2
2 files changed, 51 insertions, 51 deletions
diff --git a/src/base/cba/cbaSimple.c b/src/base/cba/cbaSimple.c
index 573a1720..628c205d 100644
--- a/src/base/cba/cbaSimple.c
+++ b/src/base/cba/cbaSimple.c
@@ -164,7 +164,7 @@ static int Ptr_ManCheckArray( Vec_Ptr_t * vArray )
assert( 0 );
return 0;
}
-Vec_Ptr_t * Ptr_ManDumpNode( Abc_Obj_t * pObj )
+Vec_Ptr_t * Ptr_ManDeriveNode( Abc_Obj_t * pObj )
{
Abc_Obj_t * pFanin; int i;
Vec_Ptr_t * vNode = Vec_PtrAlloc( 2 + Abc_ObjFaninNum(pObj) );
@@ -176,17 +176,17 @@ Vec_Ptr_t * Ptr_ManDumpNode( Abc_Obj_t * pObj )
assert( Ptr_ManCheckArray(vNode) );
return vNode;
}
-Vec_Ptr_t * Ptr_ManDumpNodes( Abc_Ntk_t * pNtk )
+Vec_Ptr_t * Ptr_ManDeriveNodes( Abc_Ntk_t * pNtk )
{
Abc_Obj_t * pObj; int i;
Vec_Ptr_t * vNodes = Vec_PtrAlloc( Abc_NtkNodeNum(pNtk) );
Abc_NtkForEachNode( pNtk, pObj, i )
- Vec_PtrPush( vNodes, Ptr_ManDumpNode(pObj) );
+ Vec_PtrPush( vNodes, Ptr_ManDeriveNode(pObj) );
assert( Ptr_ManCheckArray(vNodes) );
return vNodes;
}
-Vec_Ptr_t * Ptr_ManDumpBox( Abc_Obj_t * pObj )
+Vec_Ptr_t * Ptr_ManDeriveBox( Abc_Obj_t * pObj )
{
Abc_Obj_t * pNext; int i;
Abc_Ntk_t * pModel = Abc_ObjModel(pObj);
@@ -207,17 +207,17 @@ Vec_Ptr_t * Ptr_ManDumpBox( Abc_Obj_t * pObj )
assert( Ptr_ManCheckArray(vBox) );
return vBox;
}
-Vec_Ptr_t * Ptr_ManDumpBoxes( Abc_Ntk_t * pNtk )
+Vec_Ptr_t * Ptr_ManDeriveBoxes( Abc_Ntk_t * pNtk )
{
Abc_Obj_t * pObj; int i;
Vec_Ptr_t * vBoxes = Vec_PtrAlloc( Abc_NtkBoxNum(pNtk) );
Abc_NtkForEachBox( pNtk, pObj, i )
- Vec_PtrPush( vBoxes, Ptr_ManDumpBox(pObj) );
+ Vec_PtrPush( vBoxes, Ptr_ManDeriveBox(pObj) );
assert( Ptr_ManCheckArray(vBoxes) );
return vBoxes;
}
-Vec_Ptr_t * Ptr_ManDumpInputs( Abc_Ntk_t * pNtk )
+Vec_Ptr_t * Ptr_ManDeriveInputs( Abc_Ntk_t * pNtk )
{
Abc_Obj_t * pObj; int i;
Vec_Ptr_t * vSigs = Vec_PtrAlloc( Abc_NtkPiNum(pNtk) );
@@ -226,7 +226,7 @@ Vec_Ptr_t * Ptr_ManDumpInputs( Abc_Ntk_t * pNtk )
assert( Ptr_ManCheckArray(vSigs) );
return vSigs;
}
-Vec_Ptr_t * Ptr_ManDumpOutputs( Abc_Ntk_t * pNtk )
+Vec_Ptr_t * Ptr_ManDeriveOutputs( Abc_Ntk_t * pNtk )
{
Abc_Obj_t * pObj; int i;
Vec_Ptr_t * vSigs = Vec_PtrAlloc( Abc_NtkPoNum(pNtk) );
@@ -235,25 +235,25 @@ Vec_Ptr_t * Ptr_ManDumpOutputs( Abc_Ntk_t * pNtk )
assert( Ptr_ManCheckArray(vSigs) );
return vSigs;
}
-Vec_Ptr_t * Ptr_ManDumpNtk( Abc_Ntk_t * pNtk )
+Vec_Ptr_t * Ptr_ManDeriveNtk( Abc_Ntk_t * pNtk )
{
Vec_Ptr_t * vNtk = Vec_PtrAlloc( 5 );
Vec_PtrPush( vNtk, Abc_NtkName(pNtk) );
- Vec_PtrPush( vNtk, Ptr_ManDumpInputs(pNtk) );
- Vec_PtrPush( vNtk, Ptr_ManDumpOutputs(pNtk) );
- Vec_PtrPush( vNtk, Ptr_ManDumpNodes(pNtk) );
- Vec_PtrPush( vNtk, Ptr_ManDumpBoxes(pNtk) );
+ Vec_PtrPush( vNtk, Ptr_ManDeriveInputs(pNtk) );
+ Vec_PtrPush( vNtk, Ptr_ManDeriveOutputs(pNtk) );
+ Vec_PtrPush( vNtk, Ptr_ManDeriveNodes(pNtk) );
+ Vec_PtrPush( vNtk, Ptr_ManDeriveBoxes(pNtk) );
assert( Ptr_ManCheckArray(vNtk) );
return vNtk;
}
-Vec_Ptr_t * Ptr_ManDumpDes( Abc_Ntk_t * pNtk )
+Vec_Ptr_t * Ptr_ManDeriveDes( Abc_Ntk_t * pNtk )
{
Vec_Ptr_t * vDes;
Abc_Ntk_t * pTemp; int i;
vDes = Vec_PtrAlloc( 1 + Vec_PtrSize(pNtk->pDesign->vModules) );
Vec_PtrPush( vDes, pNtk->pDesign->pName );
Vec_PtrForEachEntry( Abc_Ntk_t *, pNtk->pDesign->vModules, pTemp, i )
- Vec_PtrPush( vDes, Ptr_ManDumpNtk(pTemp) );
+ Vec_PtrPush( vDes, Ptr_ManDeriveNtk(pTemp) );
assert( Ptr_ManCheckArray(vDes) );
return vDes;
}
@@ -269,7 +269,7 @@ Vec_Ptr_t * Ptr_ManDumpDes( Abc_Ntk_t * pNtk )
SeeAlso []
***********************************************************************/
-void Ptr_ManDumpNodeToBlif( FILE * pFile, Vec_Ptr_t * vNode )
+void Ptr_ManDumpNodeBlif( FILE * pFile, Vec_Ptr_t * vNode )
{
char * pName; int i;
fprintf( pFile, ".names" );
@@ -278,50 +278,50 @@ void Ptr_ManDumpNodeToBlif( FILE * pFile, Vec_Ptr_t * vNode )
fprintf( pFile, " %s\n", (char *)Vec_PtrEntry(vNode, 0) );
fprintf( pFile, "%s", Ptr_TypeToSop( (Ptr_ObjType_t)Abc_Ptr2Int(Vec_PtrEntry(vNode, 1)) ) );
}
-void Ptr_ManDumpNodesToBlif( FILE * pFile, Vec_Ptr_t * vNodes )
+void Ptr_ManDumpNodesBlif( FILE * pFile, Vec_Ptr_t * vNodes )
{
Vec_Ptr_t * vNode; int i;
Vec_PtrForEachEntry( Vec_Ptr_t *, vNodes, vNode, i )
- Ptr_ManDumpNodeToBlif( pFile, vNode );
+ Ptr_ManDumpNodeBlif( pFile, vNode );
}
-void Ptr_ManDumpBoxToBlif( FILE * pFile, Vec_Ptr_t * vBox )
+void Ptr_ManDumpBoxBlif( FILE * pFile, Vec_Ptr_t * vBox )
{
char * pName; int i;
- fprintf( pFile, "%s", (char *)Vec_PtrEntry(vBox, 0) );
+ fprintf( pFile, ".subckt %s", (char *)Vec_PtrEntry(vBox, 0) );
Vec_PtrForEachEntryStart( char *, vBox, pName, i, 2 )
fprintf( pFile, " %s=%s", pName, (char *)Vec_PtrEntry(vBox, i+1) ), i++;
fprintf( pFile, "\n" );
}
-void Ptr_ManDumpBoxesToBlif( FILE * pFile, Vec_Ptr_t * vBoxes )
+void Ptr_ManDumpBoxesBlif( FILE * pFile, Vec_Ptr_t * vBoxes )
{
Vec_Ptr_t * vBox; int i;
Vec_PtrForEachEntry( Vec_Ptr_t *, vBoxes, vBox, i )
- Ptr_ManDumpBoxToBlif( pFile, vBox );
+ Ptr_ManDumpBoxBlif( pFile, vBox );
}
-void Ptr_ManDumpSignalsToBlif( FILE * pFile, Vec_Ptr_t * vSigs, int fSkipLastComma )
+void Ptr_ManDumpSignalsBlif( FILE * pFile, Vec_Ptr_t * vSigs, int fSkipLastComma )
{
char * pSig; int i;
Vec_PtrForEachEntry( char *, vSigs, pSig, i )
fprintf( pFile, " %s", pSig );
}
-void Ptr_ManDumpModuleToBlif( FILE * pFile, Vec_Ptr_t * vNtk )
+void Ptr_ManDumpModuleBlif( FILE * pFile, Vec_Ptr_t * vNtk )
{
fprintf( pFile, ".model %s\n", (char *)Vec_PtrEntry(vNtk, 0) );
fprintf( pFile, ".inputs" );
- Ptr_ManDumpSignalsToBlif( pFile, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 1), 0 );
+ Ptr_ManDumpSignalsBlif( pFile, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 1), 0 );
fprintf( pFile, "\n" );
fprintf( pFile, ".outputs" );
- Ptr_ManDumpSignalsToBlif( pFile, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 2), 1 );
+ Ptr_ManDumpSignalsBlif( pFile, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 2), 1 );
fprintf( pFile, "\n\n" );
- Ptr_ManDumpNodesToBlif( pFile, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 3) );
+ Ptr_ManDumpNodesBlif( pFile, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 3) );
fprintf( pFile, "\n" );
- Ptr_ManDumpBoxesToBlif( pFile, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 4) );
+ Ptr_ManDumpBoxesBlif( pFile, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 4) );
fprintf( pFile, "\n" );
fprintf( pFile, ".end\n\n" );
}
-void Ptr_ManDumpToBlif( char * pFileName, Vec_Ptr_t * vDes )
+void Ptr_ManDumpBlif( char * pFileName, Vec_Ptr_t * vDes )
{
FILE * pFile;
Vec_Ptr_t * vNtk; int i;
@@ -333,7 +333,7 @@ void Ptr_ManDumpToBlif( char * pFileName, Vec_Ptr_t * vDes )
}
fprintf( pFile, "// Design \"%s\" written by ABC on %s\n\n", (char *)Vec_PtrEntry(vDes, 0), Extra_TimeStamp() );
Vec_PtrForEachEntryStart( Vec_Ptr_t *, vDes, vNtk, i, 1 )
- Ptr_ManDumpModuleToBlif( pFile, vNtk );
+ Ptr_ManDumpModuleBlif( pFile, vNtk );
fclose( pFile );
}
@@ -348,7 +348,7 @@ void Ptr_ManDumpToBlif( char * pFileName, Vec_Ptr_t * vDes )
SeeAlso []
***********************************************************************/
-void Ptr_ManDumpNodeToFile( FILE * pFile, Vec_Ptr_t * vNode )
+void Ptr_ManDumpNodeVerilog( FILE * pFile, Vec_Ptr_t * vNode )
{
char * pName; int i;
fprintf( pFile, "%s", Ptr_TypeToName( (Ptr_ObjType_t)Abc_Ptr2Int(Vec_PtrEntry(vNode, 1)) ) );
@@ -357,14 +357,14 @@ void Ptr_ManDumpNodeToFile( FILE * pFile, Vec_Ptr_t * vNode )
fprintf( pFile, ", %s", pName );
fprintf( pFile, " );\n" );
}
-void Ptr_ManDumpNodesToFile( FILE * pFile, Vec_Ptr_t * vNodes )
+void Ptr_ManDumpNodesVerilog( FILE * pFile, Vec_Ptr_t * vNodes )
{
Vec_Ptr_t * vNode; int i;
Vec_PtrForEachEntry( Vec_Ptr_t *, vNodes, vNode, i )
- Ptr_ManDumpNodeToFile( pFile, vNode );
+ Ptr_ManDumpNodeVerilog( pFile, vNode );
}
-void Ptr_ManDumpBoxToFile( FILE * pFile, Vec_Ptr_t * vBox )
+void Ptr_ManDumpBoxVerilog( FILE * pFile, Vec_Ptr_t * vBox )
{
char * pName; int i;
fprintf( pFile, "%s %s (", (char *)Vec_PtrEntry(vBox, 0), (char *)Vec_PtrEntry(vBox, 1) );
@@ -372,37 +372,37 @@ void Ptr_ManDumpBoxToFile( FILE * pFile, Vec_Ptr_t * vBox )
fprintf( pFile, " .%s(%s)%s", pName, (char *)Vec_PtrEntry(vBox, i+1), i >= Vec_PtrSize(vBox)-2 ? "" : "," ), i++;
fprintf( pFile, " );\n" );
}
-void Ptr_ManDumpBoxesToFile( FILE * pFile, Vec_Ptr_t * vBoxes )
+void Ptr_ManDumpBoxesVerilog( FILE * pFile, Vec_Ptr_t * vBoxes )
{
Vec_Ptr_t * vBox; int i;
Vec_PtrForEachEntry( Vec_Ptr_t *, vBoxes, vBox, i )
- Ptr_ManDumpBoxToFile( pFile, vBox );
+ Ptr_ManDumpBoxVerilog( pFile, vBox );
}
-void Ptr_ManDumpSignalsToFile( FILE * pFile, Vec_Ptr_t * vSigs, int fSkipLastComma )
+void Ptr_ManDumpSignalsVerilog( FILE * pFile, Vec_Ptr_t * vSigs, int fSkipLastComma )
{
char * pSig; int i;
Vec_PtrForEachEntry( char *, vSigs, pSig, i )
fprintf( pFile, " %s%s", pSig, (fSkipLastComma && i == Vec_PtrSize(vSigs)-1) ? "" : "," );
}
-void Ptr_ManDumpModuleToFile( FILE * pFile, Vec_Ptr_t * vNtk )
+void Ptr_ManDumpModuleVerilog( FILE * pFile, Vec_Ptr_t * vNtk )
{
fprintf( pFile, "module %s\n", (char *)Vec_PtrEntry(vNtk, 0) );
fprintf( pFile, "(\n" );
- Ptr_ManDumpSignalsToFile( pFile, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 1), 0 );
+ Ptr_ManDumpSignalsVerilog( pFile, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 1), 0 );
fprintf( pFile, "\n" );
- Ptr_ManDumpSignalsToFile( pFile, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 2), 1 );
+ Ptr_ManDumpSignalsVerilog( pFile, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 2), 1 );
fprintf( pFile, "\n);\ninput" );
- Ptr_ManDumpSignalsToFile( pFile, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 1), 1 );
+ Ptr_ManDumpSignalsVerilog( pFile, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 1), 1 );
fprintf( pFile, ";\noutput" );
- Ptr_ManDumpSignalsToFile( pFile, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 2), 1 );
+ Ptr_ManDumpSignalsVerilog( pFile, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 2), 1 );
fprintf( pFile, ";\n\n" );
- Ptr_ManDumpNodesToFile( pFile, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 3) );
+ Ptr_ManDumpNodesVerilog( pFile, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 3) );
fprintf( pFile, "\n" );
- Ptr_ManDumpBoxesToFile( pFile, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 4) );
+ Ptr_ManDumpBoxesVerilog( pFile, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 4) );
fprintf( pFile, "endmodule\n\n" );
}
-void Ptr_ManDumpToFile( char * pFileName, Vec_Ptr_t * vDes )
+void Ptr_ManDumpVerilog( char * pFileName, Vec_Ptr_t * vDes )
{
FILE * pFile;
Vec_Ptr_t * vNtk; int i;
@@ -414,7 +414,7 @@ void Ptr_ManDumpToFile( char * pFileName, Vec_Ptr_t * vDes )
}
fprintf( pFile, "// Design \"%s\" written by ABC on %s\n\n", (char *)Vec_PtrEntry(vDes, 0), Extra_TimeStamp() );
Vec_PtrForEachEntryStart( Vec_Ptr_t *, vDes, vNtk, i, 1 )
- Ptr_ManDumpModuleToFile( pFile, vNtk );
+ Ptr_ManDumpModuleVerilog( pFile, vNtk );
fclose( pFile );
}
@@ -499,14 +499,14 @@ void Ptr_ManFreeDes( Vec_Ptr_t * vDes )
void Ptr_ManExperiment( Abc_Ntk_t * pNtk )
{
abctime clk = Abc_Clock();
- Vec_Ptr_t * vDes = Ptr_ManDumpDes( pNtk );
+ char * pFileName = Extra_FileNameGenericAppend(pNtk->pDesign->pName, "_out.blif");
+ Vec_Ptr_t * vDes = Ptr_ManDeriveDes( pNtk );
printf( "Converting to Ptr: Memory = %6.3f MB ", 1.0*Ptr_ManMemDes(vDes)/(1<<20) );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
- Ptr_ManDumpToFile( Extra_FileNameGenericAppend(pNtk->pDesign->pName, "_out.v"), vDes );
- printf( "Finished writing output file \"%s\".\n", Extra_FileNameGenericAppend(pNtk->pDesign->pName, "_out.v") );
+ Ptr_ManDumpBlif( pFileName, vDes );
+ printf( "Finished writing output file \"%s\". ", pFileName );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
Ptr_ManFreeDes( vDes );
- Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
diff --git a/src/sat/bmc/bmcChain.c b/src/sat/bmc/bmcChain.c
index 6ef96560..324c7f6d 100644
--- a/src/sat/bmc/bmcChain.c
+++ b/src/sat/bmc/bmcChain.c
@@ -212,7 +212,7 @@ Vec_Int_t * Bmc_ChainFindFailedOutputs( Gia_Man_t * p, Vec_Ptr_t * vCexes )
Gia_Man_t * pInit;
Gia_Obj_t * pObj;
sat_solver * pSat;
- int i, j, k = 0, Lit, status = 0;
+ int i, j, Lit, status = 0;
// derive output logic cones
pInit = Gia_ManDupPosAndPropagateInit( p );
// derive SAT solver and test
generated by cgit v1.2.3 (git 2.25.1) at 2025-10-31 06:51:04 +0000