From 6c51a9238544bce6eb300b7b1c3e5bb4215bec84 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 8 Aug 2026 17:29:15 -0700 Subject: [PATCH] Adding an option t0 &cec against a truth table. --- src/aig/gia/giaDecGraph.cpp | 102 ++++++++++++++++++++++++++++++++++++ src/base/abci/abc.c | 30 ++++++++++- 2 files changed, 131 insertions(+), 1 deletion(-) diff --git a/src/aig/gia/giaDecGraph.cpp b/src/aig/gia/giaDecGraph.cpp index f467d4cdc..5b23e4f74 100644 --- a/src/aig/gia/giaDecGraph.cpp +++ b/src/aig/gia/giaDecGraph.cpp @@ -2211,4 +2211,106 @@ Gia_Man_t* Gia_ManDecGraphFromFile(char* pFileName) { return pNew; } +extern "C" int Gia_ManVerifyTruthFile(Gia_Man_t* p, char* pFileName, int fVerbose) { + const int nIns = Gia_ManCiNum(p); + const int nOuts = Gia_ManCoNum(p); + char* pBuffer; + char* table; + uint64_t nBits; + int iOut = 0; + int result = -1; + + if (Gia_ManRegNum(p) != 0) { + Abc_Print(-1, "Truth-table verification requires a combinational network.\n"); + return -1; + } + if (nIns >= 63) { + Abc_Print(-1, "A .truth file cannot represent a network with %d inputs.\n", nIns); + return -1; + } + nBits = (uint64_t)1 << nIns; + pBuffer = Extra_FileReadContents(pFileName); + if (pBuffer == NULL) { + Abc_Print(-1, "Cannot read truth-table file \"%s\".\n", pFileName); + return -1; + } + + Abc_CexFreeP(&p->pCexComb); + Gia_ObjComputeTruthTableStart(p, nIns); + table = strtok(pBuffer, " \r\n\t|"); + while (table != NULL) { + const uint64_t tableSize = strlen(table); + DecGraph::TruthTable fileTruth; + DecGraph::TruthTable giaTruth; + Gia_Obj_t* pObj; + word* pTruth; + uint64_t i; + + if (iOut == nOuts) { + Abc_Print(-1, "Truth-table file \"%s\" has more than %d outputs.\n", pFileName, nOuts); + goto finish; + } + if (tableSize != nBits) { + Abc_Print(-1, "Output %d in truth-table file \"%s\" has %llu bits; expected %llu for %d inputs.\n", + iOut, pFileName, (unsigned long long)tableSize, (unsigned long long)nBits, nIns); + goto finish; + } + for (i = 0; i < tableSize; ++i) { + if (table[i] != '0' && table[i] != '1') { + Abc_Print(-1, "Unexpected character '%c' in output %d of truth-table file \"%s\".\n", + table[i], iOut, pFileName); + goto finish; + } + } + + fileTruth.readBinaryReverse(table); + giaTruth.create(nBits); + pObj = Gia_ManCo(p, iOut); + pTruth = Gia_ObjComputeTruthTable(p, Gia_ObjFanin0(pObj)); + if (nIns >= 6) { + for (i = 0; i < giaTruth.nWords(); ++i) + giaTruth.data()[i] = Gia_ObjFaninC0(pObj) ? ~DecGraph::reverseBits(pTruth[i]) : DecGraph::reverseBits(pTruth[i]); + } else { + word value = (Gia_ObjFaninC0(pObj) ? ~pTruth[0] : pTruth[0]) & DecGraph::ones_mask[nIns]; + giaTruth.data()[0] = DecGraph::reverseBits(value); + } + + if (fileTruth != giaTruth) { + uint64_t iMint = 0; + p->pCexComb = Abc_CexAlloc(0, nIns, 1); + p->pCexComb->iPo = iOut; + for (i = 0; i < fileTruth.nWords(); ++i) { + word diff = fileTruth.data()[i] ^ giaTruth.data()[i]; + if (diff == 0) + continue; + for (int b = 0; b < 64; ++b) + if (diff & ((word)1 << (63 - b))) { + iMint = 64 * i + b; + break; + } + break; + } + for (int v = 0; v < nIns; ++v) + if ((iMint >> v) & 1) + Abc_InfoSetBit(p->pCexComb->pData, v); + if (fVerbose) + Abc_Print(1, "Truth tables differ for output %d at minterm %llu.\n", iOut, (unsigned long long)iMint); + result = 0; + goto finish; + } + ++iOut; + table = strtok(NULL, " \r\n\t|"); + } + if (iOut != nOuts) { + Abc_Print(-1, "Truth-table file \"%s\" has %d outputs; expected %d.\n", pFileName, iOut, nOuts); + goto finish; + } + result = 1; + +finish: + Gia_ObjComputeTruthTableStop(p); + ABC_FREE(pBuffer); + return result; +} + ABC_NAMESPACE_IMPL_END diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 6d5f66097..86a9fd2ca 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -702,6 +702,11 @@ extern int Cec_GiaReplayTest( Gia_Man_t * p, Wlc_Ntk_t * pWlc, char * pFileName, /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +#ifdef __cplusplus +extern "C" +#endif +int Gia_ManVerifyTruthFile( Gia_Man_t * p, char * pFileName, int fVerbose ); + /**Function************************************************************* Synopsis [] @@ -44166,6 +44171,29 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv ) } FileName = pAbc->pGia->pSpec; } + if ( fUseSim && nArgcNew == 1 && !strcmp( Extra_FileNameExtension(FileName), "truth" ) ) + { + abctime clk = Abc_Clock(); + int Status = Gia_ManVerifyTruthFile( pGias[0], FileName, pPars->fVerbose ); + if ( Status == 1 ) + Abc_Print( 1, "Network and truth table are equivalent. " ); + else if ( Status == 0 ) + Abc_Print( 1, "Network and truth table are NOT equivalent. " ); + else + { + Vec_PtrFree( vDefines ); + Vec_PtrFree( vBoxes ); + Vec_PtrFree( vInsts ); + return 1; + } + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + pAbc->Status = Status; + Abc_FrameReplaceCex( pAbc, &pGias[0]->pCexComb ); + Vec_PtrFree( vDefines ); + Vec_PtrFree( vBoxes ); + Vec_PtrFree( vInsts ); + return 0; + } pGias[1] = Abc_ReadAigerOrVerilogFile( FileName, pFileName2, pTopModule, vDefines, vBoxes, vInsts, &Abc_ReadAigerOrVerilogFileStatus ); if ( pGias[1] == NULL ) { @@ -44327,7 +44355,7 @@ usage: Abc_Print( -2, "\t-s : toggle silent operation [default = %s]\n", pPars->fSilent ? "yes":"no"); Abc_Print( -2, "\t-x : toggle using new solver [default = %s]\n", fUseNewX? "yes":"no"); Abc_Print( -2, "\t-y : toggle using new solver [default = %s]\n", fUseNewY? "yes":"no"); - Abc_Print( -2, "\t-t : toggle using simulation [default = %s]\n", fUseSim? "yes":"no"); + Abc_Print( -2, "\t-t : toggle using simulation; accepts one .truth file for the current network [default = %s]\n", fUseSim? "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");