Context Navigation

bmcBmc.c @ 54

Last change on this file since 54 was 38, checked in by cecile, 13 years ago
first attempt debug with ltl formula
File size: 91.8 KB

Line
1	/CFile*********************************************************************
2
3	FileName [bmcBmc.c]
4
5	PackageName [bmc]
6
7	Synopsis [SAT-based ltl model checker.]
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
19	static char rcsid[] UNUSED = "$Id: bmcBmc.c,v 1.72 2005/10/14 04:41:11 awedh Exp $";
20
21	/---------------------------------------------------------------------------/
22	/* Constant declarations */
23	/---------------------------------------------------------------------------/
24
25	/---------------------------------------------------------------------------/
26	/* Type declarations */
27	/---------------------------------------------------------------------------/
28
29	/---------------------------------------------------------------------------/
30	/* Structure declarations */
31	/---------------------------------------------------------------------------/
32
33	/---------------------------------------------------------------------------/
34	/* Variable declarations */
35	/---------------------------------------------------------------------------/
36
37	/AutomaticStart***********************************************************/
38
39	/---------------------------------------------------------------------------/
40	/* Static function prototypes */
41	/---------------------------------------------------------------------------/
42
43	static int checkIndex(int index, BmcCnfClauses_t *cnfClauses);
44	static int doAnd(int left, int right);
45	static int doOr(int left, int right);
46
47	/AutomaticEnd*************************************************************/
48
49	/---------------------------------------------------------------------------/
50	/* Definition of exported functions */
51	/---------------------------------------------------------------------------/
52
53	/---------------------------------------------------------------------------/
54	/* Definition of internal functions */
55	/---------------------------------------------------------------------------/
56
57	/Function******************************************************************
58
59	Synopsis [Apply Bounded Model Checking (BMC) on a propositional formula.]
60
61	Description [If the property dos not hold in any initial state, the
62	property holds.
63
64	Note: Before calling this function, the LTL formula must be negated.
65
66	]
67
68	SideEffects []
69
70	SeeAlso []
71
72	******************************************************************************/
73	void
74	BmcLtlVerifyProp(
75	Ntk_Network_t *network,
76	Ctlsp_Formula_t *ltlFormula,
77	st_table *CoiTable,
78	BmcOption_t *options)
79	{
80	mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
81	st_table nodeToMvfAigTable = NIL(st_table); / maps each node to its mvfAig */
82	BmcCnfClauses_t *cnfClauses = NIL(BmcCnfClauses_t);
83
84
85	FILE *cnfFile;
86
87	array_t *result = NIL(array_t);
88	long startTime, endTime;
89	bAigEdge_t property;
90	array_t *unitClause;
91
92	assert(Ctlsp_isPropositionalFormula(ltlFormula));
93
94	startTime = util_cpu_ctime();
95
96	if (options->verbosityLevel != BmcVerbosityNone_c){
97	(void) fprintf(vis_stdout, "LTL formula is propositional\n");
98	}
99	property = BmcCreateMaigOfPropFormula(network, manager, ltlFormula);
100
101	if (property == mAig_NULL){
102	return;
103	}
104	if (property == bAig_One){
105	(void) fprintf(vis_stdout,"# BMC: Empty counterexample because the property is always FALSE\n");
106	(void) fprintf(vis_stdout,"# BMC: formula failed\n");
107	if (options->verbosityLevel != BmcVerbosityNone_c){
108	fprintf(vis_stdout, "-- bmc time = %10g\n",
109	(double)(util_cpu_ctime() - startTime) / 1000.0);
110	}
111	return;
112	} else if (property == bAig_Zero){
113	(void) fprintf(vis_stdout,"# BMC: The property is always TRUE\n");
114	(void) fprintf(vis_stdout,"# BMC: formula passed\n");
115	if (options->verbosityLevel != BmcVerbosityNone_c){
116	fprintf(vis_stdout, "-- bmc time = %10g\n",
117	(double)(util_cpu_ctime() - startTime) / 1000.0);
118	}
119	return;
120	}
121	cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
122	if (cnfFile == NIL(FILE)) {
123	(void) fprintf(vis_stderr,
124	"** bmc error: Cannot create CNF output file %s\n",
125	options->satInFile);
126	return;
127	}
128	/* nodeToMvfAigTable Maps each node to its Multi-function And/Inv graph */
129	nodeToMvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(network,
130	MVFAIG_NETWORK_APPL_KEY);
131	assert(nodeToMvfAigTable != NIL(st_table));
132	/*
133	Create clauses database
134	*/
135	cnfClauses = BmcCnfClausesAlloc();
136	unitClause = array_alloc(int, 1);
137
138	/*
139	Create an initialized path of length 0
140	*/
141	BmcCnfGenerateClausesForPath(network, 0, 0, BMC_INITIAL_STATES, cnfClauses, nodeToMvfAigTable, CoiTable);
142
143	/* Generate CNF for the property */
144	array_insert(int, unitClause, 0,
145	BmcGenerateCnfFormulaForAigFunction(manager, property, 0, cnfClauses));
146
147	BmcCnfInsertClause(cnfClauses, unitClause);
148	BmcWriteClauses(manager, cnfFile, cnfClauses, options);
149	(void) fclose(cnfFile);
150
151	result = BmcCheckSAT(options);
152	if (options->satSolverError){
153	(void) fprintf(vis_stdout,"# BMC: Error in calling SAT solver\n");
154	} else {
155	if (result != NIL(array_t)){
156	(void) fprintf(vis_stdout, "# BMC: formula failed\n");
157	if(options->verbosityLevel != BmcVerbosityNone_c){
158	(void) fprintf(vis_stdout,
159	"# BMC: Found a counterexample of length = 0 \n");
160	}
161	if (options->dbgLevel == 1) {
162	BmcPrintCounterExample(network, nodeToMvfAigTable, cnfClauses,
163	result, 0, CoiTable, options, NIL(array_t));
164	}
165	array_free(result);
166	} else {
167	if(options->verbosityLevel != BmcVerbosityNone_c){
168	fprintf(vis_stdout,"# BMC: no counterexample found of length up to 0\n");
169	}
170	(void) fprintf(vis_stdout, "# BMC: formula Passed\n");
171	}
172	}
173	array_free(unitClause);
174	BmcCnfClausesFree(cnfClauses);
175
176	if (options->verbosityLevel != BmcVerbosityNone_c){
177	endTime = util_cpu_ctime();
178	fprintf(vis_stdout, "-- bmc time = %10g\n",
179	(double)(endTime - startTime) / 1000.0);
180	}
181	fflush(vis_stdout);
182	return;
183	} /* BmcLtlVerifyProp */
184
185
186	/Function******************************************************************
187
188	Synopsis [Check if the LTL formula in the form G(p) (invariant),
189	where p is a propositional formula, is an Inductive Invariant]
190
191	Description [Check if the LTL formula in the form G(p), where p is a
192	propositional formula, is an Inductive Invariant
193
194	An LTL formula G(p), where p is a propositional formul, is an
195	inductive invariant if the following two conditions hold:
196
197	1- p holds in all the intial states.
198	2- If p holds in a state s, then it also holds in all states
199	that are reachable from s.
200
201	G(p) is an inductive invariant if :
202	SAT( I(0) and !p(0)) return UNSAT and
203	SAT( p(i) and T(i, i+1) and !p(i+1)) returns UNSAT.
204
205	Return value:
206	0 if the property is not an inductive invariant
207	1 if the property is an inductive invariant
208	-1 error
209	]
210
211	SideEffects []
212
213	SeeAlso []
214
215	******************************************************************************/
216	int
217	BmcLtlCheckInductiveInvariant(
218	Ntk_Network_t *network,
219	bAigEdge_t property,
220	BmcOption_t *options,
221	st_table *CoiTable)
222	{
223	mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
224	BmcCnfClauses_t *cnfClauses = NIL(BmcCnfClauses_t);
225	array_t *unitClause;
226	int cnfIndex;
227	array_t *result = NIL(array_t);
228	FILE *cnfFile;
229	st_table nodeToMvfAigTable = NIL(st_table); / maps each node to its mvfAig */
230	int savedVerbosityLevel = options->verbosityLevel;
231	int returnValue = 0; /* the property is not an inductive invariant */
232
233	cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
234	if (cnfFile == NIL(FILE)) {
235	(void) fprintf(vis_stderr,
236	"** bmc error: Cannot create CNF output file %s\n",
237	options->satInFile);
238	return -1;
239	}
240	/*
241	nodeToMvfAigTable Maps each node to its Multi-function And/Inv graph
242	*/
243	nodeToMvfAigTable =
244	(st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
245
246	assert(nodeToMvfAigTable != NIL(st_table));
247
248	/*
249	Clause database
250	*/
251	cnfClauses = BmcCnfClausesAlloc();
252	/*
253	Check if the property holds in all intial states
254	*/
255	/*
256	Generate CNF clauses for initial states
257	*/
258	BmcCnfGenerateClausesForPath(network, 0, 0, BMC_INITIAL_STATES,
259	cnfClauses, nodeToMvfAigTable, CoiTable);
260	/*
261	Generate CNF clauses for the property
262	*/
263	cnfIndex = BmcGenerateCnfFormulaForAigFunction(manager, property, 0, cnfClauses);
264	unitClause = array_alloc(int, 1);
265	array_insert(int, unitClause, 0, cnfIndex); /* because property is the negation of
266	the LTL formula*/
267	BmcCnfInsertClause(cnfClauses, unitClause);
268
269	options->verbosityLevel = BmcVerbosityNone_c;
270	BmcWriteClauses(manager, cnfFile, cnfClauses, options);
271	(void) fclose(cnfFile);
272	result = BmcCheckSAT(options);
273	options->verbosityLevel = (Bmc_VerbosityLevel) savedVerbosityLevel;
274	BmcCnfClausesFree(cnfClauses);
275	if (options->satSolverError){
276	return -1;
277	}
278	if (result == NIL(array_t)){ /* the property holds at all initial states */
279	cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
280	if (cnfFile == NIL(FILE)) {
281	(void) fprintf(vis_stderr,
282	"** bmc error: Cannot create CNF output file %s\n",
283	options->satInFile);
284	return -1;
285	}
286	/*
287	Check if the property holds in state i, it also holds in state i+1
288	*/
289	cnfClauses = BmcCnfClausesAlloc();
290	/*
291	Generate CNF clauses for a transition from state i to state i+1.
292	*/
293	BmcCnfGenerateClausesForPath(network, 0, 1, BMC_NO_INITIAL_STATES,
294	cnfClauses, nodeToMvfAigTable, CoiTable);
295
296	cnfIndex = BmcGenerateCnfFormulaForAigFunction(manager, property, 0, cnfClauses);
297	array_insert(int, unitClause, 0, -cnfIndex); /* because property is the negation of
298	the LTL formula */
299	BmcCnfInsertClause(cnfClauses, unitClause);
300
301	cnfIndex = BmcGenerateCnfFormulaForAigFunction(manager, property, 1, cnfClauses);
302	array_insert(int, unitClause, 0, cnfIndex); /* because property is the negation of
303	the LTL formula */
304	BmcCnfInsertClause(cnfClauses, unitClause);
305	options->verbosityLevel = BmcVerbosityNone_c;
306	BmcWriteClauses(manager, cnfFile, cnfClauses, options);
307	(void) fclose(cnfFile);
308	result = BmcCheckSAT(options);
309	options->verbosityLevel = (Bmc_VerbosityLevel) savedVerbosityLevel;
310	BmcCnfClausesFree(cnfClauses);
311	if (options->satSolverError){
312	returnValue = -1;
313	}
314	if (result != NIL(array_t)){
315	returnValue = 0; /* the property is not an inductive invariant */
316	} else {
317	returnValue = 1; /* the property is an inductive invariant */
318	}
319	}
320	array_free(unitClause);
321	return returnValue;
322	} /* BmcLtlCheckInductiveInvariant() */
323
324
325	/Function******************************************************************
326
327	Synopsis [Apply Bounded Model Checking (BMC) on an LTL formula of
328	the form G(p), where p is a propositional formula.]
329
330	Description [Given a model M, an LTL formula f = Gp, and a bound k,
331	we first find a counterexample of length k to a state that violates
332	p. If -r switch of the BMC command is specified, we apply the
333	induction proof to check if the property f passes. The property f
334	passes if there is no simple path in M that leads to a state that
335	violates p, or no simple path in M starting at an initial state.
336
337	Note: Before calling this function, the LTL formula must be negated.
338
339	]
340
341	SideEffects []
342
343	SeeAlso []
344
345	******************************************************************************/
346	void
347	BmcLtlVerifyGp(
348	Ntk_Network_t *network,
349	Ctlsp_Formula_t *ltlFormula,
350	st_table *CoiTable,
351	BmcOption_t *options)
352	{
353	mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
354	st_table nodeToMvfAigTable = NIL(st_table); / maps each node to its mvfAig */
355	BmcCnfClauses_t *cnfClauses = NIL(BmcCnfClauses_t);
356	BmcCnfStates_t *state;
357
358	FILE *cnfFile;
359	array_t *Pclause = array_alloc(int, 0);
360
361	int k, bound, initK, propK;
362	array_t *result = NIL(array_t);
363	long startTime, endTime;
364	bAigEdge_t property;
365	int minK = options->minK;
366	int maxK = options->maxK;
367	int i, initState = BMC_INITIAL_STATES;
368	array_t *unitClause;
369
370	int bmcError = FALSE;
371
372	Bmc_PropertyStatus formulaStatus;
373
374	assert(Ctlsp_LtlFormulaIsFp(ltlFormula));
375
376	startTime = util_cpu_ctime();
377
378	if (options->verbosityLevel != BmcVerbosityNone_c){
379	(void)fprintf(vis_stdout, "LTL formula is of type G(p)\n");
380	}
381	property = BmcCreateMaigOfPropFormula(network, manager, ltlFormula->right);
382
383	if (property == mAig_NULL){
384	return;
385	}
386	if (property == bAig_One){
387	(void) fprintf(vis_stdout,"# BMC: Empty counterexample because the property is always FALSE\n");
388	(void) fprintf(vis_stdout,"# BMC: formula failed\n");
389	if (options->verbosityLevel != BmcVerbosityNone_c){
390	fprintf(vis_stdout, "-- bmc time = %10g\n",
391	(double)(util_cpu_ctime() - startTime) / 1000.0);
392	}
393	return;
394	} else if (property == bAig_Zero){
395	(void) fprintf(vis_stdout,"# BMC: The property is always TRUE\n");
396	(void) fprintf(vis_stdout,"# BMC: formula passed\n");
397	if (options->verbosityLevel != BmcVerbosityNone_c){
398	fprintf(vis_stdout, "-- bmc time = %10g\n",
399	(double)(util_cpu_ctime() - startTime) / 1000.0);
400	}
401	return;
402	}
403
404	#if 0
405	if (options->verbosityLevel == BmcVerbosityMax_c){
406	(void) fprintf(vis_stdout, "\nBMC: Check if the property is an inductive invariant\n");
407	}
408	checkInductiveInvariant = BmcLtlCheckInductiveInvariant(network, property, options, CoiTable);
409
410	if(checkInductiveInvariant == -1){
411	return;
412	}
413	if (checkInductiveInvariant == 1){
414	(void) fprintf(vis_stdout,"# BMC: The property is an inductive invariant\n");
415	(void) fprintf(vis_stdout,"# BMC: formula passed\n");
416	if (options->verbosityLevel != BmcVerbosityNone_c){
417	fprintf(vis_stdout, "-- bmc time = %10g\n",
418	(double)(util_cpu_ctime() - startTime) / 1000.0);
419	}
420	return;
421	}
422	#endif
423	if (options->verbosityLevel != BmcVerbosityNone_c){
424	(void)fprintf(vis_stdout, "Apply BMC on counterexample of length >= %d and <= %d (+%d)\n",
425	minK, maxK, options->step);
426	}
427	initK = 0;
428	propK = 0;
429	formulaStatus = BmcPropertyUndecided_c;
430
431	/* nodeToMvfAigTable Maps each node to its Multi-function And/Inv graph */
432	nodeToMvfAigTable =
433	(st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
434	assert(nodeToMvfAigTable != NIL(st_table));
435
436	/*
437	Create clauses database
438	*/
439	cnfClauses = BmcCnfClausesAlloc();
440	/*
441	init = BmcCreateMaigOfInitialStates(network, nodeToMvfAigTable, CoiTable);
442	*/
443	for(bound = minK; bound <= maxK; bound += options->step){
444	if (options->verbosityLevel == BmcVerbosityMax_c) {
445	(void) fprintf(vis_stdout,
446	"\nBMC: Generate counterexample of length %d\n",
447	bound);
448	}
449	cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
450	if (cnfFile == NIL(FILE)) {
451	(void) fprintf(vis_stderr,
452	"** bmc error: Cannot create CNF output file %s\n",
453	options->satInFile);
454	bmcError = TRUE;
455	break;
456	}
457	BmcCnfGenerateClausesForPath(network, initK, bound, initState, cnfClauses, nodeToMvfAigTable, CoiTable);
458
459	initState = BMC_NO_INITIAL_STATES;
460
461	/* Generate CNF for the property */
462	Pclause = array_alloc(int, 0);
463	/*
464	state = BmcCnfClausesFreeze(cnfClauses);
465	*/
466	for(k=propK; k <= bound; k++){
467	array_insert_last(
468	int, Pclause, BmcGenerateCnfFormulaForAigFunction(manager, property,
469	k, cnfClauses));
470	}
471
472	state = BmcCnfClausesFreeze(cnfClauses);
473
474	BmcCnfInsertClause(cnfClauses, Pclause);
475	BmcWriteClauses(manager, cnfFile, cnfClauses, options);
476	(void) fclose(cnfFile);
477	BmcCnfClausesRestore(cnfClauses, state);
478	result = BmcCheckSAT(options);
479	if (options->satSolverError){
480	array_free(Pclause);
481	break;
482	}
483	if (result != NIL(array_t)){
484	bound++;
485	array_free(Pclause);
486	/*
487	formula failed\n"
488	*/
489	formulaStatus = BmcPropertyFailed_c;
490	break;
491	}
492	unitClause = array_alloc(int, 1);
493	for(i=0; i<array_n(Pclause); i++){
494	array_insert(int, unitClause, 0, -array_fetch(int, Pclause, i));
495	BmcCnfInsertClause(cnfClauses, unitClause);
496	}
497	array_free(unitClause);
498	array_free(Pclause);
499	FREE(state);
500	initK = bound;
501	propK = bound+1;
502
503	/*
504	Prove if the property passes using the induction proof of SSS0.
505	*/
506	if((result == NIL(array_t)) &&
507	(options->inductiveStep !=0) &&
508	(bound % options->inductiveStep == 0)){
509	BmcCnfClauses_t *cnfClauses;
510	array_t *result = NIL(array_t);
511	array_t *unitClause = array_alloc(int, 1);
512	int savedVerbosityLevel = options->verbosityLevel;
513	long startTime = util_cpu_ctime();
514
515	if (options->verbosityLevel == BmcVerbosityMax_c) {
516	(void) fprintf(vis_stdout, "\nBMC: Check for induction\n");
517	}
518	options->verbosityLevel = BmcVerbosityNone_c;
519
520	if(options->earlyTermination){
521	/*
522	Early termination condition
523
524	Check if there is no simple path of length 'bound' starts from
525	initial states
526
527	*/
528	cnfClauses = BmcCnfClausesAlloc();
529
530	cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
531	if (cnfFile == NIL(FILE)) {
532	(void)fprintf(vis_stderr,
533	"** bmc error: Cannot create CNF output file %s\n",
534	options->satInFile);
535	bmcError = TRUE;
536	break;
537	}
538	/*
539	Generate an initialized simple path path of length bound.
540	*/
541	BmcCnfGenerateClausesForLoopFreePath(network, 0, bound, BMC_INITIAL_STATES,
542	cnfClauses, nodeToMvfAigTable, CoiTable);
543	BmcWriteClauses(manager, cnfFile, cnfClauses, options);
544	(void) fclose(cnfFile);
545	BmcCnfClausesFree(cnfClauses);
546
547	result = BmcCheckSAT(options);
548	if(options->satSolverError){
549	break;
550	}
551	if(result == NIL(array_t)){
552	if (savedVerbosityLevel == BmcVerbosityMax_c) {
553	(void) fprintf(vis_stdout,
554	"# BMC: No simple path starting at an initial state\n");
555	}
556	formulaStatus = BmcPropertyPassed_c;
557	} else {
558	array_free(result);
559	}
560	} /* Early termination */
561	if(formulaStatus != BmcPropertyPassed_c){
562	cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
563	if (cnfFile == NIL(FILE)) {
564	(void)fprintf(vis_stderr,
565	"** bmc error: Cannot create CNF output file %s\n",
566	options->satInFile);
567	bmcError = TRUE;
568	break;
569	}
570	cnfClauses = BmcCnfClausesAlloc();
571	/*
572	Generate a simple path of length k+1
573	*/
574	BmcCnfGenerateClausesForLoopFreePath(network, 0, bound+1, BMC_NO_INITIAL_STATES,
575	cnfClauses, nodeToMvfAigTable, CoiTable);
576	/*
577	All the states to bound satisfy the property.
578	*/
579	unitClause = array_alloc(int, 1);
580	for(k=0; k <= bound; k++){
581	array_insert(
582	int, unitClause, 0, -BmcGenerateCnfFormulaForAigFunction(manager, property,
583	k, cnfClauses));
584	BmcCnfInsertClause(cnfClauses, unitClause);
585	}
586	/*
587	The property fails at bound +1
588	*/
589	array_insert(int, unitClause, 0,
590	BmcGenerateCnfFormulaForAigFunction(manager, property,
591	bound+1, cnfClauses));
592	BmcCnfInsertClause(cnfClauses, unitClause);
593	array_free(unitClause);
594
595	BmcWriteClauses(manager, cnfFile, cnfClauses, options);
596	BmcCnfClausesFree(cnfClauses);
597	(void) fclose(cnfFile);
598	result = BmcCheckSAT(options);
599	if (options->satSolverError){
600	break;
601	}
602	if(result == NIL(array_t)) {
603	if (savedVerbosityLevel == BmcVerbosityMax_c) {
604	(void) fprintf(vis_stdout,
605	"# BMC: No simple path leading to a bad state\n");
606	}
607	formulaStatus = BmcPropertyPassed_c;
608	}
609	}
610	options->verbosityLevel = (Bmc_VerbosityLevel) savedVerbosityLevel;
611	if (options->verbosityLevel != BmcVerbosityNone_c){
612	endTime = util_cpu_ctime();
613	fprintf(vis_stdout, "-- check for induction time = %10g\n",
614	(double)(endTime - startTime) / 1000.0);
615	}
616	} /* Check induction */
617	if(formulaStatus != BmcPropertyUndecided_c){
618	break;
619	}
620	} /* for bound loop */
621	if( bmcError == FALSE){
622	if (options->satSolverError){
623	(void) fprintf(vis_stdout,"# BMC: Error in calling SAT solver\n");
624	} else {
625	if(formulaStatus == BmcPropertyUndecided_c){
626	if (options->verbosityLevel != BmcVerbosityNone_c){
627	(void) fprintf(vis_stdout,
628	"# BMC: no counterexample found of length up to %d \n",
629	options->maxK);
630	}
631	}
632	if(formulaStatus == BmcPropertyFailed_c) {
633	(void) fprintf(vis_stdout, "# BMC: formula failed\n");
634	if(options->verbosityLevel != BmcVerbosityNone_c){
635	(void) fprintf(vis_stdout,
636	"# BMC: Found a counterexample of length = %d \n", bound-1);
637	}
638	if (options->dbgLevel == 1) {
639	BmcPrintCounterExample(network, nodeToMvfAigTable, cnfClauses,
640	result, bound-1, CoiTable, options, NIL(array_t));
641	}
642	} else if(formulaStatus == BmcPropertyPassed_c) {
643	(void) fprintf(vis_stdout, "# BMC: formula Passed\n");
644	} else if(formulaStatus == BmcPropertyUndecided_c) {
645	(void) fprintf(vis_stdout,"# BMC: formula undecided\n");
646	}
647	}
648	}
649	/* free all used memories */
650	if(cnfClauses != NIL(BmcCnfClauses_t)){
651	BmcCnfClausesFree(cnfClauses);
652	}
653	if(result != NIL(array_t)) {
654	array_free(result);
655	}
656	/*
657	array_free(Pclause);
658	*/
659	if (options->verbosityLevel != BmcVerbosityNone_c){
660	endTime = util_cpu_ctime();
661	fprintf(vis_stdout, "-- bmc time = %10g\n",
662	(double)(endTime - startTime) / 1000.0);
663	}
664	fflush(vis_stdout);
665	return;
666	} /* BmcLtlVerifyGp() */
667
668	/Function******************************************************************
669
670	Synopsis [Apply Bounded Model Checking (BMC) on an LTL formula of
671	the form F(p), where p is propositional.]
672
673	Description [Given a model M, an LTL formula f = Fp, and a bound k,
674	we first find a k-loop counterexample of length k at which all
675	states violate p. If -r switch of the BMC command is specified, we
676	apply the method in the paper "Proving More Properties with Bounded
677	Model Checking" to check if the property f passes.
678
679	Note: Before calling this function, the LTL formula must be negated.
680
681	]
682	SideEffects []
683
684	SeeAlso []
685
686	******************************************************************************/
687	void
688	BmcLtlVerifyFp(
689	Ntk_Network_t *network,
690	Ctlsp_Formula_t *ltlFormula,
691	st_table *CoiTable,
692	BmcOption_t *options)
693	{
694	mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
695	st_table nodeToMvfAigTable = NIL(st_table); / maps each node to its mvfAig */
696	BmcCnfClauses_t *cnfClauses = NIL(BmcCnfClauses_t);
697
698
699	FILE *cnfFile;
700	array_t unitClause= array_alloc(int, 1), outClause;
701	int outIndex;
702	int k;
703	array_t *result = NIL(array_t);
704	long startTime, endTime;
705	bAigEdge_t property;
706	int bound;
707	int bmcError = FALSE;
708
709	Bmc_PropertyStatus formulaStatus = BmcPropertyUndecided_c;
710
711	assert(Ctlsp_LtlFormulaIsGp(ltlFormula));
712
713	startTime = util_cpu_ctime();
714	if (options->verbosityLevel != BmcVerbosityNone_c){
715	(void)fprintf(vis_stdout, "LTL formula is of type F(p)\n");
716	}
717	property = BmcCreateMaigOfPropFormula(network, manager, ltlFormula->right);
718	if (property == mAig_NULL){
719	return;
720	}
721	if (property == bAig_One){
722	(void) fprintf(vis_stdout, "# BMC: formula failed\n");
723	(void) fprintf(vis_stdout, " Empty counterexample because the property is always FALSE\n");
724	if (options->verbosityLevel != BmcVerbosityNone_c) {
725	endTime = util_cpu_ctime();
726	fprintf(vis_stdout, "-- bmc time = %10g\n",
727	(double)(endTime - startTime) / 1000.0);
728	}
729	return;
730	} else if (property == bAig_Zero){
731	(void) fprintf(vis_stdout,"# BMC: The property is always TRUE\n");
732	formulaStatus = BmcPropertyPassed_c;
733	(void) fprintf(vis_stdout,"# BMC: formula passed\n");
734	if (options->verbosityLevel != BmcVerbosityNone_c) {
735	endTime = util_cpu_ctime();
736	fprintf(vis_stdout, "-- bmc time = %10g\n",
737	(double)(endTime - startTime) / 1000.0);
738	}
739	return;
740	}
741	if (options->verbosityLevel != BmcVerbosityNone_c){
742	(void)fprintf(vis_stdout, "Apply BMC on counterexample of length >= %d and <= %d (+%d) \n",
743	options->minK, options->maxK, options->step);
744	}
745	/*
746	nodeToMvfAigTable Maps each node to its Multi-function AIG graph
747	*/
748	nodeToMvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
749	assert(nodeToMvfAigTable != NIL(st_table));
750	outClause = NIL(array_t);
751	bound = options->minK;
752	BmcGetCoiForLtlFormula(network, ltlFormula, CoiTable);
753
754	while( (result == NIL(array_t)) && (bound <= options->maxK)){
755	if (options->verbosityLevel == BmcVerbosityMax_c) {
756	(void) fprintf(vis_stdout,
757	"\nBMC: Generate counterexample of length %d\n", bound);
758	}
759	cnfClauses = BmcCnfClausesAlloc();
760	cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
761	if (cnfFile == NIL(FILE)) {
762	(void)fprintf(vis_stderr,
763	"** bmc error: Cannot create CNF output file %s\n",
764	options->satInFile);
765	bmcError = TRUE;
766	break;
767	}
768	/*
769	Generate clauses for an initialized path of length "bound".
770	*/
771	BmcCnfGenerateClausesForPath(network, 0, bound, BMC_INITIAL_STATES,
772	cnfClauses, nodeToMvfAigTable, CoiTable);
773	/*
774	Generate CNF for the property. Property fails at all states
775	*/
776	for(k=0; k <= bound; k++){
777	array_insert(int, unitClause, 0,
778	BmcGenerateCnfFormulaForAigFunction(manager, property,
779	k, cnfClauses));
780	BmcCnfInsertClause(cnfClauses, unitClause);
781	}
782
783	/* Generate CNF for a loop-back (loop from the last state to any
784	state) path.
785	(Sk -> S0) + (Sk -> S1) + ..... + (Sk-> Sk-1) + (Sk-> Sk)
786	Each transition consisits of one or more latches. We
787	AND the transiton relation of these latches. For multi-valued
788	latches, we OR the equivalence of each value of the latch. To
789	do the AND we use the CNF equivalent of the AND. a = b*c => (b
790	+ !a) * (c + !a)
791	*/
792	outClause = array_alloc(int, bound);
793	for (k=0; k <= bound; k++){
794	/*
795	Create new var for the output of the AND node.
796	*/
797	outIndex = cnfClauses->cnfGlobalIndex++;
798	BmcCnfGenerateClausesFromStateToState(network, bound, k, cnfClauses,
799	nodeToMvfAigTable, CoiTable, outIndex);
800	array_insert(int, outClause, k, outIndex);
801	} /* for k state loop */
802	BmcCnfInsertClause(cnfClauses, outClause);
803
804	BmcWriteClauses(manager, cnfFile, cnfClauses, options);
805	(void) fclose(cnfFile);
806
807	result = BmcCheckSAT(options);
808	if (options->satSolverError){
809	break;
810	}
811	if(result != NIL(array_t)){
812	formulaStatus = BmcPropertyFailed_c;
813	break;
814	}
815	BmcCnfClausesFree(cnfClauses);
816	array_free(outClause);
817	if((result == NIL(array_t)) &&
818	(options->inductiveStep !=0) &&
819	(bound % options->inductiveStep == 0)
820	)
821	{
822	int savedVerbosityLevel = options->verbosityLevel;
823	long startTime = util_cpu_ctime();
824	array_t *result = NIL(array_t);
825
826	if (options->verbosityLevel == BmcVerbosityMax_c) {
827	(void) fprintf(vis_stdout,
828	"\nBMC: Check if the property passes\n");
829	}
830	cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
831	if (cnfFile == NIL(FILE)) {
832	(void)fprintf(vis_stderr,
833	"** bmc error: Cannot create CNF output file %s\n",
834	options->satInFile);
835	bmcError = TRUE;
836	break;
837	}
838	cnfClauses = BmcCnfClausesAlloc();
839	/*
840	CNF for an initialized simple path.
841	*/
842	BmcCnfGenerateClausesForLoopFreePath(network, 0, bound, BMC_INITIAL_STATES,
843	cnfClauses, nodeToMvfAigTable, CoiTable);
844	/*
845	Generate CNF for the property. Property fails at all states
846	*/
847	for(k=0; k <= bound; k++){
848	array_insert(int, unitClause, 0,
849	BmcGenerateCnfFormulaForAigFunction(manager, property,
850	k, cnfClauses));
851	BmcCnfInsertClause(cnfClauses, unitClause);
852	}
853	BmcWriteClauses(manager, cnfFile, cnfClauses, options);
854	BmcCnfClausesFree(cnfClauses);
855	(void) fclose(cnfFile);
856	/*
857	Do not print any detail information when checking the clauses
858	*/
859	options->verbosityLevel = BmcVerbosityNone_c;
860	result = BmcCheckSAT(options);
861	options->verbosityLevel = (Bmc_VerbosityLevel) savedVerbosityLevel;
862	if (options->satSolverError){
863	break;
864	}
865	if (options->verbosityLevel != BmcVerbosityNone_c){
866	endTime = util_cpu_ctime();
867	fprintf(vis_stdout, "-- checking time = %10g\n",
868	(double)(endTime - startTime) / 1000.0);
869	}
870	if (result == NIL(array_t)){ /* UNSAT */
871	formulaStatus = BmcPropertyPassed_c;
872	break; /* formula is satisfiable */
873	}
874	array_free(result);
875	} /* Check induction */
876
877	/* free all used memories
878	BmcCnfClausesFree(cnfClauses); */
879
880	bound += options->step;
881	} /* while result and bound */
882	if (bmcError == FALSE){
883	if(!options->satSolverError){
884	if(formulaStatus == BmcPropertyFailed_c) {
885	(void) fprintf(vis_stdout, "# BMC: formula failed\n");
886	if(options->verbosityLevel != BmcVerbosityNone_c){
887	(void) fprintf(vis_stdout,
888	"# BMC: Found a counterexample of length = %d \n", bound);
889	}
890	if (options->dbgLevel == 1) {
891	BmcPrintCounterExample(network, nodeToMvfAigTable, cnfClauses,
892	result, bound, CoiTable, options, outClause);
893	}
894	array_free(result);
895	BmcCnfClausesFree(cnfClauses);
896	array_free(outClause);
897	} else if(formulaStatus == BmcPropertyPassed_c) {
898	(void) fprintf(vis_stdout, "# BMC: formula Passed\n");
899	} else if(formulaStatus == BmcPropertyUndecided_c) {
900	(void) fprintf(vis_stdout,"# BMC: formula undecided\n");
901	if (options->verbosityLevel != BmcVerbosityNone_c){
902	(void) fprintf(vis_stdout,
903	"# BMC: no counterexample found of length up to %d \n",
904	options->maxK);
905	}
906	}
907	} else {
908	(void) fprintf(vis_stdout,"# BMC: Error in calling SAT solver\n");
909	}
910	}
911	if (options->verbosityLevel != BmcVerbosityNone_c) {
912	endTime = util_cpu_ctime();
913	fprintf(vis_stdout, "-- bmc time = %10g\n",
914	(double)(endTime - startTime) / 1000.0);
915	}
916	if(unitClause != NIL(array_t)) {
917	array_free(unitClause);
918	}
919	fflush(vis_stdout);
920	return;
921	} /* BmcLtlVerifyFp() */
922
923	/Function******************************************************************
924
925	Synopsis [Apply Bounded Model Checking (BMC) on an LTL formula of
926	the form FG(p), where p is propositional.]
927
928	Description [Given a model M, an LTL formula f = FGp, and a bound
929	k, we first find a k-loop counterexample of length k at which p
930	false inside the loop. If -r switch of the BMC command is
931	specified, we apply the method in the paper "Proving More
932	Properties with Bounded Model Checking" to check if the property f
933	passes.
934
935	Note: Before calling this function, the LTL formula must be negated.
936
937	]
938
939	SideEffects []
940
941	SeeAlso []
942
943	******************************************************************************/
944	void
945	BmcLtlVerifyFGp(
946	Ntk_Network_t *network,
947	Ctlsp_Formula_t *ltlFormula,
948	st_table *CoiTable,
949	BmcOption_t *options)
950	{
951	mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
952	st_table nodeToMvfAigTable = NIL(st_table); / node to mvfAig */
953	BmcCnfClauses_t *cnfClauses = NIL(BmcCnfClauses_t);
954	FILE *cnfFile;
955
956	array_t orClause, tmpClause, *loopClause;
957	int k, l, andIndex, loop;
958	array_t *result = NIL(array_t);
959	long startTime, endTime;
960	int minK = options->minK;
961	int maxK = options->maxK;
962	Ctlsp_Formula_t *propFormula;
963	bAigEdge_t property;
964
965	Bmc_PropertyStatus formulaStatus;
966	int bmcError = FALSE;
967
968	int m=-1, n=-1;
969	int checkLevel = 0;
970	/*
971	Refer to Theorem 1 in the paper "Proving More Properties with Bounded Model Checking"
972
973	If checkLevel == 0 --> check for beta' only. If UNSAT, m=k and chekLevel = 1
974	If checkLevel == 1 --> check for beta only. If UNSAT, checkLevel = 2.
975	If checkLevel == 2 --> check for alpha only. If UNSAT, n=k and checkLevel = 3.
976	If gama is UNSAT up to (m+n-1) and checkLvel = 3, formula passes.
977	checkLevel = 4 if (m+n-1) > maxK; */
978
979	/*
980	Remember the LTL property was negated
981	*/
982	assert(Ctlsp_LtlFormulaIsGFp(ltlFormula));
983
984	/* ************** */
985
986	/* Initialization */
987
988	/* ************** */
989	loopClause = NIL(array_t);
990	startTime = util_cpu_ctime();
991	/*
992	nodeToMvfAigTable maps each node to its multi-function And/Inv graph
993	*/
994	nodeToMvfAigTable =
995	(st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
996	if (nodeToMvfAigTable == NIL(st_table)){
997	(void) fprintf(vis_stderr,
998	"** bmc error: you need to build the AIG structure first\n");
999	return;
1000	}
1001	propFormula = Ctlsp_FormulaReadRightChild(Ctlsp_FormulaReadRightChild(ltlFormula));
1002	property = BmcCreateMaigOfPropFormula(network, manager, propFormula);
1003	if (options->verbosityLevel != BmcVerbosityNone_c){
1004	(void)fprintf(vis_stdout, "LTL formula is of type FG(p)\n");
1005	(void) fprintf(vis_stdout, "Apply BMC on counterexample of length >= %d and <= %d (+%d) \n",
1006	minK, maxK, options->step);
1007	}
1008	tmpClause = array_alloc(int, 2);
1009	k= minK;
1010	formulaStatus = BmcPropertyUndecided_c;
1011	while( (result == NIL(array_t)) && (k <= maxK)){
1012	/*
1013	Search for a k-loop counterexample of length k.
1014	*/
1015	if (options->verbosityLevel == BmcVerbosityMax_c) {
1016	(void) fprintf(vis_stdout, "\nGenerate counterexample of length %d\n", k);
1017	}
1018	/*
1019	Create a clause database
1020	*/
1021	cnfClauses = BmcCnfClausesAlloc();
1022
1023	cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
1024	if (cnfFile == NIL(FILE)) {
1025	(void)fprintf(vis_stderr,
1026	"** bmc error: Cannot create CNF output file %s\n",
1027	options->satInFile);
1028	bmcError = TRUE;
1029	break;
1030	}
1031
1032	/**********************************************
1033	\gama(k)
1034	***********************************************/
1035	/*
1036	Generate an initialized path of length k.
1037	*/
1038	BmcCnfGenerateClausesForPath(network, 0, k, BMC_INITIAL_STATES, cnfClauses, nodeToMvfAigTable, CoiTable);
1039	/*
1040	k-loop
1041	*/
1042	orClause = array_alloc(int, 0);
1043	loopClause = array_alloc(int, k+1);
1044	for(l=0; l<=k; l++){
1045	/*
1046	Use to check if there is a loop from k to l.
1047	*/
1048	loop = cnfClauses->cnfGlobalIndex++;
1049	BmcCnfGenerateClausesFromStateToState(network, k, l, cnfClauses, nodeToMvfAigTable, CoiTable, loop);
1050	array_insert(int, loopClause, l, loop);
1051
1052	andIndex = cnfClauses->cnfGlobalIndex++;
1053	array_insert(int, tmpClause, 0, loop);
1054	array_insert(int, tmpClause, 1, -andIndex);
1055	BmcCnfInsertClause(cnfClauses, tmpClause);
1056
1057	/*
1058	l
1059	If [[F p]] if p true in a state from l to k.
1060	k
1061	*/
1062	array_insert(int, tmpClause, 0,
1063	BmcGenerateCnfForLtl(network, Ctlsp_FormulaCreate(Ctlsp_F_c, propFormula, NIL(Ctlsp_Formula_t)),
1064	l, k, -1, cnfClauses));
1065	BmcCnfInsertClause(cnfClauses, tmpClause);
1066
1067	array_insert_last(int, orClause, andIndex);
1068	} /* for l loop */
1069	BmcCnfInsertClause(cnfClauses, orClause);
1070	array_free(orClause);
1071	BmcWriteClauses(manager, cnfFile, cnfClauses, options);
1072	(void) fclose(cnfFile);
1073
1074	result = BmcCheckSAT(options);
1075	if(options->satSolverError){
1076	break;
1077	}
1078	if(result != NIL(array_t)) {
1079	formulaStatus = BmcPropertyFailed_c;
1080	break;
1081	}
1082	array_free(loopClause);
1083	/* free all used memories */
1084	BmcCnfClausesFree(cnfClauses);
1085
1086	/* ====================================================================
1087	Use termination criteria to prove that the property passes.
1088	==================================================================== */
1089	if((result == NIL(array_t)) &&
1090	(options->inductiveStep !=0) &&
1091	(k % options->inductiveStep == 0)
1092	)
1093	{
1094	array_t *unitClause = array_alloc(int, 0);
1095	array_t *result = NIL(array_t);
1096	int savedVerbosityLevel = options->verbosityLevel;
1097
1098	options->verbosityLevel = BmcVerbosityNone_c;
1099	/* ===========================
1100	Early termination condition
1101	=========================== */
1102	if(options->earlyTermination){
1103	if (savedVerbosityLevel == BmcVerbosityMax_c) {
1104	(void) fprintf(vis_stdout, "\nChecking the early termination at k= %d\n", k);
1105	}
1106	cnfClauses = BmcCnfClausesAlloc();
1107
1108	cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
1109	if (cnfFile == NIL(FILE)) {
1110	(void)fprintf(vis_stderr,
1111	"** abmc error: Cannot create CNF output file %s\n",
1112	options->satInFile);
1113	bmcError = TRUE;
1114	break;
1115	}
1116	/*
1117	Generate an initialized simple path path of length k.
1118	*/
1119	BmcCnfGenerateClausesForLoopFreePath(network, 0, k, BMC_INITIAL_STATES,
1120	cnfClauses, nodeToMvfAigTable, CoiTable);
1121	BmcWriteClauses(manager, cnfFile, cnfClauses, options);
1122	(void) fclose(cnfFile);
1123	BmcCnfClausesFree(cnfClauses);
1124
1125	result = BmcCheckSAT(options);
1126	if(options->satSolverError){
1127	break;
1128	}
1129	if(result == NIL(array_t)) {
1130	formulaStatus = BmcPropertyPassed_c;
1131	if (savedVerbosityLevel == BmcVerbosityMax_c) {
1132	(void) fprintf(vis_stdout, "# BMC: By early termination\n");
1133	}
1134	break;
1135	}
1136	} /* Early termination */
1137
1138	/*
1139	Check \beta''(k)
1140	*/
1141	if(checkLevel == 0){
1142	int i;
1143
1144	cnfClauses = BmcCnfClausesAlloc();
1145	if (savedVerbosityLevel == BmcVerbosityMax_c) {
1146	(void) fprintf(vis_stdout, "# BMC: Check beta'' \n");
1147	}
1148	cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
1149	if (cnfFile == NIL(FILE)) {
1150	(void)fprintf(vis_stderr,
1151	"** bmc error: Cannot create CNF output file %s\n",
1152	options->satInFile);
1153	bmcError = TRUE;
1154	break;
1155	}
1156	/*
1157	Generate a simple path of length k+1.
1158	*/
1159	BmcCnfGenerateClausesForLoopFreePath(network, 0, k+1, BMC_NO_INITIAL_STATES,
1160	cnfClauses, nodeToMvfAigTable, CoiTable);
1161	for(i=1; i<=k+1; i++){
1162	array_insert(int, unitClause, 0,
1163	-BmcGenerateCnfFormulaForAigFunction(manager, property,
1164	i, cnfClauses));
1165	BmcCnfInsertClause(cnfClauses, unitClause);
1166	}
1167	array_insert(int, unitClause, 0,
1168	BmcGenerateCnfFormulaForAigFunction(manager, property,
1169	0, cnfClauses));
1170	BmcCnfInsertClause(cnfClauses, unitClause);
1171
1172	BmcWriteClauses(manager, cnfFile, cnfClauses, options);
1173	(void) fclose(cnfFile);
1174
1175	result = BmcCheckSAT(options);
1176	BmcCnfClausesFree(cnfClauses);
1177	if(options->satSolverError){
1178	break;
1179	}
1180	if(result == NIL(array_t)) {
1181	m = k;
1182	printf("Beta'': Value of m = %d\n", m);
1183	checkLevel = 1;
1184	}
1185	} /* Check for beta'' */
1186
1187	/*
1188	Check \beta'(k)
1189	*/
1190	if(checkLevel == 0){
1191	int i;
1192
1193	cnfClauses = BmcCnfClausesAlloc();
1194	if (savedVerbosityLevel == BmcVerbosityMax_c) {
1195	(void) fprintf(vis_stdout, "# BMC: Check beta' \n");
1196	}
1197	cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
1198	if (cnfFile == NIL(FILE)) {
1199	(void)fprintf(vis_stderr,
1200	"** bmc error: Cannot create CNF output file %s\n",
1201	options->satInFile);
1202	bmcError = TRUE;
1203	break;
1204	}
1205	/*
1206	Generate a simple path of length k+1.
1207	*/
1208	BmcCnfGenerateClausesForLoopFreePath(network, 0, k+1, BMC_NO_INITIAL_STATES,
1209	cnfClauses, nodeToMvfAigTable, CoiTable);
1210	for(i=0; i<=k; i++){
1211	array_insert(int, unitClause, 0,
1212	-BmcGenerateCnfFormulaForAigFunction(manager, property,
1213	i, cnfClauses));
1214	BmcCnfInsertClause(cnfClauses, unitClause);
1215	}
1216	array_insert(int, unitClause, 0,
1217	BmcGenerateCnfFormulaForAigFunction(manager, property,
1218	k+1, cnfClauses));
1219	BmcCnfInsertClause(cnfClauses, unitClause);
1220
1221	BmcWriteClauses(manager, cnfFile, cnfClauses, options);
1222	(void) fclose(cnfFile);
1223
1224	result = BmcCheckSAT(options);
1225	BmcCnfClausesFree(cnfClauses);
1226	if(options->satSolverError){
1227	break;
1228	}
1229	if(result == NIL(array_t)) {
1230	m = k;
1231	printf("Beta': Value of m = %d\n", m);
1232	checkLevel = 1;
1233	}
1234	} /* Check for beta' */
1235	/*
1236	Check for beta
1237	*/
1238	if(checkLevel == 1){
1239	cnfClauses = BmcCnfClausesAlloc();
1240	if (savedVerbosityLevel == BmcVerbosityMax_c) {
1241	(void) fprintf(vis_stdout, "# BMC: Check beta\n");
1242	}
1243	cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
1244	if (cnfFile == NIL(FILE)) {
1245	(void)fprintf(vis_stderr,
1246	"** bmc error: Cannot create CNF output file %s\n",
1247	options->satInFile);
1248	bmcError = TRUE;
1249	break;
1250	}
1251	/*
1252	Generate a simple path of length k+1.
1253	*/
1254	BmcCnfGenerateClausesForLoopFreePath(network, 0, k+1, BMC_NO_INITIAL_STATES,
1255	cnfClauses, nodeToMvfAigTable, CoiTable);
1256	array_insert(int, unitClause, 0,
1257	-BmcGenerateCnfFormulaForAigFunction(manager, property,
1258	k, cnfClauses));
1259	BmcCnfInsertClause(cnfClauses, unitClause);
1260	array_insert(int, unitClause, 0,
1261	BmcGenerateCnfFormulaForAigFunction(manager, property,
1262	k+1, cnfClauses));
1263	BmcCnfInsertClause(cnfClauses, unitClause);
1264
1265	BmcWriteClauses(manager, cnfFile, cnfClauses, options);
1266	(void) fclose(cnfFile);
1267
1268	result = BmcCheckSAT(options);
1269	BmcCnfClausesFree(cnfClauses);
1270	if(options->satSolverError){
1271	break;
1272	}
1273	if(result == NIL(array_t)) {
1274	checkLevel = 2;
1275	}
1276	} /* Check beta */
1277
1278	if(checkLevel == 2){ /* we check \alpha if \beta UNSAT */
1279	if (savedVerbosityLevel == BmcVerbosityMax_c) {
1280	(void) fprintf(vis_stdout, "# BMC: Check alpha \n");
1281	}
1282	/*
1283	\alpha(k)
1284	*/
1285	cnfClauses = BmcCnfClausesAlloc();
1286
1287	cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
1288	if (cnfFile == NIL(FILE)) {
1289	(void)fprintf(vis_stderr,
1290	"** bmc error: Cannot create CNF output file %s\n",
1291	options->satInFile);
1292	bmcError = TRUE;
1293	break;
1294	}
1295	/*
1296	Generate an initialized path of length k.
1297	*/
1298	BmcCnfGenerateClausesForLoopFreePath(network, 0, k, BMC_INITIAL_STATES,
1299	cnfClauses, nodeToMvfAigTable, CoiTable);
1300
1301	array_insert(int, unitClause, 0,
1302	BmcGenerateCnfFormulaForAigFunction(manager, property,
1303	k, cnfClauses));
1304	BmcCnfInsertClause(cnfClauses, unitClause);
1305
1306
1307	BmcWriteClauses(manager, cnfFile, cnfClauses, options);
1308	(void) fclose(cnfFile);
1309
1310	result = BmcCheckSAT(options);
1311	BmcCnfClausesFree(cnfClauses);
1312	if(options->satSolverError){
1313	break;
1314	}
1315	if(result == NIL(array_t)) {
1316	n = k;
1317	checkLevel = 3;
1318	printf("m=%d n=%d\n",m,n);
1319	if ((m+n-1) <= maxK){
1320	maxK = m+n-1;
1321	} else {
1322	checkLevel = 4;
1323	}
1324	}
1325	}/* Check alpha */
1326	array_free(unitClause);
1327	options->verbosityLevel = (Bmc_VerbosityLevel) savedVerbosityLevel;
1328	} /* Prove the property passes*/
1329	k += options->step;
1330	} /* while result and k*/
1331	if (bmcError == FALSE){
1332	if(options->satSolverError){
1333	(void) fprintf(vis_stdout,"# BMC: Error in calling SAT solver\n");
1334	} else {
1335	if(checkLevel == 3){
1336	(void) fprintf(vis_stdout, "# BMC: (m+n-1) Complete the theorem\n");
1337	formulaStatus = BmcPropertyPassed_c;
1338	}
1339	if(formulaStatus == BmcPropertyFailed_c) {
1340	(void) fprintf(vis_stdout, "# BMC: formula failed\n");
1341	if(options->verbosityLevel != BmcVerbosityNone_c){
1342	(void) fprintf(vis_stdout,
1343	"# BMC: Found a counterexample of length = %d \n", k);
1344	}
1345	if (options->dbgLevel == 1) {
1346	BmcPrintCounterExample(network, nodeToMvfAigTable, cnfClauses,
1347	result, k, CoiTable, options, loopClause);
1348	BmcCnfClausesFree(cnfClauses);
1349	array_free(loopClause);
1350	}
1351	} else if(formulaStatus == BmcPropertyPassed_c) {
1352	(void) fprintf(vis_stdout, "# BMC: formula Passed\n");
1353	} else if(formulaStatus == BmcPropertyUndecided_c) {
1354	(void) fprintf(vis_stdout,"# BMC: formula undecided\n");
1355	if (options->verbosityLevel != BmcVerbosityNone_c){
1356	(void) fprintf(vis_stdout,
1357	"# BMC: no counterexample found of length up to %d \n",
1358	maxK);
1359	}
1360	}
1361	}
1362	}
1363	/*
1364	free all used memories
1365	*/
1366	array_free(tmpClause);
1367
1368	if(result != NIL(array_t)){
1369	array_free(result);
1370	}
1371	if (options->verbosityLevel != BmcVerbosityNone_c) {
1372	endTime = util_cpu_ctime();
1373	fprintf(vis_stdout, "-- abmc time = %10g\n",
1374	(double)(endTime - startTime) / 1000.0);
1375	}
1376	fflush(vis_stdout);
1377	return;
1378	} /* BmcLtlVerifyGFp() */
1379
1380	/Function******************************************************************
1381
1382	Synopsis [Apply Bounded Model Checking (BMC) on an LTL formula of
1383	depth = 1]
1384
1385	Description [The depth of the LTL formula f is the maximum level of
1386	nesting of temporal operators in f. If the depth of the LTL
1387	formula = 1, the translation of the formula in case of loop is
1388	independent of the loop.
1389
1390	Note: Before calling this function, the LTL formula must be negated.
1391
1392	]
1393
1394	SideEffects []
1395
1396	SeeAlso []
1397
1398	******************************************************************************/
1399	void
1400	BmcLtlVerifyUnitDepth(
1401	Ntk_Network_t *network,
1402	Ctlsp_Formula_t *ltlFormula,
1403	st_table *CoiTable,
1404	BmcOption_t *options)
1405	{
1406	mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
1407	st_table nodeToMvfAigTable = NIL(st_table); / node to mvfAig */
1408	BmcCnfClauses_t *cnfClauses = NIL(BmcCnfClauses_t);
1409	FILE *cnfFile;
1410
1411	array_t *orClause =NIL(array_t);
1412	array_t loopClause, tmpclause;
1413	int l, loopIndex, andIndex, loop;
1414	int noLoopIndex;
1415	array_t *result = NIL(array_t);
1416
1417	int leftValue = 0;
1418	int rightValue = 0;
1419	long startTime, endTime;
1420	int k;
1421	int minK = options->minK;
1422	int maxK = options->maxK;
1423	/* Store the index of a loop from k to all sate from 0 to k */
1424
1425	Bmc_PropertyStatus formulaStatus;
1426	BmcCheckForTermination_t *terminationStatus = 0;
1427	int bmcStatus=0; /* Holds the status of running BMC
1428	= -1 if there is an error */
1429
1430	assert(Ctlsp_LtlFormulaDepth(ltlFormula) == 1);
1431
1432	/* ************** */
1433	/* Initialization */
1434	/* ************** */
1435
1436	startTime = util_cpu_ctime();
1437	/*
1438	nodeToMvfAigTable maps each node to its multi-function AIG graph
1439	*/
1440	nodeToMvfAigTable =
1441	(st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
1442	assert(nodeToMvfAigTable != NIL(st_table));
1443
1444	loopClause = NIL(array_t);
1445
1446	if (options->verbosityLevel != BmcVerbosityNone_c){
1447	(void) fprintf(vis_stdout, "Unit depth LTL formula\n");
1448	(void) fprintf(vis_stdout, "Apply BMC on counterexample of length >= %d and <= %d (+%d) \n",
1449	minK, maxK, options->step);
1450	}
1451	if(options->inductiveStep !=0){
1452	/*
1453	Use the termination criteria to prove the property passes.
1454	*/
1455	terminationStatus = BmcAutTerminationAlloc(network,
1456	Ctlsp_LtllFormulaNegate(ltlFormula),
1457	NIL(array_t));
1458	assert(terminationStatus);
1459	}
1460	k = minK;
1461	formulaStatus = BmcPropertyUndecided_c;
1462	while( (result == NIL(array_t)) && (k <= maxK)){
1463	if (options->verbosityLevel == BmcVerbosityMax_c) {
1464	(void) fprintf(vis_stdout, "\nGenerate counterexample of length %d\n", k);
1465	}
1466	/*
1467	Create clause database
1468	*/
1469	cnfClauses = BmcCnfClausesAlloc();
1470
1471	cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
1472	if (cnfFile == NIL(FILE)) {
1473	(void)fprintf(vis_stderr,
1474	"** bmc error: Cannot create CNF output file %s\n",
1475	options->satInFile);
1476	bmcStatus = -1;
1477	break;
1478	}
1479	/*
1480	Generate clauses represent an initialized path of length k
1481	*/
1482	BmcCnfGenerateClausesForPath(network, 0, k, BMC_INITIAL_STATES,
1483	cnfClauses, nodeToMvfAigTable, CoiTable);
1484	/*
1485	Generate clauses represent paths which satisfy the LTL formula if
1486	there is no loop.
1487	*/
1488	noLoopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, -1, cnfClauses);
1489	leftValue = checkIndex(noLoopIndex, cnfClauses);
1490	if (leftValue != 1) { /* no loop part of the basic encoding is not TRUE */
1491	orClause = array_alloc(int, 0);
1492	/*
1493	No need to check for !Lk in the basic encoding
1494	*/
1495	if (leftValue == -1){ /* no loop part of the basic encoding is not FALSE */
1496	array_insert_last(int, orClause, noLoopIndex);
1497	}
1498	/*
1499	Generate clauses represent paths which satisfy the LTL formula if
1500	there is a loop.
1501	*/
1502	loopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, 0, cnfClauses);
1503	rightValue = checkIndex(loopIndex, cnfClauses);
1504	if (rightValue == 0){ /* loop part of the basic encoding is FALSE */
1505	break;
1506	}
1507	/*
1508	rightValue can be 1 or -1
1509	leftValue can be 0 or -1
1510	*/
1511	if (noLoopIndex == loopIndex){ /* do not check for the existence of a loop*/
1512	break;
1513	}
1514	/*
1515	Clauses for loop-back path.
1516	*/
1517	loopClause = array_alloc(int, k+2);
1518	for(l=0; l<=k; l++){
1519	loop = cnfClauses->cnfGlobalIndex++;
1520	BmcCnfGenerateClausesFromStateToState(network, k, l, cnfClauses,
1521	nodeToMvfAigTable, CoiTable, loop);
1522	array_insert(int, loopClause, l, loop);
1523	} /* for l loop */
1524	loop = cnfClauses->cnfGlobalIndex++;
1525	array_insert(int, loopClause, k+1, -loop);
1526	BmcCnfInsertClause(cnfClauses, loopClause);
1527	if(rightValue == -1){
1528	andIndex = cnfClauses->cnfGlobalIndex++;
1529	tmpclause = array_alloc(int, 2);
1530
1531	array_insert(int, tmpclause, 0, loop);
1532	array_insert(int, tmpclause, 1, -andIndex);
1533	BmcCnfInsertClause(cnfClauses, tmpclause);
1534
1535	array_insert(int, tmpclause, 0, loopIndex);
1536	array_insert(int, tmpclause, 1, -andIndex);
1537	BmcCnfInsertClause(cnfClauses, tmpclause);
1538
1539	array_free(tmpclause);
1540	array_insert_last(int, orClause, andIndex);
1541	} else {
1542	array_insert_last(int, orClause, loop);
1543	}
1544	}
1545	/* if((leftValue == 1) \|\| (rightValue == 1)){ */
1546	if(leftValue == 1){
1547	assert(k==1);
1548	/*
1549	formula failed
1550	*/
1551	formulaStatus = BmcPropertyFailed_c;
1552	if (options->verbosityLevel != BmcVerbosityNone_c){
1553	(void) fprintf(vis_stdout,"# BMC: Empty counterexample because the property is always FALSE\n");
1554	}
1555	break;
1556	} else if((leftValue == 0) && (rightValue == 0)){
1557	if (options->verbosityLevel != BmcVerbosityNone_c){
1558	(void) fprintf(vis_stdout,"# BMC: the formula is trivially true");
1559	(void) fprintf(vis_stdout," for counterexamples of length %d\n", k);
1560	}
1561	} else {
1562	BmcCnfInsertClause(cnfClauses, orClause);
1563	array_free(orClause);
1564	BmcWriteClauses(manager, cnfFile, cnfClauses, options);
1565	(void) fclose(cnfFile);
1566
1567	result = BmcCheckSAT(options);
1568	if(options->satSolverError){
1569	break;
1570	}
1571	if(result != NIL(array_t)) {
1572	/*
1573	formula failed
1574	*/
1575	formulaStatus = BmcPropertyFailed_c;
1576	} else {
1577	/* free some used memories */
1578	BmcCnfClausesFree(cnfClauses);
1579	array_free(loopClause);
1580	/*
1581	Use the termination check
1582	*/
1583
1584	if(terminationStatus && (formulaStatus == BmcPropertyUndecided_c) && (bmcStatus != 1)){
1585	if((options->inductiveStep !=0) &&
1586	(k % options->inductiveStep == 0)
1587	)
1588	{
1589	/*
1590	Check for termination for the current value of k.
1591	*/
1592	terminationStatus->k = k;
1593	bmcStatus = BmcAutLtlCheckForTermination(network,
1594	NIL(array_t), terminationStatus,
1595	nodeToMvfAigTable, CoiTable, options);
1596	if(bmcStatus == 1){
1597	maxK = options->maxK;
1598	}
1599	if(bmcStatus == 3){
1600	formulaStatus = BmcPropertyPassed_c;
1601	break;
1602	}
1603	if(bmcStatus == -1){
1604	break;
1605	}
1606	}
1607	} /* terminationStatus */
1608	}
1609	}
1610	k += options->step;
1611	} /* while result and k*/
1612
1613	/*
1614	If no error.
1615	*/
1616	if(bmcStatus != -1){
1617	if(bmcStatus == 1){
1618	(void) fprintf(vis_stdout,
1619	"# BMC: no counterexample found of length up to %d \n", options->maxK);
1620	(void) fprintf(vis_stdout, "# BMC: By termination criterion (m+n-1)\n");
1621	formulaStatus = BmcPropertyPassed_c;
1622	}
1623	if(options->satSolverError){
1624	(void) fprintf(vis_stdout,"# BMC: Error in calling SAT solver\n");
1625	} else {
1626	if(formulaStatus == BmcPropertyFailed_c) {
1627	(void) fprintf(vis_stdout, "# BMC: formula failed\n");
1628	if(options->verbosityLevel != BmcVerbosityNone_c){
1629	(void) fprintf(vis_stdout,
1630	"# BMC: Found a counterexample of length = %d \n", k);
1631	}
1632	if ((options->dbgLevel == 1) && (result != NIL(array_t))) {
1633	BmcPrintCounterExample(network, nodeToMvfAigTable, cnfClauses,
1634	result, k, CoiTable, options, loopClause);
1635	}
1636	/* free some used memories */
1637	BmcCnfClausesFree(cnfClauses);
1638	array_free(loopClause);
1639	array_free(result);
1640	} else if(formulaStatus == BmcPropertyPassed_c) {
1641	(void) fprintf(vis_stdout, "# BMC: formula Passed\n");
1642	(void) fprintf(vis_stdout, "# Termination depth = %d\n", maxK);
1643	} else if(formulaStatus == BmcPropertyUndecided_c) {
1644	(void) fprintf(vis_stdout,"# BMC: formula undecided\n");
1645	if (options->verbosityLevel != BmcVerbosityNone_c){
1646	(void) fprintf(vis_stdout,
1647	"# BMC: no counterexample found of length up to %d \n",
1648	maxK);
1649	}
1650	}
1651	}
1652	}
1653	if (options->verbosityLevel != BmcVerbosityNone_c) {
1654	endTime = util_cpu_ctime();
1655	fprintf(vis_stdout, "-- bmc time = %10g\n",
1656	(double)(endTime - startTime) / 1000.0);
1657	}
1658	if(terminationStatus){
1659	BmcAutTerminationFree(terminationStatus);
1660	}
1661	fflush(vis_stdout);
1662	return;
1663	} /* Bmc_VerifyUnitDepth() */
1664
1665	/Function******************************************************************
1666
1667	Synopsis [Use BMC to verify a general LTL formulae]
1668
1669	Description [Implements the Bounded Model Checking technique as in the paper
1670	"Symbolic Model Checking without BDDs". We also have implemented some of the
1671	improvements in the BMC encoding described in the paper "Improving the
1672	Encoding of LTL Model Checking into SAT" ]
1673
1674	SideEffects []
1675
1676	SeeAlso []
1677
1678	******************************************************************************/
1679	void
1680	BmcLtlVerifyGeneralLtl(
1681	Ntk_Network_t *network,
1682	Ctlsp_Formula_t *ltlFormula,
1683	st_table *CoiTable,
1684	array_t *constraintArray,
1685	BmcOption_t *options)
1686	{
1687	mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
1688	st_table nodeToMvfAigTable = NIL(st_table); / node to mvfAig */
1689	BmcCnfClauses_t *cnfClauses = NIL(BmcCnfClauses_t);
1690	FILE *cnfFile;
1691
1692	array_t *orClause = NIL(array_t);
1693	array_t loopClause, tmpclause;
1694	int l, loopIndex, andIndex, loop;
1695	int noLoopIndex;
1696	array_t *result = NIL(array_t);
1697	array_t *fairnessArray = NIL(array_t);
1698	int leftValue = 0;
1699	int rightValue = 0;
1700	long startTime, endTime;
1701	int k;
1702	int minK = options->minK;
1703	int maxK = options->maxK;
1704	boolean boundedFormula;
1705	int depth;
1706	/* Store the index of loop from k to all sate from 0 to k */
1707
1708	array_t ltlConstraintArray; / constraints converted to LTL */
1709	int f;
1710	boolean fairness = (constraintArray != NIL(array_t));
1711
1712	BmcCheckForTermination_t *terminationStatus = 0;
1713	Bmc_PropertyStatus formulaStatus;
1714	int bmcStatus=0; /* Holds the status of running BMC
1715	= -1 if there is an error */
1716
1717	/* ************** */
1718	/* Initialization */
1719	/* ************** */
1720	startTime = util_cpu_ctime();
1721	/*
1722	nodeToMvfAigTable maps each node to its multi-function And/Inv graph
1723	*/
1724	nodeToMvfAigTable =
1725	(st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
1726	assert(nodeToMvfAigTable != NIL(st_table));
1727
1728	loopClause = NIL(array_t);
1729	noLoopIndex = 0;
1730	ltlConstraintArray = NIL(array_t);
1731	if(fairness){
1732	Ctlsp_Formula_t *formula;
1733	int i;
1734	/*
1735	All formulae in constraintArray are propositional, propositional
1736	constraint.
1737	*/
1738	ltlConstraintArray = array_alloc(Ctlsp_Formula_t *, 0);
1739	arrayForEachItem(Ctlsp_Formula_t *, constraintArray, i, formula) {
1740	/*
1741	To help making propositional constraint easy to encode.
1742	*/
1743	formula = Ctlsp_FormulaCreate(Ctlsp_F_c, formula, NIL(Ctlsp_Formula_t));
1744	array_insert(Ctlsp_Formula_t *, ltlConstraintArray, i, formula);
1745	BmcGetCoiForLtlFormula(network, formula, CoiTable);
1746	}
1747	}
1748	/*
1749	For bounded formulae use a tighter upper bound if possible.
1750	*/
1751	boundedFormula = Ctlsp_LtlFormulaTestIsBounded(ltlFormula, &depth);
1752	if (boundedFormula && depth < maxK && depth >= minK) {
1753	maxK = depth;
1754	} else {
1755	if(options->inductiveStep !=0){
1756	/*
1757	Use the termination criteria to prove the property passes.
1758	*/
1759	terminationStatus = BmcAutTerminationAlloc(network,
1760	Ctlsp_LtllFormulaNegate(ltlFormula),
1761	constraintArray);
1762	assert(terminationStatus);
1763	}
1764	}
1765	if (options->verbosityLevel != BmcVerbosityNone_c){
1766	(void) fprintf(vis_stdout, "General LTL BMC\n");
1767	if (boundedFormula){
1768	(void) fprintf(vis_stdout, "Bounded formula of depth %d\n", depth);
1769	}
1770	(void) fprintf(vis_stdout, "Apply BMC on counterexample of length >= %d and <= %d (+%d) \n",
1771	minK, maxK, options->step);
1772	}
1773	k= minK;
1774	formulaStatus = BmcPropertyUndecided_c;
1775	while( (result == NIL(array_t)) && (k <= maxK)){
1776	if (options->verbosityLevel == BmcVerbosityMax_c) {
1777	(void) fprintf(vis_stdout, "\nGenerate counterexample of length %d\n", k);
1778	}
1779
1780	cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
1781	if (cnfFile == NIL(FILE)) {
1782	(void)fprintf(vis_stderr,
1783	"** bmc error: Cannot create CNF output file %s\n",
1784	options->satInFile);
1785	bmcStatus = -1;
1786	break;
1787	}
1788	/*
1789	Create a clause database
1790	*/
1791	cnfClauses = BmcCnfClausesAlloc();
1792	/*
1793	Gnerate clauses for an initialized path of length k
1794	*/
1795	BmcCnfGenerateClausesForPath(network, 0, k, BMC_INITIAL_STATES,
1796	cnfClauses, nodeToMvfAigTable, CoiTable);
1797
1798	if(!fairness){ /* No fairness constraint */
1799	noLoopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, -1, cnfClauses);
1800	leftValue = checkIndex(noLoopIndex, cnfClauses);
1801	} else {
1802	leftValue = 0; /* the path must have a loop*/
1803	}
1804	if (leftValue != 1) {
1805	orClause = array_alloc(int, 0);
1806	/*
1807	No need to check for !Lk in the basic encoding
1808	*/
1809	if (leftValue == -1){
1810	array_insert_last(int, orClause, noLoopIndex);
1811	}
1812	loopClause = array_alloc(int, k+1);
1813
1814	for(l=0; l<=k; l++){
1815	loopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, l, cnfClauses);
1816	rightValue = checkIndex(loopIndex, cnfClauses);
1817	if (rightValue == 0){
1818	break;
1819	}
1820	if(fairness){
1821	Ctlsp_Formula_t *formula;
1822	int i;
1823
1824	fairnessArray = array_alloc(int, 0);
1825	arrayForEachItem(Ctlsp_Formula_t *, ltlConstraintArray, i, formula) {
1826	array_insert_last(int, fairnessArray,
1827	BmcGenerateCnfForLtl(network, formula, l, k, -1, cnfClauses));
1828	}
1829	}
1830	if (rightValue !=0){
1831	loop = cnfClauses->cnfGlobalIndex++;
1832	BmcCnfGenerateClausesFromStateToState(network, k, l, cnfClauses,
1833	nodeToMvfAigTable, CoiTable, loop);
1834	array_insert(int, loopClause, l, loop);
1835	if(rightValue == -1){
1836
1837	andIndex = cnfClauses->cnfGlobalIndex++;
1838	tmpclause = array_alloc(int, 2);
1839	array_insert(int, tmpclause, 0, loop);
1840	array_insert(int, tmpclause, 1, -andIndex);
1841	BmcCnfInsertClause(cnfClauses, tmpclause);
1842
1843	array_insert(int, tmpclause, 0, loopIndex);
1844	array_insert(int, tmpclause, 1, -andIndex);
1845	BmcCnfInsertClause(cnfClauses, tmpclause);
1846
1847	if(fairness){
1848	for(f=0; f < array_n(fairnessArray); f++){
1849	array_insert(int, tmpclause, 0, array_fetch(int, fairnessArray, f));
1850	array_insert(int, tmpclause, 1, -andIndex);
1851	BmcCnfInsertClause(cnfClauses, tmpclause);
1852	}
1853	}
1854	array_free(tmpclause);
1855	array_insert_last(int, orClause, andIndex);
1856	} else {
1857	array_insert_last(int, orClause, loop);
1858	}
1859	}
1860	if(fairness){
1861	array_free(fairnessArray);
1862	}
1863	} /* for l loop */
1864	}
1865	if((leftValue == 1) \|\| (rightValue == 1)){
1866	assert(k==1);
1867	if (options->verbosityLevel != BmcVerbosityNone_c){
1868	formulaStatus = BmcPropertyFailed_c;
1869	(void) fprintf(vis_stdout,"# BMC: Empty counterexample because the property is always FALSE\n");
1870	}
1871	break;
1872	} else if((leftValue == 0) && (rightValue == 0)){
1873	if (options->verbosityLevel != BmcVerbosityNone_c){
1874	(void) fprintf(vis_stdout,"# BMC: the formula is trivially true");
1875	(void) fprintf(vis_stdout," for counterexamples of length %d\n", k);
1876	}
1877	} else {
1878	/*
1879	BmcCnfInsertClause(cnfClauses, loopClause);
1880	*/
1881	BmcCnfInsertClause(cnfClauses, orClause);
1882	/*
1883	array_free(loopClause);
1884	*/
1885	array_free(orClause);
1886	BmcWriteClauses(manager, cnfFile, cnfClauses, options);
1887	(void) fclose(cnfFile);
1888
1889	result = BmcCheckSAT(options);
1890	if(options->satSolverError){
1891	break;
1892	}
1893	if(result != NIL(array_t)) {
1894	/*
1895	formula failed\n"
1896	*/
1897	formulaStatus = BmcPropertyFailed_c;
1898	break;
1899	}
1900	array_free(loopClause);
1901	}
1902	/* free all used memories */
1903	BmcCnfClausesFree(cnfClauses);
1904	cnfClauses = NIL(BmcCnfClauses_t);
1905
1906	/*
1907	Use the termination check if the the LTL formula is not bounded
1908	*/
1909	if(terminationStatus && (formulaStatus == BmcPropertyUndecided_c) && (bmcStatus != 1)){
1910	if((options->inductiveStep !=0) &&
1911	(k % options->inductiveStep == 0)
1912	)
1913	{
1914	/*
1915	Check for termination for the current value of k.
1916	*/
1917	terminationStatus->k = k;
1918	bmcStatus = BmcAutLtlCheckForTermination(network,
1919	constraintArray, terminationStatus,
1920	nodeToMvfAigTable, CoiTable, options);
1921	if(bmcStatus == 1){
1922	maxK = terminationStatus->k;
1923	}
1924	if(bmcStatus == 3){
1925	formulaStatus = BmcPropertyPassed_c;
1926	break;
1927	}
1928	if(bmcStatus == -1){
1929	break;
1930	}
1931	}
1932	} /* terminationStatus */
1933	k += options->step;
1934	} /* while result and k*/
1935
1936	/*
1937	If no error.
1938	*/
1939	if(bmcStatus != -1){
1940	/*
1941	if(result == NIL(array_t)){
1942	*/
1943	if(formulaStatus == BmcPropertyUndecided_c){
1944	if(bmcStatus == 1){
1945	(void) fprintf(vis_stdout,
1946	"# BMC: no counterexample found of length up to %d \n", maxK);
1947	(void) fprintf(vis_stdout, "# BMC: By termination criterion (m+n-1)\n");
1948	formulaStatus = BmcPropertyPassed_c;
1949	}
1950	if (boundedFormula && depth <= options->maxK){
1951	(void) fprintf(vis_stdout,
1952	"# BMC: no counterexample found of length up to %d \n", depth);
1953	formulaStatus = BmcPropertyPassed_c;
1954	}
1955	}
1956	if(options->satSolverError){
1957	(void) fprintf(vis_stdout,"# BMC: Error in calling SAT solver\n");
1958	} else {
1959	if(formulaStatus == BmcPropertyFailed_c) {
1960	(void) fprintf(vis_stdout, "# BMC: formula failed\n");
1961	if(options->verbosityLevel != BmcVerbosityNone_c){
1962	(void) fprintf(vis_stdout,
1963	"# BMC: Found a counterexample of length = %d \n", k);
1964	}
1965	if ((options->dbgLevel == 1) && (result != NIL(array_t))) {
1966	BmcPrintCounterExample(network, nodeToMvfAigTable, cnfClauses,
1967	result, k, CoiTable, options, loopClause);
1968	}
1969	/BmcCnfClausesFree(cnfClauses);/
1970	array_free(loopClause);
1971	} else if(formulaStatus == BmcPropertyPassed_c) {
1972	(void) fprintf(vis_stdout, "# BMC: formula Passed\n");
1973	(void) fprintf(vis_stdout, "# Termination depth = %d\n", maxK);
1974	} else if(formulaStatus == BmcPropertyUndecided_c) {
1975	(void) fprintf(vis_stdout,"# BMC: formula undecided\n");
1976	if (options->verbosityLevel != BmcVerbosityNone_c){
1977	(void) fprintf(vis_stdout,
1978	"# BMC: no counterexample found of length up to %d \n",
1979	maxK);
1980	}
1981	}
1982	}
1983	}
1984	if (options->verbosityLevel != BmcVerbosityNone_c) {
1985	endTime = util_cpu_ctime();
1986	fprintf(vis_stdout, "-- bmc time = %10g\n",
1987	(double)(endTime - startTime) / 1000.0);
1988	}
1989	/*
1990	free all used memories
1991	*/
1992	if(terminationStatus){
1993	BmcAutTerminationFree(terminationStatus);
1994	}
1995	if(result != NIL(array_t)){
1996	array_free(result);
1997	}
1998	if(cnfClauses != NIL(BmcCnfClauses_t)){
1999	BmcCnfClausesFree(cnfClauses);
2000	}
2001	if(fairness){
2002	/Ctlsp_FormulaArrayFree(ltlConstraintArray);/
2003	}
2004	fflush(vis_stdout);
2005	return;
2006	} /* BmcLtlVerifyGeneralLtl() */
2007
2008	/Function******************************************************************
2009
2010	Synopsis [Generate CNF for an LTL formula]
2011
2012	Description [Generate array of clauses for a trnasition from state i to
2013	state k. If l is non-zero, it will also generate the clauses
2014	from state l to state i.
2015
2016	if the clause array is empty {}, the propety is always TRUE
2017	if the the clause array has one empty clause {{}}, the property
2018	is always FALSE.
2019	return the clause index number.
2020	]
2021
2022	SideEffects []
2023
2024	SeeAlso []
2025
2026	******************************************************************************/
2027	int
2028	BmcGenerateCnfForLtl(
2029	Ntk_Network_t *network,
2030	Ctlsp_Formula_t *ltlFormula,
2031	int i /* from state i */,
2032	int k /* to state k */,
2033	int l /* loop */,
2034	BmcCnfClauses_t *cnfClauses)
2035	{
2036	int left, right, cnfIndex;
2037	int andIndex, orIndex;
2038	int j, n;
2039	int leftValue, rightValue, andValue, orValue;
2040
2041	mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
2042	array_t clause, tmpclause, orClause, rightClause, *leftClause;
2043	BmcCnfStates_t *state;
2044
2045	assert(ltlFormula != NIL(Ctlsp_Formula_t));
2046	right = 0;
2047	rightValue = 0;
2048
2049	if(Ctlsp_isPropositionalFormula(ltlFormula)){
2050	bAigEdge_t property = BmcCreateMaigOfPropFormula(network, manager, ltlFormula);
2051
2052	if (property == bAig_Zero){ /* FALSE */
2053	/* add an empty clause to indicate FALSE property */
2054	BmcAddEmptyClause(cnfClauses);
2055	return 0;
2056	}
2057	if (property == bAig_One){ /* TRUE */
2058	/* Don't generate any clause to indicate TRUE property.*/
2059	return 0;
2060	}
2061	/* Generate the clause of the propositional formula */
2062	/* The state of the input variables is the same as the state of the state variables. */
2063	cnfIndex = BmcGenerateCnfFormulaForAigFunction(manager, property, i, cnfClauses);
2064	return cnfIndex;
2065	}
2066	/*
2067	* Formula is NOT propositional formula
2068	*/
2069	switch(ltlFormula->type) {
2070	case Ctlsp_NOT_c:
2071	/* reach here if formula-left is always not propositional*/
2072	/* NOT must only appears infront of a propositional formula.*/
2073	if (!Ctlsp_isPropositionalFormula(ltlFormula->left)){
2074	fprintf(vis_stderr,"BMC error: the LTL formula is not in NNF\n");
2075	return 0;
2076	}
2077	/*
2078	return -1*BmcGenerateCnfForLtlNoLoop(network, ltlFormula->left, i, k,
2079	cnfIndexTable, clauseArray);
2080	*/
2081	break;
2082	case Ctlsp_AND_c:
2083	/*
2084	c = a * b --> (!a + !b + c) * (a + !c) * (b + !c).
2085	Because a and b must be one, so we need only the last two clauses.
2086	*/
2087
2088	state = BmcCnfClausesFreeze(cnfClauses);
2089	rightValue = 1;
2090
2091	left = BmcGenerateCnfForLtl(network, ltlFormula->left, i, k, l, cnfClauses);
2092	leftValue = checkIndex(left, cnfClauses);
2093
2094	if (leftValue !=0){
2095	right = BmcGenerateCnfForLtl(network, ltlFormula->right, i, k, l, cnfClauses);
2096	rightValue = checkIndex(right, cnfClauses);
2097	}
2098	if ((leftValue == 0) \|\| (rightValue == 0)){
2099	/* restore the information */
2100	BmcCnfClausesRestore(cnfClauses, state);
2101	/* add an empty clause*/
2102	BmcAddEmptyClause(cnfClauses);
2103	FREE(state);
2104	return 0; /* FALSE */
2105	}
2106	if ((leftValue == 1) && (rightValue == 1)){
2107	/* restore the information */
2108	BmcCnfClausesRestore(cnfClauses, state);
2109	FREE(state);
2110	return 0; /* TRUE */
2111	}
2112	BmcCnfClausesUnFreeze(cnfClauses, state);
2113	FREE(state);
2114	/*
2115	tmpclause = array_alloc(int, 3);
2116	array_insert(int, tmpclause, 0, -left);
2117	array_insert(int, tmpclause, 1, -right);
2118	array_insert(int, tmpclause, 2, cnfIndex);
2119	array_insert_last(array_t *, clauseArray, tmpclause);
2120	*/
2121	if (leftValue == 1){
2122	return right;
2123	}
2124	if (rightValue == 1){
2125	return left;
2126	}
2127	cnfIndex = cnfClauses->cnfGlobalIndex++;
2128	tmpclause = array_alloc(int, 2);
2129
2130	array_insert(int, tmpclause, 0, left);
2131	array_insert(int, tmpclause, 1, -cnfIndex);
2132	BmcCnfInsertClause(cnfClauses, tmpclause);
2133
2134	array_insert(int, tmpclause, 0, right);
2135	array_insert(int, tmpclause, 1, -cnfIndex);
2136	BmcCnfInsertClause(cnfClauses, tmpclause);
2137	array_free(tmpclause);
2138
2139	return cnfIndex;
2140	case Ctlsp_OR_c:
2141	/*
2142	c = a + b --> (a + b + !c) * (!a + c) * (!b + c).
2143	Because a and b must be one, so we need only the first clause.
2144	*/
2145	state = BmcCnfClausesFreeze(cnfClauses);
2146
2147	left = BmcGenerateCnfForLtl(network, ltlFormula->left, i, k, l, cnfClauses);
2148	leftValue = checkIndex(left, cnfClauses);
2149
2150	if (leftValue !=1){
2151	right = BmcGenerateCnfForLtl(network, ltlFormula->right, i, k, l, cnfClauses);
2152	rightValue = checkIndex(right, cnfClauses);
2153	}
2154	if ((leftValue == 1) \|\| (rightValue == 1)){
2155	/* restore the information */
2156	BmcCnfClausesRestore(cnfClauses, state);
2157	FREE(state);
2158	return 0; /* TRUE */
2159	}
2160	if ((leftValue == 0) && (rightValue == 0)){
2161	/* restore the information */
2162	BmcCnfClausesRestore(cnfClauses, state);
2163	/* add an empty clause*/
2164	BmcAddEmptyClause(cnfClauses);
2165	FREE(state);
2166	return 0; /* FALSE */
2167	}
2168	BmcCnfClausesUnFreeze(cnfClauses, state);
2169	FREE(state);
2170	/* Either leftValue or rightValue = 0 and the other != 1
2171	At least one clause will be added
2172	*/
2173	if (leftValue == 0){
2174	return right;
2175	}
2176	if (rightValue == 0){
2177	return left;
2178	}
2179	cnfIndex = cnfClauses->cnfGlobalIndex++;
2180
2181	tmpclause = array_alloc(int, 0);
2182	array_insert_last(int, tmpclause, -cnfIndex);
2183
2184	array_insert_last(int, tmpclause, left);
2185	/*
2186	tmpclause = array_alloc(int, 2);
2187	array_insert(int, tmpclause, 0, -left);
2188	array_insert(int, tmpclause, 1, cnfIndex);
2189	array_insert_last(array_t *, clauseArray, tmpclause);
2190	*/
2191	array_insert_last(int, tmpclause, right);
2192	/*
2193	tmpclause = array_alloc(int, 2);
2194	array_insert(int, tmpclause, 0, -right);
2195	array_insert(int, tmpclause, 1, cnfIndex);
2196	array_insert_last(array_t *, clauseArray, tmpclause);
2197	*/
2198	BmcCnfInsertClause(cnfClauses, tmpclause);
2199	array_free(tmpclause);
2200
2201	return cnfIndex;
2202	case Ctlsp_F_c:
2203	if (l >= 0){ /* loop */
2204	i = (l < i)? l: i;
2205	}
2206	cnfIndex = cnfClauses->cnfGlobalIndex++;
2207	clause = array_alloc(int, 0);
2208	for (j=i; j<= k; j++){
2209	left = BmcGenerateCnfForLtl(network, ltlFormula->left, j, k, l, cnfClauses);
2210	leftValue = checkIndex(left, cnfClauses);
2211	if (leftValue != -1){
2212	array_free(clause);
2213	return 0;
2214	}
2215	array_insert_last(int, clause, left);
2216	/*
2217	tmpclause = array_alloc(int, 2);
2218	array_insert(int, tmpclause, 1, cnfIndex);
2219	array_insert(int, tmpclause, 0, -left);
2220	array_insert_last(array_t *, clauseArray, tmpclause);
2221	*/
2222	}
2223	array_insert_last(int, clause, -cnfIndex);
2224	BmcCnfInsertClause(cnfClauses, clause);
2225	array_free(clause);
2226
2227	return cnfIndex;
2228	case Ctlsp_G_c:
2229	if (l < 0){ /* FALSE */
2230	/* add an empty clause */
2231	BmcAddEmptyClause(cnfClauses);
2232	return 0;
2233	} else {
2234	i = (l < i)? l: i;
2235	andIndex = cnfClauses->cnfGlobalIndex++;
2236	for (j=i; j<= k; j++){
2237	left = BmcGenerateCnfForLtl(network, ltlFormula->left, j, k, l, cnfClauses);
2238	leftValue = checkIndex(left, cnfClauses);
2239	if (leftValue != -1){
2240	return 0;
2241	}
2242	tmpclause = array_alloc(int, 2);
2243	array_insert(int, tmpclause, 0, left);
2244	array_insert(int, tmpclause, 1, -andIndex);
2245	BmcCnfInsertClause(cnfClauses, tmpclause);
2246	array_free(tmpclause);
2247	}/* for j loop*/
2248	} /* else */
2249	return andIndex;
2250	case Ctlsp_X_c:
2251	/* X left */
2252	if((l >= 0) && (i == k) ){
2253	i = l;
2254	} else if (i < k){
2255	i = i + 1;
2256	} else { /* FALSE */
2257	/* add an empty clause */
2258	BmcAddEmptyClause(cnfClauses);
2259	return 0;
2260	}
2261	return BmcGenerateCnfForLtl(network, ltlFormula->left, i, k, l, cnfClauses);
2262	case Ctlsp_U_c: /* (left U right) */
2263	state = BmcCnfClausesFreeze(cnfClauses);
2264
2265	leftValue = 1; /* left is TRUE*/
2266	rightValue = 1; /* right is TRUE*/
2267	orIndex = cnfClauses->cnfGlobalIndex++;
2268	orClause = array_alloc(int, 0);
2269	array_insert_last(int, orClause, -orIndex);
2270
2271	orValue = 0;
2272	for (j=i; j<= k; j++){
2273	right = BmcGenerateCnfForLtl(network, ltlFormula->right, j, k, l, cnfClauses);
2274	rightValue = checkIndex(right, cnfClauses);
2275	andIndex = cnfClauses->cnfGlobalIndex++;
2276	if (rightValue == -1){
2277	rightClause = array_alloc(int, 2);
2278	array_insert(int, rightClause, 0, right);
2279	array_insert(int, rightClause, 1, -andIndex);
2280	BmcCnfInsertClause(cnfClauses, rightClause);
2281	array_free(rightClause);
2282	}
2283	andValue = rightValue;
2284	for (n=i; (n <= j-1) && (andValue != 0); n++){
2285	left = BmcGenerateCnfForLtl(network, ltlFormula->left, n, k, l, cnfClauses);
2286	leftValue = checkIndex(left, cnfClauses);
2287	andValue = doAnd(andValue, leftValue);
2288	if (leftValue == -1){
2289	leftClause = array_alloc(int, 2);
2290	array_insert(int, leftClause, 0, left);
2291	array_insert(int, leftClause, 1, -andIndex);
2292	BmcCnfInsertClause(cnfClauses, leftClause);
2293	array_free(leftClause);
2294	}
2295	} /* for n loop */
2296	orValue = doOr(orValue, andValue);
2297	if (orValue == 1){ /* TRUE */
2298	break;
2299	}
2300	if (andValue != 0){
2301	array_insert_last(int, orClause, andIndex);
2302	}
2303	} /* for j loop*/
2304	if ( (l >=0) && (orValue !=1)){ /* loop */
2305	for (j=l; j<= i-1; j++){
2306	right = BmcGenerateCnfForLtl(network, ltlFormula->right, j, k, l, cnfClauses);
2307	rightValue = checkIndex(right, cnfClauses);
2308	andIndex = cnfClauses->cnfGlobalIndex++;
2309	if (rightValue == -1){
2310	rightClause = array_alloc(int, 2);
2311	array_insert(int, rightClause, 0, right);
2312	array_insert(int, rightClause, 1, -andIndex);
2313	BmcCnfInsertClause(cnfClauses, rightClause);
2314	array_free(rightClause);
2315	}
2316	andValue = rightValue;
2317	for (n=i; (n<= k) && (andValue != 0); n++){
2318	left = BmcGenerateCnfForLtl(network, ltlFormula->left, n, k, l, cnfClauses);
2319	leftValue = checkIndex(left, cnfClauses);
2320	andValue = doAnd(andValue, leftValue);
2321	if (leftValue == -1){
2322	leftClause = array_alloc(int, 2);
2323	array_insert(int, leftClause, 0, left);
2324	array_insert(int, leftClause, 1, -andIndex);
2325	BmcCnfInsertClause(cnfClauses, leftClause);
2326	array_free(leftClause);
2327	}
2328	} /* for n loop */
2329	for (n=l; (n<= j-1) && (andValue != 0); n++){
2330	left = BmcGenerateCnfForLtl(network, ltlFormula->left, n, k, l, cnfClauses);
2331	leftValue = checkIndex(left, cnfClauses);
2332	andValue = doAnd(andValue, leftValue);
2333	if (leftValue == -1){
2334	leftClause = array_alloc(int, 2);
2335	array_insert(int, leftClause, 0, left);
2336	array_insert(int, leftClause, 1, -andIndex);
2337	BmcCnfInsertClause(cnfClauses, leftClause);
2338	array_free(leftClause);
2339	}
2340	} /* for n loop */
2341	orValue = doOr(orValue, andValue);
2342	if (orValue == 1){ /* TRUE */
2343	break;
2344	}
2345	if (andValue != 0){
2346	array_insert_last(int, orClause, andIndex);
2347	}
2348	}/* j loop*/
2349	} /* if (l>=0) */
2350	if ((orValue == 1) \|\| (orValue == 0)){
2351	/restore the infomration back/
2352	BmcCnfClausesRestore(cnfClauses, state);
2353	FREE(state);
2354	array_free(orClause);
2355	if (orValue == 0){
2356	/* add an empty clause*/
2357	BmcAddEmptyClause(cnfClauses);
2358	}
2359	return 0;
2360	} else {
2361	BmcCnfClausesUnFreeze(cnfClauses, state);
2362	FREE(state);
2363	BmcCnfInsertClause(cnfClauses, orClause);
2364	array_free(orClause);
2365	return orIndex;
2366	}
2367	case Ctlsp_R_c:
2368	/* (left R right) */
2369	state = BmcCnfClausesFreeze(cnfClauses);
2370
2371	orIndex = cnfClauses->cnfGlobalIndex++;
2372	orClause = array_alloc(int, 0);
2373	array_insert_last(int, orClause, -orIndex);
2374
2375	orValue = 0;
2376	if (l >= 0){ /* loop */
2377	andIndex = cnfClauses->cnfGlobalIndex++;
2378	andValue = 1;
2379	for (j=(i<l?i:l); (j<= k) && (andValue != 0); j++){
2380	right = BmcGenerateCnfForLtl(network, ltlFormula->right, j, k, l, cnfClauses);
2381	rightValue = checkIndex(right, cnfClauses);
2382	andValue = doAnd(andValue, rightValue);
2383	if (rightValue == -1){
2384	rightClause = array_alloc(int, 2);
2385	array_insert(int, rightClause, 0, right);
2386	array_insert(int, rightClause, 1, -andIndex);
2387	BmcCnfInsertClause(cnfClauses, rightClause);
2388	array_free(rightClause);
2389	}
2390	} /* for j loop*/
2391	if (andValue == -1){
2392	array_insert_last(int, orClause, andIndex);
2393	}
2394	orValue = doOr(orValue, andValue);
2395	} /* loop */
2396	if(orValue != 1){
2397	for (j=i; j<= k; j++){
2398	left = BmcGenerateCnfForLtl(network, ltlFormula->left,
2399	j, k, l, cnfClauses);
2400	leftValue = checkIndex(left, cnfClauses);
2401	andIndex = cnfClauses->cnfGlobalIndex++;
2402	if (leftValue == -1){
2403	leftClause = array_alloc(int, 2);
2404	array_insert(int, leftClause, 0, left);
2405	array_insert(int, leftClause, 1, -andIndex);
2406	BmcCnfInsertClause(cnfClauses, leftClause);
2407	array_free(leftClause);
2408	}
2409	andValue = leftValue;
2410	for (n=i; (n<= j) && (andValue != 0); n++){
2411	right = BmcGenerateCnfForLtl(network, ltlFormula->right,
2412	n, k, l, cnfClauses);
2413	rightValue = checkIndex(right, cnfClauses);
2414	andValue = doAnd(andValue, rightValue);
2415	if (rightValue == -1){
2416	rightClause = array_alloc(int, 2);
2417	array_insert(int, rightClause, 0, right);
2418	array_insert(int, rightClause, 1, -andIndex);
2419	BmcCnfInsertClause(cnfClauses, rightClause);
2420	array_free(rightClause);
2421	}
2422	} /* for n loop */
2423	orValue = doOr(orValue, andValue);
2424	if (orValue == 1){ /* TRUE */
2425	break;
2426	}
2427	if (andValue != 0){
2428	array_insert_last(int, orClause, andIndex);
2429	}
2430	}/* for j loop*/
2431	if ((l >= 0) && (orValue !=1)) { /* loop */
2432	for (j=l; j<= i-1; j++){
2433	left = BmcGenerateCnfForLtl(network, ltlFormula->left,
2434	j, k, l, cnfClauses);
2435	leftValue = checkIndex(left, cnfClauses);
2436	andIndex = cnfClauses->cnfGlobalIndex++;
2437	if (leftValue == -1){
2438	leftClause = array_alloc(int, 2);
2439	array_insert(int, leftClause, 0, left);
2440	array_insert(int, leftClause, 1, -andIndex);
2441	BmcCnfInsertClause(cnfClauses, leftClause);
2442	array_free(leftClause);
2443	}
2444	andValue = leftValue;
2445	for (n=i; (n<= k) && (andValue != 0); n++){
2446	right = BmcGenerateCnfForLtl(network, ltlFormula->right,
2447	n, k, l, cnfClauses);
2448	rightValue = checkIndex(right, cnfClauses);
2449	andValue = doAnd(andValue, rightValue);
2450	if (rightValue == -1){
2451	rightClause = array_alloc(int, 2);
2452	array_insert(int, rightClause, 0, right);
2453	array_insert(int, rightClause, 1, -andIndex);
2454	BmcCnfInsertClause(cnfClauses, rightClause);
2455	array_free(rightClause);
2456	}
2457	} /* for n loop */
2458	for (n=l; (n<= j) && (andValue != 0); n++){
2459	right = BmcGenerateCnfForLtl(network, ltlFormula->right,
2460	n, k, l, cnfClauses);
2461	rightValue = checkIndex(right, cnfClauses);
2462	andValue = doAnd(andValue, rightValue);
2463	if (rightValue == -1){
2464	rightClause = array_alloc(int, 2);
2465	array_insert(int, rightClause, 0, right);
2466	array_insert(int, rightClause, 1, -andIndex);
2467	BmcCnfInsertClause(cnfClauses, rightClause);
2468	array_free(rightClause);
2469	}
2470	} /* for n loop */
2471	orValue = doOr(orValue, andValue);
2472	if (orValue == 1){ /* TRUE */
2473	break;
2474	}
2475	if (andValue != 0){
2476	array_insert_last(int, orClause, andIndex);
2477	}
2478	} /* for j loop*/
2479	} /* if (l>=0) */
2480	}/* orValue !=1*/
2481	if ((orValue == 1) \|\| (orValue == 0)){
2482	/restore the infomration back/
2483	BmcCnfClausesRestore(cnfClauses, state);
2484	FREE(state);
2485	array_free(orClause);
2486	if (orValue == 0){
2487	/* add an empty clause*/
2488	BmcAddEmptyClause(cnfClauses);
2489	}
2490	return 0;
2491	} else {
2492	BmcCnfClausesUnFreeze(cnfClauses, state);
2493	FREE(state);
2494	BmcCnfInsertClause(cnfClauses, orClause);
2495	array_free(orClause);
2496	return orIndex;
2497	}
2498	default:
2499	fail("Unexpected LTL formula type");
2500	break;
2501	}
2502	return -1; /* we should never get here */
2503	}
2504	/* BmcLTLFormulaNoLoopTranslation() */
2505
2506
2507	/Function******************************************************************
2508
2509	Synopsis [Apply bmc on an abbreviation-free LTL formula that expresses
2510	safety propery]
2511
2512	Description [If an LTL formula expresses a safety property, we generate CNF
2513	0
2514	caluse for the part with no loop: [[f]]
2515	k
2516	]
2517
2518	SideEffects []
2519
2520	SeeAlso []
2521
2522	******************************************************************************/
2523	void
2524	BmcLtlCheckSafety(
2525	Ntk_Network_t *network,
2526	Ctlsp_Formula_t *ltlFormula,
2527	BmcOption_t *options,
2528	st_table *CoiTable)
2529	{
2530	mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
2531	st_table nodeToMvfAigTable = NIL(st_table); / node to mvfAig */
2532	BmcCnfClauses_t *cnfClauses = NIL(BmcCnfClauses_t);
2533	FILE *cnfFile;
2534	int noLoopIndex;
2535	array_t *result = NIL(array_t);
2536	int leftValue = 0;
2537	long startTime, endTime;
2538	int k;
2539	int minK = options->minK;
2540	int maxK = options->maxK;
2541	boolean boundedFormula;
2542	int depth;
2543	array_t *unitClause = array_alloc(int, 1);
2544
2545	array_t *orClause = array_alloc(int, 2);
2546
2547	/* ************** */
2548	/* Initialization */
2549	/* ************** */
2550	startTime = util_cpu_ctime();
2551	/* nodeToMvfAigTable maps each node to its multi-function And/Inv graph */
2552	nodeToMvfAigTable =
2553	(st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
2554	assert(nodeToMvfAigTable != NIL(st_table));
2555
2556	/* For bounded formulae use a tighter upper bound if possible. */
2557	boundedFormula = Ctlsp_LtlFormulaTestIsBounded(ltlFormula, &depth);
2558	if (boundedFormula && depth < maxK && depth >= minK) {
2559	maxK = depth;
2560	}
2561	if (options->verbosityLevel != BmcVerbosityNone_c){
2562	(void) fprintf(vis_stdout, "saftey LTL BMC\n");
2563	if (boundedFormula){
2564	(void) fprintf(vis_stdout, "Bounded formula of depth %d\n", depth);
2565	}
2566	(void) fprintf(vis_stdout, "Apply BMC on counterexample of length >= %d and <= %d (+%d) \n",
2567	minK, maxK, options->step);
2568	}
2569	k= minK;
2570	while( (result == NIL(array_t)) && (k <= maxK)){
2571	if (options->verbosityLevel == BmcVerbosityMax_c) {
2572	(void) fprintf(vis_stdout, "\nGenerate counterexample of length %d\n", k);
2573	}
2574	cnfClauses = BmcCnfClausesAlloc();
2575	cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
2576	if (cnfFile == NIL(FILE)) {
2577	(void)fprintf(vis_stderr,
2578	"** bmc error: Cannot create CNF output file %s\n",
2579	options->satInFile);
2580	return;
2581	}
2582	BmcCnfGenerateClausesForPath(network, 0, k, BMC_INITIAL_STATES,
2583	cnfClauses, nodeToMvfAigTable, CoiTable);
2584	noLoopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, -1, cnfClauses);
2585	leftValue = checkIndex(noLoopIndex, cnfClauses);
2586
2587	if(leftValue == 1){
2588	assert(k==1);
2589	if (options->verbosityLevel != BmcVerbosityNone_c){
2590	(void) fprintf(vis_stdout,"# BMC: formula failed\n");
2591	(void) fprintf(vis_stdout,"# BMC: Empty counterexample because the property is always FALSE\n");
2592	}
2593	break;
2594	} else if(leftValue == 0){
2595	if (options->verbosityLevel != BmcVerbosityNone_c){
2596	(void) fprintf(vis_stdout,"# BMC: the formula is trivially true");
2597	(void) fprintf(vis_stdout," for counterexamples of length %d\n", k);
2598	}
2599	/*
2600	break;
2601	*/
2602	} else {
2603	array_insert(int, unitClause, 0, noLoopIndex);
2604
2605	BmcCnfInsertClause(cnfClauses, unitClause);
2606
2607	BmcWriteClauses(manager, cnfFile, cnfClauses, options);
2608	(void) fclose(cnfFile);
2609	result = BmcCheckSAT(options);
2610	if (options->satSolverError){
2611	break;
2612	}
2613	if(result != NIL(array_t)) {
2614	(void) fprintf(vis_stdout, "# BMC: formula failed\n");
2615	if(options->verbosityLevel != BmcVerbosityNone_c){
2616	(void) fprintf(vis_stdout,
2617	"# BMC: Found a counterexample of length = %d \n", k);
2618	}
2619	if (options->dbgLevel == 1) {
2620	BmcPrintCounterExample(network, nodeToMvfAigTable, cnfClauses,
2621	result, k, CoiTable, options, NIL(array_t));
2622	}
2623	break;
2624	}
2625	}
2626	/* free all used memories */
2627	BmcCnfClausesFree(cnfClauses);
2628	#if 0
2629
2630	/*
2631	Check induction
2632	*/
2633	{
2634	BmcCnfClauses_t *noLoopCnfClauses = BmcCnfClausesAlloc();
2635	array_t *noLoopResult = NIL(array_t);
2636	array_t *unitClause = array_alloc(int, 1);
2637	int i;
2638
2639	printf("Check Induction \n");
2640
2641	cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
2642	if (cnfFile == NIL(FILE)) {
2643	(void)fprintf(vis_stderr,
2644	"** bmc error: Cannot create CNF output file %s\n",
2645	options->satInFile);
2646	return;
2647	}
2648	/*
2649	Generate a loop free path
2650	*/
2651	BmcCnfGenerateClausesForLoopFreePath(network, 0, k+1, BMC_NO_INITIAL_STATES,
2652	noLoopCnfClauses, nodeToMvfAigTable, CoiTable);
2653	/*
2654	The property true at states from 0 to k
2655	*/
2656	unitClause = array_alloc(int, 1);
2657	for(i=0; i<=k; i++){
2658	array_insert(int, unitClause, 0,
2659	-BmcGenerateCnfForLtl(network, ltlFormula, i, k, -1, noLoopCnfClauses));
2660	BmcCnfInsertClause(noLoopCnfClauses, unitClause);
2661	}
2662
2663	/*
2664	The property fails at k +1
2665	*/
2666	array_insert(int, unitClause, 0,
2667	BmcGenerateCnfForLtl(network, ltlFormula, 0, k+1, -1, noLoopCnfClauses));
2668	BmcCnfInsertClause(noLoopCnfClauses, unitClause);
2669	array_free(unitClause);
2670
2671	BmcWriteClauses(manager, cnfFile, noLoopCnfClauses, options);
2672	(void) fclose(cnfFile);
2673	noLoopResult = BmcCheckSAT(options);
2674	if(noLoopResult == NIL(array_t)) {
2675	(void) fprintf(vis_stdout, "# BMC: formula passed\n");
2676	(void) fprintf(vis_stdout,
2677	"# BMC: No more loop free path \n");
2678
2679	break;
2680	}
2681	/*
2682	BmcPrintCounterExample(network, nodeToMvfAigTable, noLoopCnfClauses,
2683	noLoopResult, bound+1, CoiTable, options, NIL(array_t));
2684	*/
2685	BmcCnfClausesFree(noLoopCnfClauses);
2686	} /* Check induction */
2687
2688	#endif
2689	k += options->step;
2690
2691	#if 0
2692
2693	/* Check if reach the depth of the model */
2694	cnfClauses = BmcCnfClausesAlloc();
2695	cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
2696	if (cnfFile == NIL(FILE)) {
2697	(void)fprintf(vis_stderr,
2698	"** bmc error: Cannot create CNF output file %s\n",
2699	options->satInFile);
2700	return;
2701	}
2702	/*
2703	Generate a loop free path
2704	*/
2705	{
2706	BmcCnfGenerateClausesForPath(network, 0, k, BMC_INITIAL_STATES,
2707	cnfClauses, nodeToMvfAigTable, CoiTable);
2708	/*
2709	initIndex = BmcCnfGenerateClausesFromStateToState(network, -1, 0, cnfClauses, nodeToMvfAigTable, CoiTable, -1);
2710	noLoopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, -1, cnfClauses);
2711
2712	array_insert(int, orClause, 0, initIndex);
2713	array_insert(int, orClause, 1, -noLoopIndex);
2714
2715	BmcCnfInsertClause(cnfClauses, orClause);
2716	*/
2717	BmcWriteClauses(manager, cnfFile, cnfClauses, options);
2718	(void) fclose(cnfFile);
2719	result = BmcCheckSAT(options);
2720	if(result == NIL(array_t)) {
2721	(void) fprintf(vis_stdout, "# BMC: formula passed\n");
2722	(void) fprintf(vis_stdout,
2723	"# BMC: No more loop free path \n");
2724
2725	return;
2726	}
2727	/*
2728	BmcPrintCounterExample(network, nodeToMvfAigTable, cnfClauses,
2729	result, k, CoiTable, options, NIL(array_t));
2730	*/
2731	result = NIL(array_t);
2732	}
2733	BmcCnfClausesFree(cnfClauses);
2734
2735
2736	/* Check if reach the depth of the model */
2737	cnfClauses = BmcCnfClausesAlloc();
2738	cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
2739	if (cnfFile == NIL(FILE)) {
2740	(void)fprintf(vis_stderr,
2741	"** bmc error: Cannot create CNF output file %s\n",
2742	options->satInFile);
2743	return;
2744	}
2745	/*
2746	Generate a loop free path
2747	*/
2748	{
2749	BmcCnfGenerateClausesForPath(network, 0, k, BMC_NO_INITIAL_STATES,
2750	cnfClauses, nodeToMvfAigTable, CoiTable);
2751	/*
2752	initIndex = BmcCnfGenerateClausesFromStateToState(network, -1, 0, cnfClauses, nodeToMvfAigTable, CoiTable, -1);
2753	*/
2754	noLoopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, -1, cnfClauses);
2755	array_insert(int, unitClause, 0, noLoopIndex);
2756
2757	BmcCnfInsertClause(cnfClauses, unitClause);
2758	/*
2759	array_insert(int, orClause, 0, initIndex);
2760	array_insert(int, orClause, 1, -noLoopIndex);
2761
2762	BmcCnfInsertClause(cnfClauses, orClause);
2763	*/
2764	BmcWriteClauses(manager, cnfFile, cnfClauses, options);
2765	(void) fclose(cnfFile);
2766	result = BmcCheckSAT(options);
2767	if(result == NIL(array_t)) {
2768	(void) fprintf(vis_stdout, "# BMC: (Bad state) formula passed\n");
2769	(void) fprintf(vis_stdout,
2770	"# BMC: No more loop free path \n");
2771
2772	return;
2773	}
2774	/*
2775	BmcPrintCounterExample(network, nodeToMvfAigTable, cnfClauses,
2776	result, k, CoiTable, options, NIL(array_t));
2777	*/
2778	result = NIL(array_t);
2779	}
2780	BmcCnfClausesFree(cnfClauses);
2781	#endif
2782
2783
2784	} /* while result and k*/
2785	if (options->satSolverError == FALSE){
2786	if ((result == NIL(array_t)) && (k > maxK)){
2787	if (boundedFormula && depth <= options->maxK){
2788	(void) fprintf(vis_stdout,"# BMC: formula passed\n");
2789	} else {
2790	(void) fprintf(vis_stdout,"# BMC: formula undecided\n");
2791	}
2792	if (options->verbosityLevel != BmcVerbosityNone_c){
2793	(void) fprintf(vis_stdout,
2794	"# BMC: no counterexample found of length up to %d \n",
2795	maxK);
2796	}
2797	}
2798	}
2799	/* free all used memories */
2800	if (k == 0){
2801	BmcCnfClausesFree(cnfClauses);
2802	}
2803	if(result != NIL(array_t)){
2804	array_free(result);
2805	}
2806	if (options->verbosityLevel != BmcVerbosityNone_c) {
2807	endTime = util_cpu_ctime();
2808	fprintf(vis_stdout, "-- bmc time = %10g\n",
2809	(double)(endTime - startTime) / 1000.0);
2810	}
2811	array_free(unitClause);
2812	array_free(orClause);
2813	fflush(vis_stdout);
2814	return;
2815	} /* BmcLtlCheckSafety() */
2816
2817
2818	/---------------------------------------------------------------------------/
2819	/* Definition of static functions */
2820	/---------------------------------------------------------------------------/
2821
2822
2823	/Function******************************************************************
2824
2825	Synopsis [Check if the index of the varaible in CNF is TURE, FALSE, or
2826	none]
2827
2828	Description []
2829
2830	SideEffects []
2831
2832	******************************************************************************/
2833	static int
2834	checkIndex(
2835	int index,
2836	BmcCnfClauses_t *cnfClauses)
2837	{
2838	int rtnValue = -1; /* it is not TRUE or FALSE*/
2839
2840	if (index == 0){ /* TRUE or FALSE*/
2841	if (cnfClauses->emptyClause){ /* last added clause was empty = FALSE*/
2842	rtnValue = 0; /* FALSE */
2843	} else {
2844	/*
2845	if (cnfClauses->noOfClauses == 0)
2846	rtnValue = 1;
2847	}
2848	*/
2849	rtnValue = 1; /* TRUE */
2850	}
2851	}
2852	return rtnValue;
2853	}
2854
2855	/Function******************************************************************
2856
2857	Synopsis []
2858
2859	Description [
2860	0 1 -1
2861	----------
2862	0 0 0 0
2863	1 0 1 -1
2864	-1 0 -1 -1
2865
2866	]
2867
2868	SideEffects []
2869
2870	******************************************************************************/
2871	static int
2872	doAnd(
2873	int left,
2874	int right)
2875	{
2876	if ((left == -1) && (right == -1)){
2877	return -1;
2878	}
2879	return (left * right);
2880
2881	} /* doAnd */
2882
2883	/Function******************************************************************
2884
2885	Synopsis []
2886
2887	Description [
2888	0 1 -1
2889	-----------
2890	0 0 1 -1
2891	1 1 1 -1
2892	-1 -1 -1 -1
2893
2894	]
2895
2896	SideEffects []
2897
2898	******************************************************************************/
2899	static int
2900	doOr(
2901	int left,
2902	int right)
2903	{
2904	if ((left == -1) \|\| (right == -1)){
2905	return -1;
2906	}
2907	if ((left == 1) \|\| (right == 1)){
2908	return 1;
2909	}
2910	return 0;
2911
2912	} /* doOr */

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

Context Navigation

source: vis_dev/vis-2.3/src/bmc/bmcBmc.c @ 54

Download in other formats: