diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 4016ff3d8..1ab933ad8 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -278,6 +278,7 @@ static int Abc_CommandSimSec ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandMatch ( Abc_Frame_t * pAbc, int argc, char ** argv ); //static int Abc_CommandHaig ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandQbf ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAigSim ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandFraig ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandFraigTrust ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -1107,6 +1108,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "New AIG", "csweep", Abc_CommandCSweep, 1 ); // Cmd_CommandAdd( pAbc, "New AIG", "haig", Abc_CommandHaig, 1 ); Cmd_CommandAdd( pAbc, "New AIG", "qbf", Abc_CommandQbf, 0 ); + Cmd_CommandAdd( pAbc, "New AIG", "aigsim", Abc_CommandAigSim, 0 ); Cmd_CommandAdd( pAbc, "Fraiging", "fraig", Abc_CommandFraig, 1 ); Cmd_CommandAdd( pAbc, "Fraiging", "fraig_trust", Abc_CommandFraigTrust, 1 ); @@ -19269,6 +19271,68 @@ usage: return 1; } + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAigSim( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern int SimulateAigTop( char *fname1, char *fname2, char * mask, int verbose ); + char * pMask = NULL; + char ** pArgvNew = NULL; + int nArgcNew = 0; + int c, fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Mvh" ) ) != EOF ) + { + switch ( c ) + { + case 'M': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-M\" should be followed by a string.\n" ); + goto usage; + } + pMask = argv[globalUtilOptind]; + globalUtilOptind++; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + pArgvNew = argv + globalUtilOptind; + nArgcNew = argc - globalUtilOptind; + if ( nArgcNew != 2 ) { + Abc_Print( -1, "Expecting two files names on the command line.\n" ); + return 1; + } + SimulateAigTop( pArgvNew[0], pArgvNew[1], pMask, fVerbose ); + return 0; + +usage: + Abc_Print( -2, "usage: aigsim -M [-vh] \n" ); + Abc_Print( -2, "\t combinational AIG simulation\n" ); + Abc_Print( -2, "\t-M : mask to select inputs for simulation [default = unused]\n" ); + Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + Abc_Print( -2, "\t : the first file to simulate\n"); + Abc_Print( -2, "\t : the second file to simulate\n"); + return 1; +} + /**Function************************************************************* Synopsis [] diff --git a/src/misc/util/module.make b/src/misc/util/module.make index e77877881..701c1c251 100644 --- a/src/misc/util/module.make +++ b/src/misc/util/module.make @@ -1,4 +1,5 @@ -SRC += src/misc/util/utilBridge.c \ +SRC += src/misc/util/utilAigSim.c \ + src/misc/util/utilBridge.c \ src/misc/util/utilBipart.c \ src/misc/util/utilBSet.c \ src/misc/util/utilCex.c \ diff --git a/src/misc/util/utilAigSim.c b/src/misc/util/utilAigSim.c new file mode 100644 index 000000000..36deb1f0a --- /dev/null +++ b/src/misc/util/utilAigSim.c @@ -0,0 +1,657 @@ +/**CFile**************************************************************** + + FileName [utilAigSim.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [AIG simulation.] + + Synopsis [AIG simulation.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - Feburary 13, 2011.] + + Revision [$Id: utilAigSim.c,v 1.00 2011/02/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include +#include +#include +#include +#include +#include +#include +#include // mkstemp(), close(), unlink() + +#define AIGSIM_LIBRARY_ONLY + +#ifdef AIGSIM_LIBRARY_ONLY +#include "misc/util/abc_namespaces.h" +#endif + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +#define ABC_ALLOC(type, n) ((type*)malloc((size_t)(n) * sizeof(type))) +#define ABC_CALLOC(type, n) ((type*)calloc((size_t)(n), sizeof(type))) +#define ABC_FREE(p) do { free(p); (p) = NULL; } while (0) + +typedef struct AigNode_ { uint32_t f0, f1; } AigNode; +typedef struct AigMan_ { + AigNode *nodes; + int nObjs, nCis, nAnds, nCos; +} AigMan; + +static inline int Aig_LitId(uint32_t lit) { return (int)(lit >> 1); } +static inline int Aig_LitCompl(uint32_t lit) { return (int)(lit & 1u); } +static inline uint32_t Aig_Lit(int id, int c) { return ((uint32_t)id << 1) | (uint32_t)(c & 1); } + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +static AigMan* Aig_ManStartCompact(int nCis, int nAnds, int nCos) { + AigMan *p = ABC_CALLOC(AigMan, 1); + p->nCis = nCis; p->nAnds = nAnds; p->nCos = nCos; + p->nObjs = 1 + nCis + nAnds + nCos; + p->nodes = ABC_CALLOC(AigNode, p->nObjs); + return p; +} +static void Aig_ManStop(AigMan *p) { ABC_FREE(p->nodes); ABC_FREE(p); } + +/* ---------------------- AIGER binary loader ----------------------- */ +/* Simple combinational (.aig) reader: header + O ASCII lines + A delta-encoded ANDs */ + +static int read_line(FILE *f, char *buf, size_t cap) { + if (!fgets(buf, (int)cap, f)) return 0; + size_t n = strlen(buf); + while (n && (buf[n-1] == '\n' || buf[n-1] == '\r')) buf[--n] = 0; + return 1; +} +static int parse_header(const char *s, unsigned *M, unsigned *I, unsigned *L, unsigned *O, unsigned *A) { + if (strncmp(s, "aig ", 4) != 0) return 0; + const char *p = s + 4; + *M = (unsigned)strtoul(p, (char**)&p, 10); + *I = (unsigned)strtoul(p, (char**)&p, 10); + *L = (unsigned)strtoul(p, (char**)&p, 10); + *O = (unsigned)strtoul(p, (char**)&p, 10); + *A = (unsigned)strtoul(p, (char**)&p, 10); + return 1; +} +static int read_ascii_uint_line(FILE *f, unsigned *out) { + char buf[128]; if (!read_line(f, buf, sizeof(buf))) return 0; + char *p = buf; while (*p && isspace((unsigned char)*p)) p++; + *out = (unsigned)strtoul(p, NULL, 10); + return 1; +} +static int read_uleb128(FILE *f, unsigned *out) { + unsigned x = 0, shift = 0; + for (;;) { + int ch = fgetc(f); if (ch == EOF) return 0; + x |= ((unsigned)(ch & 0x7F)) << shift; + if (!(ch & 0x80)) break; + shift += 7; if (shift > 28) return 0; + } + *out = x; return 1; +} +static AigMan* Aig_ManLoadAigerBinary(const char *filename, int verbose) { + FILE *f = fopen(filename, "rb"); + if (!f) { fprintf(stderr, "Error: cannot open '%s'\n", filename); return NULL; } + char hdr[256]; + if (!read_line(f, hdr, sizeof(hdr))) { fprintf(stderr, "Error: cannot read header\n"); fclose(f); return NULL; } + unsigned M=0,I=0,L=0,O=0,A=0; + if (!parse_header(hdr, &M,&I,&L,&O,&A)) { fprintf(stderr, "Error: bad header: %s\n", hdr); fclose(f); return NULL; } + if (verbose) printf("[aiger] %s : M=%u I=%u L=%u O=%u A=%u\n", filename, M,I,L,O,A); + if (L != 0) { fprintf(stderr, "Error: latches (L=%u) not supported.\n", L); fclose(f); return NULL; } + + unsigned *outs = ABC_ALLOC(unsigned, O); + for (unsigned i = 0; i < O; i++) if (!read_ascii_uint_line(f, &outs[i])) { + fprintf(stderr, "Error: cannot read output literal %u\n", i); ABC_FREE(outs); fclose(f); return NULL; + } + + AigMan *p = Aig_ManStartCompact((int)I, (int)A, (int)O); + + for (unsigned k = 0; k < A; k++) { + unsigned lhs_var = I + k + 1; + unsigned lhs_lit = lhs_var << 1; + unsigned d1=0, d2=0; + if (!read_uleb128(f, &d1) || !read_uleb128(f, &d2)) { + fprintf(stderr, "Error: cannot decode AND gate %u\n", k); + ABC_FREE(outs); Aig_ManStop(p); fclose(f); return NULL; + } + unsigned rhs0 = lhs_lit - d1; + unsigned rhs1 = rhs0 - d2; + p->nodes[(int)lhs_var].f0 = (uint32_t)rhs0; + p->nodes[(int)lhs_var].f1 = (uint32_t)rhs1; + } + + for (unsigned i = 0; i < O; i++) { + int id = p->nCis + p->nAnds + 1 + (int)i; // CO objects at the end + p->nodes[id].f0 = (uint32_t)outs[i]; + } + + ABC_FREE(outs); + fclose(f); + return p; +} + +/* ---------------------- sim helpers ---------------------- */ + +static inline uint64_t u64_mask_n(int nBits) { + return (nBits >= 64) ? ~0ull : ((nBits <= 0) ? 0ull : ((1ull << nBits) - 1ull)); +} +static void u128_to_dec(unsigned __int128 x, char *buf, size_t cap) { + char tmp[64]; int n = 0; + if (!x) { snprintf(buf, cap, "0"); return; } + while (x && n < (int)sizeof(tmp)) { tmp[n++] = (char)('0' + (unsigned)(x % 10)); x /= 10; } + int k = 0; while (n && k + 1 < (int)cap) buf[k++] = tmp[--n]; + buf[k] = 0; +} + +enum { NW = 64, BATCH = NW * 64 }; // 4096 patterns/round + +static inline uint64_t SimLit(const uint64_t *S, uint32_t lit, int w) { + uint64_t v = S[(size_t)Aig_LitId(lit) * NW + (size_t)w]; + return Aig_LitCompl(lit) ? ~v : v; +} + +static inline void SimulateOne(const AigMan *p, uint64_t *S) { + const int firstAnd = p->nCis + 1; + const int lastAnd = p->nCis + p->nAnds; + for (int id = firstAnd; id <= lastAnd; ++id) { + uint32_t f0 = p->nodes[id].f0, f1 = p->nodes[id].f1; + size_t off = (size_t)id * NW; + for (int w = 0; w < NW; ++w) + S[off + (size_t)w] = SimLit(S, f0, w) & SimLit(S, f1, w); + } +} + +/* ---------------------- mask string parser ---------------------- */ +/* maskStr grammar: sequence of tokens N or (N) + N : N individual bits (each enumerated independently) + (N) : N bits grouped together (enumerated as all-0 or all-1) + Total widths must sum to nCis. + Output: varMasks[0..nVars-1] (each is a bitmask of input bits controlled by that var). +*/ + +static void PrintMaskSegmentsOneLine(const char *maskStr, + const int *segS, const int *segW, const int *segG, int nSeg, + int nVars, int nCis) +{ + char buf[1024]; + int n = 0; + n += snprintf(buf + n, sizeof(buf) - (size_t)n, "[mask] \"%s\" segs:", maskStr ? maskStr : ""); + for (int i = 0; i < nSeg; ++i) { + int s = segS[i], e = s + segW[i] - 1; + if (segG[i]) n += snprintf(buf + n, sizeof(buf) - (size_t)n, " (%d-%d)", s, e); + else n += snprintf(buf + n, sizeof(buf) - (size_t)n, " %d-%d", s, e); + } + n += snprintf(buf + n, sizeof(buf) - (size_t)n, " vars=%d nCis=%d", nVars, nCis); + printf("%s\n", buf); +} + +static int ParseMaskString(const char *maskStr, int nCis, uint64_t *varMasks, int *pnVars, int verbose) { + if (!maskStr || !*maskStr) { + for (int i = 0; i < nCis; ++i) varMasks[i] = 1ull << i; + *pnVars = nCis; + if (verbose) PrintMaskSegmentsOneLine("default", + (int[]){0}, (int[]){nCis}, (int[]){0}, 1, *pnVars, nCis); + return 1; + } + + // For printing segments: each token becomes one segment + int segS[128], segW[128], segG[128], nSeg = 0; + + const char *p = maskStr; + int off = 0, nVars = 0; + + while (*p) { + while (*p && isspace((unsigned char)*p)) p++; + if (!*p) break; + + int grouped = 0; + if (*p == '(') { grouped = 1; p++; while (*p && isspace((unsigned char)*p)) p++; } + + if (!isdigit((unsigned char)*p)) { + fprintf(stderr, "Error: bad mask near '%s'\n", p); + return 0; + } + + char *end = NULL; + long w = strtol(p, &end, 10); + if (w <= 0 || w > 64) { + fprintf(stderr, "Error: bad width %ld in mask\n", w); + return 0; + } + p = end; + + while (*p && isspace((unsigned char)*p)) p++; + if (grouped) { + if (*p != ')') { fprintf(stderr, "Error: missing ')' in mask\n"); return 0; } + p++; + } + + if (off + (int)w > nCis) { + fprintf(stderr, "Error: mask widths exceed nCis (%d)\n", nCis); + return 0; + } + + segS[nSeg] = off; + segW[nSeg] = (int)w; + segG[nSeg] = grouped; + nSeg++; + + if (grouped) { + uint64_t m = ((w == 64) ? ~0ull : (((1ull << (unsigned)w) - 1ull) << (unsigned)off)); + if (nVars >= 64) { fprintf(stderr, "Error: too many vars in mask\n"); return 0; } + varMasks[nVars++] = m; + } else { + for (int t = 0; t < (int)w; ++t) { + if (nVars >= 64) { fprintf(stderr, "Error: too many vars in mask\n"); return 0; } + varMasks[nVars++] = 1ull << (unsigned)(off + t); + } + } + off += (int)w; + } + + if (off != nCis) { + fprintf(stderr, "Error: mask widths sum to %d but nCis=%d\n", off, nCis); + return 0; + } + + *pnVars = nVars; + if (verbose) PrintMaskSegmentsOneLine(maskStr, segS, segW, segG, nSeg, nVars, nCis); + return 1; +} + +/* ---------------------- file/binary helpers ---------------------- */ + +static int ends_with(const char *s, const char *suf) { + size_t ns = strlen(s), nf = strlen(suf); + return (ns >= nf) && !strcmp(s + (ns - nf), suf); +} + +static int make_tmp_file(char *path, size_t cap, const char *prefix) { + // Creates an existing temp file (for input) + snprintf(path, cap, "/tmp/%sXXXXXX", prefix); + int fd = mkstemp(path); + if (fd < 0) return 0; + close(fd); + return 1; +} + +static int make_tmp_path_noexist(char *path, size_t cap, const char *prefix) { + // Creates a unique temp path that does not exist (for output) + snprintf(path, cap, "/tmp/%sXXXXXX", prefix); + int fd = mkstemp(path); + if (fd < 0) return 0; + close(fd); + unlink(path); + return 1; +} + +static int write_words(const char *fname, const uint64_t *data, size_t nWords) { + FILE *f = fopen(fname, "wb"); + if (!f) return 0; + size_t wr = fwrite(data, sizeof(uint64_t), nWords, f); + fclose(f); + return wr == nWords; +} + +static int read_words(const char *fname, uint64_t *data, size_t nWords) { + FILE *f = fopen(fname, "rb"); + if (!f) return 0; + size_t rd = fread(data, sizeof(uint64_t), nWords, f); + fclose(f); + return rd == nWords; +} + +/* ---------------------- compare: AIG vs AIG ---------------------- */ + +static int SimulateCompareAigAig(const AigMan *p1, const AigMan *p2, + const uint64_t *varMasks, int nVars, int verbose) +{ + if (p1->nCis != p2->nCis || p1->nCos != p2->nCos) { + fprintf(stderr, "Error: interface mismatch: (I,O)=(%d,%d) vs (%d,%d)\n", + p1->nCis, p1->nCos, p2->nCis, p2->nCos); + return 0; + } + if (p1->nCis > 64 || p1->nCos > 64) { + fprintf(stderr, "Error: supports nCis<=64 and nCos<=64 (got I=%d O=%d)\n", p1->nCis, p1->nCos); + return 0; + } + + const uint64_t inMask = u64_mask_n(p1->nCis); + const uint64_t outMask = u64_mask_n(p1->nCos); + const unsigned __int128 combs = ((unsigned __int128)1) << (unsigned)nVars; + + uint32_t *co1 = ABC_ALLOC(uint32_t, p1->nCos); + uint32_t *co2 = ABC_ALLOC(uint32_t, p2->nCos); + for (int o = 0; o < p1->nCos; ++o) { + co1[o] = p1->nodes[p1->nCis + p1->nAnds + 1 + o].f0; + co2[o] = p2->nodes[p2->nCis + p2->nAnds + 1 + o].f0; + } + + uint64_t *S1 = ABC_CALLOC(uint64_t, (size_t)p1->nObjs * NW); + uint64_t *S2 = ABC_CALLOC(uint64_t, (size_t)p2->nObjs * NW); + + uint64_t inVec[BATCH], valid[NW]; + unsigned long long rounds = 0; + unsigned __int128 patsDone = 0; + + clock_t t0 = clock(); + + for (unsigned __int128 base = 0; base < combs; base += BATCH) { + unsigned __int128 remain = combs - base; + int nThis = (remain < BATCH) ? (int)remain : BATCH; + + int left = nThis; + for (int w = 0; w < NW; ++w) { + if (left >= 64) { valid[w] = ~0ull; left -= 64; } + else if (left > 0) { valid[w] = ((left == 64) ? ~0ull : ((1ull << left) - 1ull)); left = 0; } + else valid[w] = 0ull; + } + + // Clear CI words in both sims + for (int i = 0; i < p1->nCis; ++i) { + size_t off1 = (size_t)(1 + i) * NW; + size_t off2 = (size_t)(1 + i) * NW; + for (int w = 0; w < NW; ++w) S1[off1 + (size_t)w] = 0ull, S2[off2 + (size_t)w] = 0ull; + } + + // Fill CIs + for (int ptn = 0; ptn < nThis; ++ptn) { + uint64_t idx = (uint64_t)(base + (unsigned)ptn); + uint64_t in = 0; + for (int j = 0; j < nVars; ++j) if ((idx >> j) & 1ull) in |= varMasks[j]; + in &= inMask; + inVec[ptn] = in; + + int w = ptn >> 6; + uint64_t bit = 1ull << (ptn & 63); + uint64_t x = in; + while (x) { + int i = __builtin_ctzll(x); + x &= x - 1; + S1[(size_t)(1 + i) * NW + (size_t)w] |= bit; + S2[(size_t)(1 + i) * NW + (size_t)w] |= bit; + } + } + + // Simulate AIG #1 then AIG #2 + SimulateOne(p1, S1); + SimulateOne(p2, S2); + + // Compare COs + for (int o = 0; o < p1->nCos; ++o) { + for (int w = 0; w < NW; ++w) { + uint64_t y1 = SimLit(S1, co1[o], w); + uint64_t y2 = SimLit(S2, co2[o], w); + uint64_t diff = (y1 ^ y2) & valid[w]; + if (!diff) continue; + + int bit = __builtin_ctzll(diff); + int ptn = (w << 6) | bit; + + uint64_t out1 = 0, out2 = 0; + for (int oo = 0; oo < p1->nCos; ++oo) { + out1 |= ((SimLit(S1, co1[oo], w) >> bit) & 1ull) << oo; + out2 |= ((SimLit(S2, co2[oo], w) >> bit) & 1ull) << oo; + } + + int inHex = (p1->nCis + 3) / 4; + int outHex = (p1->nCos + 3) / 4; + char gbuf[64]; u128_to_dec(patsDone + (unsigned)ptn, gbuf, sizeof(gbuf)); + + printf("FAIL pattern=%s out_bit=%d\n", gbuf, o); + printf(" in = 0x%0*llx\n", inHex, (unsigned long long)(inVec[ptn] & inMask)); + printf(" y1 = 0x%0*llx\n", outHex, (unsigned long long)(out1 & outMask)); + printf(" y2 = 0x%0*llx\n", outHex, (unsigned long long)(out2 & outMask)); + + ABC_FREE(S1); ABC_FREE(S2); ABC_FREE(co1); ABC_FREE(co2); + return 0; + } + } + + rounds++; + patsDone += (unsigned)nThis; + if (verbose && (rounds % 256ull) == 0ull) { + char buf[64]; u128_to_dec(patsDone, buf, sizeof(buf)); + printf("[sim] rounds=%llu patterns=%s\n", rounds, buf); + } + } + + clock_t t1 = clock(); + double sec = (double)(t1 - t0) / (double)CLOCKS_PER_SEC; + + char totBuf[64]; u128_to_dec(combs, totBuf, sizeof(totBuf)); + printf("OK patterns=%s rounds=%llu time=%.3fs\n", totBuf, rounds, sec); + + ABC_FREE(S1); ABC_FREE(S2); ABC_FREE(co1); ABC_FREE(co2); + return 1; +} + +/* ---------------------- compare: AIG vs external binary ---------------------- */ + +static int SimulateCompareAigBin(const AigMan *p1, const char *bin, + const uint64_t *varMasks, int nVars, int verbose) +{ + if (p1->nCis > 64 || p1->nCos > 64) { + fprintf(stderr, "Error: supports nCis<=64 and nCos<=64 (got I=%d O=%d)\n", p1->nCis, p1->nCos); + return 0; + } + + const uint64_t inMask = u64_mask_n(p1->nCis); + const uint64_t outMask = u64_mask_n(p1->nCos); + const unsigned __int128 combs = ((unsigned __int128)1) << (unsigned)nVars; + + // Precompute AIG CO literals + uint32_t *co1 = ABC_ALLOC(uint32_t, p1->nCos); + for (int o = 0; o < p1->nCos; ++o) + co1[o] = p1->nodes[p1->nCis + p1->nAnds + 1 + o].f0; + + uint64_t *S1 = ABC_CALLOC(uint64_t, (size_t)p1->nObjs * NW); + uint64_t *out2 = ABC_ALLOC(uint64_t, (size_t)p1->nCos * NW); + + // Temp IO files for the binary + char inFile[128], outFile[128], cmd[512]; + if (!make_tmp_file(inFile, sizeof(inFile), "aigsim_in_") || + !make_tmp_path_noexist(outFile, sizeof(outFile), "aigsim_out_")) { + fprintf(stderr, "Error: cannot create temp files\n"); + ABC_FREE(S1); ABC_FREE(co1); ABC_FREE(out2); + return 0; + } + + uint64_t inVec[BATCH], valid[NW]; + unsigned long long rounds = 0; + unsigned __int128 patsDone = 0; + + clock_t t0 = clock(); + + for (unsigned __int128 base = 0; base < combs; base += BATCH) { + unsigned __int128 remain = combs - base; + int nThis = (remain < BATCH) ? (int)remain : BATCH; + + int left = nThis; + for (int w = 0; w < NW; ++w) { + if (left >= 64) { valid[w] = ~0ull; left -= 64; } + else if (left > 0) { valid[w] = ((left == 64) ? ~0ull : ((1ull << left) - 1ull)); left = 0; } + else valid[w] = 0ull; + } + + // Clear CI words + for (int i = 0; i < p1->nCis; ++i) { + size_t off = (size_t)(1 + i) * NW; + for (int w = 0; w < NW; ++w) S1[off + (size_t)w] = 0ull; + } + + // Fill CIs for this batch + for (int ptn = 0; ptn < nThis; ++ptn) { + uint64_t idx = (uint64_t)(base + (unsigned)ptn); + uint64_t in = 0; + for (int j = 0; j < nVars; ++j) if ((idx >> j) & 1ull) in |= varMasks[j]; + in &= inMask; + inVec[ptn] = in; + + int w = ptn >> 6; + uint64_t bit = 1ull << (ptn & 63); + + uint64_t x = in; + while (x) { + int i = __builtin_ctzll(x); + x &= x - 1; + S1[(size_t)(1 + i) * NW + (size_t)w] |= bit; + } + } + + // Simulate AIG + SimulateOne(p1, S1); + + // Write input sim-info file: nCis * NW words, CI major, word minor + if (!write_words(inFile, &S1[1 * NW], (size_t)p1->nCis * NW)) { + fprintf(stderr, "Error: cannot write %s\n", inFile); + goto fail; + } + + // Run external binary: " " + remove(outFile); + snprintf(cmd, sizeof(cmd), "%s %s %s", bin, inFile, outFile); + int rc = system(cmd); + if (rc != 0) { + fprintf(stderr, "Error: system() failed (rc=%d): %s\n", rc, cmd); + goto fail; + } + + // Read output sim-info file: nCos * NW words + if (!read_words(outFile, out2, (size_t)p1->nCos * NW)) { + fprintf(stderr, "Error: cannot read %s (expected %d*%d words)\n", outFile, p1->nCos, NW); + goto fail; + } + + // Compare AIG outputs vs binary outputs + for (int o = 0; o < p1->nCos; ++o) { + for (int w = 0; w < NW; ++w) { + uint64_t y1 = SimLit(S1, co1[o], w); + uint64_t y2 = out2[(size_t)o * NW + (size_t)w]; + uint64_t diff = (y1 ^ y2) & valid[w]; + if (!diff) continue; + + int bit = __builtin_ctzll(diff); + int ptn = (w << 6) | bit; + + uint64_t out1 = 0, outB = 0; + for (int oo = 0; oo < p1->nCos; ++oo) { + out1 |= ((SimLit(S1, co1[oo], w) >> bit) & 1ull) << oo; + outB |= ((out2[(size_t)oo * NW + (size_t)w] >> bit) & 1ull) << oo; + } + + int inHex = (p1->nCis + 3) / 4; + int outHex = (p1->nCos + 3) / 4; + char gbuf[64]; u128_to_dec(patsDone + (unsigned)ptn, gbuf, sizeof(gbuf)); + + printf("FAIL pattern=%s out_bit=%d\n", gbuf, o); + printf(" in = 0x%0*llx\n", inHex, (unsigned long long)(inVec[ptn] & inMask)); + printf(" aig = 0x%0*llx\n", outHex, (unsigned long long)(out1 & outMask)); + printf(" bin = 0x%0*llx\n", outHex, (unsigned long long)(outB & outMask)); + goto fail; + } + } + + rounds++; + patsDone += (unsigned)nThis; + if (verbose && (rounds % 256ull) == 0ull) { + char buf[64]; u128_to_dec(patsDone, buf, sizeof(buf)); + printf("[sim] rounds=%llu patterns=%s\n", rounds, buf); + } + } + + { + clock_t t1 = clock(); + double sec = (double)(t1 - t0) / (double)CLOCKS_PER_SEC; + char totBuf[64]; u128_to_dec(combs, totBuf, sizeof(totBuf)); + printf("OK patterns=%s rounds=%llu time=%.3fs\n", totBuf, rounds, sec); + } + + remove(inFile); + remove(outFile); + ABC_FREE(S1); ABC_FREE(co1); ABC_FREE(out2); + return 1; + +fail: + remove(inFile); + remove(outFile); + ABC_FREE(S1); ABC_FREE(co1); ABC_FREE(out2); + return 0; +} + +/* ---------------------- top API ---------------------- */ + +int SimulateAigTop( char *fname1, char *fname2, char *mask, int verbose ) +{ + AigMan *p1 = Aig_ManLoadAigerBinary(fname1, verbose); + if (!p1) return 2; + + uint64_t varMasks[64]; + int nVars = 0; + if (!ParseMaskString(mask, p1->nCis, varMasks, &nVars, verbose)) { + Aig_ManStop(p1); + return 2; + } + + int ok = 0; + + if (ends_with(fname2, ".aig")) { + AigMan *p2 = Aig_ManLoadAigerBinary(fname2, verbose); + if (!p2) { Aig_ManStop(p1); return 2; } + ok = SimulateCompareAigAig(p1, p2, varMasks, nVars, verbose); + Aig_ManStop(p2); + } else { + // fname2 is an external binary: bin + ok = SimulateCompareAigBin(p1, fname2, varMasks, nVars, verbose); + } + + Aig_ManStop(p1); + return ok ? 0 : 3; +} + +/* ---------------------- main ---------------------- */ +/* Usage: + ./aig_equiv_2aigs [-v] file1.aig file2.aig_or_binary [mask_str] + + mask_str example for 16 inputs: + "2(4)10" -> 2 individual bits, then 4 grouped bits (all-0/all-1), then 10 individual bits +*/ +#ifndef AIGSIM_LIBRARY_ONLY +int main(int argc, char **argv) { + int verbose = 0; + const char *f1 = NULL, *f2 = NULL; + const char *mask = NULL; + + int ai = 1; + if (ai < argc && !strcmp(argv[ai], "-v")) { verbose = 1; ai++; } + if (ai + 1 >= argc) { + fprintf(stderr, "Usage: %s [-v] file1.aig file2.aig_or_binary [mask_str]\n", argv[0]); + return 1; + } + f1 = argv[ai++]; + f2 = argv[ai++]; + if (ai < argc) mask = argv[ai++]; + + return SimulateAigTop((char*)f1, (char*)f2, (char*)mask, verbose); +} +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END +