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