summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/gia/gia.h2
-rw-r--r--src/aig/gia/giaDup.c12
-rw-r--r--src/aig/gia/giaEquiv.c4
-rw-r--r--src/aig/gia/giaTim.c2
-rw-r--r--src/base/abci/abc.c66
-rw-r--r--src/proof/cec/cecCec.c2
6 files changed, 68 insertions, 20 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 2083f8ea..cf033362 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -852,7 +852,7 @@ extern Gia_Man_t * Gia_ManDupWithNewPo( Gia_Man_t * p1, Gia_Man_t * p2 )
extern Gia_Man_t * Gia_ManDupDfsCiMap( Gia_Man_t * p, int * pCi2Lit, Vec_Int_t * vLits );
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 fDualOut, int fSeq, int fVerbose );
+extern Gia_Man_t * Gia_ManMiter( Gia_Man_t * pAig0, Gia_Man_t * pAig1, int nInsDup, int fDualOut, int fSeq, int fVerbose );
extern Gia_Man_t * Gia_ManTransformMiter( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManChoiceMiter( Vec_Ptr_t * vGias );
extern Gia_Man_t * Gia_ManDupWithConstraints( Gia_Man_t * p, Vec_Int_t * vPoTypes );
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 37bdfefd..2782ccf1 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -1650,7 +1650,7 @@ int Gia_ManMiter_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
SeeAlso []
***********************************************************************/
-Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int fDualOut, int fSeq, int fVerbose )
+Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int nInsDup, int fDualOut, int fSeq, int fVerbose )
{
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj;
@@ -1702,7 +1702,10 @@ Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int fDualOut, int fSeq
Gia_ManForEachPi( p0, pObj, i )
pObj->Value = Gia_ManAppendCi( pNew );
Gia_ManForEachPi( p1, pObj, i )
- pObj->Value = Gia_ObjToLit( pNew, Gia_ManPi(pNew, i) );
+ if ( i < Gia_ManPiNum(p1) - nInsDup )
+ pObj->Value = Gia_ObjToLit( pNew, Gia_ManPi(pNew, i) );
+ else
+ pObj->Value = Gia_ManAppendCi( pNew );
// create latch outputs
Gia_ManForEachRo( p0, pObj, i )
pObj->Value = Gia_ManAppendCi( pNew );
@@ -1743,7 +1746,10 @@ Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int fDualOut, int fSeq
Gia_ManForEachCi( p0, pObj, i )
pObj->Value = Gia_ManAppendCi( pNew );
Gia_ManForEachCi( p1, pObj, i )
- pObj->Value = Gia_ObjToLit( pNew, Gia_ManCi(pNew, i) );
+ if ( i < Gia_ManPiNum(p1) - nInsDup )
+ pObj->Value = Gia_ObjToLit( pNew, Gia_ManCi(pNew, i) );
+ else
+ pObj->Value = Gia_ManAppendCi( pNew );
// create combinational outputs
Gia_ManForEachCo( p0, pObj, i )
{
diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
index 5ddd9b08..c7d4d5c7 100644
--- a/src/aig/gia/giaEquiv.c
+++ b/src/aig/gia/giaEquiv.c
@@ -1775,7 +1775,7 @@ int Gia_ManFilterEquivsForSpeculation( Gia_Man_t * pGia, char * pName1, char * p
Abc_Print( 1, "Cannot read second file %s.\n", pName2 );
return 0;
}
- pMiter = Gia_ManMiter( pGia1, pGia2, 0, 1, 0 );
+ pMiter = Gia_ManMiter( pGia1, pGia2, 0, 0, 1, 0 );
if ( pMiter == NULL )
{
Gia_ManStop( pGia1 );
@@ -1914,7 +1914,7 @@ int Gia_ManFilterEquivsUsingParts( Gia_Man_t * pGia, char * pName1, char * pName
Abc_Print( 1, "Cannot read second file %s.\n", pName2 );
return 0;
}
- pMiter = Gia_ManMiter( pGia1, pGia2, 0, 1, 0 );
+ pMiter = Gia_ManMiter( pGia1, pGia2, 0, 0, 1, 0 );
if ( pMiter == NULL )
{
Gia_ManStop( pGia1 );
diff --git a/src/aig/gia/giaTim.c b/src/aig/gia/giaTim.c
index a00c6d0c..f4b5bcb6 100644
--- a/src/aig/gia/giaTim.c
+++ b/src/aig/gia/giaTim.c
@@ -553,7 +553,7 @@ int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, void * pParsInit )
pGia1 = Gia_ManDupCollapse( pGia, pGia->pAigExtra, NULL );
Vec_IntFreeP( &vBoxPres );
// compute the miter
- pMiter = Gia_ManMiter( pGia0, pGia1, 1, 0, fVerbose );
+ pMiter = Gia_ManMiter( pGia0, pGia1, 0, 1, 0, fVerbose );
if ( pMiter )
{
Cec_ParCec_t ParsCec, * pPars = &ParsCec;
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index c7ffe95a..bb021ca1 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -15249,16 +15249,27 @@ int Abc_CommandInit( Abc_Frame_t * pAbc, int argc, char ** argv )
int fOnes;
int fRandom;
int fDontCare;
+ char * pInitStr;
// set defaults
fZeros = 0;
fOnes = 0;
fRandom = 0;
fDontCare = 0;
+ pInitStr = NULL;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "zordh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Szordh" ) ) != EOF )
{
switch ( c )
{
+ case 'S':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-S\" should be followed by a file name.\n" );
+ goto usage;
+ }
+ pInitStr = argv[globalUtilOptind];
+ globalUtilOptind++;
+ break;
case 'z':
fZeros ^= 1;
break;
@@ -15290,6 +15301,23 @@ int Abc_CommandInit( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
}
+ if ( pInitStr != NULL )
+ {
+ if ( (int)strlen(pInitStr) != Abc_NtkLatchNum(pNtk) )
+ {
+ Abc_Print( -1, "The length of init string (%d) differs from the number of flops (%d).\n", strlen(pInitStr), Abc_NtkLatchNum(pNtk) );
+ return 1;
+ }
+ Abc_NtkForEachLatch( pNtk, pObj, i )
+ if ( pInitStr[i] == '0' )
+ Abc_LatchSetInit0( pObj );
+ else if ( pInitStr[i] == '1' )
+ Abc_LatchSetInit1( pObj );
+ else
+ Abc_LatchSetInitDc( pObj );
+ return 0;
+ }
+
if ( fZeros )
{
Abc_NtkForEachLatch( pNtk, pObj, i )
@@ -15319,13 +15347,14 @@ int Abc_CommandInit( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- Abc_Print( -2, "usage: init [-zordh]\n" );
- Abc_Print( -2, "\t resets initial states of all latches\n" );
- Abc_Print( -2, "\t-z : set zeros initial states [default = %s]\n", fZeros? "yes": "no" );
- Abc_Print( -2, "\t-o : set ones initial states [default = %s]\n", fOnes? "yes": "no" );
- Abc_Print( -2, "\t-d : set don't-care initial states [default = %s]\n", fDontCare? "yes": "no" );
- Abc_Print( -2, "\t-r : set random initial states [default = %s]\n", fRandom? "yes": "no" );
- Abc_Print( -2, "\t-h : print the command usage\n");
+ Abc_Print( -2, "usage: init [-zordh] [-S <init_string>]\n" );
+ Abc_Print( -2, "\t resets initial states of all latches\n" );
+ Abc_Print( -2, "\t-z : set zeros initial states [default = %s]\n", fZeros? "yes": "no" );
+ Abc_Print( -2, "\t-o : set ones initial states [default = %s]\n", fOnes? "yes": "no" );
+ Abc_Print( -2, "\t-d : set don't-care initial states [default = %s]\n", fDontCare? "yes": "no" );
+ Abc_Print( -2, "\t-r : set random initial states [default = %s]\n", fRandom? "yes": "no" );
+ Abc_Print( -2, "\t-h : print the command usage\n");
+ Abc_Print( -2, "\t-S str : (optional) initial state [default = unused]\n" );
return 1;
}
@@ -26104,15 +26133,27 @@ int Abc_CommandAbc9Miter( Abc_Frame_t * pAbc, int argc, char ** argv )
char ** pArgvNew;
int nArgcNew;
int c;
+ int nInsDup = 0;
int fDualOut = 0;
int fSeq = 0;
int fTrans = 0;
int fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "dstvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Idstvh" ) ) != EOF )
{
switch ( c )
{
+ case 'I':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nInsDup = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nInsDup < 0 )
+ goto usage;
+ break;
case 'd':
fDualOut ^= 1;
break;
@@ -26179,14 +26220,15 @@ int Abc_CommandAbc9Miter( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
}
// compute the miter
- pAux = Gia_ManMiter( pAbc->pGia, pSecond, fDualOut, fSeq, fVerbose );
+ pAux = Gia_ManMiter( pAbc->pGia, pSecond, nInsDup, fDualOut, fSeq, fVerbose );
Gia_ManStop( pSecond );
Abc_FrameUpdateGia( pAbc, pAux );
return 0;
usage:
- Abc_Print( -2, "usage: &miter [-dstvh] <file>\n" );
+ Abc_Print( -2, "usage: &miter [-I num] [-dstvh] <file>\n" );
Abc_Print( -2, "\t creates miter of two designs (current AIG vs. <file>)\n" );
+ Abc_Print( -2, "\t-I num : the number of last PIs to replicate [default = %d]\n", nInsDup );
Abc_Print( -2, "\t-d : toggle creating dual-output miter [default = %s]\n", fDualOut? "yes": "no" );
Abc_Print( -2, "\t-s : toggle creating sequential miter [default = %s]\n", fSeq? "yes": "no" );
Abc_Print( -2, "\t-t : toggle XORing pair-wise POs of the miter [default = %s]\n", fTrans? "yes": "no" );
@@ -27431,7 +27473,7 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
}
// compute the miter
- pMiter = Gia_ManMiter( pAbc->pGia, pSecond, 1, 0, pPars->fVerbose );
+ pMiter = Gia_ManMiter( pAbc->pGia, pSecond, 0, 1, 0, pPars->fVerbose );
if ( pMiter )
{
pAbc->Status = Cec_ManVerify( pMiter, pPars );
diff --git a/src/proof/cec/cecCec.c b/src/proof/cec/cecCec.c
index 72c3e7db..37df4d8d 100644
--- a/src/proof/cec/cecCec.c
+++ b/src/proof/cec/cecCec.c
@@ -301,7 +301,7 @@ int Cec_ManVerifyTwo( Gia_Man_t * p0, Gia_Man_t * p1, int fVerbose )
int RetValue;
Cec_ManCecSetDefaultParams( pPars );
pPars->fVerbose = fVerbose;
- pMiter = Gia_ManMiter( p0, p1, 1, 0, pPars->fVerbose );
+ pMiter = Gia_ManMiter( p0, p1, 0, 1, 0, pPars->fVerbose );
if ( pMiter == NULL )
return -1;
RetValue = Cec_ManVerify( pMiter, pPars );
generated by cgit v1.2.3 (git 2.25.1) at 2025-10-31 13:10:33 +0000