Skip to content

Commit c4b2b5c

Browse files
alanminkoalanminko
committed
Adding extension "y" for obj ID mapping.
1 parent 9b0786f commit c4b2b5c

File tree

7 files changed

+174
-12
lines changed

7 files changed

+174
-12
lines changed

‎src/aig/gia/gia.h‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -189,6 +189,7 @@ struct Gia_Man_t_
189189
Vec_Int_t * vCoNumsOrig; // original CO names
190190
Vec_Int_t * vIdsOrig; // original object IDs
191191
Vec_Int_t * vIdsEquiv; // original object IDs proved equivalent
192+
Vec_Int_t * vEquLitIds; // original object IDs proved equivalent
192193
Vec_Int_t * vCofVars; // cofactoring variables
193194
Vec_Vec_t * vClockDoms; // clock domains
194195
Vec_Flt_t * vTiming; // arrival/required/slack
@@ -1729,7 +1730,7 @@ extern void * Gia_ManUpdateTimMan2( Gia_Man_t * p, Vec_Int_t * vBox
17291730
extern Gia_Man_t * Gia_ManUpdateExtraAig( void * pTime, Gia_Man_t * pAig, Vec_Int_t * vBoxPres );
17301731
extern Gia_Man_t * Gia_ManUpdateExtraAig2( void * pTime, Gia_Man_t * pAig, Vec_Int_t * vBoxesLeft );
17311732
extern Gia_Man_t * Gia_ManDupCollapse( Gia_Man_t * p, Gia_Man_t * pBoxes, Vec_Int_t * vBoxPres, int fSeq );
1732-
extern int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, int nBTLimit, int nTimeLim, int fSeq, int fDumpFiles, int fVerbose, char * pFileSpec );
1733+
extern int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, int nBTLimit, int nTimeLim, int fSeq, int fNameMap, int fDumpFiles, int fVerbose, char * pFileSpec );
17331734
extern Vec_Int_t * Gia_ManDeriveBoxMapping( Gia_Man_t * pGia );
17341735
/*=== giaTruth.c ===========================================================*/
17351736
extern word Gia_LutComputeTruth6( Gia_Man_t * p, int iObj, Vec_Wrd_t * vTruths );

‎src/aig/gia/giaAiger.c‎

Lines changed: 29 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -907,6 +907,25 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fGiaSi
907907
printf( "Cannot read extension \"w\" because AIG is rehashed. Use \"&r -s <file.aig>\".\n" );
908908
Vec_IntFree( vPairs );
909909
}
910+
// read object ID mapping
911+
else if ( *pCur == 'y' )
912+
{
913+
pCur++;
914+
int nInts = Gia_AigerReadInt(pCur)/4; pCur += 4;
915+
if ( fSkipStrash ) {
916+
pNew->vEquLitIds = Vec_IntStart( nInts );
917+
memcpy( Vec_IntArray(pNew->vEquLitIds), pCur, (size_t)4*nInts );
918+
if ( Vec_IntSize(pNew->vEquLitIds) != Gia_ManObjNum(pNew) ) {
919+
printf( "Cannot read extension \"y\" because object count changed. Use \"&r -s <file.aig>\".\n" );
920+
Vec_IntFreeP( &pNew->vEquLitIds );
921+
}
922+
else if ( fVerbose ) printf( "Finished reading extension \"y\".\n" );
923+
}
924+
else {
925+
if ( fVerbose ) printf( "Cannot read extension \"y\" because AIG is rehashed. Use \"&r -s <file.aig>\".\n" );
926+
}
927+
pCur += 4*nInts;
928+
}
910929
else break;
911930
}
912931
}
@@ -1529,6 +1548,7 @@ void Gia_AigerWriteS( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, in
15291548
Gia_FileWriteBufferSize( pFile, Vec_IntSize(p->vRegClasses) );
15301549
for ( i = 0; i < Vec_IntSize(p->vRegClasses); i++ )
15311550
Gia_FileWriteBufferSize( pFile, Vec_IntEntry(p->vRegClasses, i) );
1551+
if ( fVerbose ) printf( "Finished writing extension \"r\".\n" );
15321552
}
15331553
// write register inits
15341554
if ( p->vRegInits )
@@ -1677,6 +1697,15 @@ void Gia_AigerWriteS( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, in
16771697
assert( Vec_IntSize(p->vObjClasses) == Gia_ManObjNum(p) );
16781698
fwrite( Vec_IntArray(p->vObjClasses), 1, 4*Gia_ManObjNum(p), pFile );
16791699
}
1700+
// write object classes
1701+
if ( p->vEquLitIds )
1702+
{
1703+
fprintf( pFile, "y" );
1704+
Gia_FileWriteBufferSize( pFile, 4*Gia_ManObjNum(p) );
1705+
assert( Vec_IntSize(p->vEquLitIds) == Gia_ManObjNum(p) );
1706+
fwrite( Vec_IntArray(p->vEquLitIds), 1, 4*Gia_ManObjNum(p), pFile );
1707+
if ( fVerbose ) printf( "Finished writing extension \"y\".\n" );
1708+
}
16801709
// write name
16811710
if ( p->pName )
16821711
{
@@ -1916,4 +1945,3 @@ int main( int argc, char ** argv )
19161945

19171946

19181947
ABC_NAMESPACE_IMPL_END
1919-

‎src/aig/gia/giaMan.c‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -106,6 +106,7 @@ void Gia_ManStop( Gia_Man_t * p )
106106
Vec_IntFreeP( &p->vCofVars );
107107
Vec_IntFreeP( &p->vIdsOrig );
108108
Vec_IntFreeP( &p->vIdsEquiv );
109+
Vec_IntFreeP( &p->vEquLitIds );
109110
Vec_IntFreeP( &p->vLutConfigs );
110111
Vec_IntFreeP( &p->vEdgeDelay );
111112
Vec_IntFreeP( &p->vEdgeDelayR );
@@ -641,7 +642,7 @@ void Gia_ManPrintStats( Gia_Man_t * p, Gps_Par_t * pPars )
641642
}
642643
if ( pPars && pPars->fSlacks )
643644
Gia_ManDfsSlacksPrint( p );
644-
if ( Gia_ManHasMapping(p) && pPars->fMapOutStats )
645+
if ( Gia_ManHasMapping(p) && pPars && pPars->fMapOutStats )
645646
Gia_ManPrintOutputLutStats( p );
646647
}
647648

‎src/aig/gia/giaTim.c‎

Lines changed: 129 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -952,7 +952,114 @@ Gia_Man_t * Gia_ManDupCollapse( Gia_Man_t * p, Gia_Man_t * pBoxes, Vec_Int_t * v
952952
SeeAlso []
953953
954954
***********************************************************************/
955-
int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, int nBTLimit, int nTimeLim, int fSeq, int fDumpFiles, int fVerbose, char * pFileSpec )
955+
956+
/*
957+
› Please have a look at how name mapping is done in procedure Abc_FrameReadMiniLutNameMapping() in file "src/aig/gia/
958+
giaMini.c". The main idea is to map the object IDs in the design after synthesis (pAbc->pGiaMiniLut) into the object IDs in
959+
the design before synthesis (pAbc->pGiaMiniAig). The computation is divided into three steps: (1) computing object
960+
equivalences using Gia_ManComputeGiaEquivs(), which annotates the input AIG (pGia) containing both designs before and after
961+
synthesis with equivalence class information; this information contains equivalence classes of objects from both designs; (2)
962+
creating a map (pRes) of the resulting object IDs (in pAbc->pGiaMiniLut) into the original object IDs (in pAbc->pGiaMiniAig)
963+
using procedure Gia_ManMapMiniLut2MiniAig(); this map is enabled by having two arrays (one of them is pAbc->vCopyMiniAig
964+
mapping objects of pAbc->pGiaMiniAig in the original object IDs; the other one is pAbc->vCopyMiniLut mapping objects of
965+
pAbc->pGiaMiniLut into the IDs of pAbc->pGiaMiniLut); (3) verification procedure (commented out by default)
966+
Gia_ManNameMapVerify() which checks that the resulting mapping computed by Gia_ManMapMiniLut2MiniAig() is correct. Please
967+
let me know if this computation is clear.
968+
*/
969+
970+
Vec_Int_t * Gia_ManVerifyFindNameMapping( Gia_Man_t * p, Gia_Man_t * p1, Gia_Man_t * p2, Vec_Int_t * vMap1, Vec_Int_t * vMap2 )
971+
{
972+
Vec_Int_t * vRes = Vec_IntStartFull(Vec_IntSize(vMap2));
973+
Vec_Int_t * vMap = Vec_IntStartFull( Gia_ManObjNum(p) );
974+
int i, Entry, iRepr, fCompl, iLit;
975+
Gia_Obj_t * pObj;
976+
Gia_ManSetPhase( p1 );
977+
Gia_ManSetPhase( p2 );
978+
Vec_IntForEachEntry( vMap1, Entry, i )
979+
{
980+
if ( Entry == -1 )
981+
continue;
982+
pObj = Gia_ManObj( p1, Abc_Lit2Var(Entry) );
983+
if ( ~pObj->Value == 0 )
984+
continue;
985+
fCompl = Abc_LitIsCompl(Entry) ^ pObj->fPhase;
986+
iRepr = Gia_ObjReprSelf( p, Abc_Lit2Var(pObj->Value) );
987+
Vec_IntWriteEntry( vMap, iRepr, Abc_Var2Lit( i, fCompl ) );
988+
}
989+
Vec_IntForEachEntry( vMap2, Entry, i )
990+
{
991+
if ( Entry == -1 )
992+
continue;
993+
pObj = Gia_ManObj( p2, Abc_Lit2Var(Entry) );
994+
if ( ~pObj->Value == 0 )
995+
continue;
996+
fCompl = Abc_LitIsCompl(Entry) ^ pObj->fPhase;
997+
iRepr = Gia_ObjReprSelf( p, Abc_Lit2Var(pObj->Value) );
998+
if ( (iLit = Vec_IntEntry(vMap, iRepr)) == -1 )
999+
continue;
1000+
Vec_IntWriteEntry( vRes, i, Abc_LitNotCond( iLit, fCompl ) );
1001+
}
1002+
Vec_IntFill( vMap, Gia_ManCoNum(p1), -1 );
1003+
Vec_IntForEachEntry( vMap1, Entry, i )
1004+
{
1005+
if ( Entry == -1 )
1006+
continue;
1007+
pObj = Gia_ManObj( p1, Abc_Lit2Var(Entry) );
1008+
if ( !Gia_ObjIsCo(pObj) )
1009+
continue;
1010+
Vec_IntWriteEntry( vMap, Gia_ObjCioId(pObj), i );
1011+
}
1012+
Vec_IntForEachEntry( vMap2, Entry, i )
1013+
{
1014+
if ( Entry == -1 )
1015+
continue;
1016+
pObj = Gia_ManObj( p2, Abc_Lit2Var(Entry) );
1017+
if ( !Gia_ObjIsCo(pObj) )
1018+
continue;
1019+
1020+
assert( Vec_IntEntry(vRes, i) == -1 );
1021+
Vec_IntWriteEntry( vRes, i, Abc_Var2Lit( Vec_IntEntry(vMap, Gia_ObjCioId(pObj)), 0 ) );
1022+
assert( Vec_IntEntry(vRes, i) != -1 );
1023+
}
1024+
Vec_IntFree( vMap );
1025+
return vRes;
1026+
}
1027+
1028+
void Gia_ManVerifyVerifyNameMapping( Gia_Man_t * p, Gia_Man_t * p1, Gia_Man_t * p2, Vec_Int_t * vMap1, Vec_Int_t * vMap2, Vec_Int_t * vMapRes )
1029+
{
1030+
int iImpl, iReprSpec, iReprImpl, nSize = Vec_IntSize(vMap2);
1031+
Gia_Obj_t * pObjSpec, * pObjImpl;
1032+
if ( vMapRes == NULL || p == NULL || p->pReprs == NULL )
1033+
return;
1034+
assert( Vec_IntSize(vMapRes) == nSize );
1035+
Gia_ManSetPhase( p1 );
1036+
Gia_ManSetPhase( p2 );
1037+
for ( iImpl = 0; iImpl < nSize; iImpl++ )
1038+
if ( Vec_IntEntry(vMapRes, iImpl) >= 0 )
1039+
{
1040+
int Entry = Vec_IntEntry( vMapRes, iImpl );
1041+
int iSpec = Abc_Lit2Var( Entry );
1042+
int fCompl = Abc_LitIsCompl( Entry );
1043+
int iLitSpec = Vec_IntEntry( vMap1, iSpec );
1044+
int iLitImpl = Vec_IntEntry( vMap2, iImpl );
1045+
pObjSpec = Gia_ManObj( p1, Abc_Lit2Var(iLitSpec) );
1046+
if ( Gia_ObjIsCo(pObjSpec) )
1047+
continue;
1048+
if ( ~pObjSpec->Value == 0 )
1049+
continue;
1050+
pObjImpl = Gia_ManObj( p2, Abc_Lit2Var(iLitImpl) );
1051+
if ( ~pObjImpl->Value == 0 )
1052+
continue;
1053+
iReprSpec = Gia_ObjReprSelf( p, Abc_Lit2Var(pObjSpec->Value) );
1054+
iReprImpl = Gia_ObjReprSelf( p, Abc_Lit2Var(pObjImpl->Value) );
1055+
if ( iReprSpec != iReprImpl )
1056+
printf( "Found functional mismatch for ImplId %d and SpecId %d.\n", iImpl, iSpec );
1057+
if ( (pObjImpl->fPhase ^ Abc_LitIsCompl(iLitImpl)) != (pObjSpec->fPhase ^ Abc_LitIsCompl(iLitSpec) ^ fCompl) )
1058+
printf( "Found phase mismatch for ImplId %d and SpecId %d.\n", iImpl, iSpec );
1059+
}
1060+
}
1061+
1062+
int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, int nBTLimit, int nTimeLim, int fSeq, int fObjIdMap, int fDumpFiles, int fVerbose, char * pFileSpec )
9561063
{
9571064
int Status = -1;
9581065
Gia_Man_t * pSpec, * pGia0, * pGia1, * pMiter;
@@ -1052,12 +1159,30 @@ int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, int nBTLimit, int nTimeLim, int fS
10521159
{
10531160
Cec_ParCec_t ParsCec, * pPars = &ParsCec;
10541161
Cec_ManCecSetDefaultParams( pPars );
1055-
pPars->nBTLimit = nBTLimit;
1056-
pPars->TimeLimit = nTimeLim;
1057-
pPars->fVerbose = fVerbose;
1162+
pPars->nBTLimit = nBTLimit;
1163+
pPars->TimeLimit = nTimeLim;
1164+
pPars->fUseOrigIds = fObjIdMap;
1165+
pPars->fVerbose = fVerbose;
10581166
Status = Cec_ManVerify( pMiter, pPars );
10591167
if ( pPars->iOutFail >= 0 )
10601168
Abc_Print( 1, "Verification failed for at least one output (%d).\n", pPars->iOutFail );
1169+
if ( fObjIdMap ) {
1170+
Gia_Man_t * pReduced = Gia_ManOrigIdsReduce( pMiter, pMiter->vIdsEquiv );
1171+
Gia_ManStop( pReduced );
1172+
Gia_Obj_t * pObj; int i;
1173+
Vec_Int_t * vCopy0 = Vec_IntAlloc(Gia_ManObjNum(pSpec));
1174+
Gia_ManForEachObj( pSpec, pObj, i )
1175+
Vec_IntPush( vCopy0, pObj->Value );
1176+
Vec_Int_t * vCopy1 = Vec_IntAlloc(Gia_ManObjNum(pGia));
1177+
Gia_ManForEachObj( pGia, pObj, i )
1178+
Vec_IntPush( vCopy1, pObj->Value );
1179+
Vec_IntFreeP( &pGia->vEquLitIds );
1180+
pGia->vEquLitIds = Gia_ManVerifyFindNameMapping( pMiter, pGia0, pGia1, vCopy0, vCopy1 );
1181+
assert( Vec_IntSize(pGia->vEquLitIds) == Gia_ManObjNum(pGia) );
1182+
Gia_ManVerifyVerifyNameMapping( pMiter, pGia0, pGia1, vCopy0, vCopy1, pGia->vEquLitIds );
1183+
Vec_IntFree( vCopy0 );
1184+
Vec_IntFree( vCopy1 );
1185+
}
10611186
Gia_ManStop( pMiter );
10621187
}
10631188
}
@@ -1094,4 +1219,3 @@ Vec_Int_t * Gia_ManDeriveBoxMapping( Gia_Man_t * pGia )
10941219

10951220

10961221
ABC_NAMESPACE_IMPL_END
1097-

‎src/base/abci/abc.c‎

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -42227,9 +42227,9 @@ int Abc_CommandAbc9ICec( Abc_Frame_t * pAbc, int argc, char ** argv )
4222742227
int Abc_CommandAbc9Verify( Abc_Frame_t * pAbc, int argc, char ** argv )
4222842228
{
4222942229
char * pFileSpec = NULL;
42230-
int c, nBTLimit = 1000, nTimeLim = 0, fSeq = 0, fDumpFiles = 0, fVerbose = 0;
42230+
int c, nBTLimit = 1000, nTimeLim = 0, fSeq = 0, fObjIdMap = 0, fDumpFiles = 0, fVerbose = 0;
4223142231
Extra_UtilGetoptReset();
42232-
while ( ( c = Extra_UtilGetopt( argc, argv, "CTsdvh" ) ) != EOF )
42232+
while ( ( c = Extra_UtilGetopt( argc, argv, "CTsmdvh" ) ) != EOF )
4223342233
{
4223442234
switch ( c )
4223542235
{
@@ -42258,6 +42258,9 @@ int Abc_CommandAbc9Verify( Abc_Frame_t * pAbc, int argc, char ** argv )
4225842258
case 's':
4225942259
fSeq ^= 1;
4226042260
break;
42261+
case 'm':
42262+
fObjIdMap ^= 1;
42263+
break;
4226142264
case 'd':
4226242265
fDumpFiles ^= 1;
4226342266
break;
@@ -42276,15 +42279,16 @@ int Abc_CommandAbc9Verify( Abc_Frame_t * pAbc, int argc, char ** argv )
4227642279
Extra_FileNameCorrectPath( pFileSpec );
4227742280
printf( "Taking spec from file \"%s\".\n", pFileSpec );
4227842281
}
42279-
Gia_ManVerifyWithBoxes( pAbc->pGia, nBTLimit, nTimeLim, fSeq, fDumpFiles, fVerbose, pFileSpec );
42282+
Gia_ManVerifyWithBoxes( pAbc->pGia, nBTLimit, nTimeLim, fSeq, fObjIdMap, fDumpFiles, fVerbose, pFileSpec );
4228042283
return 0;
4228142284

4228242285
usage:
42283-
Abc_Print( -2, "usage: &verify [-CT num] [-sdvh] <file>\n" );
42286+
Abc_Print( -2, "usage: &verify [-CT num] [-smdvh] <file>\n" );
4228442287
Abc_Print( -2, "\t performs verification of combinational design\n" );
4228542288
Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", nBTLimit );
4228642289
Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", nTimeLim );
4228742290
Abc_Print( -2, "\t-s : toggle using sequential verification [default = %s]\n", fSeq? "yes":"no");
42291+
Abc_Print( -2, "\t-m : toggle producing object ID mapping (CEC only) [default = %s]\n", fObjIdMap? "yes":"no");
4228842292
Abc_Print( -2, "\t-d : toggle dumping AIGs to be compared [default = %s]\n", fDumpFiles? "yes":"no");
4228942293
Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes":"no");
4229042294
Abc_Print( -2, "\t-h : print the command usage\n");

‎src/proof/cec/cec.h‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -135,6 +135,7 @@ struct Cec_ParCec_t_
135135
int fUseSmartCnf; // use smart CNF computation
136136
int fRewriting; // enables AIG rewriting
137137
int fNaive; // performs naive SAT-based checking
138+
int fUseOrigIds; // enable recording of original IDs
138139
int fSilent; // print no messages
139140
int fVeryVerbose; // verbose stats
140141
int fVerbose; // verbose stats

‎src/proof/cec/cecCec.c‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -359,11 +359,13 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars )
359359
pParsFra->nItersMax = 1000;
360360
pParsFra->nBTLimit = pPars->nBTLimit;
361361
pParsFra->TimeLimit = pPars->TimeLimit;
362+
pParsFra->fUseOrigIds = pPars->fUseOrigIds;
362363
pParsFra->fVerbose = pPars->fVerbose;
363364
pParsFra->fVeryVerbose = pPars->fVeryVerbose;
364365
pParsFra->fCheckMiter = 1;
365366
pParsFra->fDualOut = 1;
366367
pNew = Cec_ManSatSweeping( p, pParsFra, pPars->fSilent );
368+
ABC_SWAP( Vec_Int_t *, pInit->vIdsEquiv, p->vIdsEquiv );
367369
pPars->iOutFail = pParsFra->iOutFail;
368370
// update
369371
pInit->pCexComb = p->pCexComb; p->pCexComb = NULL;
@@ -383,6 +385,7 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars )
383385
}
384386
return 0;
385387
}
388+
Vec_IntFreeP( &pInit->vIdsEquiv );
386389
p = Gia_ManDup( pInit );
387390
Gia_ManEquivFixOutputPairs( p );
388391
p = Gia_ManCleanup( pNew = p );

0 commit comments

Comments
 (0)