1
2
3
4
5
6
7
8
9void error(void)
10{
11
12 {
13 goto ERROR;
14 ERROR: ;
15 return;
16}
17}
18int main_in1_val ;
19int main_in1_val_t ;
20int main_in1_ev ;
21int main_in1_req_up ;
22int main_in2_val ;
23int main_in2_val_t ;
24int main_in2_ev ;
25int main_in2_req_up ;
26int main_diff_val ;
27int main_diff_val_t ;
28int main_diff_ev ;
29int main_diff_req_up ;
30int main_sum_val ;
31int main_sum_val_t ;
32int main_sum_ev ;
33int main_sum_req_up ;
34int main_pres_val ;
35int main_pres_val_t ;
36int main_pres_ev ;
37int main_pres_req_up ;
38int main_dbl_val ;
39int main_dbl_val_t ;
40int main_dbl_ev ;
41int main_dbl_req_up ;
42int main_zero_val ;
43int main_zero_val_t ;
44int main_zero_ev ;
45int main_zero_req_up ;
46int main_clk_val ;
47int main_clk_val_t ;
48int main_clk_ev ;
49int main_clk_req_up ;
50int main_clk_pos_edge ;
51int main_clk_neg_edge ;
52int N_generate_st ;
53int N_generate_i ;
54int S1_addsub_st ;
55int S1_addsub_i ;
56int S2_presdbl_st ;
57int S2_presdbl_i ;
58int S3_zero_st ;
59int S3_zero_i ;
60int D_z ;
61int D_print_st ;
62int D_print_i ;
63void N_generate(void)
64{ int a ;
65 int b ;
66
67 {
68 main_in1_val_t = a;
69 main_in1_req_up = 1;
70 main_in2_val_t = b;
71 main_in2_req_up = 1;
72
73 return;
74}
75}
76void S1_addsub(void)
77{ int a ;
78 int b ;
79
80 {
81 a = main_in1_val;
82 b = main_in2_val;
83 main_sum_val_t = a + b;
84 main_sum_req_up = 1;
85 main_diff_val_t = a - b;
86 main_diff_req_up = 1;
87
88 return;
89}
90}
91void S2_presdbl(void)
92{ int a ;
93 int b ;
94 int c ;
95 int d ;
96
97 {
98 a = main_sum_val;
99 b = main_diff_val;
100 main_pres_val_t = a;
101 main_pres_req_up = 1;
102 c = a + b;
103 d = a - b;
104 main_dbl_val_t = c + d;
105 main_dbl_req_up = 1;
106
107 return;
108}
109}
110void S3_zero(void)
111{ int a ;
112 int b ;
113
114 {
115 a = main_pres_val;
116 b = main_dbl_val;
117 main_zero_val_t = b - (a + a);
118 main_zero_req_up = 1;
119
120 return;
121}
122}
123void D_print(void)
124{
125
126 {
127 D_z = main_zero_val;
128
129 return;
130}
131}
132void eval(void)
133{ int tmp ;
134 int tmp___0 ;
135 int tmp___1 ;
136 int tmp___2 ;
137 int tmp___3 ;
138
139 {
140 {
141 while (1) {
142 while_0_continue: ;
143 if ((int )N_generate_st == 0) {
144
145 } else {
146 if ((int )S1_addsub_st == 0) {
147
148 } else {
149 if ((int )S2_presdbl_st == 0) {
150
151 } else {
152 if ((int )S3_zero_st == 0) {
153
154 } else {
155 if ((int )D_print_st == 0) {
156
157 } else {
158 goto while_0_break;
159 }
160 }
161 }
162 }
163 }
164 if ((int )N_generate_st == 0) {
165 {
166 tmp = __VERIFIER_nondet_int();
167 }
168 if (tmp) {
169 {
170 N_generate_st = 1;
171 N_generate();
172 }
173 } else {
174
175 }
176 } else {
177
178 }
179 if ((int )S1_addsub_st == 0) {
180 {
181 tmp___0 = __VERIFIER_nondet_int();
182 }
183 if (tmp___0) {
184 {
185 S1_addsub_st = 1;
186 S1_addsub();
187 }
188 } else {
189
190 }
191 } else {
192
193 }
194 if ((int )S2_presdbl_st == 0) {
195 {
196 tmp___1 = __VERIFIER_nondet_int();
197 }
198 if (tmp___1) {
199 {
200 S2_presdbl_st = 1;
201 S2_presdbl();
202 }
203 } else {
204
205 }
206 } else {
207
208 }
209 if ((int )S3_zero_st == 0) {
210 {
211 tmp___2 = __VERIFIER_nondet_int();
212 }
213 if (tmp___2) {
214 {
215 S3_zero_st = 1;
216 S3_zero();
217 }
218 } else {
219
220 }
221 } else {
222
223 }
224 if ((int )D_print_st == 0) {
225 {
226 tmp___3 = __VERIFIER_nondet_int();
227 }
228 if (tmp___3) {
229 {
230 D_print_st = 1;
231 D_print();
232 }
233 } else {
234
235 }
236 } else {
237
238 }
239 }
240 while_0_break: ;
241 }
242
243 return;
244}
245}
246void start_simulation(void)
247{ int kernel_st ;
248
249 {
250 kernel_st = 0;
251 if ((int )main_in1_req_up == 1) {
252 if (main_in1_val != main_in1_val_t) {
253 main_in1_val = main_in1_val_t;
254 main_in1_ev = 0;
255 } else {
256
257 }
258 main_in1_req_up = 0;
259 } else {
260
261 }
262 if ((int )main_in2_req_up == 1) {
263 if (main_in2_val != main_in2_val_t) {
264 main_in2_val = main_in2_val_t;
265 main_in2_ev = 0;
266 } else {
267
268 }
269 main_in2_req_up = 0;
270 } else {
271
272 }
273 if ((int )main_sum_req_up == 1) {
274 if (main_sum_val != main_sum_val_t) {
275 main_sum_val = main_sum_val_t;
276 main_sum_ev = 0;
277 } else {
278
279 }
280 main_sum_req_up = 0;
281 } else {
282
283 }
284 if ((int )main_diff_req_up == 1) {
285 if (main_diff_val != main_diff_val_t) {
286 main_diff_val = main_diff_val_t;
287 main_diff_ev = 0;
288 } else {
289
290 }
291 main_diff_req_up = 0;
292 } else {
293
294 }
295 if ((int )main_pres_req_up == 1) {
296 if (main_pres_val != main_pres_val_t) {
297 main_pres_val = main_pres_val_t;
298 main_pres_ev = 0;
299 } else {
300
301 }
302 main_pres_req_up = 0;
303 } else {
304
305 }
306 if ((int )main_dbl_req_up == 1) {
307 if (main_dbl_val != main_dbl_val_t) {
308 main_dbl_val = main_dbl_val_t;
309 main_dbl_ev = 0;
310 } else {
311
312 }
313 main_dbl_req_up = 0;
314 } else {
315
316 }
317 if ((int )main_zero_req_up == 1) {
318 if (main_zero_val != main_zero_val_t) {
319 main_zero_val = main_zero_val_t;
320 main_zero_ev = 0;
321 } else {
322
323 }
324 main_zero_req_up = 0;
325 } else {
326
327 }
328 if ((int )main_clk_req_up == 1) {
329 if ((int )main_clk_val != (int )main_clk_val_t) {
330 main_clk_val = main_clk_val_t;
331 main_clk_ev = 0;
332 if ((int )main_clk_val == 1) {
333 main_clk_pos_edge = 0;
334 main_clk_neg_edge = 2;
335 } else {
336 main_clk_neg_edge = 0;
337 main_clk_pos_edge = 2;
338 }
339 } else {
340
341 }
342 main_clk_req_up = 0;
343 } else {
344
345 }
346 if ((int )N_generate_i == 1) {
347 N_generate_st = 0;
348 } else {
349 N_generate_st = 2;
350 }
351 if ((int )S1_addsub_i == 1) {
352 S1_addsub_st = 0;
353 } else {
354 S1_addsub_st = 2;
355 }
356 if ((int )S2_presdbl_i == 1) {
357 S2_presdbl_st = 0;
358 } else {
359 S2_presdbl_st = 2;
360 }
361 if ((int )S3_zero_i == 1) {
362 S3_zero_st = 0;
363 } else {
364 S3_zero_st = 2;
365 }
366 if ((int )D_print_i == 1) {
367 D_print_st = 0;
368 } else {
369 D_print_st = 2;
370 }
371 if ((int )main_in1_ev == 0) {
372 main_in1_ev = 1;
373 } else {
374
375 }
376 if ((int )main_in2_ev == 0) {
377 main_in2_ev = 1;
378 } else {
379
380 }
381 if ((int )main_sum_ev == 0) {
382 main_sum_ev = 1;
383 } else {
384
385 }
386 if ((int )main_diff_ev == 0) {
387 main_diff_ev = 1;
388 } else {
389
390 }
391 if ((int )main_pres_ev == 0) {
392 main_pres_ev = 1;
393 } else {
394
395 }
396 if ((int )main_dbl_ev == 0) {
397 main_dbl_ev = 1;
398 } else {
399
400 }
401 if ((int )main_zero_ev == 0) {
402 main_zero_ev = 1;
403 } else {
404
405 }
406 if ((int )main_clk_ev == 0) {
407 main_clk_ev = 1;
408 } else {
409
410 }
411 if ((int )main_clk_pos_edge == 0) {
412 main_clk_pos_edge = 1;
413 } else {
414
415 }
416 if ((int )main_clk_neg_edge == 0) {
417 main_clk_neg_edge = 1;
418 } else {
419
420 }
421 if ((int )main_clk_pos_edge == 1) {
422 N_generate_st = 0;
423 } else {
424
425 }
426 if ((int )main_clk_pos_edge == 1) {
427 S1_addsub_st = 0;
428 } else {
429
430 }
431 if ((int )main_clk_pos_edge == 1) {
432 S2_presdbl_st = 0;
433 } else {
434
435 }
436 if ((int )main_clk_pos_edge == 1) {
437 S3_zero_st = 0;
438 } else {
439
440 }
441 if ((int )main_clk_pos_edge == 1) {
442 D_print_st = 0;
443 } else {
444
445 }
446 if ((int )main_in1_ev == 1) {
447 main_in1_ev = 2;
448 } else {
449
450 }
451 if ((int )main_in2_ev == 1) {
452 main_in2_ev = 2;
453 } else {
454
455 }
456 if ((int )main_sum_ev == 1) {
457 main_sum_ev = 2;
458 } else {
459
460 }
461 if ((int )main_diff_ev == 1) {
462 main_diff_ev = 2;
463 } else {
464
465 }
466 if ((int )main_pres_ev == 1) {
467 main_pres_ev = 2;
468 } else {
469
470 }
471 if ((int )main_dbl_ev == 1) {
472 main_dbl_ev = 2;
473 } else {
474
475 }
476 if ((int )main_zero_ev == 1) {
477 main_zero_ev = 2;
478 } else {
479
480 }
481 if ((int )main_clk_ev == 1) {
482 main_clk_ev = 2;
483 } else {
484
485 }
486 if ((int )main_clk_pos_edge == 1) {
487 main_clk_pos_edge = 2;
488 } else {
489
490 }
491 if ((int )main_clk_neg_edge == 1) {
492 main_clk_neg_edge = 2;
493 } else {
494
495 }
496 {
497 while (1) {
498 while_1_continue: ;
499 {
500 kernel_st = 1;
501 eval();
502 }
503 kernel_st = 2;
504 if ((int )main_in1_req_up == 1) {
505 if (main_in1_val != main_in1_val_t) {
506 main_in1_val = main_in1_val_t;
507 main_in1_ev = 0;
508 } else {
509
510 }
511 main_in1_req_up = 0;
512 } else {
513
514 }
515 if ((int )main_in2_req_up == 1) {
516 if (main_in2_val != main_in2_val_t) {
517 main_in2_val = main_in2_val_t;
518 main_in2_ev = 0;
519 } else {
520
521 }
522 main_in2_req_up = 0;
523 } else {
524
525 }
526 if ((int )main_sum_req_up == 1) {
527 if (main_sum_val != main_sum_val_t) {
528 main_sum_val = main_sum_val_t;
529 main_sum_ev = 0;
530 } else {
531
532 }
533 main_sum_req_up = 0;
534 } else {
535
536 }
537 if ((int )main_diff_req_up == 1) {
538 if (main_diff_val != main_diff_val_t) {
539 main_diff_val = main_diff_val_t;
540 main_diff_ev = 0;
541 } else {
542
543 }
544 main_diff_req_up = 0;
545 } else {
546
547 }
548 if ((int )main_pres_req_up == 1) {
549 if (main_pres_val != main_pres_val_t) {
550 main_pres_val = main_pres_val_t;
551 main_pres_ev = 0;
552 } else {
553
554 }
555 main_pres_req_up = 0;
556 } else {
557
558 }
559 if ((int )main_dbl_req_up == 1) {
560 if (main_dbl_val != main_dbl_val_t) {
561 main_dbl_val = main_dbl_val_t;
562 main_dbl_ev = 0;
563 } else {
564
565 }
566 main_dbl_req_up = 0;
567 } else {
568
569 }
570 if ((int )main_zero_req_up == 1) {
571 if (main_zero_val != main_zero_val_t) {
572 main_zero_val = main_zero_val_t;
573 main_zero_ev = 0;
574 } else {
575
576 }
577 main_zero_req_up = 0;
578 } else {
579
580 }
581 if ((int )main_clk_req_up == 1) {
582 if ((int )main_clk_val != (int )main_clk_val_t) {
583 main_clk_val = main_clk_val_t;
584 main_clk_ev = 0;
585 if ((int )main_clk_val == 1) {
586 main_clk_pos_edge = 0;
587 main_clk_neg_edge = 2;
588 } else {
589 main_clk_neg_edge = 0;
590 main_clk_pos_edge = 2;
591 }
592 } else {
593
594 }
595 main_clk_req_up = 0;
596 } else {
597
598 }
599 kernel_st = 3;
600 if ((int )main_in1_ev == 0) {
601 main_in1_ev = 1;
602 } else {
603
604 }
605 if ((int )main_in2_ev == 0) {
606 main_in2_ev = 1;
607 } else {
608
609 }
610 if ((int )main_sum_ev == 0) {
611 main_sum_ev = 1;
612 } else {
613
614 }
615 if ((int )main_diff_ev == 0) {
616 main_diff_ev = 1;
617 } else {
618
619 }
620 if ((int )main_pres_ev == 0) {
621 main_pres_ev = 1;
622 } else {
623
624 }
625 if ((int )main_dbl_ev == 0) {
626 main_dbl_ev = 1;
627 } else {
628
629 }
630 if ((int )main_zero_ev == 0) {
631 main_zero_ev = 1;
632 } else {
633
634 }
635 if ((int )main_clk_ev == 0) {
636 main_clk_ev = 1;
637 } else {
638
639 }
640 if ((int )main_clk_pos_edge == 0) {
641 main_clk_pos_edge = 1;
642 } else {
643
644 }
645 if ((int )main_clk_neg_edge == 0) {
646 main_clk_neg_edge = 1;
647 } else {
648
649 }
650 if ((int )main_clk_pos_edge == 1) {
651 N_generate_st = 0;
652 } else {
653
654 }
655 if ((int )main_clk_pos_edge == 1) {
656 S1_addsub_st = 0;
657 } else {
658
659 }
660 if ((int )main_clk_pos_edge == 1) {
661 S2_presdbl_st = 0;
662 } else {
663
664 }
665 if ((int )main_clk_pos_edge == 1) {
666 S3_zero_st = 0;
667 } else {
668
669 }
670 if ((int )main_clk_pos_edge == 1) {
671 D_print_st = 0;
672 } else {
673
674 }
675 if ((int )main_in1_ev == 1) {
676 main_in1_ev = 2;
677 } else {
678
679 }
680 if ((int )main_in2_ev == 1) {
681 main_in2_ev = 2;
682 } else {
683
684 }
685 if ((int )main_sum_ev == 1) {
686 main_sum_ev = 2;
687 } else {
688
689 }
690 if ((int )main_diff_ev == 1) {
691 main_diff_ev = 2;
692 } else {
693
694 }
695 if ((int )main_pres_ev == 1) {
696 main_pres_ev = 2;
697 } else {
698
699 }
700 if ((int )main_dbl_ev == 1) {
701 main_dbl_ev = 2;
702 } else {
703
704 }
705 if ((int )main_zero_ev == 1) {
706 main_zero_ev = 2;
707 } else {
708
709 }
710 if ((int )main_clk_ev == 1) {
711 main_clk_ev = 2;
712 } else {
713
714 }
715 if ((int )main_clk_pos_edge == 1) {
716 main_clk_pos_edge = 2;
717 } else {
718
719 }
720 if ((int )main_clk_neg_edge == 1) {
721 main_clk_neg_edge = 2;
722 } else {
723
724 }
725 if ((int )N_generate_st == 0) {
726
727 } else {
728 if ((int )S1_addsub_st == 0) {
729
730 } else {
731 if ((int )S2_presdbl_st == 0) {
732
733 } else {
734 if ((int )S3_zero_st == 0) {
735
736 } else {
737 if ((int )D_print_st == 0) {
738
739 } else {
740 goto while_1_break;
741 }
742 }
743 }
744 }
745 }
746 }
747 while_1_break: ;
748 }
749
750 return;
751}
752}
753int main(void)
754{ int count ;
755 int __retres2 ;
756
757 {
758 {
759
760 main_in1_ev = 2;
761 main_in1_req_up = 0;
762 main_in2_ev = 2;
763 main_in2_req_up = 0;
764 main_diff_ev = 2;
765 main_diff_req_up = 0;
766 main_sum_ev = 2;
767 main_sum_req_up = 0;
768 main_pres_ev = 2;
769 main_pres_req_up = 0;
770 main_dbl_ev = 2;
771 main_dbl_req_up = 0;
772 main_zero_ev = 2;
773 main_zero_req_up = 0;
774 main_clk_val = 0;
775 main_clk_ev = 2;
776 main_clk_req_up = 0;
777 main_clk_pos_edge = 2;
778 main_clk_neg_edge = 2;
779
780
781 count = 0;
782 N_generate_i = 0;
783 S1_addsub_i = 0;
784 S2_presdbl_i = 0;
785 S3_zero_i = 0;
786 D_print_i = 0;
787 start_simulation();
788 }
789 {
790 while (1) {
791 while_2_continue: ;
792 {
793 main_clk_val_t = 1;
794 main_clk_req_up = 1;
795 start_simulation();
796 count += 1;
797 }
798 if (count == 5) {
799 if (! (D_z == 0)) {
800 {
801 error();
802 }
803 } else {
804
805 }
806 count = 0;
807 } else {
808
809 }
810 {
811 main_clk_val_t = 0;
812 main_clk_req_up = 1;
813 start_simulation();
814 }
815 }
816 while_2_break: ;
817 }
818 __retres2 = 0;
819 return (__retres2);
820}
821}