diff options
Diffstat (limited to 'src/aig/ssw/ssw.h')
-rw-r--r-- | src/aig/ssw/ssw.h | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h index 3bdc63f6..aaaa6407 100644 --- a/src/aig/ssw/ssw.h +++ b/src/aig/ssw/ssw.h @@ -54,6 +54,18 @@ struct Ssw_Pars_t_ int nIters; // the number of iterations performed }; +// sequential counter-example +typedef struct Ssw_Cex_t_ Ssw_Cex_t; +struct Ssw_Cex_t_ +{ + int iPo; // the zero-based number of PO, for which verification failed + int iFrame; // the zero-based number of the time-frame, for which verificaiton failed + int nRegs; // the number of registers in the miter + int nPis; // the number of primary inputs in the miter + int nBits; // the number of words of bit data used + unsigned pData[0]; // the cex bit data (the number of bits: nRegs + (iFrame+1) * nPis) +}; + //////////////////////////////////////////////////////////////////////// /// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// |