From a30c08bbe55d624ec3269577bf16f2f09215be12 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 9 Sep 2008 08:01:00 -0700 Subject: Version abc80909 --- src/aig/ssw/ssw.h | 12 ++++++++++++ 1 file changed, 12 insertions(+) (limited to 'src/aig/ssw/ssw.h') 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 /// //////////////////////////////////////////////////////////////////////// -- cgit v1.2.3