summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/aig/gia/gia.h1
-rw-r--r--src/aig/gia/giaDup.c64
-rw-r--r--src/base/abci/abc.c187
-rw-r--r--src/base/wlc/wlcCom.c15
-rw-r--r--src/base/wln/wlnRtl.c6
5 files changed, 265 insertions, 8 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 5548def6..d871905c 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -1351,6 +1351,7 @@ extern Gia_Man_t * Gia_ManPermuteInputs( Gia_Man_t * p, int nPpis, int n
extern Gia_Man_t * Gia_ManDupDfsClasses( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupTopAnd( Gia_Man_t * p, int fVerbose );
extern Gia_Man_t * Gia_ManMiter( Gia_Man_t * pAig0, Gia_Man_t * pAig1, int nInsDup, int fDualOut, int fSeq, int fImplic, int fVerbose );
+extern Gia_Man_t * Gia_ManMiterInverse( Gia_Man_t * pBot, Gia_Man_t * pTop, int fDualOut, int fVerbose );
extern Gia_Man_t * Gia_ManDupAndOr( Gia_Man_t * p, int nOuts, int fUseOr, int fCompl );
extern Gia_Man_t * Gia_ManDupZeroUndc( Gia_Man_t * p, char * pInit, int nNewPis, int fGiaSimple, int fVerbose );
extern Gia_Man_t * Gia_ManMiter2( Gia_Man_t * p, char * pInit, int fVerbose );
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index b3fcd295..da4881cd 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -2934,6 +2934,70 @@ Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int nInsDup, int fDual
/**Function*************************************************************
+ Synopsis [Creates miter of two designs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManMiterInverse( Gia_Man_t * pBot, Gia_Man_t * pTop, int fDualOut, int fVerbose )
+{
+ Gia_Man_t * pNew, * pTemp;
+ Gia_Obj_t * pObj;
+ int i, iLit;
+ int nInputs1 = Gia_ManCiNum(pTop) - Gia_ManCoNum(pBot);
+ int nInputs2 = Gia_ManCiNum(pBot) - Gia_ManCoNum(pTop);
+ if ( nInputs1 == nInputs2 )
+ printf( "Assuming that the circuits have %d shared inputs, ordered first.\n", nInputs1 );
+ else
+ {
+ printf( "The number of inputs and outputs does not match.\n" );
+ return NULL;
+ }
+ pNew = Gia_ManStart( Gia_ManObjNum(pBot) + Gia_ManObjNum(pTop) );
+ pNew->pName = Abc_UtilStrsav( "miter" );
+ Gia_ManFillValue( pBot );
+ Gia_ManFillValue( pTop );
+ Gia_ManConst0(pBot)->Value = 0;
+ Gia_ManConst0(pTop)->Value = 0;
+ Gia_ManHashAlloc( pNew );
+ Gia_ManForEachCi( pBot, pObj, i )
+ pObj->Value = Gia_ManAppendCi( pNew );
+ Gia_ManForEachCo( pBot, pObj, i )
+ Gia_ManMiter_rec( pNew, pBot, Gia_ObjFanin0(pObj) );
+ Gia_ManForEachCo( pBot, pObj, i )
+ pObj->Value = Gia_ObjFanin0Copy(pObj);
+ Gia_ManForEachCi( pTop, pObj, i )
+ if ( i < nInputs1 )
+ pObj->Value = Gia_ManCi(pBot, i)->Value;
+ else
+ pObj->Value = Gia_ManCo(pBot, i-nInputs1)->Value;
+ Gia_ManForEachCo( pTop, pObj, i )
+ Gia_ManMiter_rec( pNew, pTop, Gia_ObjFanin0(pObj) );
+ Gia_ManForEachCo( pTop, pObj, i )
+ {
+ if ( fDualOut )
+ {
+ Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+ Gia_ManAppendCo( pNew, Gia_ManCi(pBot, i+nInputs1)->Value );
+ }
+ else
+ {
+ iLit = Gia_ManHashXor( pNew, Gia_ObjFanin0Copy(pObj), Gia_ManCi(pBot, i+nInputs1)->Value );
+ Gia_ManAppendCo( pNew, iLit );
+ }
+ }
+ Gia_ManHashStop( pNew );
+ pNew = Gia_ManCleanup( pTemp = pNew );
+ Gia_ManStop( pTemp );
+ return pNew;
+}
+
+/**Function*************************************************************
+
Synopsis [Computes the AND of all POs.]
Description []
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 70479041..1d97f5e4 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -469,6 +469,7 @@ static int Abc_CommandAbc9Reduce ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9EquivMark ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9EquivFilter ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Cec ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9ICec ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Verify ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Sweep ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Force ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -1212,6 +1213,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&equiv_mark", Abc_CommandAbc9EquivMark, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&equiv_filter", Abc_CommandAbc9EquivFilter, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&cec", Abc_CommandAbc9Cec, 0 );
+ Cmd_CommandAdd( pAbc, "ABC9", "&icec", Abc_CommandAbc9ICec, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&verify", Abc_CommandAbc9Verify, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&sweep", Abc_CommandAbc9Sweep, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&force", Abc_CommandAbc9Force, 0 );
@@ -37950,6 +37952,191 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandAbc9ICec( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ Cec_ParCec_t ParsCec, * pPars = &ParsCec;
+ FILE * pFile;
+ Gia_Man_t * pGias[2] = {NULL, NULL}, * pMiter;
+ char ** pArgvNew;
+ int c, nArgcNew, fUseNew = 0, fDumpMiter = 0;
+ Cec_ManCecSetDefaultParams( pPars );
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "CTaxvwh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'C':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nBTLimit = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nBTLimit < 0 )
+ goto usage;
+ break;
+ case 'T':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->TimeLimit = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->TimeLimit < 0 )
+ goto usage;
+ break;
+ case 'a':
+ fDumpMiter ^= 1;
+ break;
+ case 'x':
+ fUseNew ^= 1;
+ break;
+ case 'v':
+ pPars->fVerbose ^= 1;
+ break;
+ case 'w':
+ pPars->fVeryVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ pArgvNew = argv + globalUtilOptind;
+ nArgcNew = argc - globalUtilOptind;
+ if ( nArgcNew > 2 )
+ {
+ Abc_Print( -1, "Abc_CommandAbc9Cec(): Wrong number of command-line arguments.\n" );
+ return 1;
+ }
+ if ( nArgcNew == 2 )
+ {
+ char * pFileNames[2] = { pArgvNew[0], pArgvNew[1] }, * pTemp;
+ int n;
+ for ( n = 0; n < 2; n++ )
+ {
+ // fix the wrong symbol
+ for ( pTemp = pFileNames[n]; *pTemp; pTemp++ )
+ if ( *pTemp == '>' )
+ *pTemp = '\\';
+ if ( (pFile = fopen( pFileNames[n], "r" )) == NULL )
+ {
+ Abc_Print( -1, "Cannot open input file \"%s\". ", pFileNames[n] );
+ if ( (pFileNames[n] = Extra_FileGetSimilarName( pFileNames[n], ".aig", NULL, NULL, NULL, NULL )) )
+ Abc_Print( 1, "Did you mean \"%s\"?", pFileNames[n] );
+ Abc_Print( 1, "\n" );
+ return 1;
+ }
+ fclose( pFile );
+ pGias[n] = Gia_AigerRead( pFileNames[n], 0, 0, 0 );
+ if ( pGias[n] == NULL )
+ {
+ Abc_Print( -1, "Reading AIGER from file \"%s\" has failed.\n", pFileNames[n] );
+ return 0;
+ }
+ }
+ }
+ else
+ {
+ char * FileName, * pTemp;
+ if ( pAbc->pGia == NULL )
+ {
+ Abc_Print( -1, "Abc_CommandAbc9Cec(): There is no current AIG.\n" );
+ return 1;
+ }
+ pGias[0] = pAbc->pGia;
+ if ( nArgcNew == 1 )
+ FileName = pArgvNew[0];
+ else
+ {
+ assert( nArgcNew == 0 );
+ if ( pAbc->pGia->pSpec == NULL )
+ {
+ Abc_Print( -1, "File name is not given on the command line.\n" );
+ return 1;
+ }
+ FileName = pAbc->pGia->pSpec;
+ }
+ // fix the wrong symbol
+ for ( pTemp = FileName; *pTemp; pTemp++ )
+ if ( *pTemp == '>' )
+ *pTemp = '\\';
+ if ( (pFile = fopen( FileName, "r" )) == NULL )
+ {
+ Abc_Print( -1, "Cannot open input file \"%s\". ", FileName );
+ if ( (FileName = Extra_FileGetSimilarName( FileName, ".aig", NULL, NULL, NULL, NULL )) )
+ Abc_Print( 1, "Did you mean \"%s\"?", FileName );
+ Abc_Print( 1, "\n" );
+ return 1;
+ }
+ fclose( pFile );
+ pGias[1] = Gia_AigerRead( FileName, 0, 0, 0 );
+ if ( pGias[1] == NULL )
+ {
+ Abc_Print( -1, "Reading AIGER has failed.\n" );
+ return 0;
+ }
+ }
+ // compute the miter
+ pMiter = Gia_ManMiterInverse( pGias[0], pGias[1], !fUseNew, pPars->fVerbose );
+ if ( pMiter )
+ {
+ if ( fDumpMiter )
+ {
+ Abc_Print( 0, "The verification miter is written into file \"%s\".\n", "cec_miter.aig" );
+ Gia_AigerWrite( pMiter, "cec_miter.aig", 0, 0, 0 );
+ }
+ if ( fUseNew )
+ {
+ abctime clk = Abc_Clock();
+ extern Gia_Man_t * Cec4_ManSimulateTest3( Gia_Man_t * p, int nBTLimit, int fVerbose );
+ Gia_Man_t * pNew = Cec4_ManSimulateTest3( pMiter, pPars->nBTLimit, pPars->fVerbose );
+ if ( Gia_ManAndNum(pNew) == 0 )
+ Abc_Print( 1, "Networks are equivalent. " );
+ else
+ Abc_Print( 1, "Networks are UNDECIDED. " );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ Gia_ManStop( pNew );
+ }
+ else
+ {
+ pAbc->Status = Cec_ManVerify( pMiter, pPars );
+ Abc_FrameReplaceCex( pAbc, &pGias[0]->pCexComb );
+ }
+ Gia_ManStop( pMiter );
+ }
+ if ( pGias[0] != pAbc->pGia )
+ Gia_ManStop( pGias[0] );
+ Gia_ManStop( pGias[1] );
+ return 0;
+
+usage:
+ Abc_Print( -2, "usage: &icec [-CT num] [-axvwh]\n" );
+ Abc_Print( -2, "\t combinational equivalence checker for inverse circuits\n" );
+ Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
+ Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", pPars->TimeLimit );
+ Abc_Print( -2, "\t-a : toggle writing the miter [default = %s]\n", fDumpMiter? "yes":"no");
+ Abc_Print( -2, "\t-x : toggle using new solver [default = %s]\n", fUseNew? "yes":"no");
+ Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes":"no");
+ Abc_Print( -2, "\t-w : toggle printing SAT solver statistics [default = %s]\n", pPars->fVeryVerbose? "yes":"no");
+ Abc_Print( -2, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_CommandAbc9Verify( Abc_Frame_t * pAbc, int argc, char ** argv )
{
char * pFileSpec = NULL;
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index b6456ba4..b1573e73 100644
--- a/src/base/wlc/wlcCom.c
+++ b/src/base/wlc/wlcCom.c
@@ -310,7 +310,7 @@ usage:
******************************************************************************/
int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
{
- extern Gia_Man_t * Wln_BlastSystemVerilog( char * pFileName, char * pTopModule, int fSkipStrash, int fInvert, int fVerbose );
+ extern Gia_Man_t * Wln_BlastSystemVerilog( char * pFileName, char * pTopModule, int fSkipStrash, int fInvert, int fTechMap, int fVerbose );
extern Wln_Ntk_t * Wln_ReadSystemVerilog( char * pFileName, char * pTopModule, int fVerbose );
FILE * pFile;
@@ -319,10 +319,11 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
int fCollapse = 0;
int fBlast = 0;
int fInvert = 0;
+ int fTechMap = 0;
int fSkipStrash = 0;
int c, fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "Tcaisvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Tcaismvh" ) ) != EOF )
{
switch ( c )
{
@@ -347,6 +348,9 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
case 's':
fSkipStrash ^= 1;
break;
+ case 'm':
+ fTechMap ^= 1;
+ break;
case 'v':
fVerbose ^= 1;
break;
@@ -378,9 +382,9 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Gia_Man_t * pNew = NULL;
if ( !strcmp( Extra_FileNameExtension(pFileName), "v" ) )
- pNew = Wln_BlastSystemVerilog( pFileName, pTopModule, fSkipStrash, fInvert, fVerbose );
+ pNew = Wln_BlastSystemVerilog( pFileName, pTopModule, fSkipStrash, fInvert, fTechMap, fVerbose );
else if ( !strcmp( Extra_FileNameExtension(pFileName), "sv" ) )
- pNew = Wln_BlastSystemVerilog( pFileName, pTopModule, fSkipStrash, fInvert, fVerbose );
+ pNew = Wln_BlastSystemVerilog( pFileName, pTopModule, fSkipStrash, fInvert, fTechMap, fVerbose );
else
{
printf( "Abc_CommandYosys(): Unknown file extension.\n" );
@@ -404,13 +408,14 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
}
return 0;
usage:
- Abc_Print( -2, "usage: %%yosys [-T <module>] [-caisvh] <file_name>\n" );
+ Abc_Print( -2, "usage: %%yosys [-T <module>] [-caismvh] <file_name>\n" );
Abc_Print( -2, "\t reads Verilog or SystemVerilog using Yosys\n" );
Abc_Print( -2, "\t-T : specify the top module name (default uses \"-auto-top\"\n" );
Abc_Print( -2, "\t-c : toggle collapsing the design using Yosys [default = %s]\n", fCollapse? "yes": "no" );
Abc_Print( -2, "\t-a : toggle bit-blasting the design using Yosys [default = %s]\n", fBlast? "yes": "no" );
Abc_Print( -2, "\t-i : toggle interting the outputs (useful for miters) [default = %s]\n", fInvert? "yes": "no" );
Abc_Print( -2, "\t-s : toggle no structural hashing during bit-blasting [default = %s]\n", fSkipStrash? "no strash": "strash" );
+ Abc_Print( -2, "\t-m : toggle using \"techmap\" to blast operators [default = %s]\n", fTechMap? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
diff --git a/src/base/wln/wlnRtl.c b/src/base/wln/wlnRtl.c
index 040c74bb..aff88af9 100644
--- a/src/base/wln/wlnRtl.c
+++ b/src/base/wln/wlnRtl.c
@@ -120,15 +120,15 @@ Wln_Ntk_t * Wln_ReadSystemVerilog( char * pFileName, char * pTopModule, int fVer
unlink( pFileTemp );
return pNtk;
}
-Gia_Man_t * Wln_BlastSystemVerilog( char * pFileName, char * pTopModule, int fSkipStrash, int fInvert, int fVerbose )
+Gia_Man_t * Wln_BlastSystemVerilog( char * pFileName, char * pTopModule, int fSkipStrash, int fInvert, int fTechMap, int fVerbose )
{
Gia_Man_t * pGia = NULL;
char Command[1000];
char * pFileTemp = "_temp_.aig";
int fSVlog = strstr(pFileName, ".sv") != NULL;
- sprintf( Command, "%s -qp \"read_verilog %s%s; hierarchy %s%s; flatten; proc; aigmap; write_aiger %s\"",
+ sprintf( Command, "%s -qp \"read_verilog %s%s; hierarchy %s%s; flatten; proc; %saigmap; write_aiger %s\"",
Wln_GetYosysName(), fSVlog ? "-sv ":"", pFileName,
- pTopModule ? "-top " : "-auto-top", pTopModule ? pTopModule : "", pFileTemp );
+ pTopModule ? "-top " : "-auto-top", pTopModule ? pTopModule : "", fTechMap ? "techmap; setundef -zero; " : "", pFileTemp );
if ( fVerbose )
printf( "%s\n", Command );
if ( !Wln_ConvertToRtl(Command, pFileTemp) )
generated by cgit v1.2.3 (git 2.25.1) at 2025-10-31 00:33:16 +0000