ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Functions
llb4Cex.c File Reference
#include "llbInt.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satSolver.h"
Include dependency graph for llb4Cex.c:

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START Abc_Cex_t * Llb4_Nonlin4TransformCex (Aig_Man_t *pAig, Vec_Ptr_t *vStates, int iCexPo, int fVerbose)
 DECLARATIONS ///.
 
Vec_Ptr_t * Llb4_Nonlin4VerifyCex (Aig_Man_t *pAig, Abc_Cex_t *p)
 
Abc_Cex_t * Llb4_Nonlin4NormalizeCex (Aig_Man_t *pAigOrg, Aig_Man_t *pAigRpm, Abc_Cex_t *pCexRpm)
 

Function Documentation

◆ Llb4_Nonlin4NormalizeCex()

Abc_Cex_t * Llb4_Nonlin4NormalizeCex ( Aig_Man_t * pAigOrg,
Aig_Man_t * pAigRpm,
Abc_Cex_t * pCexRpm )

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

Synopsis [Translates a sequence of states into a counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 279 of file llb4Cex.c.

280{
281 Abc_Cex_t * pCexOrg;
282 Vec_Ptr_t * vStates;
283 // check parameters of the AIG
284 if ( Saig_ManRegNum(pAigOrg) != Saig_ManRegNum(pAigRpm) )
285 {
286 printf( "Llb4_Nonlin4NormalizeCex(): The number of flops in the original and reparametrized AIGs do not agree.\n" );
287 return NULL;
288 }
289/*
290 if ( Saig_ManRegNum(pAigRpm) != pCexRpm->nRegs )
291 {
292 printf( "Llb4_Nonlin4NormalizeCex(): The number of flops in the reparametrized AIG and in the CEX do not agree.\n" );
293 return NULL;
294 }
295*/
296 if ( Saig_ManPiNum(pAigRpm) != pCexRpm->nPis )
297 {
298 printf( "Llb4_Nonlin4NormalizeCex(): The number of PIs in the reparametrized AIG and in the CEX do not agree.\n" );
299 return NULL;
300 }
301 // get the sequence of states
302 vStates = Llb4_Nonlin4VerifyCex( pAigRpm, pCexRpm );
303 if ( vStates == NULL )
304 {
305 Abc_Print( 1, "Llb4_Nonlin4NormalizeCex(): The given CEX does not fail outputs of pAigRpm.\n" );
306 return NULL;
307 }
308 // derive updated counter-example
309 pCexOrg = Llb4_Nonlin4TransformCex( pAigOrg, vStates, pCexRpm->iPo, 0 );
310 Vec_PtrFree( vStates );
311 return pCexOrg;
312}
Llb4_Nonlin4VerifyCex
Vec_Ptr_t * Llb4_Nonlin4VerifyCex(Aig_Man_t *pAig, Abc_Cex_t *p)
Definition llb4Cex.c:206
Llb4_Nonlin4TransformCex
ABC_NAMESPACE_IMPL_START Abc_Cex_t * Llb4_Nonlin4TransformCex(Aig_Man_t *pAig, Vec_Ptr_t *vStates, int iCexPo, int fVerbose)
DECLARATIONS ///.
Definition llb4Cex.c:47
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition utilCex.h:39
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
Here is the call graph for this function:

◆ Llb4_Nonlin4TransformCex()

ABC_NAMESPACE_IMPL_START Abc_Cex_t * Llb4_Nonlin4TransformCex ( Aig_Man_t * pAig,
Vec_Ptr_t * vStates,
int iCexPo,
int fVerbose )

DECLARATIONS ///.

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

FileName [llb2Cex.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [BDD based reachability.]

Synopsis [Non-linear quantification scheduling.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

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

] FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Translates a sequence of states into a counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 47 of file llb4Cex.c.

48{
49 Abc_Cex_t * pCex;
50 Cnf_Dat_t * pCnf;
51 Vec_Int_t * vAssumps;
52 sat_solver * pSat;
53 Aig_Obj_t * pObj;
54 unsigned * pNext, * pThis;
55 int i, k, iBit, status, nRegs;//, clk = Abc_Clock();
56/*
57 Vec_PtrForEachEntry( unsigned *, vStates, pNext, i )
58 {
59 printf( "%4d : ", i );
60 Extra_PrintBinary( stdout, pNext, Aig_ManRegNum(pAig) );
61 printf( "\n" );
62 }
63*/
64 // derive SAT solver
65 nRegs = Aig_ManRegNum(pAig); pAig->nRegs = 0;
66 pCnf = Cnf_Derive( pAig, Aig_ManCoNum(pAig) );
67 pAig->nRegs = nRegs;
68// Cnf_DataTranformPolarity( pCnf, 0 );
69 // convert into SAT solver
70 pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
71 if ( pSat == NULL )
72 {
73 printf( "Llb4_Nonlin4TransformCex(): Counter-example generation has failed.\n" );
74 Cnf_DataFree( pCnf );
75 return NULL;
76 }
77 // simplify the problem
78 status = sat_solver_simplify(pSat);
79 if ( status == 0 )
80 {
81 printf( "Llb4_Nonlin4TransformCex(): SAT solver is invalid.\n" );
82 sat_solver_delete( pSat );
83 Cnf_DataFree( pCnf );
84 return NULL;
85 }
86 // start the counter-example
87 pCex = Abc_CexAlloc( Saig_ManRegNum(pAig), Saig_ManPiNum(pAig), Vec_PtrSize(vStates) );
88 pCex->iFrame = Vec_PtrSize(vStates)-1;
89 pCex->iPo = -1;
90
91 // solve each time frame
92 iBit = Saig_ManRegNum(pAig);
93 pThis = (unsigned *)Vec_PtrEntry( vStates, 0 );
94 vAssumps = Vec_IntAlloc( 2 * Aig_ManRegNum(pAig) );
95 Vec_PtrForEachEntryStart( unsigned *, vStates, pNext, i, 1 )
96 {
97 // create assumptions
98 Vec_IntClear( vAssumps );
99 Saig_ManForEachLo( pAig, pObj, k )
100 Vec_IntPush( vAssumps, toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], !Abc_InfoHasBit(pThis,k) ) );
101 Saig_ManForEachLi( pAig, pObj, k )
102 Vec_IntPush( vAssumps, toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], !Abc_InfoHasBit(pNext,k) ) );
103 // solve SAT problem
104 status = sat_solver_solve( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps),
105 (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
106 // if the problem is SAT, get the counterexample
107 if ( status != l_True )
108 {
109 printf( "Llb4_Nonlin4TransformCex(): There is no transition between state %d and %d.\n", i-1, i );
110 Vec_IntFree( vAssumps );
111 sat_solver_delete( pSat );
112 Cnf_DataFree( pCnf );
113 ABC_FREE( pCex );
114 return NULL;
115 }
116 // get the assignment of PIs
117 Saig_ManForEachPi( pAig, pObj, k )
118 if ( sat_solver_var_value(pSat, pCnf->pVarNums[Aig_ObjId(pObj)]) )
119 Abc_InfoSetBit( pCex->pData, iBit + k );
120 // update the counter
121 iBit += Saig_ManPiNum(pAig);
122 pThis = pNext;
123 }
124
125 // add the last frame when the property fails
126 Vec_IntClear( vAssumps );
127 if ( iCexPo >= 0 )
128 {
129 Saig_ManForEachPo( pAig, pObj, k )
130 if ( k == iCexPo )
131 Vec_IntPush( vAssumps, toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], 0 ) );
132 }
133 else
134 {
135 Saig_ManForEachPo( pAig, pObj, k )
136 Vec_IntPush( vAssumps, toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], 0 ) );
137 }
138
139 // add clause
140 status = sat_solver_addclause( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps) );
141 if ( status == 0 )
142 {
143 printf( "Llb4_Nonlin4TransformCex(): The SAT solver is unsat after adding last clause.\n" );
144 Vec_IntFree( vAssumps );
145 sat_solver_delete( pSat );
146 Cnf_DataFree( pCnf );
147 ABC_FREE( pCex );
148 return NULL;
149 }
150 // create assumptions
151 Vec_IntClear( vAssumps );
152 Saig_ManForEachLo( pAig, pObj, k )
153 Vec_IntPush( vAssumps, toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], !Abc_InfoHasBit(pThis,k) ) );
154 // solve the last frame
155 status = sat_solver_solve( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps),
156 (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
157 if ( status != l_True )
158 {
159 printf( "Llb4_Nonlin4TransformCex(): There is no last transition that makes the property fail.\n" );
160 Vec_IntFree( vAssumps );
161 sat_solver_delete( pSat );
162 Cnf_DataFree( pCnf );
163 ABC_FREE( pCex );
164 return NULL;
165 }
166 // get the assignment of PIs
167 Saig_ManForEachPi( pAig, pObj, k )
168 if ( sat_solver_var_value(pSat, pCnf->pVarNums[Aig_ObjId(pObj)]) )
169 Abc_InfoSetBit( pCex->pData, iBit + k );
170 iBit += Saig_ManPiNum(pAig);
171 assert( iBit == pCex->nBits );
172
173 // free the sat_solver
174 Vec_IntFree( vAssumps );
175 sat_solver_delete( pSat );
176 Cnf_DataFree( pCnf );
177
178 // verify counter-example
179 status = Saig_ManFindFailedPoCex( pAig, pCex );
180 if ( status >= 0 && status < Saig_ManPoNum(pAig) )
181 pCex->iPo = status;
182 else
183 {
184 printf( "Llb4_Nonlin4TransformCex(): Counter-example verification has FAILED.\n" );
185 ABC_FREE( pCex );
186 return NULL;
187 }
188 // report the results
189// if ( fVerbose )
190// Abc_PrintTime( 1, "SAT-based cex generation time", Abc_Clock() - clk );
191 return pCex;
192}
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
Aig_Obj_t
struct Aig_Obj_t_ Aig_Obj_t
Definition aig.h:51
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
l_True
#define l_True
Definition bmcBmcS.c:35
sat_solver_addclause
#define sat_solver_addclause
Definition cecSatG2.c:37
sat_solver
#define sat_solver
Definition cecSatG2.c:34
sat_solver_solve
#define sat_solver_solve
Definition cecSatG2.c:45
Cnf_Derive
Cnf_Dat_t * Cnf_Derive(Aig_Man_t *pAig, int nOutputs)
Definition cnfCore.c:165
Cnf_Dat_t
struct Cnf_Dat_t_ Cnf_Dat_t
Definition cnf.h:52
Cnf_DataFree
void Cnf_DataFree(Cnf_Dat_t *p)
Definition cnfMan.c:207
Cnf_DataWriteIntoSolver
void * Cnf_DataWriteIntoSolver(Cnf_Dat_t *p, int nFrames, int fInit)
Definition cnfMan.c:579
Saig_ManForEachLi
#define Saig_ManForEachLi(p, pObj, i)
Definition saig.h:98
Saig_ManForEachPo
#define Saig_ManForEachPo(p, pObj, i)
Definition saig.h:93
Saig_ManFindFailedPoCex
int Saig_ManFindFailedPoCex(Aig_Man_t *pAig, Abc_Cex_t *p)
Definition saigDup.c:436
Saig_ManForEachLo
#define Saig_ManForEachLo(p, pObj, i)
Definition saig.h:96
Saig_ManForEachPi
#define Saig_ManForEachPi(p, pObj, i)
Definition saig.h:91
sat_solver_simplify
int sat_solver_simplify(sat_solver *s)
Definition satSolver.c:1515
sat_solver_delete
void sat_solver_delete(sat_solver *s)
Definition satSolver.c:1341
Cnf_Dat_t_::pVarNums
int * pVarNums
Definition cnf.h:63
Abc_CexAlloc
ABC_NAMESPACE_IMPL_START Abc_Cex_t * Abc_CexAlloc(int nRegs, int nRealPis, int nFrames)
DECLARATIONS ///.
Definition utilCex.c:51
assert
#define assert(ex)
Definition util_old.h:213
Vec_PtrForEachEntryStart
#define Vec_PtrForEachEntryStart(Type, vVec, pEntry, i, Start)
Definition vecPtr.h:57
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Llb4_Nonlin4VerifyCex()

Vec_Ptr_t * Llb4_Nonlin4VerifyCex ( Aig_Man_t * pAig,
Abc_Cex_t * p )

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

Synopsis [Resimulates the counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 206 of file llb4Cex.c.

207{
208 Vec_Ptr_t * vStates;
209 Aig_Obj_t * pObj, * pObjRi, * pObjRo;
210 int i, k, iBit = 0;
211 // create storage for states
212 vStates = Vec_PtrAllocSimInfo( p->iFrame+1, Abc_BitWordNum(Aig_ManRegNum(pAig)) );
213 Vec_PtrCleanSimInfo( vStates, 0, Abc_BitWordNum(Aig_ManRegNum(pAig)) );
214 // verify counter-example
215 Aig_ManCleanMarkB(pAig);
216 Aig_ManConst1(pAig)->fMarkB = 1;
217 Saig_ManForEachLo( pAig, pObj, i )
218 pObj->fMarkB = 0; //Abc_InfoHasBit(p->pData, iBit++);
219 // do not require equal flop count in the AIG and in the CEX
220 iBit = p->nRegs;
221 for ( i = 0; i <= p->iFrame; i++ )
222 {
223 // save current state
224 Saig_ManForEachLo( pAig, pObj, k )
225 if ( pObj->fMarkB )
226 Abc_InfoSetBit( (unsigned *)Vec_PtrEntry(vStates, i), k );
227 // compute new state
228 Saig_ManForEachPi( pAig, pObj, k )
229 pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
230 Aig_ManForEachNode( pAig, pObj, k )
231 pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) &
232 (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
233 Aig_ManForEachCo( pAig, pObj, k )
234 pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
235 if ( i == p->iFrame )
236 break;
237 Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k )
238 pObjRo->fMarkB = pObjRi->fMarkB;
239 }
240/*
241 {
242 unsigned * pNext;
243 Vec_PtrForEachEntry( unsigned *, vStates, pNext, i )
244 {
245 printf( "%4d : ", i );
246 Extra_PrintBinary( stdout, pNext, Aig_ManRegNum(pAig) );
247 printf( "\n" );
248 }
249 }
250*/
251 assert( iBit == p->nBits );
252// if ( Aig_ManCo(pAig, p->iPo)->fMarkB == 0 )
253// Vec_PtrFreeP( &vStates );
254 for ( i = Saig_ManPoNum(pAig) - 1; i >= 0; i-- )
255 {
256 if ( Aig_ManCo(pAig, i)->fMarkB )
257 {
258 p->iPo = i;
259 break;
260 }
261 }
262 if ( i == -1 )
263 Vec_PtrFreeP( &vStates );
264 Aig_ManCleanMarkB(pAig);
265 return vStates;
266}
Aig_ManCleanMarkB
void Aig_ManCleanMarkB(Aig_Man_t *p)
Definition aigUtil.c:167
Aig_ManForEachNode
#define Aig_ManForEachNode(p, pObj, i)
Definition aig.h:413
Aig_ManForEachCo
#define Aig_ManForEachCo(p, pObj, i)
Definition aig.h:398
p
Cube * p
Definition exorList.c:222
Saig_ManForEachLiLo
#define Saig_ManForEachLiLo(p, pObjLi, pObjLo, i)
Definition saig.h:101
Aig_Obj_t_::fMarkB
unsigned int fMarkB
Definition aig.h:80
Here is the call graph for this function:
Here is the caller graph for this function: