diff --git a/.vscode/settings.json b/.vscode/settings.json index 9874127..6b25936 100644 --- a/.vscode/settings.json +++ b/.vscode/settings.json @@ -86,6 +86,10 @@ "map": "cpp", "shared_mutex": "cpp", "thread": "cpp", - "typeindex": "cpp" + "typeindex": "cpp", + "csignal": "cpp", + "strstream": "cpp", + "codecvt": "cpp", + "cfenv": "cpp" } } \ No newline at end of file diff --git a/Atalanta b/Atalanta new file mode 160000 index 0000000..12d4053 --- /dev/null +++ b/Atalanta @@ -0,0 +1 @@ +Subproject commit 12d405311c3dc9f371a9009bb5cdc8844fe34f90 diff --git a/CMakeLists.txt b/CMakeLists.txt index 0d0cc75..bc2c70b 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -1,19 +1,9 @@ -cmake_minimum_required(VERSION 3.0) +cmake_minimum_required(VERSION 3.20) -project(atpg) -set(CMAKE_CXX_STANDARD 17) +project(atpg-ls) -# 设置编译器优化选项 -set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Ofast -march=native -flto") +# 子模块 +add_subdirectory(tg-pro) +add_subdirectory(src) -# 设置源文件和头文件的路径 -aux_source_directory(${PROJECT_SOURCE_DIR}/src SOURCES) -set(INCLUDES ${PROJECT_SOURCE_DIR}/src) - -message(${SOURCES}) - -# 生成可执行文件 -add_executable(${PROJECT_NAME} ${SOURCES}) - -# 添加头文件 -include_directories(${INCLUDES}) \ No newline at end of file +target_link_libraries(atpg atpg_backend sat_solver) \ No newline at end of file diff --git a/atpg b/atpg deleted file mode 100755 index 14619b5..0000000 Binary files a/atpg and /dev/null differ diff --git a/b01.test b/b01.test new file mode 100644 index 0000000..b255349 --- /dev/null +++ b/b01.test @@ -0,0 +1,26 @@ +* 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 new file mode 100644 index 0000000..8647a95 --- /dev/null +++ b/b01.txt @@ -0,0 +1,1128 @@ +-- 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/crun b/crun index 6a6824a..6718396 100755 --- a/crun +++ b/crun @@ -2,13 +2,17 @@ clear -cmake . && make -j +mkdir -p build +cd build + +cmake .. && make -j if [ $? -ne 0 ]; then echo "compile failed." else + cd .. clear echo "========================" - time ./atpg -i $1 --lut=12 --seed=19260817 + time ./build/src/atpg -i $1 --lut=12 --seed=19260817 fi diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt new file mode 100644 index 0000000..c3f90f3 --- /dev/null +++ b/src/CMakeLists.txt @@ -0,0 +1,18 @@ +cmake_minimum_required(VERSION 3.20) + +project(atpg) + +set(CMAKE_CXX_STANDARD 17) + +# 设置编译器优化选项 +set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Ofast -march=native -flto -static") + +# 设置源文件和头文件的路径 +aux_source_directory(${PROJECT_SOURCE_DIR} SOURCES) +set(INCLUDES ${PROJECT_SOURCE_DIR}) + +# 添加头文件 +include_directories(${INCLUDES}, ${PROJECT_SOURCE_DIR}/../tg-pro/src) + +# 生成可执行文件 +add_executable(${PROJECT_NAME} ${SOURCES}) \ No newline at end of file diff --git a/src/checker.cpp b/src/checker.cpp index 044880d..a5aa118 100644 --- a/src/checker.cpp +++ b/src/checker.cpp @@ -2,6 +2,8 @@ #include "circuit.h" +using namespace atpg_ls; + double LUTCircuit::check() { // static bool init = 0; diff --git a/src/circuit.cpp b/src/circuit.cpp index 7731696..f62b5bb 100644 --- a/src/circuit.cpp +++ b/src/circuit.cpp @@ -4,6 +4,8 @@ #include "circuit.h" #include "paras.h" +using namespace atpg_ls; + void LUTCircuit::print() { std::set st; @@ -184,7 +186,7 @@ void Circuit::init_avg_dist() { } for(Gate* g : gates) { - printf("gate: %s total: %d cnt: %d\n", g->name.c_str(), total_dist[g->id], total_cnt[g->id]); + // printf("gate: %s total: %d cnt: %d\n", g->name.c_str(), total_dist[g->id], total_cnt[g->id]); assert(total_cnt[g->id] > 0); g->avg_dist = total_dist[g->id] / total_cnt[g->id]; diff --git a/src/circuit.h b/src/circuit.h index 9ae08c7..57efb16 100644 --- a/src/circuit.h +++ b/src/circuit.h @@ -5,6 +5,8 @@ using ll = long long; +namespace atpg_ls { + class Simulator; class Circuit; @@ -26,7 +28,7 @@ void ls_flip(LUT *lut); void ls_main(); void ls_init(); void ls_random_sol(); -void ls_gen_sol(); +void ls_gen_sol(Gate* target, int stuck_at); // checker double check(); @@ -53,4 +55,6 @@ LUTCircuit* build_lut_circuit(); void init_topo_index(); void init_avg_dist(); -}; \ No newline at end of file +}; + +} \ No newline at end of file diff --git a/src/fault.h b/src/fault.h index 2c405e5..3722f04 100644 --- a/src/fault.h +++ b/src/fault.h @@ -2,9 +2,13 @@ #include "gate.h" +namespace atpg_ls { + class Fault { public: Gate* gate; enum Type { SA0, SA1 } type; Fault(Gate* gate, Type type):gate(gate),type(type) {} -}; \ No newline at end of file +}; + +} \ No newline at end of file diff --git a/src/gate.cpp b/src/gate.cpp index 82b80a3..5fdb84d 100644 --- a/src/gate.cpp +++ b/src/gate.cpp @@ -2,6 +2,8 @@ #include "assert.h" +using namespace atpg_ls; + int Gate::cal_propagate_len(bool x) { int fpl[2]; diff --git a/src/gate.h b/src/gate.h index 577d630..ea3c24f 100644 --- a/src/gate.h +++ b/src/gate.h @@ -8,6 +8,8 @@ #include #include +namespace atpg_ls { + class LUT; class Gate { @@ -57,4 +59,6 @@ public: // [ cal_FPLS(~Vx, fanouts) - cal_FPLS(Vx, fanouts) ] * - FPLS_COST(x) // [ cal_FDS(~Vx, fanouts) - cal_FDS(Vx, fanouts) ] * - FDS_COST(x) -}; \ No newline at end of file +}; + +} \ No newline at end of file diff --git a/src/ls.cpp b/src/ls.cpp index 353a849..67dda36 100644 --- a/src/ls.cpp +++ b/src/ls.cpp @@ -5,6 +5,9 @@ #include "circuit.h" #include "paras.h" #include "simulator.h" +#include "sat_atpg.h" + +using namespace atpg_ls; LUT* LUTCircuit::ls_pick() { @@ -144,19 +147,79 @@ void LUTCircuit::ls_main() { printf("staring local search ...\n"); + 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()); + continue; + } + faults.push(std::make_pair(g, 0)); + faults.push(std::make_pair(g, 1)); + } + } + auto start = std::chrono::high_resolution_clock::now(); - while(num_undetected_fault != 0) { + while(!faults.empty()) { + + while(!faults.empty()) { + auto [g, stuck_at] = faults.front(); + if(fault_detected[g->id-1][stuck_at]) { + faults.pop(); + } else { + break; + } + } + + if(faults.empty()) break; ls_random_sol(); - ls_gen_sol(); + auto [g, stuck_at] = faults.front(); faults.pop(); + printf("start with fault: %s SA%d\t", g->name.c_str(), stuck_at); - // exit(0); + std::vector inputs; + + printf("verify ..."); + + int res1 = sat_atpg(g->name.c_str(), stuck_at, inputs); + + if(res1 == 0) { + printf(" unsat!\n"); + continue; + } + + assert(inputs.size() == PIs.size()); + + for(int i=0; ivalue = inputs[i]; + } + + int score; + simulator->simulate(PIs, score, fault_detected); + + if(simulator->name2gate[g->name]->fault_detected[stuck_at]) { + printf(" successful!\n"); + } else { + printf(" failed!\n"); + } + + for(LUT* lut : luts) { + lut->input_var = 0; + for(int i=0; ifanins.size(); i++) { + LUT* in = lut->fanins[i]; + lut->input_var |= (in->value << i); + } + } + + ls_gen_sol(g, stuck_at); int res = simulator->verify(this, fault_detected); assert(res == 1); + assert(simulator->name2gate[g->name]->fault_detected[stuck_at]); + int num_fault = 0; for(Gate* g : simulator->gates) { @@ -192,11 +255,10 @@ void LUTCircuit::ls_main() { std::cout << "Execution time: " << duration << " milliseconds" << std::endl; } -void LUTCircuit::ls_gen_sol() { +void LUTCircuit::ls_gen_sol(Gate* target, int stuck_at) { for(int step=0; ; step++) { // printf("step: %d\n", step); - LUT* pick = ls_pick(); @@ -223,7 +285,10 @@ void LUTCircuit::ls_gen_sol() { if(pick->isPI) { int score; simulator->simulate(PIs, score, fault_detected); - printf("step: %d fd: %d\n", step, score); + if(!simulator->name2gate[target->name]->fault_detected[stuck_at]) { + ls_flip(pick); + } + // printf("step: %d fd: %d\n", step, score); } } } diff --git a/src/lut.cpp b/src/lut.cpp index 9c121f5..db89922 100644 --- a/src/lut.cpp +++ b/src/lut.cpp @@ -3,6 +3,8 @@ #include "lut.h" #include "paras.h" +using namespace atpg_ls; + void LUT::flip_value() { value ^= 1; for(auto&[out, id] : fanouts_with_id) { diff --git a/src/lut.h b/src/lut.h index 7b94d85..2af1887 100644 --- a/src/lut.h +++ b/src/lut.h @@ -1,9 +1,11 @@ #pragma once -class LUTCircuit; - #include "gate.h" +namespace atpg_ls { + +class LUTCircuit; + class LUT { public: LUT(Gate *gate, LUTCircuit *circuit); @@ -71,3 +73,5 @@ public: void cal_score(); void cal_update(); }; + +} diff --git a/src/main.cpp b/src/main.cpp index a76cad8..11021c0 100644 --- a/src/main.cpp +++ b/src/main.cpp @@ -1,6 +1,9 @@ #include "circuit.h" #include "simulator.h" #include "paras.h" +#include "sat_atpg.h" + +using namespace atpg_ls; int main(int argc, char *argv[]) { @@ -18,6 +21,8 @@ int main(int argc, char *argv[]) { circuit->init_topo_index(); simulator->init_topo_index(); circuit->init_avg_dist(); + + sat_atpg_init(OPT(instance).c_str()); // circuit-> printf("building lut circuit ...\n"); @@ -31,8 +36,6 @@ int main(int argc, char *argv[]) { printf("LUT:\t%ld\n", C->luts.size()); printf("================================ \n"); - - // C->print(); C->ls_main(); return 0; diff --git a/src/parse.cpp b/src/parse.cpp index 5e3451b..26cb84b 100644 --- a/src/parse.cpp +++ b/src/parse.cpp @@ -6,6 +6,8 @@ #include #include +using namespace atpg_ls; + void line2tokens(const std::string &line, std::vector &tokens) { std::string token; for(char c : line) { diff --git a/src/sat_atpg.cpp b/src/sat_atpg.cpp new file mode 100644 index 0000000..4492319 --- /dev/null +++ b/src/sat_atpg.cpp @@ -0,0 +1,106 @@ +#include "sat_atpg.h" + +#include "circuit_graph.h" +#include "iscas89_parser.h" +#include "circuit_to_cnf.h" +#include "fault_cnf.h" +#include "fault_manager.h" +#include "sat/sat_solver.h" +#include "solver_proxy.h" + +#include "util/log.h" +#include "util/timer.h" + +#include +#include +#include +#include + + +CircuitGraph *graph; +Iscas89Parser *parser; +FaultManager *fault_manager; +FaultCnfMaker *fault_cnf_maker; +std::unique_ptr solver; +ProxyCnf *proxy; + +std::map fault_map; + +bool sat_atpg(const char* name, int stuck_at, std::vector &input_vector) { + + if(fault_map.count(std::string(name)) == 0) { + return false; + } + + Fault f = fault_map[std::string(name)]; + f.stuck_at = stuck_at; + + fault_cnf_maker->make_fault(f, *proxy); + + SatSolver::SolveStatus status = solver->solve_prepared(); + + for (Line* l : graph->get_inputs()) { + int8_t val = solver->get_value(line_to_literal(l->id)); + input_vector.push_back(val == -1 ? 0 : 1); + } + + if(status == SatSolver::Sat) { + return true; + } else if(status == SatSolver::Unsat) { + return false; + } else { + assert(false); + printf(">> UNKNOWN\n"); + } +} + +void sat_atpg_init(const char* file) { + + graph = new CircuitGraph(); + parser = new Iscas89Parser(); + + std::ifstream ifs(file); + if (!ifs.good()) { + std::cout << "can't open file" << file; + exit(-1); + } + + if (!parser->parse(ifs, *graph)) { + std::cout << "can't parse file" << file; + exit(-1); + } + + solver = SolverFactory::make_solver(); + + if (!solver) { + std::cout << "No SAT solver, can't run"; + exit(-1); + } + + fault_manager = new FaultManager(*graph); + + fault_cnf_maker = new FaultCnfMaker(*graph); + fault_cnf_maker->set_threshold_ratio(0.6); + + + proxy = new ProxyCnf(*solver); + + 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); + + 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); + } 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; + } + } + } + + // exit(0); +} \ No newline at end of file diff --git a/src/sat_atpg.h b/src/sat_atpg.h new file mode 100644 index 0000000..afc1926 --- /dev/null +++ b/src/sat_atpg.h @@ -0,0 +1,6 @@ +#pragma once + +#include "circuit.h" + +bool sat_atpg(const char* name, int stuck_at, std::vector &input_vector); +void sat_atpg_init(const char* file); \ No newline at end of file diff --git a/src/score.cpp b/src/score.cpp index a2d3514..1b223ab 100644 --- a/src/score.cpp +++ b/src/score.cpp @@ -1,6 +1,8 @@ #include "lut.h" #include "circuit.h" +using namespace atpg_ls; + void LUT::cal_score() { score = 0; diff --git a/src/simulator.cpp b/src/simulator.cpp index 49defbb..15fe79f 100644 --- a/src/simulator.cpp +++ b/src/simulator.cpp @@ -1,5 +1,7 @@ #include "simulator.h" +using namespace atpg_ls; + int Simulator::verify(LUTCircuit *lut_circuit, int** fault_detected) { // lut_circuit->check(); @@ -33,7 +35,9 @@ int Simulator::verify(LUTCircuit *lut_circuit, int** fault_detected) { LUT* l = lut->fanins[i]; input_var |= l->value << i; } + assert(input_var == lut->input_var); + if(!lut->isPI) assert(lut->value_table[lut->input_var] == lut->value); // printf(">> LUT: %s\n", lut->name); diff --git a/src/simulator.h b/src/simulator.h index b8c9d96..b03acea 100644 --- a/src/simulator.h +++ b/src/simulator.h @@ -2,8 +2,12 @@ #include "circuit.h" +namespace atpg_ls { + class Simulator : public Circuit { public: void simulate(std::vector &inputs, int &score, int** fault_detected); int verify(LUTCircuit *lut_circuit, int** fault_detected); -}; \ No newline at end of file +}; + +} \ No newline at end of file diff --git a/tg-pro b/tg-pro new file mode 160000 index 0000000..7f0eef8 --- /dev/null +++ b/tg-pro @@ -0,0 +1 @@ +Subproject commit 7f0eef881be4d91aef0095e3a889e485a4e42f5d