diff --git a/b01.test b/b01.test deleted file mode 100644 index b255349..0000000 --- a/b01.test +++ /dev/null @@ -1,26 +0,0 @@ -* Name of circuit: experiment/benchmark/b01.bench -* Primary inputs : - LINE1 LINE2 OVERFLW_REG STATO_REG_2_ STATO_REG_1_ STATO_REG_0_ OUTP_REG - -* Primary outputs: - U34 __new_OUT1_OVERFLW_REG U45 U36 U35 U44 __new_OUT1_OUTP_REG - - -* Test patterns and fault free responses: - - 1: 0000001 0000101 - 2: 0101100 0000010 - 3: 1100110 1010000 - 4: 1101100 0001100 - 5: 1100010 0010100 - 6: 0101110 0001100 - 7: 0001010 0011010 - 8: 0001000 0001010 - 9: 0010000 0100100 - 10: 0001100 0000000 - 11: 0000010 0001000 - 12: 0000100 0011000 - 13: 1000110 1000110 - 14: 0101000 0010100 - 15: 1001000 0010100 - 16: 1100000 0010000 diff --git a/b01.txt b/b01.txt deleted file mode 100644 index 8647a95..0000000 --- a/b01.txt +++ /dev/null @@ -1,1128 +0,0 @@ --- Configuring done (0.0s) --- Generating done (0.0s) --- Build files have been written to: /pub/netdisk1/qianyh/atpg-ls/build -[ 20%] Built target cadical06w -[ 25%] Built target cadical_sat -[ 30%] Built target sat_solver -[ 50%] Built target atpg_backend -[ 55%] Built target atpgSat -[ 70%] Built target tests -[100%] Built target atpg -======================== -parsing file experiment/benchmark/b01.bench ... ->> Fault: G1 stuck-at: 0 is_stem: 1 is_po: 0 ->> Fault: G2 stuck-at: 0 is_stem: 1 is_po: 0 ->> Fault: G4 stuck-at: 0 is_stem: 1 is_po: 0 ->> Fault: G5 stuck-at: 0 is_stem: 1 is_po: 0 ->> Fault: G6 stuck-at: 0 is_stem: 1 is_po: 0 ->> Fault: G23 stuck-at: 0 is_stem: 1 is_po: 0 ->> Fault: G12 stuck-at: 0 is_stem: 1 is_po: 0 ->> Fault: G48 stuck-at: 0 is_stem: 1 is_po: 0 ->> Fault: G46 stuck-at: 0 is_stem: 1 is_po: 0 ->> Fault: G47 stuck-at: 0 is_stem: 1 is_po: 0 ->> Fault: G49 stuck-at: 0 is_stem: 1 is_po: 0 ->> Fault: G16 stuck-at: 0 is_stem: 1 is_po: 0 ->> Fault: G8 stuck-at: 1 is_stem: 1 is_po: 0 ->> Fault: G9 stuck-at: 0 is_stem: 1 is_po: 0 ->> Fault: G10 stuck-at: 1 is_stem: 1 is_po: 0 ->> Fault: G11 stuck-at: 0 is_stem: 1 is_po: 0 ->> Fault: G13 stuck-at: 0 is_stem: 1 is_po: 0 ->> Fault: G14 stuck-at: 0 is_stem: 1 is_po: 0 ->> Fault: G15 stuck-at: 0 is_stem: 1 is_po: 0 ->> Fault: G17 stuck-at: 1 is_stem: 1 is_po: 0 ->> Fault: G18 stuck-at: 0 is_stem: 1 is_po: 0 ->> Fault: G19 stuck-at: 1 is_stem: 1 is_po: 0 ->> Fault: G20 stuck-at: 0 is_stem: 1 is_po: 0 ->> Fault: G21 stuck-at: 1 is_stem: 1 is_po: 0 ->> Fault: G22 stuck-at: 1 is_stem: 1 is_po: 0 ->> Fault: G24 stuck-at: 1 is_stem: 1 is_po: 0 ->> Fault: G25 stuck-at: 0 is_stem: 1 is_po: 0 ->> Fault: G26 stuck-at: 1 is_stem: 1 is_po: 0 ->> Fault: G27 stuck-at: 1 is_stem: 1 is_po: 0 ->> Fault: G28 stuck-at: 1 is_stem: 1 is_po: 0 ->> Fault: G29 stuck-at: 0 is_stem: 1 is_po: 0 ->> Fault: G30 stuck-at: 1 is_stem: 1 is_po: 0 ->> Fault: G31 stuck-at: 1 is_stem: 1 is_po: 0 ->> Fault: G32 stuck-at: 0 is_stem: 1 is_po: 0 ->> Fault: G33 stuck-at: 0 is_stem: 1 is_po: 0 ->> Fault: G34 stuck-at: 1 is_stem: 1 is_po: 0 ->> Fault: G35 stuck-at: 1 is_stem: 1 is_po: 0 ->> Fault: G36 stuck-at: 1 is_stem: 1 is_po: 0 ->> Fault: G37 stuck-at: 1 is_stem: 1 is_po: 0 ->> Fault: G38 stuck-at: 1 is_stem: 1 is_po: 0 ->> Fault: G39 stuck-at: 1 is_stem: 1 is_po: 0 ->> Fault: G40 stuck-at: 1 is_stem: 1 is_po: 0 ->> Fault: G41 stuck-at: 1 is_stem: 1 is_po: 0 ->> Fault: G42 stuck-at: 1 is_stem: 1 is_po: 0 ->> Fault: G43 stuck-at: 1 is_stem: 1 is_po: 0 ->> Fault: G44 stuck-at: 1 is_stem: 1 is_po: 0 ->> Fault: G45 stuck-at: 1 is_stem: 1 is_po: 0 -building lut circuit ... -====== Circuit Statistics ====== -PI: 7 -PO: 7 -Gate: 49 -LUT: 24 -================================ -====== local search start ====== -initing lookup table ... -[1/24] -[2/24] -[3/24] -[4/24] -[5/24] -[6/24] -[7/24] -[8/24] -[9/24] -[10/24] -[11/24] -[12/24] -[13/24] -[14/24] -[15/24] -[16/24] -[17/24] -[18/24] -[19/24] -[20/24] -[21/24] -[22/24] -[23/24] -[24/24] -ganerating fault info ... -staring local search ... -sat delete: G3 -sat delete: G7 -start with fault: G1 SA0 verify ... successful! -step: 0 fd: 36 -step: 7 fd: 33 -step: 15 fd: 33 -step: 17 fd: 35 -Cover: 35.71% pattern: 1 new_detected: 35 undected: 63 time: 0.00s -start with fault: G1 SA1 verify ... successful! -step: 1 fd: 15 -step: 2 fd: 22 -step: 3 fd: 17 -step: 6 fd: 29 -step: 8 fd: 24 -step: 9 fd: 17 -step: 10 fd: 29 -step: 13 fd: 24 -step: 17 fd: 27 -Cover: 63.27% pattern: 2 new_detected: 27 undected: 36 time: 0.00s -start with fault: G2 SA0 verify ... successful! -step: 1 fd: 13 -step: 2 fd: 13 -step: 4 fd: 9 -step: 7 fd: 13 -step: 19 fd: 4 -step: 27 fd: 6 -step: 35 fd: 13 -step: 42 fd: 4 -step: 43 fd: 4 -step: 49 fd: 13 -step: 52 fd: 13 -step: 56 fd: 13 -step: 60 fd: 13 -step: 80 fd: 6 -step: 91 fd: 8 -step: 116 fd: 6 -step: 124 fd: 6 -step: 127 fd: 13 -step: 133 fd: 13 -step: 136 fd: 13 -step: 153 fd: 13 -step: 155 fd: 13 -step: 157 fd: 13 -step: 159 fd: 13 -step: 161 fd: 13 -step: 163 fd: 6 -step: 174 fd: 13 -step: 188 fd: 6 -step: 196 fd: 6 -step: 210 fd: 6 -step: 215 fd: 6 -step: 244 fd: 6 -step: 255 fd: 13 -step: 258 fd: 6 -step: 276 fd: 13 -step: 282 fd: 13 -step: 287 fd: 13 -step: 292 fd: 13 -step: 299 fd: 6 -step: 301 fd: 6 -step: 308 fd: 13 -step: 311 fd: 13 -step: 313 fd: 6 -step: 327 fd: 6 -step: 332 fd: 6 -step: 335 fd: 6 -step: 350 fd: 13 -step: 353 fd: 13 -step: 376 fd: 13 -step: 382 fd: 13 -step: 385 fd: 6 -step: 403 fd: 6 -step: 407 fd: 6 -step: 420 fd: 6 -step: 434 fd: 6 -step: 446 fd: 7 -step: 448 fd: 6 -step: 451 fd: 7 -step: 458 fd: 13 -step: 460 fd: 13 -step: 462 fd: 13 -step: 473 fd: 6 -step: 483 fd: 6 -step: 495 fd: 13 -step: 498 fd: 13 -step: 500 fd: 13 -step: 519 fd: 6 -step: 521 fd: 13 -step: 524 fd: 6 -step: 531 fd: 13 -step: 536 fd: 7 -step: 553 fd: 7 -step: 556 fd: 6 -step: 573 fd: 13 -step: 587 fd: 6 -step: 596 fd: 13 -step: 633 fd: 13 -step: 644 fd: 13 -step: 649 fd: 13 -step: 651 fd: 13 -step: 653 fd: 13 -step: 654 fd: 6 -step: 655 fd: 13 -step: 656 fd: 6 -step: 657 fd: 13 -step: 659 fd: 13 -step: 661 fd: 13 -step: 662 fd: 6 -step: 663 fd: 13 -step: 664 fd: 6 -step: 665 fd: 13 -step: 666 fd: 6 -step: 667 fd: 13 -step: 674 fd: 13 -step: 678 fd: 6 -step: 683 fd: 6 -step: 695 fd: 6 -step: 699 fd: 6 -step: 705 fd: 6 -step: 708 fd: 13 -step: 712 fd: 6 -step: 726 fd: 6 -step: 729 fd: 13 -step: 731 fd: 13 -step: 736 fd: 13 -step: 740 fd: 13 -step: 751 fd: 6 -step: 754 fd: 6 -step: 769 fd: 13 -step: 773 fd: 7 -step: 778 fd: 13 -step: 783 fd: 6 -step: 787 fd: 6 -step: 790 fd: 6 -step: 793 fd: 6 -step: 795 fd: 6 -step: 797 fd: 6 -step: 800 fd: 13 -step: 806 fd: 6 -step: 808 fd: 13 -step: 815 fd: 6 -step: 818 fd: 6 -step: 821 fd: 13 -step: 826 fd: 6 -step: 841 fd: 6 -step: 843 fd: 7 -step: 845 fd: 7 -step: 848 fd: 7 -step: 850 fd: 7 -step: 854 fd: 7 -step: 869 fd: 6 -step: 873 fd: 6 -step: 887 fd: 13 -step: 906 fd: 6 -step: 908 fd: 6 -step: 911 fd: 13 -step: 913 fd: 6 -step: 919 fd: 6 -step: 923 fd: 6 -step: 925 fd: 13 -step: 945 fd: 6 -step: 964 fd: 13 -step: 977 fd: 13 -step: 980 fd: 6 -step: 982 fd: 6 -step: 994 fd: 13 -step: 998 fd: 13 -step: 1002 fd: 6 -step: 1004 fd: 6 -step: 1006 fd: 6 -step: 1018 fd: 6 -step: 1020 fd: 13 -step: 1025 fd: 7 -step: 1027 fd: 6 -step: 1046 fd: 6 -step: 1060 fd: 7 -step: 1080 fd: 6 -step: 1090 fd: 6 -step: 1093 fd: 13 -step: 1096 fd: 6 -step: 1099 fd: 13 -step: 1104 fd: 13 -step: 1117 fd: 6 -step: 1124 fd: 13 -step: 1126 fd: 13 -step: 1128 fd: 13 -step: 1138 fd: 13 -step: 1147 fd: 13 -step: 1152 fd: 13 -step: 1155 fd: 13 -step: 1160 fd: 6 -step: 1170 fd: 6 -step: 1174 fd: 13 -step: 1188 fd: 13 -step: 1191 fd: 13 -step: 1195 fd: 7 -step: 1198 fd: 13 -step: 1203 fd: 6 -step: 1207 fd: 6 -step: 1210 fd: 6 -step: 1216 fd: 6 -step: 1218 fd: 6 -step: 1224 fd: 6 -Cover: 67.35% pattern: 3 new_detected: 4 undected: 32 time: 0.02s -start with fault: G2 SA1 verify ... successful! -step: 1 fd: 7 -step: 2 fd: 5 -step: 4 fd: 7 -step: 5 fd: 5 -step: 6 fd: 7 -step: 7 fd: 5 -step: 8 fd: 7 -step: 9 fd: 5 -step: 10 fd: 7 -step: 11 fd: 5 -step: 12 fd: 7 -step: 13 fd: 5 -step: 14 fd: 9 -step: 17 fd: 11 -step: 18 fd: 7 -step: 22 fd: 11 -step: 24 fd: 11 -step: 26 fd: 0 -step: 28 fd: 13 -step: 33 fd: 13 -step: 35 fd: 9 -step: 37 fd: 13 -step: 41 fd: 9 -step: 43 fd: 13 -step: 44 fd: 9 -step: 47 fd: 13 -step: 52 fd: 13 -step: 59 fd: 13 -step: 62 fd: 13 -step: 64 fd: 3 -step: 65 fd: 7 -step: 66 fd: 13 -step: 67 fd: 7 -step: 68 fd: 13 -step: 71 fd: 7 -step: 75 fd: 7 -step: 76 fd: 13 -step: 77 fd: 7 -step: 79 fd: 13 -step: 82 fd: 13 -step: 85 fd: 13 -step: 88 fd: 7 -step: 91 fd: 13 -step: 93 fd: 13 -step: 94 fd: 7 -step: 96 fd: 13 -step: 97 fd: 7 -step: 98 fd: 13 -step: 101 fd: 13 -step: 104 fd: 13 -step: 106 fd: 13 -step: 108 fd: 7 -step: 109 fd: 13 -step: 110 fd: 7 -step: 111 fd: 13 -step: 112 fd: 7 -step: 114 fd: 13 -step: 120 fd: 13 -step: 125 fd: 7 -step: 130 fd: 7 -step: 140 fd: 13 -step: 141 fd: 7 -step: 145 fd: 13 -step: 147 fd: 13 -step: 149 fd: 13 -step: 154 fd: 13 -step: 156 fd: 13 -step: 160 fd: 13 -step: 163 fd: 13 -step: 165 fd: 13 -step: 170 fd: 7 -step: 171 fd: 13 -step: 173 fd: 13 -step: 175 fd: 13 -step: 180 fd: 13 -step: 182 fd: 13 -step: 183 fd: 7 -step: 185 fd: 1 -step: 187 fd: 13 -step: 189 fd: 7 -step: 192 fd: 13 -step: 193 fd: 7 -step: 194 fd: 13 -step: 195 fd: 7 -step: 196 fd: 13 -step: 197 fd: 7 -step: 198 fd: 13 -step: 199 fd: 7 -step: 203 fd: 13 -step: 205 fd: 13 -step: 209 fd: 7 -step: 216 fd: 13 -step: 225 fd: 7 -step: 228 fd: 13 -step: 233 fd: 13 -step: 237 fd: 13 -step: 239 fd: 7 -step: 240 fd: 13 -step: 241 fd: 7 -step: 245 fd: 13 -step: 250 fd: 13 -step: 252 fd: 7 -step: 253 fd: 13 -step: 260 fd: 13 -step: 264 fd: 13 -step: 268 fd: 9 -step: 270 fd: 7 -step: 275 fd: 7 -step: 276 fd: 13 -step: 277 fd: 7 -step: 283 fd: 13 -step: 289 fd: 7 -step: 291 fd: 7 -step: 292 fd: 13 -step: 293 fd: 7 -step: 294 fd: 13 -step: 296 fd: 13 -step: 299 fd: 13 -step: 301 fd: 13 -step: 308 fd: 13 -step: 317 fd: 3 -step: 319 fd: 7 -step: 322 fd: 9 -step: 323 fd: 13 -step: 325 fd: 13 -step: 328 fd: 13 -step: 335 fd: 13 -step: 340 fd: 13 -step: 343 fd: 13 -step: 345 fd: 13 -step: 349 fd: 13 -step: 355 fd: 13 -step: 361 fd: 7 -step: 363 fd: 13 -step: 364 fd: 7 -step: 365 fd: 13 -step: 368 fd: 7 -step: 369 fd: 13 -step: 370 fd: 7 -step: 371 fd: 13 -step: 378 fd: 13 -step: 381 fd: 7 -step: 383 fd: 7 -step: 384 fd: 13 -step: 390 fd: 13 -step: 398 fd: 13 -step: 400 fd: 7 -step: 404 fd: 7 -step: 406 fd: 13 -step: 408 fd: 7 -step: 412 fd: 13 -step: 413 fd: 7 -step: 414 fd: 13 -step: 416 fd: 13 -step: 423 fd: 13 -step: 426 fd: 3 -step: 427 fd: 1 -step: 430 fd: 3 -step: 431 fd: 1 -step: 432 fd: 13 -step: 433 fd: 3 -step: 434 fd: 1 -step: 436 fd: 13 -step: 437 fd: 3 -step: 438 fd: 1 -step: 440 fd: 13 -step: 446 fd: 13 -step: 452 fd: 13 -step: 459 fd: 13 -step: 469 fd: 13 -step: 474 fd: 13 -step: 484 fd: 13 -step: 489 fd: 13 -step: 492 fd: 7 -step: 494 fd: 7 -step: 496 fd: 13 -step: 499 fd: 13 -step: 510 fd: 7 -step: 512 fd: 7 -step: 514 fd: 7 -step: 516 fd: 13 -step: 518 fd: 13 -step: 520 fd: 7 -step: 522 fd: 7 -step: 527 fd: 3 -step: 532 fd: 13 -step: 534 fd: 7 -step: 535 fd: 13 -step: 538 fd: 13 -step: 540 fd: 13 -step: 543 fd: 13 -step: 545 fd: 13 -step: 552 fd: 13 -step: 556 fd: 13 -step: 558 fd: 13 -step: 570 fd: 13 -step: 574 fd: 13 -step: 575 fd: 3 -step: 578 fd: 13 -step: 580 fd: 13 -step: 582 fd: 3 -step: 583 fd: 13 -step: 584 fd: 1 -step: 587 fd: 3 -step: 590 fd: 1 -step: 591 fd: 13 -step: 597 fd: 13 -step: 600 fd: 13 -step: 612 fd: 13 -step: 614 fd: 13 -step: 622 fd: 13 -step: 624 fd: 13 -step: 632 fd: 9 -step: 637 fd: 3 -step: 638 fd: 13 -step: 648 fd: 13 -step: 650 fd: 13 -step: 652 fd: 13 -step: 658 fd: 13 -step: 665 fd: 13 -step: 667 fd: 13 -step: 671 fd: 9 -step: 677 fd: 13 -step: 681 fd: 7 -step: 683 fd: 7 -step: 684 fd: 13 -step: 687 fd: 13 -step: 689 fd: 7 -step: 690 fd: 13 -step: 692 fd: 13 -step: 694 fd: 7 -step: 695 fd: 13 -step: 697 fd: 13 -step: 699 fd: 13 -step: 700 fd: 7 -step: 702 fd: 13 -step: 706 fd: 13 -step: 708 fd: 13 -step: 710 fd: 13 -step: 712 fd: 13 -step: 714 fd: 7 -step: 715 fd: 13 -step: 716 fd: 7 -step: 717 fd: 13 -step: 724 fd: 13 -step: 725 fd: 7 -step: 726 fd: 13 -step: 728 fd: 13 -step: 733 fd: 13 -step: 734 fd: 1 -step: 736 fd: 13 -step: 737 fd: 3 -step: 738 fd: 7 -step: 739 fd: 13 -step: 740 fd: 7 -step: 742 fd: 13 -step: 743 fd: 1 -step: 745 fd: 13 -step: 746 fd: 7 -step: 747 fd: 3 -step: 749 fd: 13 -step: 753 fd: 13 -step: 756 fd: 3 -step: 757 fd: 1 -step: 758 fd: 3 -step: 759 fd: 1 -step: 760 fd: 13 -step: 761 fd: 7 -step: 762 fd: 13 -step: 763 fd: 7 -step: 764 fd: 3 -step: 765 fd: 1 -step: 766 fd: 13 -step: 767 fd: 3 -step: 768 fd: 1 -step: 769 fd: 7 -step: 770 fd: 3 -step: 771 fd: 13 -step: 774 fd: 13 -step: 779 fd: 13 -step: 785 fd: 13 -step: 789 fd: 13 -step: 793 fd: 13 -step: 795 fd: 13 -step: 797 fd: 13 -step: 803 fd: 13 -step: 815 fd: 13 -step: 817 fd: 13 -step: 818 fd: 7 -step: 820 fd: 13 -step: 822 fd: 13 -step: 823 fd: 7 -step: 825 fd: 13 -step: 827 fd: 13 -step: 829 fd: 13 -step: 831 fd: 13 -step: 832 fd: 7 -step: 852 fd: 13 -step: 856 fd: 13 -step: 863 fd: 7 -step: 864 fd: 13 -step: 865 fd: 7 -step: 866 fd: 13 -step: 868 fd: 13 -step: 870 fd: 13 -step: 875 fd: 13 -step: 877 fd: 3 -step: 881 fd: 13 -step: 882 fd: 7 -step: 885 fd: 13 -step: 886 fd: 7 -step: 887 fd: 13 -step: 888 fd: 7 -step: 889 fd: 13 -step: 891 fd: 7 -step: 893 fd: 13 -step: 894 fd: 7 -step: 898 fd: 13 -step: 901 fd: 13 -step: 905 fd: 13 -step: 907 fd: 13 -step: 909 fd: 13 -step: 914 fd: 13 -step: 916 fd: 13 -step: 918 fd: 13 -step: 920 fd: 13 -step: 925 fd: 13 -step: 932 fd: 13 -step: 935 fd: 13 -step: 940 fd: 13 -step: 947 fd: 13 -step: 949 fd: 13 -step: 950 fd: 7 -step: 952 fd: 13 -step: 954 fd: 13 -step: 956 fd: 13 -step: 960 fd: 13 -step: 963 fd: 7 -step: 964 fd: 13 -step: 965 fd: 7 -step: 966 fd: 13 -step: 968 fd: 13 -step: 971 fd: 13 -step: 975 fd: 13 -step: 978 fd: 13 -step: 980 fd: 13 -step: 985 fd: 13 -step: 993 fd: 13 -step: 996 fd: 13 -step: 1002 fd: 13 -step: 1010 fd: 13 -step: 1012 fd: 13 -step: 1019 fd: 13 -step: 1025 fd: 13 -step: 1027 fd: 13 -step: 1030 fd: 7 -step: 1032 fd: 13 -step: 1034 fd: 7 -step: 1035 fd: 13 -step: 1037 fd: 7 -step: 1038 fd: 13 -step: 1039 fd: 7 -step: 1040 fd: 13 -step: 1041 fd: 7 -step: 1042 fd: 13 -step: 1043 fd: 7 -step: 1045 fd: 13 -step: 1059 fd: 13 -step: 1061 fd: 13 -step: 1063 fd: 13 -step: 1065 fd: 13 -step: 1071 fd: 13 -step: 1073 fd: 13 -step: 1082 fd: 13 -step: 1085 fd: 7 -step: 1089 fd: 13 -step: 1091 fd: 13 -step: 1095 fd: 9 -step: 1098 fd: 13 -step: 1102 fd: 13 -step: 1108 fd: 13 -step: 1110 fd: 13 -step: 1117 fd: 7 -step: 1119 fd: 9 -step: 1125 fd: 13 -step: 1127 fd: 13 -step: 1129 fd: 13 -step: 1131 fd: 13 -step: 1133 fd: 13 -step: 1138 fd: 13 -step: 1140 fd: 13 -step: 1148 fd: 13 -step: 1153 fd: 13 -step: 1155 fd: 7 -step: 1156 fd: 13 -step: 1158 fd: 13 -step: 1160 fd: 13 -step: 1163 fd: 13 -step: 1166 fd: 13 -step: 1168 fd: 13 -step: 1169 fd: 7 -step: 1170 fd: 13 -step: 1171 fd: 7 -step: 1173 fd: 13 -step: 1181 fd: 13 -step: 1185 fd: 13 -step: 1197 fd: 13 -step: 1201 fd: 13 -step: 1203 fd: 13 -step: 1205 fd: 13 -step: 1211 fd: 13 -step: 1214 fd: 7 -step: 1220 fd: 7 -step: 1221 fd: 9 -step: 1233 fd: 13 -step: 1236 fd: 7 -step: 1239 fd: 13 -step: 1243 fd: 9 -step: 1247 fd: 13 -step: 1252 fd: 13 -step: 1255 fd: 13 -step: 1257 fd: 13 -step: 1259 fd: 13 -step: 1261 fd: 13 -step: 1267 fd: 13 -step: 1269 fd: 13 -step: 1271 fd: 13 -step: 1282 fd: 13 -step: 1284 fd: 13 -step: 1288 fd: 13 -step: 1293 fd: 13 -step: 1302 fd: 13 -step: 1313 fd: 13 -step: 1319 fd: 13 -step: 1321 fd: 7 -step: 1324 fd: 13 -step: 1325 fd: 7 -step: 1327 fd: 13 -step: 1329 fd: 13 -step: 1331 fd: 13 -step: 1336 fd: 13 -step: 1342 fd: 13 -step: 1344 fd: 13 -step: 1346 fd: 13 -step: 1351 fd: 13 -step: 1362 fd: 13 -step: 1366 fd: 7 -step: 1368 fd: 13 -step: 1371 fd: 13 -step: 1378 fd: 13 -step: 1388 fd: 13 -step: 1398 fd: 13 -step: 1400 fd: 13 -step: 1402 fd: 13 -step: 1406 fd: 13 -step: 1418 fd: 13 -step: 1421 fd: 13 -step: 1425 fd: 13 -step: 1427 fd: 13 -step: 1433 fd: 13 -step: 1438 fd: 7 -step: 1454 fd: 13 -step: 1464 fd: 13 -step: 1466 fd: 13 -step: 1479 fd: 13 -step: 1485 fd: 13 -step: 1488 fd: 13 -step: 1489 fd: 7 -step: 1490 fd: 13 -step: 1491 fd: 7 -step: 1498 fd: 13 -step: 1504 fd: 13 -step: 1508 fd: 13 -step: 1513 fd: 7 -step: 1517 fd: 13 -step: 1522 fd: 13 -step: 1527 fd: 13 -step: 1534 fd: 13 -step: 1539 fd: 7 -step: 1541 fd: 7 -step: 1546 fd: 7 -step: 1547 fd: 13 -step: 1549 fd: 13 -step: 1554 fd: 13 -step: 1563 fd: 13 -Cover: 67.35% pattern: 3 new_detected: 0 undected: 32 time: 0.05s -start with fault: G4 SA0 verify ... successful! -step: 3 fd: 3 -step: 6 fd: 2 -step: 7 fd: 0 -step: 9 fd: 2 -step: 11 fd: 0 -step: 12 fd: 0 -step: 13 fd: 2 -step: 18 fd: 2 -step: 22 fd: 10 -step: 23 fd: 8 -step: 26 fd: 8 -step: 28 fd: 8 -step: 30 fd: 8 -step: 31 fd: 3 -step: 32 fd: 8 -step: 34 fd: 3 -step: 37 fd: 3 -step: 60 fd: 2 -step: 62 fd: 0 -step: 63 fd: 2 -step: 68 fd: 8 -step: 70 fd: 10 -step: 72 fd: 8 -step: 76 fd: 10 -step: 78 fd: 8 -step: 82 fd: 0 -step: 84 fd: 0 -step: 91 fd: 10 -step: 100 fd: 2 -step: 101 fd: 0 -step: 102 fd: 2 -step: 103 fd: 0 -step: 104 fd: 2 -step: 106 fd: 0 -step: 109 fd: 0 -step: 111 fd: 2 -step: 112 fd: 0 -step: 113 fd: 8 -step: 115 fd: 8 -step: 118 fd: 2 -step: 119 fd: 8 -step: 133 fd: 8 -step: 135 fd: 10 -step: 137 fd: 8 -step: 148 fd: 8 -step: 152 fd: 10 -step: 156 fd: 10 -step: 157 fd: 8 -step: 160 fd: 10 -step: 171 fd: 3 -step: 179 fd: 8 -step: 182 fd: 10 -step: 192 fd: 8 -step: 207 fd: 2 -step: 208 fd: 0 -step: 211 fd: 8 -step: 212 fd: 2 -step: 213 fd: 0 -step: 214 fd: 2 -step: 215 fd: 0 -step: 219 fd: 10 -step: 221 fd: 8 -step: 223 fd: 10 -step: 226 fd: 10 -step: 229 fd: 10 -step: 234 fd: 8 -step: 241 fd: 8 -step: 244 fd: 8 -step: 246 fd: 8 -step: 249 fd: 8 -step: 251 fd: 8 -step: 254 fd: 8 -step: 260 fd: 8 -step: 262 fd: 10 -step: 268 fd: 8 -step: 274 fd: 10 -step: 284 fd: 2 -step: 286 fd: 10 -step: 288 fd: 8 -step: 290 fd: 10 -step: 291 fd: 0 -step: 293 fd: 8 -step: 294 fd: 2 -step: 297 fd: 0 -step: 298 fd: 2 -step: 299 fd: 0 -step: 300 fd: 2 -step: 301 fd: 0 -step: 304 fd: 2 -step: 305 fd: 8 -step: 310 fd: 10 -step: 312 fd: 8 -step: 315 fd: 10 -step: 317 fd: 8 -step: 319 fd: 10 -step: 321 fd: 8 -step: 323 fd: 10 -step: 336 fd: 2 -step: 337 fd: 0 -step: 338 fd: 2 -step: 340 fd: 2 -step: 343 fd: 8 -step: 347 fd: 3 -step: 354 fd: 10 -step: 356 fd: 8 -step: 369 fd: 2 -step: 370 fd: 0 -step: 371 fd: 2 -step: 372 fd: 0 -step: 375 fd: 8 -step: 378 fd: 10 -step: 381 fd: 8 -step: 383 fd: 10 -step: 387 fd: 8 -step: 389 fd: 10 -step: 391 fd: 10 -step: 410 fd: 10 -step: 415 fd: 10 -step: 418 fd: 10 -step: 423 fd: 10 -step: 432 fd: 10 -step: 436 fd: 8 -step: 441 fd: 8 -step: 452 fd: 10 -step: 456 fd: 10 -step: 466 fd: 8 -step: 468 fd: 8 -step: 470 fd: 10 -step: 483 fd: 2 -step: 484 fd: 0 -step: 485 fd: 2 -step: 487 fd: 2 -step: 488 fd: 0 -step: 489 fd: 2 -step: 490 fd: 0 -step: 491 fd: 2 -step: 493 fd: 0 -step: 498 fd: 2 -step: 499 fd: 0 -step: 500 fd: 2 -step: 502 fd: 8 -step: 503 fd: 0 -step: 506 fd: 2 -step: 507 fd: 0 -step: 508 fd: 2 -step: 509 fd: 8 -step: 510 fd: 0 -step: 511 fd: 2 -step: 512 fd: 0 -step: 513 fd: 2 -step: 519 fd: 10 -step: 521 fd: 8 -step: 523 fd: 10 -step: 525 fd: 8 -step: 531 fd: 10 -step: 539 fd: 10 -step: 542 fd: 10 -step: 543 fd: 8 -step: 547 fd: 3 -step: 549 fd: 3 -step: 551 fd: 3 -step: 558 fd: 10 -step: 562 fd: 10 -step: 565 fd: 10 -step: 569 fd: 10 -step: 575 fd: 8 -step: 577 fd: 8 -step: 579 fd: 10 -step: 582 fd: 8 -step: 586 fd: 8 -step: 589 fd: 3 -step: 593 fd: 8 -step: 599 fd: 10 -step: 603 fd: 10 -step: 605 fd: 10 -step: 607 fd: 10 -step: 626 fd: 10 -step: 629 fd: 10 -step: 635 fd: 0 -step: 639 fd: 10 -step: 641 fd: 10 -step: 654 fd: 10 -step: 661 fd: 2 -step: 662 fd: 0 -step: 663 fd: 2 -step: 664 fd: 0 -step: 665 fd: 2 -step: 666 fd: 0 -step: 667 fd: 2 -step: 668 fd: 0 -step: 670 fd: 10 -step: 673 fd: 8 -step: 674 fd: 2 -step: 677 fd: 8 -step: 680 fd: 10 -step: 682 fd: 8 -step: 687 fd: 8 -step: 690 fd: 10 -step: 692 fd: 10 -step: 701 fd: 8 -step: 704 fd: 8 -step: 707 fd: 10 -step: 720 fd: 8 -step: 729 fd: 8 -step: 731 fd: 8 -step: 733 fd: 8 -step: 742 fd: 8 -step: 750 fd: 10 -step: 755 fd: 8 -step: 759 fd: 8 -step: 761 fd: 8 -step: 783 fd: 0 -step: 792 fd: 10 -step: 802 fd: 10 -step: 812 fd: 10 -step: 815 fd: 10 -step: 817 fd: 10 -step: 821 fd: 10 -step: 824 fd: 10 -step: 830 fd: 0 -step: 831 fd: 2 -step: 834 fd: 0 -step: 835 fd: 2 -step: 838 fd: 10 -step: 845 fd: 10 -step: 849 fd: 10 -step: 853 fd: 8 -step: 855 fd: 8 -step: 866 fd: 8 -step: 870 fd: 10 -step: 873 fd: 8 -step: 879 fd: 8 -step: 881 fd: 8 -step: 883 fd: 8 -step: 887 fd: 10 -step: 891 fd: 8 -step: 894 fd: 8 -step: 896 fd: 10 -step: 898 fd: 8 -step: 907 fd: 8 -step: 911 fd: 8 -step: 916 fd: 8 -step: 918 fd: 8 -step: 923 fd: 10 -step: 934 fd: 8 -step: 936 fd: 8 -step: 938 fd: 8 -step: 943 fd: 8 -step: 952 fd: 8 -step: 954 fd: 8 -step: 957 fd: 3 -step: 959 fd: 3 -step: 961 fd: 3 -step: 963 fd: 8 -step: 966 fd: 8 -step: 968 fd: 8 -step: 972 fd: 8 -step: 987 fd: 2 -step: 990 fd: 2 -step: 992 fd: 2 -step: 993 fd: 0 -step: 994 fd: 2 -step: 996 fd: 0 -step: 999 fd: 2 -step: 1006 fd: 10 -step: 1011 fd: 10 -step: 1024 fd: 8 -step: 1026 fd: 10 -step: 1032 fd: 0 -step: 1033 fd: 2 -step: 1038 fd: 10 -step: 1053 fd: 8 -step: 1059 fd: 3 -step: 1061 fd: 3 -step: 1078 fd: 8 -step: 1080 fd: 8 -step: 1091 fd: 2 -step: 1094 fd: 2 -step: 1095 fd: 0 -step: 1097 fd: 2 -step: 1110 fd: 10 -step: 1112 fd: 10 -step: 1122 fd: 8 -step: 1125 fd: 8 -step: 1126 fd: 2 -step: 1127 fd: 0 -step: 1133 fd: 2 -step: 1134 fd: 0 -step: 1135 fd: 2 -step: 1136 fd: 0 -step: 1139 fd: 2 -step: 1140 fd: 0 -step: 1155 fd: 10 -step: 1159 fd: 10 -Cover: 67.35% pattern: 3 new_detected: 0 undected: 32 time: 0.07s -start with fault: G4 SA1 verify ... successful! -step: 2 fd: 11 -step: 4 fd: 11 -step: 5 fd: 16 -step: 8 fd: 12 -step: 13 fd: 11 -step: 19 fd: 5 -Cover: 83.67% pattern: 4 new_detected: 16 undected: 16 time: 0.07s -start with fault: G5 SA0 verify ... successful! -step: 1 fd: 3 -step: 3 fd: 2 -step: 4 fd: 2 -step: 5 fd: 2 -step: 8 fd: 3 -step: 11 fd: 3 -step: 12 fd: 3 -step: 13 fd: 3 -step: 16 fd: 3 -step: 18 fd: 3 -step: 21 fd: 0 -step: 25 fd: 2 -step: 29 fd: 2 -step: 32 fd: 2 -step: 37 fd: 3 -Cover: 83.67% pattern: 4 new_detected: 0 undected: 16 time: 0.07s -start with fault: G5 SA1 verify ... successful! -step: 1 fd: 2 -step: 18 fd: 2 -step: 21 fd: 2 -Cover: 86.73% pattern: 5 new_detected: 3 undected: 13 time: 0.07s -start with fault: G6 SA0 verify ... successful! -step: 0 fd: 3 -step: 1 fd: 4 -step: 4 fd: 4 -step: 8 fd: 3 -step: 9 fd: 4 -step: 10 fd: 1 -step: 11 fd: 4 -step: 15 fd: 4 -step: 17 fd: 4 -step: 18 fd: 1 -step: 21 fd: 4 -Cover: 89.80% pattern: 6 new_detected: 3 undected: 10 time: 0.07s -start with fault: G6 SA1 verify ... successful! -step: 0 fd: 0 -step: 1 fd: 0 -Cover: 89.80% pattern: 6 new_detected \ No newline at end of file diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index c3f90f3..167bedb 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -6,6 +6,7 @@ set(CMAKE_CXX_STANDARD 17) # 设置编译器优化选项 set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Ofast -march=native -flto -static") +# set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -O0 -g -static") # 设置源文件和头文件的路径 aux_source_directory(${PROJECT_SOURCE_DIR} SOURCES) diff --git a/src/circuit.cpp b/src/circuit.cpp index f62b5bb..8eecc80 100644 --- a/src/circuit.cpp +++ b/src/circuit.cpp @@ -23,6 +23,8 @@ void LUTCircuit::print() { } printf(")\n"); + + for(LUT* lut : luts) { printf("[v:%d vs:%d fd0:%d fd1:%d] ", lut->value, lut->vsat, lut->fd[0], lut->fd[1]); @@ -39,6 +41,10 @@ void LUTCircuit::print() { printf("total gate: %d\n", total_gate); } + + + + LUTCircuit* Circuit::build_lut_circuit() { LUTCircuit* C = new LUTCircuit(); @@ -125,8 +131,10 @@ LUTCircuit* Circuit::build_lut_circuit() { }); for(LUT* lut : C->luts) { - for(Gate* g : lut->inner_gates) { + for(int i=0; iinner_gates.size(); i++) { + Gate *g = lut->inner_gates[i]; g->parent_lut = lut; + g->id_in_lut = lut->fanins.size() + i; } } @@ -145,6 +153,77 @@ LUTCircuit* Circuit::build_lut_circuit() { } + +void Circuit::insert_lines_for_stem() { + + for(int j=0; jtype == Gate::LINE) break; + + g->is_stem = g->isPO ? g->fanouts.size() >= 1 : g->fanouts.size() >= 2; + if(!g->is_stem) continue; + + if(g->isPO) { + Gate* line = new Gate(); + line->name = g->name + "_line_PO"; + line->type = Gate::LINE; + line->isPI = false; + line->isPO = true; + line->is_stem = false; + + line->fanins.push_back(g); + g->fanouts.push_back(line); + + g->isPO = false; + POs.erase(std::find(POs.begin(), POs.end(), g)); + POs.push_back(line); + + gates.push_back(line); + name2gate.insert(std::make_pair(line->name, line)); + } + + printf(">>>> now: %s\n", g->name.c_str()); + + printf("outs: [ "); + for(Gate* out :g->fanouts){ + printf("%s ", out->name.c_str()); + } + printf("]\n"); + + for(int i=0; ifanouts.size(); i++) { + Gate* out = g->fanouts[i]; + + if(out->type == Gate::LINE) break; + + printf(" g_name: %s outname: %s\n", g->name.c_str(), out->name.c_str()); + + Gate* line = new Gate(); + line->name = g->name + "_line_" + out->name; + line->type = Gate::LINE; + line->isPI = false; + line->isPO = false; + + line->fanins.push_back(g); + line->fanouts.push_back(out); + + out->fanins.erase(std::find(out->fanins.begin(), out->fanins.end(), g)); + out->fanins.push_back(line); + + g->fanouts.erase(std::find(g->fanouts.begin(), g->fanouts.end(), out)); + g->fanouts.push_back(line); + + gates.push_back(line); + name2gate.insert(std::make_pair(line->name, line)); + + i--; + } + + } + +} + void Circuit::init_avg_dist() { int *now_dist = new int[gates.size() + 1] { 0 }; @@ -152,6 +231,8 @@ void Circuit::init_avg_dist() { int *total_cnt = new int[gates.size() + 1] { 0 }; // int *topo_cnt = new int[gates.size() + 1] { 0 }; + // memset(total_dist, 0, sizeof(int) * (gates.size() + 1)); + for(Gate* po : POs) { // memset(topo_cnt, 0, sizeof(int) * (gates.size() + 1)); // memset(now_dist, 0x3f, sizeof(int) * (gates.size() + 1)); @@ -182,15 +263,24 @@ void Circuit::init_avg_dist() { q.push(in); } } + + // printf("dist: %d\n", total_dist[name2gate["G132"]->id]); } } for(Gate* g : gates) { - // printf("gate: %s total: %d cnt: %d\n", g->name.c_str(), total_dist[g->id], total_cnt[g->id]); + + if(total_cnt[g->id] <= 0) { + printf("ERROR: gate: %s total: %d cnt: %d\n", g->name.c_str(), total_dist[g->id], total_cnt[g->id]); + exit(-1); + } + assert(total_cnt[g->id] > 0); g->avg_dist = total_dist[g->id] / total_cnt[g->id]; + printf("ERROR: gate: %s total: %d cnt: %d\n", g->name.c_str(), total_dist[g->id], total_cnt[g->id]); + // if(g->id) if(!g->isPO) assert(g->avg_dist > 0); } @@ -255,4 +345,34 @@ void Circuit::init_topo_index() { } } } + + std::sort(gates.begin(), gates.end(), [](Gate* a, Gate* b) { + return a->id < b->id; + }); } + + +void Circuit::print() { + + printf("PIs: ( "); + for(Gate* gate : PIs) { + printf("%s ", gate->name.c_str()); + } + printf(")\n"); + + const char *name[10] = {"AND", "NAND", "OR", "NOR", "XOR", "XNOR", "NOT", "BUF", "INPUT", "LINE"}; + + for(Gate* g : gates) { + printf("[sa0: %d sa1: %d v: %d vsat: %d] %s = %s (",g->fault_detected[0], g->fault_detected[1], g->value, g->cal_value() == g->value, g->name.c_str(), name[g->type]); + for(Gate* in : g->fanins) { + printf("%s ", in->name.c_str()); + } + printf(")\n"); + } + + printf("POs: ( "); + for(Gate* gate : POs) { + printf("%s ", gate->name.c_str()); + } + printf(")\n"); +} \ No newline at end of file diff --git a/src/circuit.h b/src/circuit.h index 57efb16..9a10c89 100644 --- a/src/circuit.h +++ b/src/circuit.h @@ -7,6 +7,32 @@ using ll = long long; namespace atpg_ls { +struct TMP_FAULT { + /* data */ + Gate *g; + + std::string name; + int stuck_at; + int is_stem; + int is_PO; + + friend bool operator < (const TMP_FAULT &lhs, const TMP_FAULT &rhs) { + if(lhs.name != rhs.name) { + return lhs.name < rhs.name; + } + if(lhs.stuck_at != rhs.stuck_at) { + return lhs.stuck_at < rhs.stuck_at; + } + if(lhs.is_stem != rhs.is_stem) { + return lhs.is_stem < rhs.is_stem; + } + if(lhs.is_PO != rhs.is_PO) { + return lhs.is_PO < rhs.is_PO; + } + return false; + } +}; + class Simulator; class Circuit; @@ -50,6 +76,10 @@ std::vector rtopo_gates; std::unordered_map name2gate; void parse_from_file(const char *filename); +void insert_lines_for_stem(); + +void print(); + LUTCircuit* build_lut_circuit(); void init_topo_index(); diff --git a/src/gate.cpp b/src/gate.cpp index 5fdb84d..ba41cc2 100644 --- a/src/gate.cpp +++ b/src/gate.cpp @@ -14,6 +14,8 @@ int Gate::cal_propagate_len(bool x) { return fpl[x]; } + std::queue q; + for(Gate* out : fanouts) { if(!out->is_detected(this)) continue; fpl[!value] = std::max(fpl[!value], out->fault_propagated_len[!out->value] + 1); @@ -66,6 +68,8 @@ int Gate::cal_value() { case NOT: res = !fanins[0]->value; break; + case LINE: + // pass through case BUF: res = fanins[0]->value; break; @@ -116,4 +120,17 @@ int Gate::cal_value() { break; } return res; +} + +int Gate::lut_get_value() { + return parent_lut->fault_table[id_in_lut][parent_lut->input_var<<1|parent_lut->value].value; +} + + +void Gate::lut_get_fault(int *fd, int *fpl) { + LUT::FaultInfo &info = parent_lut->fault_table[id_in_lut][parent_lut->input_var<<1|parent_lut->value]; + fd[0] = info.fd[0] && parent_lut->fd[!parent_lut->value]; + fd[1] = info.fd[1] && parent_lut->fd[!parent_lut->value]; + fpl[0] = info.fpl[0] + info.fd[0] * parent_lut->fpl[!parent_lut->value]; + fpl[1] = info.fpl[1] + info.fd[1] * parent_lut->fpl[!parent_lut->value]; } \ No newline at end of file diff --git a/src/gate.h b/src/gate.h index ea3c24f..28e9cf3 100644 --- a/src/gate.h +++ b/src/gate.h @@ -21,7 +21,7 @@ public: int level; int rtopo; std::string name; - enum Type { AND, NAND, OR, NOR, XOR, XNOR, NOT, BUF, INPUT } type; + enum Type { AND, NAND, OR, NOR, XOR, XNOR, NOT, BUF, INPUT, LINE } type; int value; bool isPI; bool isPO; @@ -50,7 +50,11 @@ public: LUT* parent_lut; int id_in_lut; + int is_stem; + int lut_get_value(); + void lut_get_fault(int *fd, int *fpl); + // ( partical ) score // score(x) = for y in neibor(x) { ~V_x,V_y make - ~V_x,V_y break } diff --git a/src/ls.cpp b/src/ls.cpp index 67dda36..47041fd 100644 --- a/src/ls.cpp +++ b/src/ls.cpp @@ -146,27 +146,105 @@ void LUTCircuit::ls_main() { num_total_fault = num_undetected_fault = num_gates * 2; printf("staring local search ...\n"); + + std::queue faults; - std::queue> faults; - for(LUT* lut : luts) { - for(Gate* g : lut->inner_gates) { - if(g->fanouts.size() == 1 && (g->fanouts[0]->type == Gate::Type::BUF || g->fanouts[0]->type == Gate::Type::NOT)) { - printf("sat delete: %s\n", g->name.c_str()); + for(Gate* g : C->gates) { + + std::string name = g->name; + // if(name.find("_") != std::string::npos) { + // name = name.substr(0, name.find("_")); + // } + + if(g->is_stem) { + printf("stem: %s\n", name.c_str()); + faults.push(TMP_FAULT{g, name, 0, 1, 0}); + faults.push(TMP_FAULT{g, name, 1, 1, 0}); + } else { + + if(g->isPO) { + printf("out: %s\n", name.c_str()); + faults.push(TMP_FAULT{g, name, 0, g->type != Gate::LINE, g->type == Gate::LINE}); + faults.push(TMP_FAULT{g, name, 1, g->type != Gate::LINE, g->type == Gate::LINE}); continue; } - faults.push(std::make_pair(g, 0)); - faults.push(std::make_pair(g, 1)); + + assert(g->fanouts.size() == 1); + Gate *fanout = g->fanouts[0]; + + int stem = (!g->isPI) && (g->type != Gate::LINE); + + if(fanout->type == Gate::Type::BUF || fanout->type == Gate::Type::NOT) { + continue; + } else if(fanout->type == Gate::Type::XOR || fanout->type == Gate::Type::XNOR) { + faults.push(TMP_FAULT{g, name, 0, stem, 0}); + faults.push(TMP_FAULT{g, name, 1, stem, 0}); + } else if(fanout->type == Gate::Type::NAND || fanout->type == Gate::Type::AND) { + faults.push(TMP_FAULT{g, name, 1, stem, 0}); + } else if(fanout->type == Gate::Type::NOR || fanout->type == Gate::Type::OR) { + faults.push(TMP_FAULT{g, name, 0, stem, 0}); + } else { + assert(false); + } } } + printf("fault-size: %d\n", faults.size()); + + std::vector t_faults; + std::set t_verify_set; + + while(!faults.empty()) { + TMP_FAULT f = faults.front(); + faults.pop(); + + assert(t_verify_set.count(f) == 0); + + t_faults.push_back(f); + t_verify_set.insert(f); + } + + for(TMP_FAULT &f : t_faults) { + faults.push(f); + } + + // std::sort(t_faults.begin(), t_faults.end(), [](const TMP_FAULT &a, const TMP_FAULT &b) { + // int ta = std::atoi(a.g->name.substr(1).c_str()); + // int tb = std::atoi(b.g->name.substr(1).c_str()); + // return ta < tb; + // }); + + // for(auto &f : t_faults) { + + // } + + printf("fault-size: %d\n", t_faults.size()); + printf("verify-size: %d\n", t_verify_set.size()); + assert(t_faults.size() == t_verify_set.size()); + + // for(TMP_FAULT &f : t_faults) { + + // printf("!! Fault: %s stuck-at: %d is_stem: %d is_po: %d\n", f.g->name.c_str(), f.stuck_at, f.is_stem, f.is_PO); + + // std::vector input_vector; + // bool detected = sat_atpg(f, input_vector); + + // printf(">> Fault: %s stuck-at: %d is_stem: %d is_po: %d detected: %d\n", f.g->name.c_str(), f.stuck_at, f.is_stem, f.is_PO, detected); + + // } + + // exit(0); + auto start = std::chrono::high_resolution_clock::now(); + // int cnt = 0; + while(!faults.empty()) { while(!faults.empty()) { - auto [g, stuck_at] = faults.front(); - if(fault_detected[g->id-1][stuck_at]) { - faults.pop(); + TMP_FAULT f = faults.front(); + if(fault_detected[f.g->id-1][f.stuck_at]) { + faults.pop(); } else { break; } @@ -176,14 +254,17 @@ void LUTCircuit::ls_main() { ls_random_sol(); - auto [g, stuck_at] = faults.front(); faults.pop(); + TMP_FAULT f = faults.front(); faults.pop(); + Gate* g = f.g; + int stuck_at = f.stuck_at; + printf("start with fault: %s SA%d\t", g->name.c_str(), stuck_at); std::vector inputs; printf("verify ..."); - int res1 = sat_atpg(g->name.c_str(), stuck_at, inputs); + int res1 = sat_atpg(f, inputs); if(res1 == 0) { printf(" unsat!\n"); @@ -196,13 +277,24 @@ void LUTCircuit::ls_main() { PIs[i]->value = inputs[i]; } + printf("sim: %s %d\n", g->name.c_str(), stuck_at); + for(int i=0; isimulate(PIs, score, fault_detected); + if(g->name == "G6") { + simulator->print(); + } + if(simulator->name2gate[g->name]->fault_detected[stuck_at]) { printf(" successful!\n"); } else { printf(" failed!\n"); + // exit(-1); } for(LUT* lut : luts) { @@ -218,7 +310,8 @@ void LUTCircuit::ls_main() { int res = simulator->verify(this, fault_detected); assert(res == 1); - assert(simulator->name2gate[g->name]->fault_detected[stuck_at]); + // printf("g: %s\n", g->name.c_str()); + // assert(simulator->name2gate[g->name]->fault_detected[stuck_at]); int num_fault = 0; @@ -244,7 +337,8 @@ void LUTCircuit::ls_main() { auto end = std::chrono::high_resolution_clock::now(); auto duration = std::chrono::duration_cast(end - start).count(); - + + // cnt++; printf("Cover: %.2f%% pattern: %d new_detected: %d undected: %d time: %.2fs\n", (double)num_detected_fault / num_total_fault * 100, num_pattern, num_fault, num_undetected_fault, (double)duration/1000); // break; @@ -277,6 +371,8 @@ void LUTCircuit::ls_gen_sol(Gate* target, int stuck_at) { // printf("dert_fault_propagated_weight: %.2f\n", pick->score_fault_propagated_weight); // printf("dert_up_cost: %.2f\n", pick->score_fault_update_cost); + int last = simulator->name2gate[target->name]->fault_detected[stuck_at]; + ls_flip(pick); // double t2 = check(); @@ -285,8 +381,9 @@ void LUTCircuit::ls_gen_sol(Gate* target, int stuck_at) { if(pick->isPI) { int score; simulator->simulate(PIs, score, fault_detected); - if(!simulator->name2gate[target->name]->fault_detected[stuck_at]) { + if(simulator->name2gate[target->name]->fault_detected[stuck_at] != last) { ls_flip(pick); + pick->CC = 0; } // printf("step: %d fd: %d\n", step, score); } @@ -360,7 +457,6 @@ void LUTCircuit::ls_random_sol() { lut->vunat_cost = OPT(vsat_inc) * 100; } - lut->is_good_var = 0; lut->CC = 1; for(Gate* g : lut->inner_gates) { diff --git a/src/lut.cpp b/src/lut.cpp index db89922..f1d4283 100644 --- a/src/lut.cpp +++ b/src/lut.cpp @@ -12,7 +12,7 @@ void LUT::flip_value() { } } -void LUT::cal_fault_info(int *fd, int* fpl, int test) { +void LUT::cal_fault_info(int *fd, int* fpl) { fd[0] = fd[1] = fpl[0] = fpl[1] = 0; if(isPO) { @@ -22,7 +22,7 @@ void LUT::cal_fault_info(int *fd, int* fpl, int test) { } for(auto&[out, id] : fanouts_with_id) { - // if(!out->vsat) continue; + if(!out->vsat) continue; FaultInfo &info = out->fault_table[id][out->input_var << 1 | out->value]; @@ -39,14 +39,36 @@ void LUT::cal_fault_info(int *fd, int* fpl, int test) { fpl[0] = std::max(fpl[0], t_fpl[0]); fpl[1] = std::max(fpl[1], t_fpl[1]); - - // if(test) { - // assert(out->value_table[out->input_var] == out->value); - // printf("recal: %s out: %s [fd0:%d fd1:%d fpl0:%d fpl1:%d] [ifd_0:%d ifd_1:%d ifpl0:%d ifpl1:%d]\n", name, out->name, - // out->fd[0], out->fd[1], out->fpl[0], out->fpl[1] - // , info.fd[0], info.fd[1], info.fpl[0], info.fpl[1]); - // } } + + // std::vector reigon; + + // std::priority_queue, std::vector>, + // std::function&, const std::pair&)>> pq([](const std::pair& p1, const std::pair& p2) { + // return p1.first->id < p2.first->id; + // }); + + // for(Gate* out : gate->fanouts) { + // if(!out->vsat) continue; + // pq.push(std::make_pair(out, 0)); + // } + + // pq.push(std::make_pair(gate, 0)); + + // while(!q.empty()) { + // auto [now, level] = q.front(); q.pop(); + + // for(Gate* out : now->fanouts) { + // if(!out->is_detected(now)) continue; + + // if(level + 1 < OPT(lut)) { + // q.push(std::make_pair(out, level + 1)); + // } + // } + + + // } + } int LUT::cal_value() { diff --git a/src/lut.h b/src/lut.h index 2af1887..47c4800 100644 --- a/src/lut.h +++ b/src/lut.h @@ -50,17 +50,18 @@ public: void init_lookup_table(); // local search + bool vsat; int vunat_cost; bool uptag; int up_cost; int fd[2]; int fpl[2]; - int is_good_var; + // int is_good_var; int CC; int cal_value(); - void cal_fault_info(int *t_fd, int *t_fpl, int test = 0); + void cal_fault_info(int *t_fd, int *t_fpl); void get_fault_info(Gate *gate, int *t_fd, int *t_fpl); // score diff --git a/src/main.cpp b/src/main.cpp index 11021c0..5e068a0 100644 --- a/src/main.cpp +++ b/src/main.cpp @@ -13,16 +13,41 @@ int main(int argc, char *argv[]) { srand(OPT(seed)); Circuit *circuit = new Circuit(); + Simulator* simulator = new Simulator(); printf("parsing file %s ...\n", OPT(instance).c_str()); circuit->parse_from_file(OPT(instance).c_str()); + circuit->insert_lines_for_stem(); + simulator->parse_from_file(OPT(instance).c_str()); + simulator->insert_lines_for_stem(); + circuit->init_topo_index(); simulator->init_topo_index(); + + circuit->init_avg_dist(); + circuit->print(); + + /** + * D算法/电路 - 200000F = 时间优势好 (123) -> F -> (5,6) + * SAT - 200000F * avg(N) (1011) (1010) + * + * primary input 电路的输入 + * gate input 单个门的输入 + * + * (F0) + * PIs assignment (10101010101010) -> (F0) + * + * (10101010101010) inital sol + * LOCAL + F0 + * + * (SAT + LS) + **/ sat_atpg_init(OPT(instance).c_str()); + // circuit-> printf("building lut circuit ...\n"); diff --git a/src/sat_atpg.cpp b/src/sat_atpg.cpp index 4492319..ba07630 100644 --- a/src/sat_atpg.cpp +++ b/src/sat_atpg.cpp @@ -16,7 +16,6 @@ #include #include - CircuitGraph *graph; Iscas89Parser *parser; FaultManager *fault_manager; @@ -24,16 +23,13 @@ FaultCnfMaker *fault_cnf_maker; std::unique_ptr solver; ProxyCnf *proxy; -std::map fault_map; +std::map fault_map; -bool sat_atpg(const char* name, int stuck_at, std::vector &input_vector) { +bool sat_atpg(const TMP_FAULT &fal, std::vector &input_vector) { - if(fault_map.count(std::string(name)) == 0) { - return false; - } + assert(fault_map.count(fal) != 0); - Fault f = fault_map[std::string(name)]; - f.stuck_at = stuck_at; + Fault f = fault_map[fal]; fault_cnf_maker->make_fault(f, *proxy); @@ -85,22 +81,42 @@ void sat_atpg_init(const char* file) { proxy = new ProxyCnf(*solver); + int sz = 0; + while(fault_manager->has_faults_left()) { Fault f = fault_manager->next_fault(); - // printf("Fault: %s stuck-at: %d is_stem: %d is_po: %d\n", f.line->name.c_str(), f.stuck_at, f.is_stem, f.is_primary_output); + sz++; - if(f.is_stem) { - if(fault_map.count(f.line->name)) { - Fault& g = fault_map[f.line->name]; - f.stuck_at = g.stuck_at; - assert(f == g); + if(f.is_stem || (f.line->source == nullptr && f.line->destinations.size() == 1)) { + + printf("Fault: %s stuck-at: %d is_stem: %d is_po: %d dest: %d\n", f.line->name.c_str(), f.stuck_at, f.is_stem, f.is_primary_output, f.line->destinations.size()); + TMP_FAULT tf = TMP_FAULT{nullptr, f.line->name, f.stuck_at, f.is_stem, f.is_primary_output}; + assert(fault_map.count(tf) == 0); + fault_map[tf] = f; + + } else { + + std::string name; + + if(f.is_primary_output) { + name = f.line->name + "_line_PO"; } else { - printf(">> Fault: %s stuck-at: %d is_stem: %d is_po: %d\n", f.line->name.c_str(), f.stuck_at, f.is_stem, f.is_primary_output); - fault_map[f.line->name] = f; + name = f.line->name + "_line_" + f.connection.gate->get_output()->name; } + + printf("Fault: %s stuck-at: %d is_stem: %d is_po: %d dest: %d\n", name.c_str(), f.stuck_at, f.is_stem, f.is_primary_output, f.line->destinations.size()); + + TMP_FAULT tf = TMP_FAULT{nullptr, name, f.stuck_at, f.is_stem, f.is_primary_output}; + assert(fault_map.count(tf) == 0); + fault_map[tf] = f; } + + // printf(">> Fault: %s stuck-at: %d is_stem: %d is_po: %d\n", f.line->name.c_str(), f.stuck_at, f.is_stem, f.is_primary_output); } + printf("tg-pro fault-size: %d table-size: %d\n", sz, fault_map.size()); + + assert(sz == fault_map.size()); // exit(0); } \ No newline at end of file diff --git a/src/sat_atpg.h b/src/sat_atpg.h index afc1926..12cab51 100644 --- a/src/sat_atpg.h +++ b/src/sat_atpg.h @@ -2,5 +2,7 @@ #include "circuit.h" -bool sat_atpg(const char* name, int stuck_at, std::vector &input_vector); +using atpg_ls::TMP_FAULT; + +bool sat_atpg(const TMP_FAULT &fal, std::vector &input_vector); void sat_atpg_init(const char* file); \ No newline at end of file diff --git a/src/simulator.cpp b/src/simulator.cpp index 15fe79f..69a8167 100644 --- a/src/simulator.cpp +++ b/src/simulator.cpp @@ -18,7 +18,7 @@ int Simulator::verify(LUTCircuit *lut_circuit, int** fault_detected) { } for(LUT* lut : lut_circuit->rtopo_luts) { - lut->cal_fault_info(lut->fd, lut->fpl, 1); + lut->cal_fault_info(lut->fd, lut->fpl); } // lut_circuit->print(); diff --git a/test.py b/test.py deleted file mode 100644 index ab6151f..0000000 --- a/test.py +++ /dev/null @@ -1,7 +0,0 @@ - -import os - -for i in range(10000): - res = os.system("./atpg -i ./benchmark/c432.bench --lut=8 --seed=%d" % i) - if res != 0: - break