ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Functions
bmcCexDepth.c File Reference
#include "bmc.h"
Include dependency graph for bmcCexDepth.c:

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START Abc_Cex_t * Bmc_CexInnerStates (Gia_Man_t *p, Abc_Cex_t *pCex, Abc_Cex_t **ppCexImpl, int fVerbose)
 DECLARATIONS ///.
 
Abc_Cex_t * Bmc_CexCareBits (Gia_Man_t *p, Abc_Cex_t *pCexState, Abc_Cex_t *pCexImpl, Abc_Cex_t *pCexEss, int fFindAll, int fVerbose)
 
int Bmc_CexVerify (Gia_Man_t *p, Abc_Cex_t *pCex, Abc_Cex_t *pCexCare)
 
Gia_Man_t * Bmc_CexTargetEnlarge (Gia_Man_t *p, int nFrames)
 FUNCTION DEFINITIONS ///.
 
Gia_Man_t * Bmc_CexTarget (Gia_Man_t *p, int nFrames)
 
Gia_Man_t * Bmc_CexBuildNetwork2 (Gia_Man_t *p, Abc_Cex_t *pCex, int fStart)
 
Gia_Man_t * Bmc_CexBuildNetwork2_ (Gia_Man_t *p, Abc_Cex_t *pCex, int fStart)
 
Gia_Man_t * Bmc_CexBuildNetwork2Test (Gia_Man_t *p, Abc_Cex_t *pCex, int nFramesMax)
 
Gia_Man_t * Bmc_CexDepthTest (Gia_Man_t *p, Abc_Cex_t *pCex, int nFrames, int fVerbose)
 

Function Documentation

◆ Bmc_CexBuildNetwork2()

Gia_Man_t * Bmc_CexBuildNetwork2 ( Gia_Man_t * p,
Abc_Cex_t * pCex,
int fStart )

Function*************************************************************

Synopsis [Computes CE-induced network.]

Description []

SideEffects []

SeeAlso []

Definition at line 128 of file bmcCexDepth.c.

129{
130 Gia_Man_t * pNew, * pTemp;
131 Gia_Obj_t * pObj, * pObjRo, * pObjRi;
132 int fCompl0, fCompl1;
133 int i, k, iBit;
134 assert( pCex->nRegs == 0 );
135 assert( pCex->nPis == Gia_ManCiNum(p) );
136 assert( fStart <= pCex->iFrame );
137 // start the manager
138 pNew = Gia_ManStart( 1000 );
139 pNew->pName = Abc_UtilStrsav( "unate" );
140 // set const0
141 Gia_ManConst0(p)->fMark0 = 0; // value
142 Gia_ManConst0(p)->fMark1 = 1; // care
143 Gia_ManConst0(p)->Value = ~0;
144 // set init state
145 Gia_ManForEachRi( p, pObj, k )
146 {
147 pObj->fMark0 = Abc_InfoHasBit( pCex->pData, pCex->nRegs + fStart * Gia_ManCiNum(p) + Gia_ManPiNum(p) + k );
148 pObj->fMark1 = 0;
149 pObj->Value = Abc_LitNotCond( Gia_ManAppendCi(pNew), !pObj->fMark0 );
150 }
151 Gia_ManHashAlloc( pNew );
152 iBit = pCex->nRegs + fStart * Gia_ManCiNum(p);
153 for ( i = fStart; i <= pCex->iFrame; i++ )
154 {
155 // primary inputs
156 Gia_ManForEachPi( p, pObj, k )
157 {
158 pObj->fMark0 = Abc_InfoHasBit( pCex->pData, iBit++ );
159 pObj->fMark1 = 1;
160 pObj->Value = ~0;
161 }
162 iBit += Gia_ManRegNum(p);
163 // transfer
164 Gia_ManForEachRiRo( p, pObjRi, pObjRo, k )
165 {
166 pObjRo->fMark0 = pObjRi->fMark0;
167 pObjRo->fMark1 = pObjRi->fMark1;
168 pObjRo->Value = pObjRi->Value;
169 }
170 // internal nodes
171 Gia_ManForEachAnd( p, pObj, k )
172 {
173 fCompl0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
174 fCompl1 = Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj);
175 pObj->fMark0 = fCompl0 & fCompl1;
176 if ( pObj->fMark0 )
177 pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1 & Gia_ObjFanin1(pObj)->fMark1;
178 else if ( !fCompl0 && !fCompl1 )
179 pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1 | Gia_ObjFanin1(pObj)->fMark1;
180 else if ( !fCompl0 )
181 pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1;
182 else if ( !fCompl1 )
183 pObj->fMark1 = Gia_ObjFanin1(pObj)->fMark1;
184 else assert( 0 );
185 pObj->Value = ~0;
186 if ( pObj->fMark1 )
187 continue;
188 if ( pObj->fMark0 )
189 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value );
190 else if ( !fCompl0 && !fCompl1 )
191 pObj->Value = Gia_ManHashOr( pNew, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value );
192 else if ( !fCompl0 )
193 pObj->Value = Gia_ObjFanin0(pObj)->Value;
194 else if ( !fCompl1 )
195 pObj->Value = Gia_ObjFanin1(pObj)->Value;
196 else assert( 0 );
197 assert( pObj->Value > 0 );
198 }
199 // combinational outputs
200 Gia_ManForEachCo( p, pObj, k )
201 {
202 pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
203 pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1;
204 pObj->Value = Gia_ObjFanin0(pObj)->Value;
205 }
206 }
207 Gia_ManHashStop( pNew );
208 assert( iBit == pCex->nBits );
209 // create primary output
210 pObj = Gia_ManPo(p, pCex->iPo);
211 assert( pObj->fMark0 == 1 );
212 assert( pObj->fMark1 == 0 );
213 assert( pObj->Value > 0 );
214 Gia_ManAppendCo( pNew, pObj->Value );
215 // cleanup
216 pNew = Gia_ManCleanup( pTemp = pNew );
217 Gia_ManStop( pTemp );
218 return pNew;
219}
p
Cube * p
Definition exorList.c:222
Gia_ManStop
void Gia_ManStop(Gia_Man_t *p)
Definition giaMan.c:82
Gia_ManForEachAnd
#define Gia_ManForEachAnd(p, pObj, i)
Definition gia.h:1214
Gia_ManHashAlloc
void Gia_ManHashAlloc(Gia_Man_t *p)
Definition giaHash.c:105
Gia_ManForEachPi
#define Gia_ManForEachPi(p, pObj, i)
Definition gia.h:1248
Gia_ManStart
Gia_Man_t * Gia_ManStart(int nObjsMax)
FUNCTION DEFINITIONS ///.
Definition giaMan.c:57
Gia_ManHashOr
int Gia_ManHashOr(Gia_Man_t *p, int iLit0, int iLit1)
Definition giaHash.c:621
Gia_Obj_t
struct Gia_Obj_t_ Gia_Obj_t
Definition gia.h:76
Gia_Man_t
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
Gia_ManCleanup
Gia_Man_t * Gia_ManCleanup(Gia_Man_t *p)
Definition giaScl.c:84
Gia_ManHashAnd
int Gia_ManHashAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition giaHash.c:576
Gia_ManForEachCo
#define Gia_ManForEachCo(p, pObj, i)
Definition gia.h:1236
Gia_ManForEachRiRo
#define Gia_ManForEachRiRo(p, pObjRi, pObjRo, i)
Definition gia.h:1256
Gia_ManHashStop
void Gia_ManHashStop(Gia_Man_t *p)
Definition giaHash.c:149
Gia_ManForEachRi
#define Gia_ManForEachRi(p, pObj, i)
Definition gia.h:1254
Gia_Man_t_::pName
char * pName
Definition gia.h:99
Gia_Obj_t_::fMark1
unsigned fMark1
Definition gia.h:86
Gia_Obj_t_::Value
unsigned Value
Definition gia.h:89
Gia_Obj_t_::fMark0
unsigned fMark0
Definition gia.h:81
assert
#define assert(ex)
Definition util_old.h:213
Here is the call graph for this function:

◆ Bmc_CexBuildNetwork2_()

Gia_Man_t * Bmc_CexBuildNetwork2_ ( Gia_Man_t * p,
Abc_Cex_t * pCex,
int fStart )

Definition at line 220 of file bmcCexDepth.c.

221{
222 Gia_Man_t * pNew, * pTemp;
223 Gia_Obj_t * pObj, * pObjRo, * pObjRi;
224 int fCompl0, fCompl1;
225 int i, k, iBit;
226 assert( pCex->nRegs == 0 );
227 assert( pCex->nPis == Gia_ManCiNum(p) );
228 assert( fStart <= pCex->iFrame );
229 // start the manager
230 pNew = Gia_ManStart( 1000 );
231 pNew->pName = Abc_UtilStrsav( "unate" );
232 // set const0
233 Gia_ManConst0(p)->fMark0 = 0; // value
234 Gia_ManConst0(p)->Value = 1;
235 // set init state
236 Gia_ManForEachRi( p, pObj, k )
237 {
238 pObj->fMark0 = Abc_InfoHasBit( pCex->pData, pCex->nRegs + fStart * Gia_ManCiNum(p) + Gia_ManPiNum(p) + k );
239 pObj->Value = Abc_LitNotCond( Gia_ManAppendCi(pNew), !pObj->fMark0 );
240 }
241 Gia_ManHashAlloc( pNew );
242 iBit = pCex->nRegs + fStart * Gia_ManCiNum(p);
243 for ( i = fStart; i <= pCex->iFrame; i++ )
244 {
245 // primary inputs
246 Gia_ManForEachPi( p, pObj, k )
247 {
248 pObj->fMark0 = Abc_InfoHasBit( pCex->pData, iBit++ );
249 pObj->Value = 1;
250 }
251 iBit += Gia_ManRegNum(p);
252 // transfer
253 Gia_ManForEachRiRo( p, pObjRi, pObjRo, k )
254 {
255 pObjRo->fMark0 = pObjRi->fMark0;
256 pObjRo->Value = pObjRi->Value;
257 }
258 // internal nodes
259 Gia_ManForEachAnd( p, pObj, k )
260 {
261 fCompl0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
262 fCompl1 = Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj);
263 pObj->fMark0 = fCompl0 & fCompl1;
264 if ( pObj->fMark0 )
265 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value );
266 else if ( !fCompl0 && !fCompl1 )
267 pObj->Value = Gia_ManHashOr( pNew, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value );
268 else if ( !fCompl0 )
269 pObj->Value = Gia_ObjFanin0(pObj)->Value;
270 else if ( !fCompl1 )
271 pObj->Value = Gia_ObjFanin1(pObj)->Value;
272 else assert( 0 );
273 }
274 // combinational outputs
275 Gia_ManForEachCo( p, pObj, k )
276 {
277 pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
278 pObj->Value = Gia_ObjFanin0(pObj)->Value;
279 }
280 }
281 Gia_ManHashStop( pNew );
282 assert( iBit == pCex->nBits );
283 // create primary output
284 pObj = Gia_ManPo(p, pCex->iPo);
285 assert( pObj->fMark0 == 1 );
286 assert( pObj->Value > 0 );
287 Gia_ManAppendCo( pNew, pObj->Value );
288 // cleanup
289 pNew = Gia_ManCleanup( pTemp = pNew );
290 Gia_ManStop( pTemp );
291 return pNew;
292}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Bmc_CexBuildNetwork2Test()

Gia_Man_t * Bmc_CexBuildNetwork2Test ( Gia_Man_t * p,
Abc_Cex_t * pCex,
int nFramesMax )

Definition at line 294 of file bmcCexDepth.c.

295{
296 Gia_Man_t * pNew, * pTemp;
297 Vec_Ptr_t * vCones;
298 abctime clk = Abc_Clock();
299 int i;
300 nFramesMax = Abc_MinInt( nFramesMax, pCex->iFrame );
301 printf( "Processing CEX in frame %d (max frames %d).\n", pCex->iFrame, nFramesMax );
302 vCones = Vec_PtrAlloc( nFramesMax );
303 for ( i = pCex->iFrame; i > pCex->iFrame - nFramesMax; i-- )
304 {
305 printf( "Frame %5d : ", i );
306 pNew = Bmc_CexBuildNetwork2_( p, pCex, i );
307 Gia_ManPrintStats( pNew, NULL );
308 Vec_PtrPush( vCones, pNew );
309 }
310 pNew = Gia_ManDupAppendCones( p, (Gia_Man_t **)Vec_PtrArray(vCones), Vec_PtrSize(vCones), 1 );
311 Gia_AigerWrite( pNew, "miter2.aig", 0, 0, 0 );
312//Bmc_CexDumpAogStats( pNew, Abc_Clock() - clk );
313 Vec_PtrForEachEntry( Gia_Man_t *, vCones, pTemp, i )
314 Gia_ManStop( pTemp );
315 Vec_PtrFree( vCones );
316 printf( "GIA with additional properties is written into \"miter2.aig\".\n" );
317// printf( "CE-induced network is written into file \"unate.aig\".\n" );
318 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
319// Gia_ManStop( pNew );
320 return pNew;
321}
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
Bmc_CexBuildNetwork2_
Gia_Man_t * Bmc_CexBuildNetwork2_(Gia_Man_t *p, Abc_Cex_t *pCex, int fStart)
Definition bmcCexDepth.c:220
Gia_ManDupAppendCones
Gia_Man_t * Gia_ManDupAppendCones(Gia_Man_t *p, Gia_Man_t **ppCones, int nCones, int fOnlyRegs)
Definition giaDup.c:1305
Gia_ManPrintStats
void Gia_ManPrintStats(Gia_Man_t *p, Gps_Par_t *pPars)
Definition giaMan.c:495
Gia_AigerWrite
void Gia_AigerWrite(Gia_Man_t *p, char *pFileName, int fWriteSymbols, int fCompact, int fWriteNewLine)
Definition giaAiger.c:1595
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Bmc_CexCareBits()

Abc_Cex_t * Bmc_CexCareBits ( Gia_Man_t * p,
Abc_Cex_t * pCexState,
Abc_Cex_t * pCexImpl,
Abc_Cex_t * pCexEss,
int fFindAll,
int fVerbose )
extern

Definition at line 597 of file bmcCexTools.c.

598{
599 Abc_Cex_t * pNew;
600 Gia_Obj_t * pObj;
601 int fCompl0, fCompl1;
602 int i, k, iBit;
603 assert( pCexState->nRegs == 0 );
604 // start the counter-example
605 pNew = Abc_CexAlloc( 0, Gia_ManCiNum(p), pCexState->iFrame + 1 );
606 pNew->iFrame = pCexState->iFrame;
607 pNew->iPo = pCexState->iPo;
608 // set initial state
609 Gia_ManCleanMark01(p);
610 // set const0
611 Gia_ManConst0(p)->fMark0 = 0;
612 Gia_ManConst0(p)->fMark1 = 1;
613 for ( i = pCexState->iFrame; i >= 0; i-- )
614 {
615 // set correct values
616 iBit = pCexState->nPis * i;
617 Gia_ManForEachCi( p, pObj, k )
618 {
619 pObj->fMark0 = Abc_InfoHasBit(pCexState->pData, iBit+k);
620 pObj->fMark1 = 0;
621 if ( pCexImpl )
622 pObj->fMark1 |= Abc_InfoHasBit(pCexImpl->pData, iBit+k);
623 if ( pCexEss )
624 pObj->fMark1 |= Abc_InfoHasBit(pCexEss->pData, iBit+k);
625 }
626 Gia_ManForEachAnd( p, pObj, k )
627 {
628 fCompl0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
629 fCompl1 = Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj);
630 pObj->fMark0 = fCompl0 & fCompl1;
631 if ( pObj->fMark0 )
632 pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1 & Gia_ObjFanin1(pObj)->fMark1;
633 else if ( !fCompl0 && !fCompl1 )
634 pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1 | Gia_ObjFanin1(pObj)->fMark1;
635 else if ( !fCompl0 )
636 pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1;
637 else if ( !fCompl1 )
638 pObj->fMark1 = Gia_ObjFanin1(pObj)->fMark1;
639 else assert( 0 );
640 }
641 Gia_ManForEachCo( p, pObj, k )
642 pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
643 // move values from COs to CIs
644 if ( i == pCexState->iFrame )
645 {
646 assert( Gia_ManPo(p, pCexState->iPo)->fMark0 == 1 );
647 if ( fFindAll )
648 Bmc_CexCareBits_rec( p, Gia_ObjFanin0(Gia_ManPo(p, pCexState->iPo)) );
649 else
650 Bmc_CexCareBits2_rec( p, Gia_ObjFanin0(Gia_ManPo(p, pCexState->iPo)) );
651 }
652 else
653 {
654 Gia_ManForEachRi( p, pObj, k )
655 if ( Abc_InfoHasBit(pNew->pData, pNew->nPis * (i+1) + Gia_ManPiNum(p) + k) )
656 {
657 if ( fFindAll )
658 Bmc_CexCareBits_rec( p, Gia_ObjFanin0(pObj) );
659 else
660 Bmc_CexCareBits2_rec( p, Gia_ObjFanin0(pObj) );
661 }
662 }
663 // save the results
664 Gia_ManForEachCi( p, pObj, k )
665 if ( pObj->fMark1 )
666 {
667 pObj->fMark1 = 0;
668 if ( pCexImpl == NULL || !Abc_InfoHasBit(pCexImpl->pData, pNew->nPis * i + k) )
669 Abc_InfoSetBit(pNew->pData, pNew->nPis * i + k);
670 }
671 }
672 if ( pCexEss )
673 printf( "Minimized: " );
674 else
675 printf( "Care bits: " );
676 Bmc_CexPrint( pNew, Gia_ManPiNum(p), fVerbose );
677 return pNew;
678}
Bmc_CexPrint
void Bmc_CexPrint(Abc_Cex_t *pCex, int nRealPis, int fVerbose)
Definition bmcCexTools.c:307
Bmc_CexCareBits_rec
void Bmc_CexCareBits_rec(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition bmcCexTools.c:538
Bmc_CexCareBits2_rec
void Bmc_CexCareBits2_rec(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition bmcCexTools.c:566
Gia_ManForEachCi
#define Gia_ManForEachCi(p, pObj, i)
Definition gia.h:1228
Gia_ManCleanMark01
void Gia_ManCleanMark01(Gia_Man_t *p)
Definition giaUtil.c:218
Abc_CexAlloc
ABC_NAMESPACE_IMPL_START Abc_Cex_t * Abc_CexAlloc(int nRegs, int nRealPis, int nFrames)
DECLARATIONS ///.
Definition utilCex.c:51
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition utilCex.h:39
Here is the caller graph for this function:

◆ Bmc_CexDepthTest()

Gia_Man_t * Bmc_CexDepthTest ( Gia_Man_t * p,
Abc_Cex_t * pCex,
int nFrames,
int fVerbose )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 335 of file bmcCexDepth.c.

336{
337 Gia_Man_t * pNew;
338 abctime clk = Abc_Clock();
339 Abc_Cex_t * pCexImpl = NULL;
340 Abc_Cex_t * pCexStates = Bmc_CexInnerStates( p, pCex, &pCexImpl, fVerbose );
341 Abc_Cex_t * pCexCare = Bmc_CexCareBits( p, pCexStates, pCexImpl, NULL, 1, fVerbose );
342// Abc_Cex_t * pCexEss, * pCexMin;
343
344 if ( !Bmc_CexVerify( p, pCex, pCexCare ) )
345 printf( "Counter-example care-set verification has failed.\n" );
346
347// pCexEss = Bmc_CexEssentialBits( p, pCexStates, pCexCare, fVerbose );
348// pCexMin = Bmc_CexCareBits( p, pCexStates, pCexImpl, pCexEss, 0, fVerbose );
349
350// if ( !Bmc_CexVerify( p, pCex, pCexMin ) )
351// printf( "Counter-example min-set verification has failed.\n" );
352
353// Bmc_CexDumpStats( p, pCex, pCexCare, pCexEss, pCexMin, Abc_Clock() - clk );
354
355 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
356 pNew = Bmc_CexBuildNetwork2Test( p, pCexStates, nFrames );
357// Bmc_CexPerformUnrollingTest( p, pCex );
358
359 Abc_CexFreeP( &pCexStates );
360 Abc_CexFreeP( &pCexImpl );
361 Abc_CexFreeP( &pCexCare );
362// Abc_CexFreeP( &pCexEss );
363// Abc_CexFreeP( &pCexMin );
364 return pNew;
365}
Bmc_CexCareBits
Abc_Cex_t * Bmc_CexCareBits(Gia_Man_t *p, Abc_Cex_t *pCexState, Abc_Cex_t *pCexImpl, Abc_Cex_t *pCexEss, int fFindAll, int fVerbose)
Definition bmcCexTools.c:597
Bmc_CexBuildNetwork2Test
Gia_Man_t * Bmc_CexBuildNetwork2Test(Gia_Man_t *p, Abc_Cex_t *pCex, int nFramesMax)
Definition bmcCexDepth.c:294
Bmc_CexVerify
int Bmc_CexVerify(Gia_Man_t *p, Abc_Cex_t *pCex, Abc_Cex_t *pCexCare)
Definition bmcCexTools.c:346
Bmc_CexInnerStates
ABC_NAMESPACE_IMPL_START Abc_Cex_t * Bmc_CexInnerStates(Gia_Man_t *p, Abc_Cex_t *pCex, Abc_Cex_t **ppCexImpl, int fVerbose)
DECLARATIONS ///.
Definition bmcCexTools.c:435
Abc_CexFreeP
void Abc_CexFreeP(Abc_Cex_t **p)
Definition utilCex.c:361
Here is the call graph for this function:

◆ Bmc_CexInnerStates()

ABC_NAMESPACE_IMPL_START Abc_Cex_t * Bmc_CexInnerStates ( Gia_Man_t * p,
Abc_Cex_t * pCex,
Abc_Cex_t ** ppCexImpl,
int fVerbose )
extern

DECLARATIONS ///.

CFile****************************************************************

FileName [bmcCexDepth.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [SAT-based bounded model checking.]

Synopsis [CEX depth minimization.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id
bmcCexDepth.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

]

Function*************************************************************

Synopsis [Computes internal states of the CEX.]

Description []

SideEffects []

SeeAlso []

Definition at line 435 of file bmcCexTools.c.

436{
437 Abc_Cex_t * pNew, * pNew2;
438 Gia_Obj_t * pObj, * pObjRo, * pObjRi;
439 int fCompl0, fCompl1;
440 int i, k, iBit = 0;
441 assert( pCex->nRegs > 0 );
442 // start the counter-example
443 pNew = Abc_CexAlloc( 0, Gia_ManCiNum(p), pCex->iFrame + 1 );
444 pNew->iFrame = pCex->iFrame;
445 pNew->iPo = pCex->iPo;
446 // start the counter-example
447 pNew2 = Abc_CexAlloc( 0, Gia_ManCiNum(p), pCex->iFrame + 1 );
448 pNew2->iFrame = pCex->iFrame;
449 pNew2->iPo = pCex->iPo;
450 // set initial state
451 Gia_ManCleanMark01(p);
452 // set const0
453 Gia_ManConst0(p)->fMark0 = 0;
454 Gia_ManConst0(p)->fMark1 = 1;
455 // set init state
456 Gia_ManForEachRi( p, pObjRi, k )
457 {
458 pObjRi->fMark0 = 0;
459 pObjRi->fMark1 = 1;
460 }
461 iBit = pCex->nRegs;
462 for ( i = 0; i <= pCex->iFrame; i++ )
463 {
464 Gia_ManForEachPi( p, pObj, k )
465 pObj->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++);
466 Gia_ManForEachRiRo( p, pObjRi, pObjRo, k )
467 {
468 pObjRo->fMark0 = pObjRi->fMark0;
469 pObjRo->fMark1 = pObjRi->fMark1;
470 }
471 Gia_ManForEachCi( p, pObj, k )
472 {
473 if ( pObj->fMark0 )
474 Abc_InfoSetBit( pNew->pData, pNew->nPis * i + k );
475 if ( pObj->fMark1 )
476 Abc_InfoSetBit( pNew2->pData, pNew2->nPis * i + k );
477 }
478 Gia_ManForEachAnd( p, pObj, k )
479 {
480 fCompl0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
481 fCompl1 = Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj);
482 pObj->fMark0 = fCompl0 & fCompl1;
483 if ( pObj->fMark0 )
484 pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1 & Gia_ObjFanin1(pObj)->fMark1;
485 else if ( !fCompl0 && !fCompl1 )
486 pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1 | Gia_ObjFanin1(pObj)->fMark1;
487 else if ( !fCompl0 )
488 pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1;
489 else if ( !fCompl1 )
490 pObj->fMark1 = Gia_ObjFanin1(pObj)->fMark1;
491 else assert( 0 );
492 }
493 Gia_ManForEachCo( p, pObj, k )
494 {
495 pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
496 pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1;
497 }
498
499/*
500 // print input/state/output
501 printf( "%3d : ", i );
502 Gia_ManForEachPi( p, pObj, k )
503 printf( "%d", pObj->fMark0 );
504 printf( " " );
505 Gia_ManForEachRo( p, pObj, k )
506 printf( "%d", pObj->fMark0 );
507 printf( " " );
508 Gia_ManForEachPo( p, pObj, k )
509 printf( "%d", pObj->fMark0 );
510 printf( "\n" );
511*/
512 }
513 assert( iBit == pCex->nBits );
514 assert( Gia_ManPo(p, pCex->iPo)->fMark0 == 1 );
515
516 printf( "Inner states: " );
517 Bmc_CexPrint( pNew, Gia_ManPiNum(p), fVerbose );
518 printf( "Implications: " );
519 Bmc_CexPrint( pNew2, Gia_ManPiNum(p), fVerbose );
520 if ( ppCexImpl )
521 *ppCexImpl = pNew2;
522 else
523 Abc_CexFree( pNew2 );
524 return pNew;
525}
Abc_CexFree
void Abc_CexFree(Abc_Cex_t *p)
Definition utilCex.c:382
Here is the caller graph for this function:

◆ Bmc_CexTarget()

Gia_Man_t * Bmc_CexTarget ( Gia_Man_t * p,
int nFrames )

Function*************************************************************

Synopsis [Create target with quantified inputs.]

Description []

SideEffects []

SeeAlso []

Definition at line 94 of file bmcCexDepth.c.

95{
96 Gia_Man_t * pNew, * pTemp;
97 int i, Limit = nFrames * Gia_ManPiNum(p);
98 pNew = Bmc_CexTargetEnlarge( p, nFrames );
99 for ( i = 0; i < Limit; i++ )
100 {
101 printf( "%3d : ", i );
102 if ( i % Gia_ManPiNum(p) == 0 )
103 Gia_ManPrintStats( pNew, NULL );
104 pNew = Gia_ManDupExist( pTemp = pNew, i );
105 Gia_ManStop( pTemp );
106 }
107 Gia_ManPrintStats( pNew, NULL );
108 pNew = Gia_ManDupLastPis( pTemp = pNew, Gia_ManRegNum(p) );
109 Gia_ManStop( pTemp );
110 Gia_ManPrintStats( pNew, NULL );
111 pTemp = Gia_ManDupAppendCones( p, &pNew, 1, 1 );
112 Gia_ManStop( pNew );
113 Gia_AigerWrite( pTemp, "miter3.aig", 0, 0, 0 );
114 return pTemp;
115}
Bmc_CexTargetEnlarge
Gia_Man_t * Bmc_CexTargetEnlarge(Gia_Man_t *p, int nFrames)
FUNCTION DEFINITIONS ///.
Definition bmcCexDepth.c:49
Gia_ManDupLastPis
Gia_Man_t * Gia_ManDupLastPis(Gia_Man_t *p, int nLastPis)
Definition giaDup.c:597
Gia_ManDupExist
Gia_Man_t * Gia_ManDupExist(Gia_Man_t *p, int iVar)
Definition giaDup.c:2012
Here is the call graph for this function:

◆ Bmc_CexTargetEnlarge()

Gia_Man_t * Bmc_CexTargetEnlarge ( Gia_Man_t * p,
int nFrames )

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis [Performs targe enlargement of the given size.]

Description []

SideEffects []

SeeAlso []

Definition at line 49 of file bmcCexDepth.c.

50{
51 Gia_Man_t * pNew, * pOne;
52 Gia_Obj_t * pObj, * pObjRo;
53 int i, k;
54 pNew = Gia_ManStart( Gia_ManObjNum(p) );
55 pNew->pName = Abc_UtilStrsav( p->pName );
56 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
57 Gia_ManHashAlloc( pNew );
58 Gia_ManConst0(p)->Value = 0;
59 for ( k = 0; k < nFrames; k++ )
60 Gia_ManForEachPi( p, pObj, i )
61 Gia_ManAppendCi( pNew );
62 Gia_ManForEachRo( p, pObj, i )
63 pObj->Value = Gia_ManAppendCi( pNew );
64 for ( k = 0; k < nFrames; k++ )
65 {
66 Gia_ManForEachPi( p, pObj, i )
67 pObj->Value = Gia_ManCiLit( pNew, (nFrames - 1 - k) * Gia_ManPiNum(p) + i );
68 Gia_ManForEachAnd( p, pObj, i )
69 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
70 Gia_ManForEachRi( p, pObj, i )
71 pObj->Value = Gia_ObjFanin0Copy(pObj);
72 Gia_ManForEachRiRo( p, pObj, pObjRo, i )
73 pObjRo->Value = pObj->Value;
74 }
75 pObj = Gia_ManPo( p, 0 );
76 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
77 Gia_ManHashStop( pNew );
78 pNew = Gia_ManCleanup( pOne = pNew );
79 Gia_ManStop( pOne );
80 return pNew;
81}
Gia_ManForEachRo
#define Gia_ManForEachRo(p, pObj, i)
Definition gia.h:1252
Gia_Man_t_::pSpec
char * pSpec
Definition gia.h:100
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Bmc_CexVerify()

int Bmc_CexVerify ( Gia_Man_t * p,
Abc_Cex_t * pCex,
Abc_Cex_t * pCexCare )
extern

Function*************************************************************

Synopsis [Verifies the care set of the counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 346 of file bmcCexTools.c.

347{
348 Gia_Obj_t * pObj;
349 int i, k;
350// assert( pCex->nRegs > 0 );
351// assert( pCexCare->nRegs == 0 );
352 Gia_ObjTerSimSet0( Gia_ManConst0(p) );
353 Gia_ManForEachRi( p, pObj, k )
354 Gia_ObjTerSimSet0( pObj );
355 for ( i = 0; i <= pCex->iFrame; i++ )
356 {
357 Gia_ManForEachPi( p, pObj, k )
358 {
359 if ( !Abc_InfoHasBit( pCexCare->pData, pCexCare->nRegs + i * pCexCare->nPis + k ) )
360 Gia_ObjTerSimSetX( pObj );
361 else if ( Abc_InfoHasBit( pCex->pData, pCex->nRegs + i * pCex->nPis + k ) )
362 Gia_ObjTerSimSet1( pObj );
363 else
364 Gia_ObjTerSimSet0( pObj );
365 }
366 Gia_ManForEachRo( p, pObj, k )
367 Gia_ObjTerSimRo( p, pObj );
368 Gia_ManForEachAnd( p, pObj, k )
369 Gia_ObjTerSimAnd( pObj );
370 Gia_ManForEachCo( p, pObj, k )
371 Gia_ObjTerSimCo( pObj );
372 }
373 pObj = Gia_ManPo( p, pCex->iPo );
374 return Gia_ObjTerSimGet1(pObj);
375}
Here is the caller graph for this function: