Context Navigation

bmcUtil.c

Last change on this file was 14, checked in by cecile, 13 years ago
vis2.3
File size: 100.8 KB

Line
1	/CFile*********************************************************************
2
3	FileName [bmcUtil.c]
4
5	PackageName [bmc]
6
7	Synopsis [Utilities for BMC package]
8
9	Author [Mohammad Awedh]
10
11	Copyright [This file was created at the University of Colorado at Boulder.
12	The University of Colorado at Boulder makes no warranty about the suitability
13	of this software for any purpose. It is presented on an AS IS basis.]
14
15	******************************************************************************/
16
17	#include "bmcInt.h"
18	#include "sat.h"
19	#include "baig.h"
20
21	static char rcsid[] UNUSED = "$Id: bmcUtil.c,v 1.82 2010/04/10 04:07:06 fabio Exp $";
22
23	/---------------------------------------------------------------------------/
24	/* Constant declarations */
25	/---------------------------------------------------------------------------/
26
27	#define MAX_LENGTH 320 /* Max. length of a string while reading a file */
28
29	/---------------------------------------------------------------------------/
30	/* Type declarations */
31	/---------------------------------------------------------------------------/
32
33
34	/---------------------------------------------------------------------------/
35	/* Structure declarations */
36	/---------------------------------------------------------------------------/
37
38
39	/---------------------------------------------------------------------------/
40	/* Variable declarations */
41	/---------------------------------------------------------------------------/
42
43
44	/AutomaticStart***********************************************************/
45
46	/---------------------------------------------------------------------------/
47	/* Static function prototypes */
48	/---------------------------------------------------------------------------/
49
50	static int StringCheckIsInteger(char string, int value);
51	static int nameCompare(const void * name1, const void * name2);
52	static void printValue(mAig_Manager_t manager, Ntk_Network_t network, st_table nodeToMvfAigTable, BmcCnfClauses_t cnfClauses, array_t varNames, st_table resultTable, int state, int *prevValue);
53	static void printValueAiger(mAig_Manager_t manager, Ntk_Network_t network, st_table nodeToMvfAigTable, BmcCnfClauses_t cnfClauses, array_t varNames, st_table resultTable, int state, int *prevValue);
54	static void printValueAigerInputs(mAig_Manager_t manager, Ntk_Network_t network, st_table nodeToMvfAigTable, BmcCnfClauses_t cnfClauses, array_t varNames, st_table resultTable, int state, int *prevValue);
55
56	/AutomaticEnd*************************************************************/
57
58	/---------------------------------------------------------------------------/
59	/* Definition of exported functions */
60	/---------------------------------------------------------------------------/
61
62
63	/Function******************************************************************
64
65	Synopsis [Compute cube that is close to target states.]
66
67	SideEffects []
68
69	******************************************************************************/
70	mdd_t *
71	Bmc_ComputeCloseCube(
72	mdd_t *states,
73	mdd_t *target,
74	int *dist,
75	Fsm_Fsm_t *modelFsm)
76	{
77	array_t *PSVars = Fsm_FsmReadPresentStateVars( modelFsm );
78	mdd_manager *mddMgr = Ntk_NetworkReadMddManager( Fsm_FsmReadNetwork( modelFsm ) );
79	mdd_t *result = BmcComputeCloseCube( states, target, dist, PSVars, mddMgr );
80
81	return result;
82	}
83
84	/Function******************************************************************
85
86	Synopsis [Build multi-valued function for a given node.]
87
88	SideEffects [The mvf of this node is a function of combinational input
89	nodes.]
90
91	******************************************************************************/
92	MvfAig_Function_t *
93	Bmc_NodeBuildMVF(
94	Ntk_Network_t *network,
95	Ntk_Node_t *node)
96	{
97	MvfAig_Function_t * MvfAig;
98	lsGen tmpGen;
99	Ntk_Node_t *tmpNode;
100	array_t *mvfArray;
101	array_t tmpRoots = array_alloc(Ntk_Node_t , 0);
102	st_table *tmpLeaves = st_init_table(st_ptrcmp, st_ptrhash);
103	array_insert_last(Ntk_Node_t *, tmpRoots, node);
104
105	Ntk_NetworkForEachCombInput(network, tmpGen, tmpNode) {
106	st_insert(tmpLeaves, (char ) tmpNode, (char ) ntmaig_UNUSED);
107	}
108
109	mvfArray = ntmaig_NetworkBuildMvfAigs(network, tmpRoots, tmpLeaves);
110	MvfAig = array_fetch(MvfAig_Function_t *, mvfArray, 0);
111	array_free(tmpRoots);
112	st_free_table(tmpLeaves);
113	array_free(mvfArray);
114	return MvfAig;
115	}
116
117
118	/Function******************************************************************
119
120	Synopsis [Returns MvfAig corresponding to a node; returns NIL if node not in
121	table.]
122
123	SideEffects [None]
124
125	******************************************************************************/
126	MvfAig_Function_t *
127	Bmc_ReadMvfAig(
128	Ntk_Node_t * node,
129	st_table * nodeToMvfAigTable)
130	{
131	MvfAig_Function_t *result;
132	if (st_lookup(nodeToMvfAigTable, node, &result)){
133	return result;
134	}
135	return NIL(MvfAig_Function_t);
136	}
137
138
139	/---------------------------------------------------------------------------/
140	/* Definition of internal functions */
141	/---------------------------------------------------------------------------/
142
143	/Function******************************************************************
144
145	Synopsis [Evaluate states satisfying X target]
146
147	Description [Evaluate states satisfying X target.]
148
149	SideEffects []
150
151	******************************************************************************/
152	mdd_t *
153	BmcFsmEvaluateX(
154	Fsm_Fsm_t *modelFsm,
155	mdd_t *targetMdd)
156	{
157	mdd_t *fromLowerBound;
158	mdd_t *fromUpperBound;
159	mdd_t *result;
160	Img_ImageInfo_t * imageInfo;
161	mdd_t *careStates;
162	array_t careStatesArray = array_alloc(array_t , 0);
163
164	imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 1, 0);
165
166	/*
167	* The lower bound is the conjunction of the fair states,
168	* and the target states.
169	*/
170	fromLowerBound = mdd_dup(targetMdd);
171	/*
172	* The upper bound is the same as the lower bound.
173	*/
174	fromUpperBound = mdd_dup(fromLowerBound);
175	/*
176	careSet is the set of all unreachabel states.
177	*/
178	careStates = mdd_one(Fsm_FsmReadMddManager(modelFsm));
179	array_insert(mdd_t *, careStatesArray, 0, careStates);
180
181	result = Img_ImageInfoComputePreImageWithDomainVars(imageInfo,
182	fromLowerBound, fromUpperBound, careStatesArray);
183	mdd_free(fromLowerBound);
184	mdd_free(fromUpperBound);
185
186	return result;
187
188	} /* BmcFsmEvaluateX */
189
190
191	/Function******************************************************************
192
193	Synopsis [Compute cube that is close to target states. Support
194	is an array of mddids representing the total support; that is, all
195	the variables on which aSet may depend. It dos the function only
196	if CUDD is the BDD package.]
197
198	SideEffects []
199
200	******************************************************************************/
201	mdd_t *
202	BmcComputeCloseCube(
203	mdd_t *aSet,
204	mdd_t *target,
205	int *dist,
206	array_t *Support,
207	mdd_manager *mddMgr)
208	{
209	if (bdd_get_package_name() == CUDD && target != NIL(mdd_t)) {
210	mdd_t range; / range of Support */
211	mdd_t legalSet; / aSet without the don't cares */
212	mdd_t *closeCube;
213
214
215	/* Check that support of set is contained in Support.
216	assert(SetCheckSupport(aSet, Support, mddMgr)); */
217	assert(!mdd_is_tautology(aSet, 0));
218	range = mdd_range_mdd(mddMgr, Support);
219	legalSet = bdd_and(aSet, range, 1, 1);
220	mdd_free(range);
221	closeCube = mdd_closest_cube(legalSet, target, dist);
222
223	mdd_free(legalSet);
224
225	return closeCube;
226	} else {
227	return aSet;
228	/return BMC_ComputeAMinterm(aSet, Support, mddMgr);/
229	}/* if CUDD */
230
231	} /* BmcComputeCloseCube */
232
233
234	/Function******************************************************************
235
236	Synopsis [Build AND/INV graph for intial states]
237
238	Description [Build AND/INV graph for intial states. Returns bAig Id
239	of the bAig Function that represents the intial states.
240
241	The initial states are computed as follows. For each latch i, the relation
242	(x_i = g_i(u)) is built, where x_i is the present state variable of latch i,
243	and g_i(u) is the multi-valued initialization function of latch i, in terms
244	of the input variables u. These relations are then conjuncted.
245	]
246
247	SideEffects []
248
249	SeeAlso []
250
251	******************************************************************************/
252	mAigEdge_t
253	BmcCreateMaigOfInitialStates(
254	Ntk_Network_t *network,
255	st_table *nodeToMvfAigTable,
256	st_table *CoiTable)
257	{
258	mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
259	st_generator *stGen;
260
261	Ntk_Node_t latch, latchInit;
262	MvfAig_Function_t initMvfAig, latchMvfAig;
263
264	bAigEdge_t resultAnd = bAig_One;
265	bAigEdge_t resultOr;
266	int i;
267
268	st_foreach_item(CoiTable, stGen, &latch, NULL) {
269
270
271	latchInit = Ntk_LatchReadInitialInput(latch);
272
273	/* Get the multi-valued function for each node*/
274	initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);
275	if (initMvfAig == NIL(MvfAig_Function_t)){
276	(void) fprintf(vis_stdout, "No multi-valued function for this node %s \n", Ntk_NodeReadName(latchInit));
277	return bAig_NULL;
278	}
279	latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
280	if (latchMvfAig == NIL(MvfAig_Function_t)){
281	latchMvfAig = Bmc_NodeBuildMVF(network, latch);
282	array_free(latchMvfAig);
283	latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
284	}
285	resultOr = bAig_Zero;
286	for(i=0; i<array_n(initMvfAig); i++){
287	resultOr = mAig_Or(manager, resultOr,
288	bAig_Eq(manager,
289	bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(initMvfAig, i)),
290	bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(latchMvfAig, i))
291	)
292	);
293	if(resultOr == bAig_One){
294	break;
295	}
296	}
297	resultAnd = mAig_And(manager, resultAnd, resultOr);
298	if(resultAnd == bAig_Zero){
299	break;
300	}
301	}/* for each latch*/
302
303	return resultAnd;
304	}
305
306
307	/Function******************************************************************
308
309	Synopsis [Builds AND/INVERTER graph (aig) for a propsitional formula]
310
311	Description [Builds AND/INVERTER graph for a propsitional formula.
312	Returns bAig ID of the function that is quivalent to the propositional
313	fomula]
314
315	SideEffects []
316
317	SeeAlso []
318
319	******************************************************************************/
320
321	mAigEdge_t
322	BmcCreateMaigOfPropFormula(
323	Ntk_Network_t *network,
324	mAig_Manager_t *manager,
325	Ctlsp_Formula_t *formula)
326	{
327	mAigEdge_t left, right, result;
328
329	if (formula == NIL(Ctlsp_Formula_t)) {
330	return mAig_NULL;
331	}
332	if (formula->type == Ctlsp_TRUE_c){
333	return mAig_One;
334	}
335	if (formula->type == Ctlsp_FALSE_c){
336	return mAig_Zero;
337	}
338
339	assert(Ctlsp_isPropositionalFormula(formula));
340
341	if (formula->type == Ctlsp_ID_c){
342	char *nodeNameString = Ctlsp_FormulaReadVariableName(formula);
343	char *nodeValueString = Ctlsp_FormulaReadValueName(formula);
344	Ntk_Node_t *node = Ntk_NetworkFindNodeByName(network, nodeNameString);
345
346	Var_Variable_t *nodeVar;
347	int nodeValue;
348
349	MvfAig_Function_t *tmpMvfAig;
350	st_table nodeToMvfAigTable; / maps each node to its mvfAig */
351
352	if (node == NIL(Ntk_Node_t)) {
353	(void) fprintf(vis_stderr, "bmc error: Could not find node corresponding to the name\t %s\n", nodeNameString);
354	return mAig_NULL;
355	}
356	nodeToMvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
357	if (nodeToMvfAigTable == NIL(st_table)){
358	(void) fprintf(vis_stderr, "bmc error: please run build_partiton_maigs first");
359	return mAig_NULL;
360	}
361	tmpMvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
362	if (tmpMvfAig == NIL(MvfAig_Function_t)){
363	tmpMvfAig = Bmc_NodeBuildMVF(network, node);
364	array_free(tmpMvfAig);
365	tmpMvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
366	}
367	nodeVar = Ntk_NodeReadVariable(node);
368	if (Var_VariableTestIsSymbolic(nodeVar)) {
369	nodeValue = Var_VariableReadIndexFromSymbolicValue(nodeVar, nodeValueString);
370	if ( nodeValue == -1 ) {
371	(void) fprintf(vis_stderr, "Value specified in RHS is not in domain of variable\n");
372	(void) fprintf(vis_stderr,"%s = %s\n", nodeNameString, nodeValueString);
373	return mAig_NULL;
374	}
375	}
376	else {
377	int check;
378	check = StringCheckIsInteger(nodeValueString, &nodeValue);
379	if( check == 0 ) {
380	(void) fprintf(vis_stderr,"Illegal value in the RHS\n");
381	(void) fprintf(vis_stderr,"%s = %s\n", nodeNameString, nodeValueString);
382	return mAig_NULL;
383	}
384	if( check == 1 ) {
385	(void) fprintf(vis_stderr,"Value in the RHS is out of range of int\n");
386	(void) fprintf(vis_stderr,"%s = %s", nodeNameString, nodeValueString);
387	return mAig_NULL;
388	}
389	if ( !(Var_VariableTestIsValueInRange(nodeVar, nodeValue))) {
390	(void) fprintf(vis_stderr,"Value specified in RHS is not in domain of variable\n");
391	(void) fprintf(vis_stderr,"%s = %s\n", nodeNameString, nodeValueString);
392	return mAig_NULL;
393
394	}
395	}
396	result = MvfAig_FunctionReadComponent(tmpMvfAig, nodeValue);
397	return bAig_GetCanonical(manager, result);
398	}
399	/*
400	right can be mAig_NULL for unery operators, but left can't be mAig_Null
401	*/
402	left = BmcCreateMaigOfPropFormula(network, manager, formula->left);
403	if (left == mAig_NULL){
404	return mAig_NULL;
405	}
406	right = BmcCreateMaigOfPropFormula(network, manager, formula->right);
407
408	switch(formula->type) {
409	case Ctlsp_NOT_c:
410	result = mAig_Not(left);
411	break;
412	case Ctlsp_OR_c:
413	result = mAig_Or(manager, left, right);
414	break;
415	case Ctlsp_AND_c:
416	result = mAig_And(manager, left, right);
417	break;
418	case Ctlsp_THEN_c:
419	result = mAig_Then(manager, left, right);
420	break;
421	case Ctlsp_EQ_c:
422	result = mAig_Eq(manager, left, right);
423	break;
424	case Ctlsp_XOR_c:
425	result = mAig_Xor(manager, left, right);
426	break;
427	default:
428	fail("Unexpected LTL type");
429	}
430	return result;
431	} /* BmcCreateMaigOfPropFormula */
432
433	/Function******************************************************************
434
435	Synopsis [Build MDD for safety property in form of AG(p). Where p is either a
436	propositional formula or a path formula contains only the temporal property X.]
437
438	Description [Build MDD for a safety formula. Returns NIL if the conversion
439	fails. The calling application is responsible for freeing the returned MDD.]
440
441	SideEffects []
442
443	SeeAlso [Ctlsp_FormulaReadClass]
444
445	******************************************************************************/
446	mdd_t *
447	BmcCreateMddOfSafetyProperty(
448	Fsm_Fsm_t *fsm,
449	Ctlsp_Formula_t *formula)
450	{
451
452	mdd_manager *manager = Ntk_NetworkReadMddManager(Fsm_FsmReadNetwork(fsm));
453	mdd_t left, right, *result;
454
455	if (formula == NIL(Ctlsp_Formula_t)) {
456	return NIL(mdd_t);
457	}
458	if (formula->type == Ctlsp_TRUE_c){
459	return bdd_one(manager);
460	}
461	if (formula->type == Ctlsp_FALSE_c){
462	return mdd_zero(manager);
463	}
464
465	#if 0
466	if (!Ctlsp_isPropositionalFormula(formula)) {
467	(void) fprintf(vis_stderr, "bmc error: Only propositional formula can be converted to bdd \n");
468	fprintf(vis_stdout, "\nFormula: ");
469	Ctlsp_FormulaPrint(vis_stdout, formula);
470	fprintf(vis_stdout, "\n");
471	return NIL(mdd_t);
472	}
473	#endif
474	/*
475	Atomic proposition.
476	*/
477	if (formula->type == Ctlsp_ID_c){
478	return BmcModelCheckAtomicFormula(fsm, formula);
479	}
480	/*
481	right can be NIL(mdd_t) for unery operators, but left can't be NIL(mdd_t)
482	*/
483	left = BmcCreateMddOfSafetyProperty(fsm, formula->left);
484	if (left == NIL(mdd_t)){
485	return NIL(mdd_t);
486	}
487	right = BmcCreateMddOfSafetyProperty(fsm, formula->right);
488	assert(right != NIL(mdd_t));
489	switch(formula->type) {
490	case Ctlsp_NOT_c:
491	result = mdd_not(left);
492	break;
493	case Ctlsp_OR_c:
494	result = mdd_or(left, right, 1, 1);
495	break;
496	case Ctlsp_AND_c:
497	result = mdd_and(left, right, 1, 1);
498	break;
499	case Ctlsp_THEN_c:
500	result = mdd_or(left, right, 0, 1);
501	break;
502	case Ctlsp_EQ_c:
503	result = mdd_xnor(left, right);
504	break;
505	case Ctlsp_XOR_c:
506	result = mdd_xor(left, right);
507	break;
508	case Ctlsp_X_c:
509	result = BmcFsmEvaluateX(fsm, left);
510	break;
511	default:
512	/*
513	return NIL(mdd_t) if the type is not supported
514	*/
515	return NIL(mdd_t);
516	/*
517	fail("Unexpected type");
518	*/
519	}
520	return result;
521	}
522
523
524	/Function******************************************************************
525
526	Synopsis [Generate the CNF formula of a given function represented by
527	AND/INVERTER graph]
528
529	Description [Generate an array of clausese for a function represented in
530	AND/INVERETER graph structure.
531
532	the CNF formula of node to the output file specifies by cnfFile.
533	It stores CNF index for each node in the cnfIndexTable. The generated CNF
534	is in dimacs format.
535	It is an error to call this function on a constand zero/one node.]
536
537	SideEffects []
538
539	SeeAlso []
540
541	******************************************************************************/
542	int
543	BmcGenerateCnfFormulaForAigFunction(
544	bAig_Manager_t *manager,
545	bAigEdge_t node,
546	int k,
547	BmcCnfClauses_t *cnfClauses)
548	{
549	int leftIndex, rightIndex, nodeIndex;
550	array_t *clause;
551
552	assert( (node != bAig_One) && (node != bAig_Zero));
553
554	if(bAig_IsInverted(node)){
555	/*
556	The generated clauses are in dimacs formate that uses negative number to indicate complement
557	*/
558	return -1*BmcGenerateCnfFormulaForAigFunction(manager, bAig_NonInvertedEdge(node), k, cnfClauses);
559	}
560	if (BmcCnfReadOrInsertNode(cnfClauses, bAig_NodeReadName(manager, node), k, &nodeIndex)){
561	return nodeIndex;
562	}
563	if (bAig_isVarNode(manager, node)){
564	return nodeIndex;
565	}
566	leftIndex = BmcGenerateCnfFormulaForAigFunction(manager,
567	bAig_GetCanonical(manager, leftChild(node)),
568	k, cnfClauses);
569	rightIndex = BmcGenerateCnfFormulaForAigFunction(manager,
570	bAig_GetCanonical(manager, rightChild(node)),
571	k, cnfClauses);
572	clause = array_alloc(int, 3);
573	array_insert(int, clause, 0, -leftIndex );
574	array_insert(int, clause, 1, -rightIndex);
575	array_insert(int, clause, 2, nodeIndex );
576	BmcCnfInsertClause(cnfClauses, clause);
577	array_free(clause);
578
579	clause = array_alloc(int, 2);
580	array_insert(int, clause, 0, leftIndex);
581	array_insert(int, clause, 1, -nodeIndex);
582	BmcCnfInsertClause(cnfClauses, clause);
583	array_free(clause);
584
585	clause = array_alloc(int, 2);
586	array_insert(int, clause, 0, rightIndex);
587	array_insert(int, clause, 1, -nodeIndex);
588	BmcCnfInsertClause(cnfClauses, clause);
589	array_free(clause);
590
591	return(nodeIndex);
592	}
593
594	/Function******************************************************************
595
596	Synopsis [Generate CNF for bdd function]
597
598	Description [
599	The function of each node f = varthenChild + -varelseChild
600	var is the variable at this node.
601	For each node there are four cases:
602	- both childeren are constant -> do nothing.
603	- the then child is constant 1 -> generate clauses for f = var + elseChild.
604	- the else child is constant 0 -> generate clauses for f = var * thenChild.
605	- the else child is constant 1 -> generate clauses for f = -var + thenChild.
606	- else -> generate clauses for f = varthenChild + -varelseChild.
607	------------------------------------------------
608	function \| clauses
609	------------------------------------------------
610	c = ab \| (-a + -b + c)(a + -c)*(b + -c)
611	c = a+b \| (a + b + -c)(-a + c)(-b + c)
612	f = ca + -cb \| (-a + -c + f)(a + -c + -f)
613	\| (-b + c + f)*(b + c + -f)
614
615	return the cnf index of the bdd function
616	]
617
618	SideEffects []
619
620	SeeAlso []
621
622	******************************************************************************/
623	int
624	BmcGenerateCnfFormulaForBdd(
625	bdd_t *bddFunction,
626	int k,
627	BmcCnfClauses_t *cnfClauses)
628	{
629	bdd_manager *bddManager = bdd_get_manager(bddFunction);
630	bdd_node node, thenNode, elseNode, funcNode;
631	int is_complemented;
632	int nodeIndex=0, thenIndex, elseIndex;
633	bdd_gen *gen;
634	int varIndex, flag;
635	array_t *tmpClause;
636
637	st_table *bddToCnfIndexTable;
638
639	bdd_t *currentBddNode;
640	int cut = 5;
641
642	if (bddFunction == NULL){
643	return 0;
644	}
645	funcNode = bdd_get_node(bddFunction, &is_complemented);
646	if (bdd_is_constant(funcNode)){
647	if (is_complemented){
648	/* add an empty clause to indicate FALSE (un-satisfiable)*/
649	BmcAddEmptyClause(cnfClauses);
650	}
651	return 0;
652	}
653	if(bdd_size(bddFunction) <= cut){
654	return BmcGenerateCnfFormulaForBddOffSet(bddFunction, k, cnfClauses);
655	}
656
657	bddToCnfIndexTable = st_init_table(st_numcmp, st_numhash);
658	foreach_bdd_node(bddFunction, gen, node){
659	if (bdd_is_constant(node)){ /* do nothing */
660	continue;
661	}
662
663	/*
664	bdd_size() returns 1 if bdd is constant one.
665	*/
666	/*
667	Use offset method to generate CNF if the size of the node <= cut (include the constant 1 node).
668	*/
669	/#if 0/
670	if(bdd_size(currentBddNode = bdd_construct_bdd_t(bddManager, bdd_regular(node))) <= cut){
671	if (bdd_size(currentBddNode) == cut){
672	nodeIndex = BmcGenerateCnfFormulaForBddOffSet(currentBddNode, k, cnfClauses);
673	st_insert(bddToCnfIndexTable, (char ) (long) bdd_regular(node), (char ) (long)nodeIndex);
674	continue;
675	}
676	continue;
677	}
678	/#endif/
679	varIndex = BmcGetCnfVarIndexForBddNode(bddManager, bdd_regular(node), k, cnfClauses);
680	nodeIndex = varIndex;
681
682	thenNode = bdd_bdd_T(node);
683	elseNode = bdd_bdd_E(node);
684
685	if (!((bdd_is_constant(thenNode)) && (bdd_is_constant(elseNode)))){
686	nodeIndex = cnfClauses->cnfGlobalIndex++; /* index of the function of this node */
687
688	if (bdd_is_constant(thenNode)){ /* the thenNode can be only constant one*/
689	flag = st_lookup_int(bddToCnfIndexTable, bdd_regular(elseNode), &elseIndex);
690	assert(flag);
691	/*
692	test if the elseNode is complemented arc?
693	*/
694	if (bdd_is_complement(elseNode)){
695	elseIndex = -1*elseIndex;
696	}
697	BmcCnfGenerateClausesForOR(elseIndex, varIndex, nodeIndex, cnfClauses);
698	} else if (bdd_is_constant(elseNode)){ /* one or zero */
699	flag = st_lookup_int(bddToCnfIndexTable, bdd_regular(thenNode), &thenIndex);
700	assert(flag);
701	/*
702	test if the elseNode is complemented arc?
703	*/
704	if (bdd_is_complement(elseNode)){ /* Constant zero */
705	BmcCnfGenerateClausesForAND(thenIndex, varIndex, nodeIndex, cnfClauses);
706	} else { /* Constant one */
707	BmcCnfGenerateClausesForOR(thenIndex, -varIndex, nodeIndex, cnfClauses);
708	}
709	} else {
710	flag = st_lookup_int(bddToCnfIndexTable, bdd_regular(thenNode), &thenIndex);
711	if(flag == 0){
712	thenIndex = BmcGenerateCnfFormulaForBddOffSet(bdd_construct_bdd_t(bddManager, bdd_regular(thenNode)), k, cnfClauses);
713	st_insert(bddToCnfIndexTable, (char ) (long) bdd_regular(thenNode), (char ) (long)thenIndex);
714	}
715	/assert(flag);/
716
717	flag = st_lookup_int(bddToCnfIndexTable, bdd_regular(elseNode), &elseIndex);
718	if(flag == 0){
719	elseIndex = BmcGenerateCnfFormulaForBddOffSet( bdd_construct_bdd_t(bddManager, bdd_regular(elseNode)), k, cnfClauses);
720	st_insert(bddToCnfIndexTable, (char ) (long) bdd_regular(elseNode), (char )(long) elseIndex);
721	}
722	/assert(flag);/
723	/*
724	test if the elseNode is complemented arc?
725	*/
726	if (bdd_is_complement(elseNode)){
727	elseIndex = -1*elseIndex;
728	}
729	tmpClause = array_alloc(int, 3);
730
731	assert(abs(thenIndex) <= cnfClauses->cnfGlobalIndex);
732	assert(abs(varIndex) <= cnfClauses->cnfGlobalIndex);
733	assert(abs(nodeIndex) <= cnfClauses->cnfGlobalIndex);
734
735	array_insert(int, tmpClause, 0, -thenIndex);
736	array_insert(int, tmpClause, 1, -varIndex);
737	array_insert(int, tmpClause, 2, nodeIndex);
738	BmcCnfInsertClause(cnfClauses, tmpClause);
739
740	array_insert(int, tmpClause, 0, thenIndex);
741	array_insert(int, tmpClause, 1, -varIndex);
742	array_insert(int, tmpClause, 2, -nodeIndex);
743	BmcCnfInsertClause(cnfClauses, tmpClause);
744
745	array_insert(int, tmpClause, 0, -elseIndex);
746	array_insert(int, tmpClause, 1, varIndex);
747	array_insert(int, tmpClause, 2, nodeIndex);
748	BmcCnfInsertClause(cnfClauses, tmpClause);
749
750	array_insert(int, tmpClause, 0, elseIndex);
751	array_insert(int, tmpClause, 1, varIndex);
752	array_insert(int, tmpClause, 2, -nodeIndex);
753	BmcCnfInsertClause(cnfClauses, tmpClause);
754
755	array_free(tmpClause);
756	}
757	}
758	st_insert(bddToCnfIndexTable, (char ) (long) bdd_regular(node), (char ) (long) nodeIndex);
759	} /* foreach_bdd_node() */
760	st_free_table(bddToCnfIndexTable);
761	return (is_complemented? -nodeIndex: nodeIndex);
762	} /* BmcGenerateCnfFormulaForBdd() */
763
764
765
766	/Function******************************************************************
767
768	Synopsis [Generate CNF for bdd function based on the off set of the
769	bdd function]
770
771	Description [Express the negation of bdd function in disjunctive
772	normal form(DNF), and generate a clause for each disjunct in the
773	DNF.]
774
775	SideEffects []
776
777	SeeAlso []
778
779	******************************************************************************/
780	int
781	BmcGenerateCnfFormulaForBddOffSet(
782	bdd_t *bddFunction,
783	int k,
784	BmcCnfClauses_t *cnfClauses)
785	{
786	bdd_manager *bddManager = bdd_get_manager(bddFunction);
787	bdd_node node, funcNode;
788	int is_complemented;
789	bdd_gen *gen;
790	int varIndex;
791	array_t *tmpClause;
792	array_t *cube;
793	int i, value;
794	bdd_t *newVar;
795
796	if (bddFunction == NULL){
797	return 0;
798	}
799	/*
800	Because the top node of bddFunction represents a variable in
801	bddFunction, newVar is used to represent the function of
802	bddFunction. Setting the cnfIndex of newVar to 1(0) is like
803	setting the function of bddFunction to 1(0).
804	*/
805	newVar = bdd_create_variable(bddManager);
806	bddFunction = bdd_xnor(newVar, bddFunction);
807	funcNode = bdd_get_node(bddFunction, &is_complemented);
808	if (bdd_is_constant(funcNode)){
809	if (is_complemented){
810	/* add an empty clause to indicate FALSE (un-satisfiable)*/
811	BmcAddEmptyClause(cnfClauses);
812	}
813	return 0;
814	}
815	bddFunction = bdd_not(bddFunction);
816
817	foreach_bdd_cube(bddFunction, gen, cube){
818	tmpClause = array_alloc(int,0);
819	arrayForEachItem(int, cube, i, value) {
820	if (value != 2){
821	node = bdd_bdd_ith_var(bddManager, i);
822	varIndex = BmcGetCnfVarIndexForBddNode(bddManager, bdd_regular(node), k, cnfClauses);
823	if (value == 1){
824	varIndex = -varIndex;
825	}
826	array_insert_last(int, tmpClause, varIndex);
827	}
828	}
829	BmcCnfInsertClause(cnfClauses, tmpClause);
830	array_free(tmpClause);
831	}/* foreach_bdd_cube() */
832	varIndex = BmcGetCnfVarIndexForBddNode(bddManager,
833	bdd_regular(bdd_get_node(newVar, &is_complemented)),
834	k, cnfClauses);
835	return (varIndex);
836	} /* BmcGenerateCnfFormulaForBddOffSet() */
837
838	#if 0
839	/Function******************************************************************
840
841	Synopsis [Generate the CNF formula of a given function represented by
842	AND/INVERTER graph]
843
844	Description [Generate an array of clausese for a function represented in
845	AND/INVERETER graph structure.
846
847	the CNF formula of node to the output file specifies by cnfFile.
848	It stores CNF index for each node in the cnfIndexTable. The generated CNF
849	is in dimacs format.
850	It is an error to call this function on a constand zero/one node.]
851
852	SideEffects []
853
854	SeeAlso []
855
856	******************************************************************************/
857	int
858	BmcGenerateCnfForAigFunction(
859	bAig_Manager_t *manager,
860	Ntk_Network_t *network,
861	bAigEdge_t node,
862	int k,
863	BmcCnfClauses_t *cnfClauses)
864	{
865	int leftIndex, rightIndex, nodeIndex;
866	array_t *clause;
867
868	if(bAig_IsInverted(node)){
869	/*
870	The generated clauses are in dimacs formate that uses negative number to indicate complement
871	*/
872	return -1*BmcGenerateCnfFormulaForAigFunction(manager, bAig_NonInvertedEdge(node), k, cnfClauses);
873	}
874	{
875	char *name = bAig_NodeReadName(manager, node);
876	char *found = strchr(name, '=');
877
878	if (found != NIL(char)){
879	int value = atoi(found+1);
880	int length = found-name;
881	char toName[length+1];
882	Ntk_Node_t *node;
883
884	toName[length] = '\0';
885	strncpy(toName, name, length);
886	node = Ntk_NetworkFindNodeByName(network, toName);
887	if ((node != NIL( Ntk_Node_t)) && Ntk_NodeTestIsLatch(node)){
888	MvfAig_Function_t *tmpMvfAig;
889	st_table nodeToMvfAigTable = (st_table ) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
890	bAigEdge_t mAigNode;
891
892	if (nodeToMvfAigTable == NIL(st_table)){
893	(void) fprintf(vis_stderr, "bmc error: please run build_partiton_maigs first");
894	return mAig_NULL;
895	}
896	if (k==0){
897	node = Ntk_LatchReadInitialInput(node);
898	} else {
899	node = Ntk_LatchReadDataInput(node);
900	k--;
901	}
902	tmpMvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
903	if (tmpMvfAig == NIL(MvfAig_Function_t)){
904	tmpMvfAig = Bmc_NodeBuildMVF(network, node);
905	array_free(tmpMvfAig);
906	tmpMvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
907	}
908	mAigNode = MvfAig_FunctionReadComponent(tmpMvfAig, value);
909	BmcGenerateCnfForAigFunction(manager, network, mAigNode, k, cnfClauses);
910	}
911	}
912	}
913	if (BmcCnfReadOrInsertNode(cnfClauses, bAig_NodeReadName(manager, node), k, &nodeIndex)){
914	return nodeIndex;
915	}
916	if (bAig_isVarNode(manager, node)){
917	return nodeIndex;
918	}
919	leftIndex = BmcGenerateCnfForAigFunction(manager, network, leftChild(node), k, cnfClauses);
920	rightIndex = BmcGenerateCnfForAigFunction(manager, network, rightChild(node), k, cnfClauses);
921
922	clause = array_alloc(int, 3);
923	array_insert(int, clause, 0, -leftIndex );
924	array_insert(int, clause, 1, -rightIndex);
925	array_insert(int, clause, 2, nodeIndex );
926	BmcCnfInsertClause(cnfClauses, clause);
927	array_free(clause);
928
929	clause = array_alloc(int, 2);
930	array_insert(int, clause, 0, leftIndex);
931	array_insert(int, clause, 1, -nodeIndex);
932	BmcCnfInsertClause(cnfClauses, clause);
933	array_free(clause);
934
935	clause = array_alloc(int, 2);
936	array_insert(int, clause, 0, rightIndex);
937	array_insert(int, clause, 1, -nodeIndex);
938	BmcCnfInsertClause(cnfClauses, clause);
939	array_free(clause);
940
941	return(nodeIndex);
942
943	}
944	#endif
945	/Function******************************************************************
946
947	Synopsis [
948	c = a <-> b = (a=0)(b=0) + (a=1)(b=1) ....
949	For a given term (a=i)*(b=i), if either is Zero, don't generate
950	clauses for this term.
951	if both are One, don't generate clauses
952	for c.
953	]
954
955	SideEffects []
956
957	******************************************************************************/
958	void
959	BmcGenerateClausesFromStateTostate(
960	bAig_Manager_t *manager,
961	bAigEdge_t *fromAigArray,
962	bAigEdge_t *toAigArray,
963	int mvfSize,
964	int fromState,
965	int toState,
966	BmcCnfClauses_t *cnfClauses,
967	int outIndex)
968	{
969	array_t clause, tmpclause;
970	int toIndex, fromIndex, cnfIndex;
971	int i;
972
973	/* used to turn off the warning messages: might be left uninitialized.
974	We are sure that these two variables will not be used uninitialized.
975	*/
976	toIndex =0;
977	fromIndex = 0;
978
979	for(i=0; i< mvfSize; i++){
980	if ((fromAigArray[i] == bAig_One) && (toAigArray[i] == bAig_One)){
981	return; /* the clause is always true */
982	}
983	}
984	clause = array_alloc(int, 0);
985	for(i=0; i< mvfSize; i++){
986	if ((fromAigArray[i] != bAig_Zero) && (toAigArray[i] != bAig_Zero)){
987	if (toAigArray[i] != bAig_One){
988	/* to State */
989
990	toIndex = BmcGenerateCnfFormulaForAigFunction(manager,toAigArray[i],
991	toState,cnfClauses);
992	}
993	if (fromAigArray[i] != bAig_One){
994	/* from State */
995	fromIndex = BmcGenerateCnfFormulaForAigFunction(manager,
996	fromAigArray[i],
997	fromState,
998	cnfClauses);
999	}
1000	/*
1001	Create new var for the output of this node. We don't create variable for this node, we only
1002	use its index number.
1003	*/
1004	cnfIndex = cnfClauses->cnfGlobalIndex++; /* index of the output of the OR of T(from, to) */
1005
1006	assert(abs(cnfIndex) <= cnfClauses->cnfGlobalIndex);
1007	assert(abs(fromIndex) <= cnfClauses->cnfGlobalIndex);
1008	assert(abs(toIndex) <= cnfClauses->cnfGlobalIndex);
1009
1010	if (toAigArray[i] == bAig_One){
1011	tmpclause = array_alloc(int, 2);
1012	array_insert(int, tmpclause, 0, -fromIndex);
1013	array_insert(int, tmpclause, 1, cnfIndex);
1014	BmcCnfInsertClause(cnfClauses, tmpclause);
1015	array_free(tmpclause);
1016
1017	tmpclause = array_alloc(int, 2);
1018	array_insert(int, tmpclause, 0, fromIndex);
1019	array_insert(int, tmpclause, 1, -cnfIndex);
1020	BmcCnfInsertClause(cnfClauses, tmpclause);
1021	array_free(tmpclause);
1022
1023	} else if (fromAigArray[i] == bAig_One){
1024	tmpclause = array_alloc(int, 2);
1025	array_insert(int, tmpclause, 0, -toIndex);
1026	array_insert(int, tmpclause, 1, cnfIndex);
1027	BmcCnfInsertClause(cnfClauses, tmpclause);
1028	array_free(tmpclause);
1029
1030	tmpclause = array_alloc(int, 2);
1031	array_insert(int, tmpclause, 0, toIndex);
1032	array_insert(int, tmpclause, 1, -cnfIndex);
1033	BmcCnfInsertClause(cnfClauses, tmpclause);
1034	array_free(tmpclause);
1035
1036	} else {
1037	tmpclause = array_alloc(int, 3);
1038	array_insert(int, tmpclause, 0, -toIndex);
1039	array_insert(int, tmpclause, 1, -fromIndex);
1040	array_insert(int, tmpclause, 2, cnfIndex);
1041	BmcCnfInsertClause(cnfClauses, tmpclause);
1042	array_free(tmpclause);
1043
1044	tmpclause = array_alloc(int, 2);
1045	array_insert(int, tmpclause, 0, toIndex);
1046	array_insert(int, tmpclause, 1, -cnfIndex);
1047	BmcCnfInsertClause(cnfClauses, tmpclause);
1048	array_free(tmpclause);
1049
1050	tmpclause = array_alloc(int, 2);
1051	array_insert(int, tmpclause, 0, fromIndex);
1052	array_insert(int, tmpclause, 1, -cnfIndex);
1053	BmcCnfInsertClause(cnfClauses, tmpclause);
1054	array_free(tmpclause);
1055	}
1056	array_insert_last(int, clause, cnfIndex);
1057	} /* if */
1058	} /* for i loop */
1059	if (outIndex != 0 ){
1060	array_insert_last(int, clause, -outIndex);
1061	}
1062	BmcCnfInsertClause(cnfClauses, clause);
1063	array_free(clause);
1064
1065	return;
1066	}
1067
1068	/Function******************************************************************
1069
1070	Synopsis [Write the set of clauses in diamacs format to the output file.]
1071
1072	SideEffects []
1073
1074	******************************************************************************/
1075	void
1076	BmcWriteClauses(
1077	mAig_Manager_t *maigManager,
1078	FILE *cnfFile,
1079	BmcCnfClauses_t *cnfClauses,
1080	BmcOption_t *options)
1081	{
1082	st_generator *stGen;
1083	char *name;
1084	int cnfIndex, i, k;
1085
1086	if (options->verbosityLevel == BmcVerbosityMax_c) {
1087	fprintf(vis_stdout,
1088	"Number of Variables = %d Number of Clauses = %d\n",
1089	cnfClauses->cnfGlobalIndex-1, cnfClauses->noOfClauses);
1090	}
1091	st_foreach_item_int(cnfClauses->cnfIndexTable, stGen, &name, &cnfIndex) {
1092	fprintf(cnfFile, "c %s %d\n",name, cnfIndex);
1093	}
1094	(void) fprintf(cnfFile, "p cnf %d %d\n", cnfClauses->cnfGlobalIndex-1,
1095	cnfClauses->noOfClauses);
1096	if (cnfClauses->clauseArray != NIL(array_t)) {
1097	for (i = 0; i < cnfClauses->nextIndex; i++) {
1098	k = array_fetch(int, cnfClauses->clauseArray, i);
1099	(void) fprintf(cnfFile, "%d%c", k, (k == 0) ? '\n' : ' ');
1100	}
1101	}
1102	return;
1103	}
1104
1105	/Function******************************************************************
1106
1107	Synopsis [Check the satisfiability of CNF formula written in file]
1108
1109	Description [Run SAT solver on input file]
1110
1111	SideEffects []
1112
1113	******************************************************************************/
1114	array_t *
1115	BmcCheckSAT(BmcOption_t *options)
1116	{
1117	array_t *result = NIL(array_t);
1118
1119
1120	if(options->satSolver == cusp){
1121	result = BmcCallCusp(options);
1122	}
1123	if(options->satSolver == CirCUs){
1124	result = BmcCallCirCUs(options);
1125	}
1126	/* Adjust alarm if timeout in effect. This is necessary because the
1127	* alarm may have gone off while the SAT solver is running. Since
1128	* the CPU time of a child process is charged to the parent only when
1129	* the child terminates, the SIGALRM handler assumes that more time
1130	* is left than it is in reality. We could do this adjustment right
1131	* after calling the SAT solver, but we prefer to give ourselves the
1132	* extra time to report the result even if this means using more time
1133	* than we are allotted.
1134	*/
1135	if (options->timeOutPeriod > 0) {
1136	int residualTime = options->timeOutPeriod -
1137	(util_cpu_ctime() - options->startTime) / 1000;
1138	/* Make sure we do not cancel the alarm if no time is left. */
1139	if (residualTime <= 0) {
1140	residualTime = 1;
1141	}
1142	(void) alarm(residualTime);
1143	}
1144
1145	return result;
1146	}
1147
1148	/Function******************************************************************
1149
1150	Synopsis [Check the satisfiability of CNF formula written in file]
1151
1152	Description [Run CirCUs on input file]
1153
1154	SideEffects []
1155
1156	******************************************************************************/
1157	array_t *
1158	BmcCallCirCUs(
1159	BmcOption_t *options)
1160	{
1161	satOption_t *satOption;
1162	array_t *result = NIL(array_t);
1163	satManager_t *cm;
1164	int maxSize;
1165
1166	satOption = sat_InitOption();
1167	satOption->verbose = options->verbosityLevel;
1168	satOption->verbose = 0;
1169
1170	cm = sat_InitManager(0);
1171	cm->comment = ALLOC(char, 2);
1172	cm->comment[0] = ' ';
1173	cm->comment[1] = '\0';
1174	cm->stdOut = stdout;
1175	cm->stdErr = stderr;
1176
1177	cm->option = satOption;
1178	cm->each = sat_InitStatistics();
1179
1180	cm->unitLits = sat_ArrayAlloc(16);
1181	cm->pureLits = sat_ArrayAlloc(16);
1182
1183	maxSize = 10000 << (bAigNodeSize-4);
1184	cm->nodesArray = ALLOC(bAigEdge_t, maxSize);
1185	cm->maxNodesArraySize = maxSize;
1186	cm->nodesArraySize = bAigNodeSize;
1187
1188	sat_AllocLiteralsDB(cm);
1189
1190	sat_ReadCNF(cm, options->satInFile);
1191
1192	if (options->verbosityLevel == BmcVerbosityMax_c) {
1193	(void)fprintf(vis_stdout,"Calling SAT solver (CirCUs) ...");
1194	(void) fflush(vis_stdout);
1195	}
1196	sat_Main(cm);
1197	if (options->verbosityLevel == BmcVerbosityMax_c) {
1198	(void) fprintf(vis_stdout," done ");
1199	(void) fprintf(vis_stdout, "(%g s)\n", cm->each->satTime);
1200	}
1201	if(cm->status == SAT_UNSAT) {
1202	if (options->verbosityLevel != BmcVerbosityNone_c){
1203	(void) fprintf(vis_stdout, "# SAT: Counterexample not found\n");
1204
1205	}
1206	fflush(cm->stdOut);
1207	} else if(cm->status == SAT_SAT) {
1208	if (options->verbosityLevel != BmcVerbosityNone_c){
1209	(void) fprintf(vis_stdout, "# SAT: Counterexample found\n");
1210	}
1211	if (options->verbosityLevel == BmcVerbosityMax_c){
1212	sat_ReportStatistics(cm, cm->each);
1213	}
1214	fflush(cm->stdOut);
1215	result = array_alloc(int, 0);
1216	{
1217	int i, size, value;
1218
1219	size = cm->initNumVariables * bAigNodeSize;
1220	for(i=bAigNodeSize; i<=size; i+=bAigNodeSize) {
1221	value = SATvalue(i);
1222	if(value == 1) {
1223	array_insert_last(int, result, SATnodeID(i));
1224	}
1225	else if(value == 0) {
1226	array_insert_last(int, result, -(SATnodeID(i)));
1227	}
1228	}
1229	}
1230	}
1231	//Bing: To avoid SEVERE memory leakage
1232	FREE(cm->nodesArray);
1233
1234	sat_FreeManager(cm);
1235
1236	return result;
1237	} /* BmcCallCirCUs */
1238
1239	/Function******************************************************************
1240
1241	Synopsis [Check the satisfiability of CNF formula written in file]
1242
1243	Description [Run external solver on input file]
1244
1245	SideEffects []
1246
1247	******************************************************************************/
1248	array_t *
1249	BmcCallCusp(BmcOption_t *options)
1250	{
1251	FILE *fp;
1252	static char parseBuffer[1024];
1253	int satStatus;
1254	char line[MAX_LENGTH];
1255	int num = 0;
1256	array_t *result = NIL(array_t);
1257	char tmpStr, tmpStr1, *tmpStr2;
1258	long solverStart;
1259	int satTimeOutPeriod = 0;
1260
1261	strcpy(parseBuffer,"cusp -distill -velim -cnf ");
1262	options->satSolverError = FALSE; /* assume no error*/
1263	if (options->timeOutPeriod > 0) {
1264	/* Compute the residual CPU time and subtract a little time to
1265	give vis a chance to clean up before its own time out expires.
1266	*/
1267	satTimeOutPeriod = options->timeOutPeriod - 1 -
1268	(util_cpu_ctime() - options->startTime) / 1000;
1269	if (satTimeOutPeriod <= 0){ /* no time left to run SAT solver*/
1270	options->satSolverError=TRUE;
1271	return NIL(array_t);
1272	}
1273	tmpStr2 = util_inttostr(satTimeOutPeriod);
1274	tmpStr1 = util_strcat3(options->satInFile," -t ", tmpStr2);
1275	tmpStr = util_strcat3(tmpStr1, " >", options->satOutFile);
1276	FREE(tmpStr1);
1277	FREE(tmpStr2);
1278	} else {
1279	tmpStr = util_strcat3(options->satInFile, " >", options->satOutFile);
1280	}
1281	strcat(parseBuffer, tmpStr);
1282	FREE(tmpStr);
1283
1284	if (options->verbosityLevel == BmcVerbosityMax_c) {
1285	(void)fprintf(vis_stdout,"Calling SAT solver (cusp) ...");
1286	(void) fflush(vis_stdout);
1287	solverStart = util_cpu_ctime();
1288	} else { /* to remove uninitialized variables warning */
1289	solverStart = 0;
1290	}
1291	/* Call Sat Solver*/
1292	satStatus = system(parseBuffer);
1293	if (satStatus != 0){
1294	(void) fprintf(vis_stderr, "Can't run cusp. It may not be in your path. Status = %d\n", satStatus);
1295	options->satSolverError = TRUE;
1296	return NIL(array_t);
1297	}
1298
1299	if (options->verbosityLevel == BmcVerbosityMax_c) {
1300	(void) fprintf(vis_stdout," done ");
1301	(void) fprintf(vis_stdout, "(%g s)\n",
1302	(double) (util_cpu_ctime() - solverStart)/1000.0);
1303	}
1304	fp = Cmd_FileOpen(options->satOutFile, "r", NIL(char *), 0);
1305	if (fp == NIL(FILE)) {
1306	(void) fprintf(vis_stderr, "** bmc error: Cannot open the file %s\n",
1307	options->satOutFile);
1308	options->satSolverError = TRUE;
1309	return NIL(array_t);
1310	}
1311	/* Skip the lines until the result */
1312	while(1) {
1313	if (fgets(line, MAX_LENGTH - 1, fp) == NULL) break;
1314	if(strstr(line,"UNSATISFIABLE") \|\|
1315	strstr(line,"SATISFIABLE") \|\|
1316	strstr(line,"MEMOUT") \|\|
1317	strstr(line,"TIMEOUT"))
1318	break;
1319	}
1320
1321	if(strstr(line,"UNSATISFIABLE") != NIL(char)) {
1322	if (options->verbosityLevel != BmcVerbosityNone_c){
1323	(void) fprintf(vis_stdout, "# SAT: Counterexample not found\n");
1324
1325	}
1326	} else if(strstr(line,"SATISFIABLE") != NIL(char)) {
1327	if (options->verbosityLevel != BmcVerbosityNone_c){
1328	(void) fprintf(vis_stdout, "# SAT: Counterexample found\n");
1329	}
1330	/* Skip the initial v of the result line */
1331	result = array_alloc(int, 0);
1332	while (fgets(line, MAX_LENGTH - 1, fp) != NULL) {
1333	char *word;
1334	if (line[0] != 'v') {
1335	(void) fprintf(vis_stderr,
1336	"** bmc error: Cannot find assignment in file %s\n",
1337	options->satOutFile);
1338	options->satSolverError = TRUE;
1339	return NIL(array_t);
1340	}
1341	word = strtok(&(line[1])," \n");
1342	while (word != NIL(char)) {
1343	num = atoi(word);
1344	if (num == 0) break;
1345	array_insert_last(int, result, num);
1346	word = strtok(NIL(char)," \n");
1347	}
1348	if (num == 0) break;
1349	}
1350	} else if(strstr(line,"MEMOUT") != NIL(char)) {
1351	(void) fprintf(vis_stdout,"# SAT: SAT Solver Memory out\n");
1352	options->satSolverError = TRUE;
1353	} else if(strstr(line,"TIMEOUT") != NIL(char)) {
1354	(void) fprintf(vis_stdout,
1355	"# SAT: SAT Solver Time out occurred after %d seconds.\n",
1356	satTimeOutPeriod);
1357	options->satSolverError = TRUE;
1358	} else {
1359	(void) fprintf(vis_stdout, "# SAT: SAT Solver failed, try again\n");
1360	options->satSolverError = TRUE;
1361	}
1362	(void) fflush(vis_stdout);
1363	(void) fclose(fp);
1364
1365	return result;
1366	} /* BmcCallCusp */
1367
1368
1369	/Function******************************************************************
1370
1371	Synopsis [Print CounterExample.]
1372
1373	SideEffects [Print a counterexample that was returned from the SAT
1374	solver in term of an array of integer "result". The counterexample
1375	starts from state 0 and of lenght eqaual to "length". If loopClause
1376	is not empty, this function print a loopback from the last state to
1377	a state in loopClause that exist in "result".]
1378
1379	******************************************************************************/
1380	void
1381	BmcPrintCounterExample(
1382	Ntk_Network_t *network,
1383	st_table *nodeToMvfAigTable,
1384	BmcCnfClauses_t *cnfClauses,
1385	array_t *result,
1386	int length,
1387	st_table *CoiTable,
1388	BmcOption_t *options,
1389	array_t *loopClause)
1390	{
1391	mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
1392	lsGen gen;
1393	st_generator *stGen;
1394	Ntk_Node_t *node;
1395	int k;
1396	array_t *latches = array_alloc(int, 0);
1397	int *prevValueLatches;
1398	array_t *inputs = array_alloc(int, 0);
1399	int *prevValueInputs;
1400	int tmp;
1401	int loop;
1402	st_table *resultTable = st_init_table(st_numcmp, st_numhash);
1403
1404	/*
1405	Initialize resultTable from the result to speed up the search in the result array.
1406	*/
1407	for(k=0; k< array_n(result); k++){
1408	st_insert(resultTable, (char ) (long) array_fetch(int, result, k), (char ) 0);
1409	}
1410	/* sort latches by name */
1411	st_foreach_item(CoiTable, stGen, &node, NULL) {
1412	array_insert_last(char*, latches, Ntk_NodeReadName(node));
1413	}
1414	array_sort(latches, nameCompare);
1415	/*
1416	Use to store the last value of each latch. If the current value of a latch
1417	differs from its corresponding value in this array, we will print the new values.
1418	*/
1419	prevValueLatches = ALLOC(int, array_n(latches));
1420	prevValueInputs = 0;
1421	if(options->printInputs == TRUE){
1422	/* sort inputs by name */
1423	Ntk_NetworkForEachInput(network, gen, node){
1424	array_insert_last(char*, inputs, Ntk_NodeReadName(node));
1425	}
1426	array_sort(inputs, nameCompare);
1427	prevValueInputs = ALLOC(int, array_n(inputs));
1428	}
1429	loop = -1; /* no loop back */
1430	if(loopClause != NIL(array_t)){
1431	for(k=0; k < array_n(loopClause); k++){
1432	/* if (searchArray(result, array_fetch(int, loopClause, k)) > -1){ */
1433	if (st_lookup_int(resultTable, (char *)(long)array_fetch(int, loopClause, k), &tmp)){
1434	loop = k;
1435	break;
1436	}
1437	}
1438	}
1439	/*
1440	Ntk_NetworkForEachPrimaryOutput(network, gen, node){
1441	array_insert_last(char*, outputs, Ntk_NodeReadName(node));
1442	}
1443	array_sort(outputs, nameCompare);
1444	*/
1445	for (k=0; k<= length; k++){
1446	if (k == 0){
1447	(void) fprintf(vis_stdout, "\n--State %d:\n", k);
1448	} else {
1449	(void) fprintf(vis_stdout, "\n--Goes to state %d:\n", k);
1450	}
1451	/*
1452	Print the current values of the latches if they are different form their
1453	previous values.
1454	*/
1455	printValue(manager, network, nodeToMvfAigTable, cnfClauses,
1456	latches, resultTable, k, prevValueLatches);
1457	#if 0
1458	(void) fprintf(vis_stdout, "--Primary output:\n");
1459	printValue(manager, network, nodeToMvfAigTable, cnfClauses, outputs, result, k);
1460	#endif
1461	if((options->printInputs == TRUE) && (k !=0)) {
1462	(void) fprintf(vis_stdout, "--On input:\n");
1463	printValue(manager, network, nodeToMvfAigTable, cnfClauses,
1464	inputs, resultTable, k-1, prevValueInputs);
1465	}
1466	} /* for k loop */
1467	if(loop != -1){
1468	(void) fprintf(vis_stdout, "\n--Goes back to state %d:\n", loop);
1469	printValue(manager, network, nodeToMvfAigTable, cnfClauses,
1470	latches, resultTable, loop, prevValueLatches);
1471	if((options->printInputs == TRUE)) {
1472	(void) fprintf(vis_stdout, "--On input:\n");
1473	printValue(manager, network, nodeToMvfAigTable, cnfClauses,
1474	inputs, resultTable, length, prevValueInputs);
1475	}
1476	}
1477	array_free(latches);
1478	FREE(prevValueLatches);
1479	if(options->printInputs == TRUE){
1480	array_free(inputs);
1481	FREE(prevValueInputs);
1482	}
1483	st_free_table(resultTable);
1484	return;
1485	} /* BmcPrintCounterExample() */
1486
1487	/Function******************************************************************
1488
1489	Synopsis [Print CounterExample in Aiger format.]
1490
1491	SideEffects [Print a counterexample that was returned from the SAT
1492	solver in term of an array of integer "result". The counterexample
1493	starts from state 0 and of lenght eqaual to "length". If loopClause
1494	is not empty, this function print a loopback from the last state to
1495	a state in loopClause that exist in "result".]
1496
1497	******************************************************************************/
1498	void
1499	BmcPrintCounterExampleAiger(
1500	Ntk_Network_t *network,
1501	st_table *nodeToMvfAigTable,
1502	BmcCnfClauses_t *cnfClauses,
1503	array_t *result,
1504	int length,
1505	st_table *CoiTable,
1506	BmcOption_t *options,
1507	array_t *loopClause)
1508	{
1509	mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
1510	lsGen gen;
1511	st_generator *stGen;
1512	Ntk_Node_t *node;
1513	int k;
1514	array_t *latches = array_alloc(int, 0);
1515	int *prevValueLatches;
1516	array_t *inputs = array_alloc(int, 0);
1517	array_t *outputs = array_alloc(int, 0);
1518	int *prevValueInputs;
1519	int *prevValueOutputs;
1520	int tmp;
1521	int loop;
1522	st_table *resultTable = st_init_table(st_numcmp, st_numhash);
1523	char *nodeName;
1524
1525	/*
1526	Initialize resultTable from the result to speed up the search in the result array.
1527	*/
1528	for(k=0; k< array_n(result); k++){
1529	st_insert(resultTable, (char ) (long) array_fetch(int, result, k), (char ) 0);
1530	}
1531	/* sort latches by name */
1532	st_foreach_item(CoiTable, stGen, &node, NULL) {
1533	array_insert_last(char*, latches, Ntk_NodeReadName(node));
1534	}
1535	/*
1536	Use to store the last value of each latch. If the current value of a latch
1537	differs from its corresponding value in this array, we will print the new values.
1538	*/
1539
1540	/* the file generation needs to be removed for final vis release */
1541
1542	FILE order = Cmd_FileOpen("inputOrder.txt", "w", NIL(char ), 0);
1543	for (k=0; k< array_n(latches); k++)
1544	{
1545	nodeName = array_fetch(char *, latches, k);
1546	if((nodeName[0] == '$') && (nodeName[1] == '_'))
1547	{
1548	fprintf(order, "%s\n", &nodeName[2]);
1549	}
1550	}
1551	fclose(order);
1552
1553	prevValueLatches = ALLOC(int, array_n(latches));
1554	Ntk_NetworkForEachInput(network, gen, node){
1555	array_insert_last(char*, inputs, Ntk_NodeReadName(node));
1556	}
1557
1558	prevValueInputs = ALLOC(int, array_n(inputs));
1559	loop = -1; /* no loop back */
1560	if(loopClause != NIL(array_t)){
1561	for(k=0; k < array_n(loopClause); k++){
1562	/* if (searchArray(result, array_fetch(int, loopClause, k)) > -1){ */
1563	if (st_lookup_int(resultTable, (char *)(long)array_fetch(int, loopClause, k), &tmp)){
1564	loop = k;
1565	break;
1566	}
1567	}
1568	}
1569
1570	Ntk_NetworkForEachPrimaryOutput(network, gen, node){
1571	array_insert_last(char*, outputs, Ntk_NodeReadName(node));
1572	}
1573	prevValueOutputs = ALLOC(int, array_n(outputs));
1574
1575	for (k=0; k< length; k++){
1576	/* This will print latches whose name doesn't start with $_. The latches whose
1577	name starts with $_ are latches added to the model by the aigtoblif translator.
1578	*/
1579	printValueAiger(manager, network, nodeToMvfAigTable, cnfClauses,
1580	latches, resultTable, k, prevValueLatches);
1581	fprintf(vis_stdout, " ");
1582	#if 0
1583	(void) fprintf(vis_stdout, "--Primary output:\n");
1584	printValue(manager, network, nodeToMvfAigTable, cnfClauses, outputs, result, k);
1585	#endif
1586
1587	if((loop<0)\|\|(k<length))
1588	{
1589
1590	/* we augment the original .mv model with latches in front of inputs and hence
1591	instead of inputs we print out the value of latches, this would have to be
1592	restored in the final release */
1593
1594	printValueAigerInputs(manager, network, nodeToMvfAigTable, cnfClauses,
1595	latches, resultTable, k, prevValueInputs);
1596	fprintf(vis_stdout, " ");
1597
1598	/* the sat-solver doesn't propagate the values to output so we generate the output
1599	1 knowing when ouptut would be 1, we will have to remove this for vis release */
1600
1601	if((k+1)==length)
1602	{
1603	fprintf(vis_stdout, "1 ");
1604	}
1605	else
1606	{
1607	fprintf(vis_stdout, "0 ");
1608	}
1609
1610	printValueAiger(manager, network, nodeToMvfAigTable, cnfClauses,
1611	latches, resultTable, k+1, prevValueLatches);
1612	}
1613	if((loop < 0)\|\|(k!=length))
1614	{
1615	fprintf(vis_stdout, "\n");
1616	}
1617
1618	} /* for k loop */
1619	if(loop != -1){
1620	(void) fprintf(vis_stdout, "\n--Goes back to state %d:\n", loop);
1621	printValueAiger(manager, network, nodeToMvfAigTable, cnfClauses,
1622	latches, resultTable, loop, prevValueLatches);
1623	(void) fprintf(vis_stdout, "--On input:\n");
1624	printValueAiger(manager, network, nodeToMvfAigTable, cnfClauses,
1625	inputs, resultTable, length, prevValueInputs);
1626	}
1627	array_free(latches);
1628	FREE(prevValueLatches);
1629	if(options->printInputs == TRUE){
1630	array_free(inputs);
1631	FREE(prevValueInputs);
1632	}
1633	st_free_table(resultTable);
1634	return;
1635	} /* BmcPrintCounterExampleAiger() */
1636
1637
1638	/Function******************************************************************
1639
1640	Synopsis [Print CounterExample.]
1641
1642	SideEffects [Print a counterexample that was returned from the SAT
1643	solver in term of an array of integer "result". The counterexample
1644	starts from state 0 and of lenght eqaual to "length". If loopClause
1645	is not empty, this function print a loopback from the last state to
1646	a state in loopClause that exist in "result".]
1647
1648	******************************************************************************/
1649	void
1650	BmcAutPrintCounterExample(
1651	Ntk_Network_t *network,
1652	Ltl_Automaton_t *automaton,
1653	st_table *nodeToMvfAigTable,
1654	BmcCnfClauses_t *cnfClauses,
1655	array_t *result,
1656	int length,
1657	st_table *CoiTable,
1658	BmcOption_t *options,
1659	array_t *loopClause)
1660	{
1661	mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
1662	lsGen gen;
1663	st_generator *stGen;
1664	Ntk_Node_t *node;
1665	int k;
1666	array_t *latches = array_alloc(int, 0);
1667	int *prevValueLatches;
1668	array_t *inputs = array_alloc(int, 0);
1669	int *prevValueInputs;
1670	int tmp;
1671	int loop;
1672	st_table *resultTable = st_init_table(st_numcmp, st_numhash);
1673
1674	/*
1675	Initialize resultTable from the result to speed up the search in the result array.
1676	*/
1677	for(k=0; k< array_n(result); k++){
1678	st_insert(resultTable, (char ) (long) array_fetch(int, result, k), (char ) 0);
1679	}
1680	/* sort latches by name */
1681	st_foreach_item(CoiTable, stGen, &node, NULL) {
1682	array_insert_last(char*, latches, Ntk_NodeReadName(node));
1683	}
1684	array_sort(latches, nameCompare);
1685	/*
1686	Use to store the last value of each latch. If the current value of a latch
1687	differs from its corresponding value in this array, we will print the new values.
1688	*/
1689	prevValueLatches = ALLOC(int, array_n(latches));
1690	prevValueInputs = 0;
1691	if(options->printInputs == TRUE){
1692	/* sort inputs by name */
1693	Ntk_NetworkForEachInput(network, gen, node){
1694	array_insert_last(char*, inputs, Ntk_NodeReadName(node));
1695	}
1696	array_sort(inputs, nameCompare);
1697	prevValueInputs = ALLOC(int, array_n(inputs));
1698	}
1699	loop = -1; /* no loop back */
1700	if(loopClause != NIL(array_t)){
1701	for(k=0; k < array_n(loopClause); k++){
1702	/* if (searchArray(result, array_fetch(int, loopClause, k)) > -1){ */
1703	if (st_lookup_int(resultTable, (char *)(long)array_fetch(int, loopClause, k), &tmp)){
1704	loop = k;
1705	break;
1706	}
1707	}
1708	}
1709	/*
1710	Ntk_NetworkForEachPrimaryOutput(network, gen, node){
1711	array_insert_last(char*, outputs, Ntk_NodeReadName(node));
1712	}
1713	array_sort(outputs, nameCompare);
1714	*/
1715	for (k=0; k<= length; k++){
1716	if (k == 0){
1717	(void) fprintf(vis_stdout, "\n--State %d:\n", k);
1718	} else {
1719	(void) fprintf(vis_stdout, "\n--Goes to state %d:\n", k);
1720	}
1721	/*
1722	Print the current values of the latches if they are different form their
1723	previous values.
1724	*/
1725	printValue(manager, network, nodeToMvfAigTable, cnfClauses,
1726	latches, resultTable, k, prevValueLatches);
1727
1728	{
1729	lsGen lsGen;
1730	vertex_t *vtx;
1731	Ltl_AutomatonNode_t *state;
1732	int stateIndex;
1733	bdd_node *node;
1734	int is_complemented;
1735
1736
1737	foreach_vertex(automaton->G, lsGen, vtx) {
1738	state = (Ltl_AutomatonNode_t *) vtx->user_data;
1739
1740	node = bdd_get_node(state->Encode, &is_complemented);
1741
1742	stateIndex = state->cnfIndex[k];
1743
1744
1745
1746
1747	if (st_lookup_int(resultTable, (char *)(long)stateIndex, &tmp)){
1748	(void) fprintf(vis_stdout,"n%d \n", state->index);
1749	}
1750	}
1751	}
1752	#if 0
1753	(void) fprintf(vis_stdout, "--Primary output:\n");
1754	printValue(manager, network, nodeToMvfAigTable, cnfClauses, outputs, result, k);
1755	#endif
1756	if((options->printInputs == TRUE) && (k !=0)) {
1757	(void) fprintf(vis_stdout, "--On input:\n");
1758	printValue(manager, network, nodeToMvfAigTable, cnfClauses,
1759	inputs, resultTable, k-1, prevValueInputs);
1760	}
1761	} /* for k loop */
1762	if(loop != -1){
1763	(void) fprintf(vis_stdout, "\n--Goes back to state %d:\n", loop);
1764	printValue(manager, network, nodeToMvfAigTable, cnfClauses,
1765	latches, resultTable, loop, prevValueLatches);
1766	if((options->printInputs == TRUE)) {
1767	(void) fprintf(vis_stdout, "--On input:\n");
1768	printValue(manager, network, nodeToMvfAigTable, cnfClauses,
1769	inputs, resultTable, length, prevValueInputs);
1770	}
1771	}
1772	array_free(latches);
1773	FREE(prevValueLatches);
1774	if(options->printInputs == TRUE){
1775	array_free(inputs);
1776	FREE(prevValueInputs);
1777	}
1778	st_free_table(resultTable);
1779	return;
1780	} /* BmcPrintCounterExample() */
1781
1782
1783	/Function******************************************************************
1784
1785	Synopsis [Generate CNF formula for a path from state 'from' to state 'to']
1786
1787	Description [Unfold the transition relation 'k' states (k = to-from +1), and
1788	generate clauses for each state.
1789
1790	For a multi-valued latch of 4 vlaues. Two binary variables are used
1791	to rpresent X, x1 and x0. For this latch, there exist three multi-valued
1792	functions.
1793	One for the binary reoresentation of the variable. For example the
1794	second entry of the mvf = 1, iff ~x1 and x0.
1795	The second mfv is for the data input of the latch. If the And/Inv graph
1796	attached to an entry of this mvf equal to 1, X equal to the binary
1797	representation corresponding to this entry. For example, if the And/
1798	INV graph attached to the first entry =1, then X = ~x1 & ~x0.
1799	To generate the CNF to the transition relation, first generate CNF to
1800	next state varaible using mvf of the latch. Then, generate CNF for
1801	latch data input using current state variavles. Finaly, generate CNF
1802	for the AND of these two MVF. This for every entry of the MVF. Then
1803	OR the results.
1804	The third MVF is for the initial value of the latch. It is treat the
1805	same as the latch data input except if the initial value is constant.
1806
1807	The initialState value may be either BMC_INITIAL_STATES to generate the clause for the intial states.
1808	BMC_NO_INITIAL_STATES otherwise.
1809	]
1810
1811	SideEffects []
1812
1813	SeeAlso []
1814
1815	******************************************************************************/
1816	void
1817	BmcCnfGenerateClausesForPath(
1818	Ntk_Network_t *network,
1819	int from,
1820	int to,
1821	int initialState,
1822	BmcCnfClauses_t *cnfClauses,
1823	st_table *nodeToMvfAigTable,
1824	st_table *CoiTable)
1825	{
1826	mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
1827	st_generator *stGen;
1828
1829	Ntk_Node_t latch, latchData, *latchInit;
1830	MvfAig_Function_t initMvfAig, dataMvfAig, *latchMvfAig;
1831	bAigEdge_t initBAig, latchBAig, *dataBAig;
1832
1833	int i, k, mvfSize;
1834
1835	st_foreach_item(CoiTable, stGen, &latch, NULL) {
1836
1837
1838	latchInit = Ntk_LatchReadInitialInput(latch);
1839	latchData = Ntk_LatchReadDataInput(latch);
1840
1841	/* Get the multi-valued function for each node*/
1842	initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);
1843	if (initMvfAig == NIL(MvfAig_Function_t)){
1844	(void) fprintf(vis_stdout, "No multi-valued function for this node %s \n", Ntk_NodeReadName(latchInit));
1845	return;
1846	}
1847	dataMvfAig = Bmc_ReadMvfAig(latchData, nodeToMvfAigTable);
1848	if (dataMvfAig == NIL(MvfAig_Function_t)){
1849	(void) fprintf(vis_stdout, "No multi-valued function for this node %s \n", Ntk_NodeReadName(latchData));
1850	return;
1851	}
1852	latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
1853	if (latchMvfAig == NIL(MvfAig_Function_t)){
1854	latchMvfAig = Bmc_NodeBuildMVF(network, latch);
1855	array_free(latchMvfAig);
1856	latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
1857	}
1858
1859	mvfSize = array_n(initMvfAig);
1860	initBAig = ALLOC(bAigEdge_t, mvfSize);
1861	dataBAig = ALLOC(bAigEdge_t, mvfSize);
1862	latchBAig = ALLOC(bAigEdge_t, mvfSize);
1863
1864	for(i=0; i< mvfSize; i++){
1865	dataBAig[i] = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(dataMvfAig, i));
1866	latchBAig[i] = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(latchMvfAig, i));
1867	initBAig[i] = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(initMvfAig, i));
1868	}
1869	/*
1870	if (from == 0){
1871	*/
1872	if (initialState == BMC_INITIAL_STATES){
1873	/* Generate the CNF for the initial state of the latch */
1874	BmcGenerateClausesFromStateTostate(manager, initBAig, latchBAig, mvfSize, -1, 0, cnfClauses, 0);
1875	}
1876	/* Generate the CNF for the transition functions */
1877	for (k=from; k < to; k++){
1878	BmcGenerateClausesFromStateTostate(manager, dataBAig, latchBAig, mvfSize, k, k+1, cnfClauses, 0);
1879	} /* for k state loop */
1880
1881	FREE(initBAig);
1882	FREE(dataBAig);
1883	FREE(latchBAig);
1884	}/* For each latch loop*/
1885
1886	return;
1887	}
1888
1889	/Function******************************************************************
1890
1891	Synopsis [Generate CNF formula for a loop-free path]
1892
1893	Description [This function generates CNF formula for a loop-free path from
1894	state fromState to state toState. A loop free path is a path from a state S0
1895	to state Sn such that every state in the path is distinct. i.e for all states
1896	in the path Si != Sj for 0<= i < j <= n.
1897
1898	The initialState value may be either BMC_INITIAL_STATES to generate the clause
1899	for the intial states. BMC_NO_INITIAL_STATES otherwise.
1900	]
1901
1902	SideEffects []
1903
1904	SeeAlso []
1905
1906	******************************************************************************/
1907	void
1908	BmcCnfGenerateClausesForLoopFreePath(
1909	Ntk_Network_t *network,
1910	int fromState,
1911	int toState,
1912	int initialState,
1913	BmcCnfClauses_t *cnfClauses,
1914	st_table *nodeToMvfAigTable,
1915	st_table *CoiTable)
1916	{
1917	int state;
1918
1919	/*
1920	Generate clauses for a path from fromState to toState.
1921	*/
1922	BmcCnfGenerateClausesForPath(network, fromState, toState, initialState, cnfClauses, nodeToMvfAigTable, CoiTable);
1923
1924	/*
1925	Restrict the above path to be loop-free path.
1926	*/
1927	/*
1928	for(state=0; state< toState; state++){
1929	*/
1930	/*
1931	Don't include the last state because we know it is not equal any of the previous states.
1932	The property fails at this state, and true at all other states.
1933	*/
1934	/*
1935	for(state=1; state < toState; state++){
1936	*/
1937	for(state= fromState + 1; state <= toState; state++){
1938	BmcCnfGenerateClausesForNoLoopToAnyPreviouseStates(network, fromState, state, cnfClauses, nodeToMvfAigTable, CoiTable);
1939	}
1940
1941	return;
1942	}
1943
1944	/Function******************************************************************
1945
1946	Synopsis [Generate Clauses for no loop from last state to any of the
1947	previouse states]
1948
1949	Description [Generate Clauses for no loop from last state (toState) to
1950	any of the previous states starting from fromState. It generates the CNF
1951	clauses such that the last state of the path is not equal to any of the
1952	path previous states.
1953	]
1954
1955	SideEffects []
1956
1957	SeeAlso []
1958
1959	******************************************************************************/
1960	void
1961	BmcCnfGenerateClausesForNoLoopToAnyPreviouseStates(
1962	Ntk_Network_t *network,
1963	int fromState,
1964	int toState,
1965	BmcCnfClauses_t *cnfClauses,
1966	st_table *nodeToMvfAigTable,
1967	st_table *CoiTable)
1968	{
1969	mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
1970	st_generator *stGen;
1971
1972	Ntk_Node_t *latch;
1973	MvfAig_Function_t *latchMvfAig;
1974	bAigEdge_t *latchBAig;
1975	array_t *orClause;
1976	int lastIndex, prevIndex, andIndex1, andIndex2;
1977	int i, k, mvfSize;
1978
1979	/*
1980	Generates the clauses to check if the toState is not equal to any previouse states starting
1981	from fromState.
1982
1983	Assume there are two state varaibles a and b. To check if Si != Sj, we must generate clauses
1984	for the formula ( ai != aj + bi != bj).
1985	*/
1986	for(k=fromState; k < toState; k++){
1987	orClause = array_alloc(int,0);
1988	st_foreach_item(CoiTable, stGen, &latch, NULL) {
1989
1990
1991	latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
1992	if (latchMvfAig == NIL(MvfAig_Function_t)){
1993	latchMvfAig = Bmc_NodeBuildMVF(network, latch);
1994	array_free(latchMvfAig);
1995	latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
1996	}
1997	mvfSize = array_n(latchMvfAig);
1998	latchBAig = ALLOC(bAigEdge_t, mvfSize);
1999
2000	for(i=0; i< mvfSize; i++){
2001	latchBAig[i] = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(latchMvfAig, i));
2002	}
2003
2004	for (i=0; i< mvfSize; i++){
2005	prevIndex = BmcGenerateCnfFormulaForAigFunction(manager, latchBAig[i], k ,cnfClauses);
2006	lastIndex = BmcGenerateCnfFormulaForAigFunction(manager, latchBAig[i], toState ,cnfClauses);
2007	andIndex1 = cnfClauses->cnfGlobalIndex++;
2008	BmcCnfGenerateClausesForAND(prevIndex, -lastIndex, andIndex1, cnfClauses);
2009	andIndex2 = cnfClauses->cnfGlobalIndex++;
2010	BmcCnfGenerateClausesForAND(-prevIndex, lastIndex, andIndex2, cnfClauses);
2011
2012	array_insert_last(int, orClause, andIndex1);
2013	array_insert_last(int, orClause, andIndex2);
2014	}
2015	FREE(latchBAig);
2016	}/* For each latch loop*/
2017	BmcCnfInsertClause(cnfClauses, orClause);
2018	array_free(orClause);
2019	} /* foreach k*/
2020	return;
2021	}
2022
2023
2024	/Function******************************************************************
2025
2026	Synopsis [Generate Clauses for last state equal to any of the
2027	previouse states]
2028
2029	Description [ Change it!
2030	Generate Clauses for no loop from last state (toState) to
2031	any of the previous states starting from fromState. It generates the CNF
2032	clauses such that the last state of the path is not equal to any of the
2033	path previous states.
2034	]
2035
2036	SideEffects []
2037
2038	SeeAlso []
2039
2040	******************************************************************************/
2041	void
2042	BmcCnfGenerateClausesForLoopToAnyPreviouseStates(
2043	Ntk_Network_t *network,
2044	int fromState,
2045	int toState,
2046	BmcCnfClauses_t *cnfClauses,
2047	st_table *nodeToMvfAigTable,
2048	st_table *CoiTable)
2049	{
2050	mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
2051	st_generator *stGen;
2052
2053	Ntk_Node_t *latch;
2054	MvfAig_Function_t *latchMvfAig;
2055	bAigEdge_t *latchBAig;
2056	array_t *orClause;
2057	int lastIndex, prevIndex, andIndex1, andIndex2;
2058	int i, k, mvfSize;
2059
2060	/*
2061	Generates the clauses to check if the toState is not equal to any previouse states starting
2062	from fromState.
2063
2064	Assume there are two state varaibles a and b. To check if Si != Sj, we must generate clauses
2065	for the formula ( ai != aj + bi != bj).
2066	*/
2067	for(k=fromState; k < toState; k++){
2068	orClause = array_alloc(int,0);
2069	st_foreach_item(CoiTable, stGen, &latch, NULL) {
2070
2071
2072	latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
2073	if (latchMvfAig == NIL(MvfAig_Function_t)){
2074	latchMvfAig = Bmc_NodeBuildMVF(network, latch);
2075	array_free(latchMvfAig);
2076	latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
2077	}
2078	mvfSize = array_n(latchMvfAig);
2079	latchBAig = ALLOC(bAigEdge_t, mvfSize);
2080
2081	for(i=0; i< mvfSize; i++){
2082	latchBAig[i] = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(latchMvfAig, i));
2083	}
2084
2085	for (i=0; i< mvfSize; i++){
2086	prevIndex = BmcGenerateCnfFormulaForAigFunction(manager, latchBAig[i], k ,cnfClauses);
2087	lastIndex = BmcGenerateCnfFormulaForAigFunction(manager, latchBAig[i], toState ,cnfClauses);
2088	andIndex1 = cnfClauses->cnfGlobalIndex++;
2089	BmcCnfGenerateClausesForAND(prevIndex, lastIndex, andIndex1, cnfClauses);
2090	andIndex2 = cnfClauses->cnfGlobalIndex++;
2091	BmcCnfGenerateClausesForAND(-prevIndex, -lastIndex, andIndex2, cnfClauses);
2092
2093	array_insert_last(int, orClause, andIndex1);
2094	array_insert_last(int, orClause, andIndex2);
2095	}
2096	FREE(latchBAig);
2097	}/* For each latch loop*/
2098	BmcCnfInsertClause(cnfClauses, orClause);
2099	array_free(orClause);
2100	} /* foreach k*/
2101	return;
2102	}
2103
2104	/Function******************************************************************
2105
2106	Synopsis [Generate CNF formula for a path from state 'from' to state 'to']
2107
2108	Description [Unfold the transition relation 'k' states (k = to-from +1), and
2109	generate clauses for each state.
2110	For a multi-valued latch of 4 vlaues. Two binary variables are used
2111	to rpresent X, x1 and x0. For this latch, there exist three multi-valued
2112	functions.
2113	One for the binary reoresentation of the variable. For example the
2114	second entry of the mvf = 1, iff ~x1 and x0.
2115	The second mfv is for the data input of the latch. If the And/Inv graph
2116	attached to an entry of this mvf equal to 1, X equal to the binary
2117	representation corresponding to this entry. For example, if the And/
2118	INV graph attached to the first entry =1, then X = ~x1 & ~x0.
2119	To generate the CNF to the transition relation, first generate CNF to
2120	next state varaible using mvf of the latch. Then, generate CNF for
2121	latch data input using current state variavles. Finaly, generate CNF
2122	for the AND of these two MVF. This for every entry of the MVF. Then
2123	OR the results.
2124	The third MVF is for the initial value of the latch. It is treat the
2125	same as the latch data input except if the initial value is constant.
2126	]
2127
2128	SideEffects []
2129
2130	SeeAlso []
2131
2132	******************************************************************************/
2133	void
2134	BmcCnfGenerateClausesFromStateToState(
2135	Ntk_Network_t *network,
2136	int from,
2137	int to,
2138	BmcCnfClauses_t *cnfClauses,
2139	st_table *nodeToMvfAigTable,
2140	st_table *CoiTable,
2141	int loop)
2142	{
2143	mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
2144	st_generator *stGen;
2145	Ntk_Node_t latch, latchData;
2146	MvfAig_Function_t dataMvfAig, latchMvfAig;
2147	bAigEdge_t latchBAig, dataBAig;
2148	int i, mvfSize;
2149
2150	st_foreach_item(CoiTable, stGen, &latch, NULL) {
2151	latchData = Ntk_LatchReadDataInput(latch);
2152
2153	dataMvfAig = Bmc_ReadMvfAig(latchData, nodeToMvfAigTable);
2154	if (dataMvfAig == NIL(MvfAig_Function_t)){
2155	(void) fprintf(vis_stdout,
2156	"No multi-valued function for this node %s \n",
2157	Ntk_NodeReadName(latchData));
2158	return;
2159	}
2160	latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
2161	if (latchMvfAig == NIL(MvfAig_Function_t)){
2162	latchMvfAig = Bmc_NodeBuildMVF(network, latch);
2163	}
2164	mvfSize = array_n(dataMvfAig);
2165	dataBAig = ALLOC(bAigEdge_t, mvfSize);
2166	latchBAig = ALLOC(bAigEdge_t, mvfSize);
2167	for(i=0; i< mvfSize; i++){
2168	dataBAig[i] = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(dataMvfAig, i));
2169	latchBAig[i] = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(latchMvfAig, i));
2170	}
2171	BmcGenerateClausesFromStateTostate(manager, dataBAig, latchBAig, mvfSize,
2172	from, to, cnfClauses, loop);
2173	FREE(dataBAig);
2174	FREE(latchBAig);
2175	} /* For each latch loop*/
2176	return;
2177	}
2178
2179	/Function******************************************************************
2180
2181	Synopsis [Generate CNF clauses for the AND gate]
2182
2183	Description []
2184
2185	SideEffects []
2186
2187	SeeAlso []
2188
2189	******************************************************************************/
2190	void
2191	BmcCnfGenerateClausesForAND(
2192	int a,
2193	int b,
2194	int c,
2195	BmcCnfClauses_t *cnfClauses)
2196	{
2197	array_t *tmpClause;
2198
2199	tmpClause = array_alloc(int, 3);
2200	array_insert(int, tmpClause, 0, -a);
2201	array_insert(int, tmpClause, 1, -b);
2202	array_insert(int, tmpClause, 2, c);
2203	BmcCnfInsertClause(cnfClauses, tmpClause);
2204	array_free(tmpClause);
2205
2206	tmpClause = array_alloc(int, 2);
2207
2208	array_insert(int, tmpClause, 0, a);
2209	array_insert(int, tmpClause, 1, -c);
2210	BmcCnfInsertClause(cnfClauses, tmpClause);
2211
2212	array_insert(int, tmpClause, 0, b);
2213	BmcCnfInsertClause(cnfClauses, tmpClause);
2214
2215	array_free(tmpClause);
2216	return;
2217	}
2218
2219	/Function******************************************************************
2220
2221	Synopsis [Generate CNF clauses for the OR gate]
2222
2223	Description []
2224
2225	SideEffects []
2226
2227	SeeAlso []
2228
2229	******************************************************************************/
2230	void
2231	BmcCnfGenerateClausesForOR(
2232	int a,
2233	int b,
2234	int c,
2235	BmcCnfClauses_t *cnfClauses)
2236	{
2237	array_t *tmpClause;
2238
2239	tmpClause = array_alloc(int, 3);
2240	array_insert(int, tmpClause, 0, a);
2241	array_insert(int, tmpClause, 1, b);
2242	array_insert(int, tmpClause, 2, -c);
2243	BmcCnfInsertClause(cnfClauses, tmpClause);
2244	array_free(tmpClause);
2245
2246	tmpClause = array_alloc(int, 2);
2247	array_insert(int, tmpClause, 0, -a);
2248	array_insert(int, tmpClause, 1, c);
2249	BmcCnfInsertClause(cnfClauses, tmpClause);
2250
2251	array_insert(int, tmpClause, 0, -b);
2252	BmcCnfInsertClause(cnfClauses, tmpClause);
2253
2254	array_free(tmpClause);
2255	return;
2256	}
2257
2258	/Function******************************************************************
2259
2260	Synopsis [Alloc Memory for BmcCnfClauses_t]
2261
2262	SideEffects []
2263
2264	SeeAlso []
2265	******************************************************************************/
2266	BmcCnfClauses_t *
2267	BmcCnfClausesAlloc(void)
2268	{
2269	BmcCnfClauses_t *result = ALLOC(BmcCnfClauses_t, 1);
2270
2271	if (!result){
2272	return result;
2273	}
2274	result->clauseArray = array_alloc(int, 0);
2275	result->cnfIndexTable = st_init_table(strcmp, st_strhash);
2276	result->freezedKeys = array_alloc(nameType_t *, 0);
2277
2278	result->nextIndex = 0;
2279	result->noOfClauses = 0;
2280	result->cnfGlobalIndex = 1;
2281	result->emptyClause = FALSE;
2282	result->freezed = FALSE;
2283
2284	return result;
2285	} /BmcCnfClausesAlloc()/
2286
2287	/Function******************************************************************
2288
2289	Synopsis [Free Memory for BmcCnfClauses_t]
2290
2291	SideEffects []
2292
2293	SeeAlso []
2294	******************************************************************************/
2295	void
2296	BmcCnfClausesFree(
2297	BmcCnfClauses_t *cnfClauses)
2298	{
2299	st_generator *stGen;
2300	char *name;
2301	int cnfIndex;
2302
2303	array_free(cnfClauses->clauseArray);
2304	array_free(cnfClauses->freezedKeys);
2305
2306	if (cnfClauses->cnfIndexTable != NIL(st_table)){
2307	st_foreach_item_int(cnfClauses->cnfIndexTable, stGen, (char **) &name, &cnfIndex) {
2308	FREE(name);
2309	}
2310	st_free_table(cnfClauses->cnfIndexTable);
2311	}
2312	FREE(cnfClauses);
2313	cnfClauses = NIL(BmcCnfClauses_t);
2314	} /* BmcCnfClausesFree() */
2315
2316	/Function******************************************************************
2317
2318	Synopsis [Freeze the current state of CNF]
2319
2320	Description [The current state of CNF is stored in the structure BmcCnfStates_t.
2321	This information may use later to store CNF to this state by calling
2322	BmcCnfClausesRestore().]
2323
2324	SideEffects []
2325
2326	SeeAlso [BmcCnfClausesRestore() BmcCnfClausesUnFreeze() ]
2327	******************************************************************************/
2328	BmcCnfStates_t *
2329	BmcCnfClausesFreeze(
2330	BmcCnfClauses_t * cnfClauses)
2331	{
2332	BmcCnfStates_t *state = ALLOC(BmcCnfStates_t, 1);
2333
2334	state->nextIndex = cnfClauses->nextIndex;
2335	state->noOfClauses = cnfClauses->noOfClauses;
2336	state->cnfGlobalIndex = cnfClauses->cnfGlobalIndex;
2337
2338	/* This variable is used when deleting any new entries in cnfClauses->freezedKeys
2339	that will be added after CNF is freezed.*/
2340	state->freezedKeySize = array_n(cnfClauses->freezedKeys);
2341
2342	state->emptyClause = cnfClauses->emptyClause;
2343	state->freezed = cnfClauses->freezed;
2344	cnfClauses->freezed = TRUE;
2345	return state;
2346	} /* mcCnfClausesFreeze() */
2347
2348	/Function******************************************************************
2349
2350	Synopsis [Unfreeze CNF]
2351
2352	Description [Keeps the current state of CNF]
2353
2354	SideEffects []
2355
2356	SeeAlso []
2357	******************************************************************************/
2358	void
2359	BmcCnfClausesUnFreeze(
2360	BmcCnfClauses_t *cnfClauses,
2361	BmcCnfStates_t *state)
2362	{
2363	int i;
2364
2365	cnfClauses->freezed = FALSE;
2366	if (array_n(cnfClauses->freezedKeys) != 0){
2367	int freezedKeySize = array_n(cnfClauses->freezedKeys);
2368
2369	for (i=0; i< (freezedKeySize-state->freezedKeySize); i++){
2370	(cnfClauses->freezedKeys)->num--;
2371	}
2372	}
2373	} /* BmcCnfClausesUnFreeze() */
2374
2375	/Function******************************************************************
2376
2377	Synopsis [Restore the CNF to its previouse state]
2378
2379	Description [Restore the CNF to its previouse state that CNF was when
2380	BmcCnfClausesFreeze() was last called]
2381
2382	SideEffects []
2383
2384	SeeAlso []
2385	******************************************************************************/
2386	void
2387	BmcCnfClausesRestore(
2388	BmcCnfClauses_t *cnfClauses,
2389	BmcCnfStates_t *state)
2390	{
2391	int i, index;
2392	nameType_t *key;
2393
2394	cnfClauses->nextIndex = state->nextIndex;
2395	cnfClauses->noOfClauses = state->noOfClauses;
2396	cnfClauses->cnfGlobalIndex = state->cnfGlobalIndex;
2397	cnfClauses->emptyClause = state->emptyClause;
2398	cnfClauses->freezed = state->freezed;
2399
2400	if (array_n(cnfClauses->freezedKeys) != 0){
2401	int freezedKeySize = array_n(cnfClauses->freezedKeys);
2402
2403	for (i=0; i< (freezedKeySize-state->freezedKeySize); i++){
2404	key = array_fetch_last(nameType_t *, cnfClauses->freezedKeys);
2405	if (st_delete_int(cnfClauses->cnfIndexTable, &key, &index)){
2406	FREE(key);
2407	}
2408	(cnfClauses->freezedKeys)->num--;
2409	}
2410	}
2411	} /* BmcCnfClausesRestore() */
2412
2413	/Function******************************************************************
2414
2415	Synopsis [Add clause to the clauseArray]
2416
2417	Description [Add a clause to the clause array. clause is of type array_t.
2418	The user must free clause.]
2419
2420	SideEffects []
2421
2422	SeeAlso []
2423	******************************************************************************/
2424	void
2425	BmcCnfInsertClause(
2426	BmcCnfClauses_t *cnfClauses,
2427	array_t *clause)
2428	{
2429	int i, lit;
2430
2431	if (clause != NIL(array_t)){
2432	if (array_n(clause) == 0){ /* empty clause */
2433	cnfClauses->emptyClause = TRUE;
2434	return;
2435	}
2436	for (i=0; i< array_n(clause); i++){
2437	lit = array_fetch(int, clause, i);
2438	array_insert(int, cnfClauses->clauseArray, cnfClauses->nextIndex++, lit);
2439	}
2440	array_insert(int, cnfClauses->clauseArray, cnfClauses->nextIndex++, 0); /End Of clause/
2441	cnfClauses->noOfClauses++;
2442	cnfClauses->emptyClause = FALSE;
2443	}
2444	return;
2445	}/* BmcCnfInsertClause() */
2446
2447	/Function******************************************************************
2448
2449	Synopsis [Add an empty clause]
2450
2451	SideEffects []
2452
2453	SeeAlso []
2454	******************************************************************************/
2455	void
2456	BmcAddEmptyClause(
2457	BmcCnfClauses_t *cnfClauses)
2458	{
2459	cnfClauses->emptyClause = TRUE;
2460	}/* BmcAddEmptyClause() */
2461
2462	/Function******************************************************************
2463
2464	Synopsis [Return the cnfIndex of the node]
2465
2466	Description [If CNF was generated for this node, return its cnfIndex, otherwise
2467	insert the name of this node in the cnfIndexTable, and return its cnfIndex. The
2468	key to the cnfIndexTable is (nodeName_state).]
2469
2470	SideEffects []
2471	******************************************************************************/
2472	int
2473	BmcCnfReadOrInsertNode(
2474	BmcCnfClauses_t *cnfClauses,
2475	nameType_t *nodeName,
2476	int state,
2477	int *nodeIndex)
2478	{
2479	nameType_t *varName;
2480	int index;
2481	char *stateStr = util_inttostr(state);
2482
2483	varName = util_strcat3(nodeName, "_", stateStr);
2484	FREE(stateStr);
2485	if (!st_lookup_int(cnfClauses->cnfIndexTable, varName, &index)) {
2486	index = cnfClauses->cnfGlobalIndex++;
2487	st_insert(cnfClauses->cnfIndexTable, varName, (char*) (long) index);
2488	if(cnfClauses->freezed == TRUE){
2489	array_insert_last(nameType_t *, cnfClauses->freezedKeys, varName);
2490	}
2491	*nodeIndex = index;
2492	return 0; /* Inserted */
2493	}
2494	else { /* The node has been visited */
2495	*nodeIndex = index;
2496	FREE(varName);
2497	return 1;
2498	}
2499	}
2500
2501
2502	/Function******************************************************************
2503
2504	Synopsis [Find the Cone of Influnce (COI) for an LTL formula]
2505
2506	Description [Return a list of state variables (latches) that are in the COI of the
2507	LTL formula.]
2508
2509	SideEffects []
2510
2511	******************************************************************************/
2512	void
2513	BmcGetCoiForLtlFormula(
2514	Ntk_Network_t *network,
2515	Ctlsp_Formula_t *formula,
2516	st_table *ltlCoiTable)
2517	{
2518	st_table *visited = st_init_table(st_ptrcmp, st_ptrhash);
2519
2520	BmcGetCoiForLtlFormulaRecursive(network, formula, ltlCoiTable, visited);
2521	st_free_table(visited);
2522	return;
2523	} /* BmcGetCoiForLtlFormula() */
2524
2525	/Function******************************************************************
2526
2527	Synopsis [Recursive function to find the COI of a network node.]
2528
2529	Description []
2530
2531	SideEffects []
2532
2533	******************************************************************************/
2534	void
2535	BmcGetCoiForLtlFormulaRecursive(
2536	Ntk_Network_t *network,
2537	Ctlsp_Formula_t *formula,
2538	st_table *ltlCoiTable,
2539	st_table *visited)
2540	{
2541	if (formula == NIL(Ctlsp_Formula_t)) {
2542	return;
2543	}
2544	/* leaf node */
2545	if (formula->type == Ctlsp_ID_c){
2546	char *name = Ctlsp_FormulaReadVariableName(formula);
2547	Ntk_Node_t *node = Ntk_NetworkFindNodeByName(network, name);
2548	int tmp;
2549
2550	if (st_lookup_int(visited, (char *) node, &tmp)){
2551	/* Node already visited */
2552	return;
2553	}
2554	BmcGetCoiForNtkNode(node, ltlCoiTable, visited);
2555	return;
2556	}
2557	BmcGetCoiForLtlFormulaRecursive(network, formula->left, ltlCoiTable, visited);
2558	BmcGetCoiForLtlFormulaRecursive(network, formula->right, ltlCoiTable, visited);
2559
2560	return;
2561	} /* BmcGetCoiForLtlFormulaRecursive() */
2562
2563	/Function******************************************************************
2564
2565	Synopsis [Genrate COI for a non-latch network node]
2566
2567	Description [For each fanins of the given node, if its latch, add it
2568	to the CoiTable and return. If it is not latch, call this function to
2569	look for any latches in the fanins of this node.]
2570
2571	SideEffects []
2572
2573	******************************************************************************/
2574	void
2575	BmcGetCoiForNtkNode(
2576	Ntk_Node_t *node,
2577	st_table *CoiTable,
2578	st_table *visited)
2579	{
2580	int i, j;
2581	Ntk_Node_t *faninNode;
2582
2583	if(node == NIL(Ntk_Node_t)){
2584	return;
2585	}
2586	if (st_lookup_int(visited, (char *) node, &j)){
2587	/* Node already visited */
2588	return;
2589	}
2590	st_insert(visited, (char ) node, (char ) 0);
2591	if (Ntk_NodeTestIsLatch(node)){
2592	st_insert(CoiTable, (char ) node, (char ) 0);
2593	}
2594	Ntk_NodeForEachFanin(node, i, faninNode) {
2595	BmcGetCoiForNtkNode(faninNode, CoiTable, visited);
2596	}
2597	return;
2598	} /* BmcGetCoiForNtkNode() */
2599
2600
2601	/Function******************************************************************
2602
2603	Synopsis [Find Mdd for states satisfying Atomic Formula.]
2604
2605	Description [An atomic formula defines a set of states in the following
2606	way: it states a designated ``net'' (specified by the full path name)
2607	takes a certain value. The net should be purely a function of latches;
2608	as a result an evaluation of the net yields a set of states.]
2609
2610	SideEffects []
2611
2612	******************************************************************************/
2613
2614	mdd_t *
2615	BmcModelCheckAtomicFormula(
2616	Fsm_Fsm_t *modelFsm,
2617	Ctlsp_Formula_t *ctlFormula)
2618	{
2619	mdd_t * resultMdd;
2620	mdd_t *tmpMdd;
2621	Ntk_Network_t *network = Fsm_FsmReadNetwork(modelFsm);
2622	char *nodeNameString = Ctlsp_FormulaReadVariableName(ctlFormula);
2623	char *nodeValueString = Ctlsp_FormulaReadValueName(ctlFormula);
2624	Ntk_Node_t *node = Ntk_NetworkFindNodeByName(network, nodeNameString);
2625
2626	Var_Variable_t *nodeVar;
2627	int nodeValue;
2628
2629	graph_t *modelPartition;
2630	vertex_t *partitionVertex;
2631	Mvf_Function_t *MVF;
2632
2633	nodeVar = Ntk_NodeReadVariable(node);
2634	if (Var_VariableTestIsSymbolic(nodeVar)) {
2635	nodeValue = Var_VariableReadIndexFromSymbolicValue(nodeVar, nodeValueString);
2636	}
2637	else {
2638	nodeValue = atoi(nodeValueString);
2639	}
2640
2641	modelPartition = Part_NetworkReadPartition(network);
2642	if (!(partitionVertex = Part_PartitionFindVertexByName(modelPartition,
2643	nodeNameString))) {
2644	lsGen tmpGen;
2645	Ntk_Node_t *tmpNode;
2646	array_t *mvfArray;
2647	array_t tmpRoots = array_alloc(Ntk_Node_t , 0);
2648	st_table *tmpLeaves = st_init_table(st_ptrcmp, st_ptrhash);
2649	array_insert_last(Ntk_Node_t *, tmpRoots, node);
2650
2651	Ntk_NetworkForEachCombInput(network, tmpGen, tmpNode) {
2652	st_insert(tmpLeaves, (char ) tmpNode, (char ) NTM_UNUSED);
2653	}
2654
2655	mvfArray = Ntm_NetworkBuildMvfs(network, tmpRoots, tmpLeaves,
2656	NIL(mdd_t));
2657	MVF = array_fetch(Mvf_Function_t *, mvfArray, 0);
2658	array_free(tmpRoots);
2659	st_free_table(tmpLeaves);
2660	array_free(mvfArray);
2661
2662	tmpMdd = Mvf_FunctionReadComponent(MVF, nodeValue);
2663	resultMdd = mdd_dup(tmpMdd);
2664	Mvf_FunctionFree(MVF);
2665	}
2666	else {
2667	MVF = Part_VertexReadFunction(partitionVertex);
2668	tmpMdd = Mvf_FunctionReadComponent(MVF, nodeValue);
2669	resultMdd = mdd_dup(tmpMdd);
2670	}
2671	if (Part_PartitionReadMethod(modelPartition) == Part_Frontier_c &&
2672	Ntk_NodeTestIsCombOutput(node)) {
2673	array_t *psVars = Fsm_FsmReadPresentStateVars(modelFsm);
2674	mdd_manager *mgr = Ntk_NetworkReadMddManager(Fsm_FsmReadNetwork(modelFsm));
2675	array_t *supportList;
2676	st_table *supportTable = st_init_table(st_numcmp, st_numhash);
2677	int i, j;
2678	int existIntermediateVars;
2679	int mddId;
2680	Mvf_Function_t *mvf;
2681	vertex_t *vertex;
2682	array_t varBddRelationArray, varArray;
2683	mdd_t iv, ivMdd, *relation;
2684
2685	for (i = 0; i < array_n(psVars); i++) {
2686	mddId = array_fetch(int, psVars, i);
2687	st_insert(supportTable, (char *)(long)mddId, NULL);
2688	}
2689
2690	existIntermediateVars = 1;
2691	while (existIntermediateVars) {
2692	existIntermediateVars = 0;
2693	supportList = mdd_get_support(mgr, resultMdd);
2694	for (i = 0; i < array_n(supportList); i++) {
2695	mddId = array_fetch(int, supportList, i);
2696	if (!st_lookup(supportTable, (char *)(long)mddId, NULL)) {
2697	vertex = Part_PartitionFindVertexByMddId(modelPartition, mddId);
2698	mvf = Part_VertexReadFunction(vertex);
2699	varBddRelationArray = mdd_fn_array_to_bdd_rel_array(mgr, mddId, mvf);
2700	varArray = mdd_id_to_bdd_array(mgr, mddId);
2701	assert(array_n(varBddRelationArray) == array_n(varArray));
2702	for (j = 0; j < array_n(varBddRelationArray); j++) {
2703	iv = array_fetch(mdd_t *, varArray, j);
2704	relation = array_fetch(mdd_t *, varBddRelationArray, j);
2705	ivMdd = bdd_cofactor(relation, iv);
2706	mdd_free(relation);
2707	tmpMdd = resultMdd;
2708	resultMdd = bdd_compose(resultMdd, iv, ivMdd);
2709	mdd_free(tmpMdd);
2710	mdd_free(iv);
2711	mdd_free(ivMdd);
2712	}
2713	array_free(varBddRelationArray);
2714	array_free(varArray);
2715	existIntermediateVars = 1;
2716	}
2717	}
2718	array_free(supportList);
2719	}
2720	st_free_table(supportTable);
2721	}
2722	return resultMdd;
2723	}
2724
2725	/Function******************************************************************
2726
2727	Synopsis [Read fairness constraints from file and check for errors.]
2728
2729	Description []
2730
2731	SideEffects []
2732
2733	SeeAlso []
2734
2735	******************************************************************************/
2736	array_t *
2737	BmcReadFairnessConstraints(
2738	FILE fp / pointer to the fairness constraint file */)
2739	{
2740	array_t constraintArray; / raw fairness constraints */
2741	array_t ltlConstraintArray; / constraints converted to LTL */
2742
2743	if (fp == NIL(FILE) ) {
2744	/* Nothing to be done. */
2745	return NIL(array_t);
2746	}
2747
2748	/* Read constraints from file and check for errors. */
2749	constraintArray = Ctlsp_FileParseFormulaArray(fp);
2750	if (constraintArray == NIL(array_t)) {
2751	(void) fprintf(vis_stderr,
2752	"** ctlsp error: error reading fairness constraints.\n");
2753	return NIL(array_t);
2754	}
2755	if (array_n(constraintArray) == 0) {
2756	(void) fprintf(vis_stderr, "** ctlsp error: fairness file is empty.\n");
2757	return NIL(array_t);
2758	}
2759	/*
2760	* Check that each constraint is an LTL formula.
2761	*/
2762	ltlConstraintArray = Ctlsp_FormulaArrayConvertToLTL(constraintArray);
2763	Ctlsp_FormulaArrayFree(constraintArray);
2764	if (ltlConstraintArray == NIL(array_t)) {
2765	(void) fprintf(vis_stderr,
2766	"** ctlsp error: fairness constraints are not LTL formulae.\n");
2767	return NIL(array_t);
2768	}
2769
2770	return ltlConstraintArray;
2771
2772	} /* BmcReadFairnessConstraints */
2773
2774
2775	/Function******************************************************************
2776
2777	Synopsis [return the cnf index for a bdd node]
2778
2779	SideEffects []
2780
2781	******************************************************************************/
2782	int
2783	BmcGetCnfVarIndexForBddNode(
2784	bdd_manager *bddManager,
2785	bdd_node *node,
2786	int state,
2787	BmcCnfClauses_t *cnfClauses)
2788	{
2789	array_t *mvar_list = mdd_ret_mvar_list(bddManager);
2790	array_t *bvar_list = mdd_ret_bvar_list(bddManager);
2791
2792	char name[100];
2793	char *nodeName;
2794	bvar_type bv;
2795	mvar_type mv;
2796	int nodeIndex = bdd_node_read_index(node);
2797	int index, rtnNodeIndex, rtnCode;
2798
2799
2800	/*
2801	If the node is for a multi-valued varaible.
2802	*/
2803	if (nodeIndex < array_n(bvar_list)){
2804	bv = array_fetch(bvar_type, bvar_list, nodeIndex);
2805	/*
2806	get the multi-valued varaible.
2807	*/
2808	mv = array_fetch(mvar_type, mvar_list, bv.mvar_id);
2809	arrayForEachItem(int, mv.bvars, index, rtnNodeIndex) {
2810	if (nodeIndex == rtnNodeIndex){
2811	break;
2812	}
2813	}
2814	assert(index < mv.encode_length);
2815	/*
2816	printf("Name of bdd node %s %d\n", mv.name, index);
2817	*/
2818	sprintf(name, "%s_%d", mv.name, index);
2819	} else {
2820	sprintf(name, "Bdd_%d", nodeIndex);
2821	}
2822	nodeName = util_strsav(name);
2823	rtnCode = BmcCnfReadOrInsertNode(cnfClauses, nodeName, state, &nodeIndex);
2824	if(rtnCode == 1) {
2825	FREE(nodeName);
2826	}
2827	return nodeIndex;
2828	}
2829
2830	/---------------------------------------------------------------------------/
2831	/* Definition of static functions */
2832	/---------------------------------------------------------------------------/
2833
2834	/Function******************************************************************
2835
2836	Synopsis [Test that the given string is an integer. Returns 0 if string is
2837	not an integer, 1 if the integer is too big for int, and 2 if integer fits
2838	in int.]
2839
2840	SideEffects [Sets the pointer value if the string is an integer small enough
2841	for int.]
2842
2843	******************************************************************************/
2844	static int
2845	StringCheckIsInteger(
2846	char *string,
2847	int *value)
2848	{
2849	char *ptr;
2850	long l;
2851
2852	l = strtol (string, &ptr, 0) ;
2853	if(*ptr != '\0')
2854	return 0;
2855	if ((l > MAXINT) \|\| (l < -1 - MAXINT))
2856	return 1 ;
2857	*value = (int) l;
2858	return 2 ;
2859	}
2860
2861	/Function******************************************************************
2862
2863	Synopsis [Compare procedure for name comparison.]
2864
2865	Description [Compare procedure for name comparison.]
2866
2867	SideEffects []
2868
2869	******************************************************************************/
2870	static int
2871	nameCompare(
2872	const void * name1,
2873	const void * name2)
2874	{
2875	return(strcmp((char)name1, (char **)name2));
2876
2877	} /* end of signatureCompare */
2878
2879
2880
2881
2882	/Function******************************************************************
2883
2884	Synopsis [Print the valuse of variables in the variable list "varNames".]
2885
2886	Description [For each variable in the variable list, this functions prints its
2887	value in the resultTable if it is different for its value in prevValue. If this
2888	variable is a symbolic variable, this function prints its symbolic value.]
2889
2890	SideEffects []
2891
2892	******************************************************************************/
2893	static void
2894	printValue(
2895	mAig_Manager_t *manager,
2896	Ntk_Network_t *network,
2897	st_table *nodeToMvfAigTable,
2898	BmcCnfClauses_t *cnfClauses,
2899	array_t *varNames,
2900	st_table *resultTable,
2901	int state,
2902	int *prevValue)
2903	{
2904	Ntk_Node_t *node;
2905	int i, j;
2906	bAigEdge_t bAigId;
2907	nameType_t varName, nodeName;
2908	int value, index;
2909	MvfAig_Function_t *MvfAig;
2910	int changed = 0;
2911	int tmp;
2912
2913	for (j=0; j< array_n(varNames); j++) {
2914	if (state == 0){
2915	prevValue[j] = -1;
2916	}
2917	nodeName = array_fetch(char *, varNames, j);
2918	/*
2919	Fetch the node corresponding to this node name.
2920	*/
2921	node = Ntk_NetworkFindNodeByName(network, nodeName);
2922	/*
2923	Get the multi-valued function for each node
2924	*/
2925	MvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
2926	/*
2927	In case of the multi-valued function is not build for this node, do nothing.
2928	We may notify the user.
2929	*/
2930	if (MvfAig == NIL(MvfAig_Function_t)){
2931	continue;
2932	}
2933	/*
2934	No CNF index for this variable at time "state in the "
2935	*/
2936	value = -1;
2937	for (i=0; i< array_n(MvfAig); i++) {
2938	bAigId = MvfAig_FunctionReadComponent(MvfAig, i);
2939	/*
2940	constant value
2941	*/
2942	if (bAigId == bAig_One){
2943	/*
2944	This variable equal the constant i.
2945	*/
2946	value = i;
2947	break;
2948	}
2949	if (bAigId != bAig_Zero){
2950	char *tmpStr;
2951
2952	nodeName = bAig_NodeReadName(manager, bAigId);
2953	/*
2954	Build the variable name at state "state".
2955	*/
2956	tmpStr = util_inttostr(state);
2957	varName = util_strcat3(nodeName, "_", tmpStr);
2958	if (st_lookup_int(cnfClauses->cnfIndexTable, varName, &index)) {
2959	if (bAig_IsInverted(bAigId)){
2960	index = -index;
2961	}
2962	/if (searchArray(result, index) > -1){/
2963	if (st_lookup_int(resultTable, (char *)(long)index, &tmp)){
2964	value = i;
2965	break;
2966	}
2967	} /* if st_lookup_int() */
2968	FREE(tmpStr);
2969	FREE(varName);
2970	} /* if (bAigId != bAig_Zero) */
2971	}
2972	if (value >= 0){
2973	if (value != prevValue[j]){
2974	Var_Variable_t *nodeVar = Ntk_NodeReadVariable(node);
2975
2976	prevValue[j] = value;
2977	changed = 1;
2978	if (Var_VariableTestIsSymbolic(nodeVar)) {
2979	char *symbolicValue = Var_VariableReadSymbolicValueFromIndex(nodeVar, value);
2980
2981	(void) fprintf(vis_stdout,"%s:%s\n", Ntk_NodeReadName(node), symbolicValue);
2982	}
2983	else {
2984	(void) fprintf(vis_stdout,"%s:%d\n", Ntk_NodeReadName(node), value);
2985	}
2986	}
2987	} else {
2988	/*
2989	This variable does not have value in the current time frame. It means its value
2990	is not important at this time frame.
2991	*/
2992	(void) fprintf(vis_stdout,"%s:X\n", Ntk_NodeReadName(node));
2993	}
2994	} /* for j loop */
2995	if (changed == 0){
2996	fprintf( vis_stdout, "<Unchanged>\n");
2997	}
2998
2999	}/* end of printValue() */
3000
3001
3002
3003	/Function******************************************************************
3004
3005	Synopsis [Print the valuse of variables in the variable list "varNames".]
3006
3007	Description [For each variable in the variable list, this functions prints the
3008	values of names, which do not start with $_ as these are true
3009	latches of the model. Since this is in aiger format, hence all
3010	the values are printed even if they didn't change from the
3011	previous values.]
3012
3013	SideEffects []
3014
3015	******************************************************************************/
3016	static void
3017	printValueAiger(
3018	mAig_Manager_t *manager,
3019	Ntk_Network_t *network,
3020	st_table *nodeToMvfAigTable,
3021	BmcCnfClauses_t *cnfClauses,
3022	array_t *varNames,
3023	st_table *resultTable,
3024	int state,
3025	int *prevValue)
3026	{
3027	Ntk_Node_t *node;
3028	int i, j;
3029	bAigEdge_t bAigId;
3030	nameType_t varName, nodeName;
3031	int value, index;
3032	MvfAig_Function_t *MvfAig;
3033	int tmp;
3034	char * NodeName;
3035
3036	for (j=0; j< array_n(varNames); j++) {
3037	if (state == 0){
3038	prevValue[j] = -1;
3039	}
3040	nodeName = array_fetch(char *, varNames, j);
3041	/*
3042	Fetch the node corresponding to this node name.
3043	*/
3044	node = Ntk_NetworkFindNodeByName(network, nodeName);
3045	/*
3046	Get the multi-valued function for each node
3047	*/
3048	MvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
3049	/*
3050	In case of the multi-valued function is not build for this node, do nothing.
3051	We may notify the user.
3052	*/
3053	if (MvfAig == NIL(MvfAig_Function_t)){
3054	continue;
3055	}
3056	/*
3057	No CNF index for this variable at time "state in the "
3058	*/
3059	value = -1;
3060	for (i=0; i< array_n(MvfAig); i++) {
3061	bAigId = MvfAig_FunctionReadComponent(MvfAig, i);
3062	/*
3063	constant value
3064	*/
3065	if (bAigId == bAig_One){
3066	/*
3067	This variable equal the constant i.
3068	*/
3069	value = i;
3070	break;
3071	}
3072	if (bAigId != bAig_Zero){
3073	char *tmpStr;
3074
3075	nodeName = bAig_NodeReadName(manager, bAigId);
3076	/*
3077	Build the variable name at state "state".
3078	*/
3079	tmpStr = util_inttostr(state);
3080	varName = util_strcat3(nodeName, "_", tmpStr);
3081	if (st_lookup_int(cnfClauses->cnfIndexTable, varName, &index)) {
3082	if (bAig_IsInverted(bAigId)){
3083	index = -index;
3084	}
3085	/if (searchArray(result, index) > -1){/
3086	if (st_lookup_int(resultTable, (char *)(long)index, &tmp)){
3087	value = i;
3088	break;
3089	}
3090	} /* if st_lookup_int() */
3091	FREE(tmpStr);
3092	FREE(varName);
3093	} /* if (bAigId != bAig_Zero) */
3094	}
3095	NodeName = Ntk_NodeReadName(node);
3096	if(!((NodeName[0] == '$') && (NodeName[1] == '_')))
3097	{
3098	if (value >= 0){
3099	Var_Variable_t *nodeVar = Ntk_NodeReadVariable(node);
3100
3101	prevValue[j] = value;
3102	if (Var_VariableTestIsSymbolic(nodeVar)) {
3103	char *symbolicValue = Var_VariableReadSymbolicValueFromIndex(nodeVar, value);
3104
3105	(void) fprintf(vis_stdout,"%s", symbolicValue);
3106	}
3107	else {
3108	(void) fprintf(vis_stdout,"%d", value);
3109	}
3110	} else {
3111	/*
3112	This variable does not have value in the current time frame. It means its value
3113	is not important at this time frame.
3114	*/
3115	(void) fprintf(vis_stdout,"x" );
3116	}
3117	} /* these nodes are latches in front of inputs so they will be printed out as inputs */
3118	} /* for j loop */
3119	}/* end of printValueAiger() */
3120
3121
3122	/Function******************************************************************
3123
3124	Synopsis [Print the valuse of variables in the variable list "varNames".]
3125
3126	Description [For each variable in the variable list, this functions checks if
3127	the name starts with $_, which means that those latches are
3128	actually storing the value of inputs. This modification to the
3129	model is externally done and not done by VIS so this method is
3130	only specific to certain type of model, the output of aigtoblif
3131	translator.]
3132
3133	SideEffects []
3134
3135	******************************************************************************/
3136	static void
3137	printValueAigerInputs(
3138	mAig_Manager_t *manager,
3139	Ntk_Network_t *network,
3140	st_table *nodeToMvfAigTable,
3141	BmcCnfClauses_t *cnfClauses,
3142	array_t *varNames,
3143	st_table *resultTable,
3144	int state,
3145	int *prevValue)
3146	{
3147	Ntk_Node_t *node;
3148	int i, j;
3149	bAigEdge_t bAigId;
3150	nameType_t varName, nodeName;
3151	int value, index;
3152	MvfAig_Function_t *MvfAig;
3153	int tmp;
3154	char * NodeName;
3155
3156	for (j=0; j< array_n(varNames); j++) {
3157	if (state == 0){
3158	prevValue[j] = -1;
3159	}
3160	nodeName = array_fetch(char *, varNames, j);
3161	/*
3162	Fetch the node corresponding to this node name.
3163	*/
3164	node = Ntk_NetworkFindNodeByName(network, nodeName);
3165	/*
3166	Get the multi-valued function for each node
3167	*/
3168	MvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
3169	/*
3170	In case of the multi-valued function is not build for this node, do nothing.
3171	We may notify the user.
3172	*/
3173	if (MvfAig == NIL(MvfAig_Function_t)){
3174	continue;
3175	}
3176	/*
3177	No CNF index for this variable at time "state in the "
3178	*/
3179	value = -1;
3180	for (i=0; i< array_n(MvfAig); i++) {
3181	bAigId = MvfAig_FunctionReadComponent(MvfAig, i);
3182	/*
3183	constant value
3184	*/
3185	if (bAigId == bAig_One){
3186	/*
3187	This variable equal the constant i.
3188	*/
3189	value = i;
3190	break;
3191	}
3192	if (bAigId != bAig_Zero){
3193	char *tmpStr;
3194
3195	nodeName = bAig_NodeReadName(manager, bAigId);
3196	/*
3197	Build the variable name at state "state".
3198	*/
3199	tmpStr = util_inttostr(state);
3200	varName = util_strcat3(nodeName, "_", tmpStr);
3201	if (st_lookup_int(cnfClauses->cnfIndexTable, varName, &index)) {
3202	if (bAig_IsInverted(bAigId)){
3203	index = -index;
3204	}
3205	/if (searchArray(result, index) > -1){/
3206	if (st_lookup_int(resultTable, (char *)(long)index, &tmp)){
3207	value = i;
3208	break;
3209	}
3210	} /* if st_lookup_int() */
3211	FREE(tmpStr);
3212	FREE(varName);
3213	} /* if (bAigId != bAig_Zero) */
3214	}
3215	NodeName = Ntk_NodeReadName(node);
3216	if((NodeName[0] == '$') && (NodeName[1] == '_'))
3217	{
3218	if (value >= 0){
3219	Var_Variable_t *nodeVar = Ntk_NodeReadVariable(node);
3220
3221	prevValue[j] = value;
3222	if (Var_VariableTestIsSymbolic(nodeVar)) {
3223	char *symbolicValue = Var_VariableReadSymbolicValueFromIndex(nodeVar, value);
3224
3225	(void) fprintf(vis_stdout,"%s", symbolicValue);
3226	}
3227	else {
3228	(void) fprintf(vis_stdout,"%d", value);
3229	}
3230	} else {
3231	/*
3232	This variable does not have value in the current time frame. It means its value
3233	is not important at this time frame.
3234	*/
3235	(void) fprintf(vis_stdout,"x" );
3236	}
3237	} /* these nodes are latches in front of inputs so they will be printed out as inputs */
3238	} /* for j loop */
3239	}/* end of printValueAigerInputs() */
3240
3241
3242

Note: See TracBrowser for help on using the repository browser.

Context Navigation

source: vis_dev/vis-2.3/src/bmc/bmcUtil.c

Download in other formats: