v1.6: 结合SAT-ATPG，覆盖率拉满

.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"
     }
 }

Atalanta

@@ -0,0 +1 @@
+Subproject commit 12d405311c3dc9f371a9009bb5cdc8844fe34f90

CMakeLists.txt

@@ -1,19 +1,9 @@
-cmake_minimum_required(VERSION 3.0)
+cmake_minimum_required(VERSION 3.20)
 
-project(atpg)
+project(atpg-ls)
-set(CMAKE_CXX_STANDARD 17)
 
-# 设置编译器优化选项
+# 子模块
-set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Ofast -march=native -flto")
+add_subdirectory(tg-pro)
+add_subdirectory(src)
 
-# 设置源文件和头文件的路径
+target_link_libraries(atpg atpg_backend sat_solver)
-aux_source_directory(${PROJECT_SOURCE_DIR}/src SOURCES)
-set(INCLUDES ${PROJECT_SOURCE_DIR}/src)
-
-message(${SOURCES})
-
-# 生成可执行文件
-add_executable(${PROJECT_NAME} ${SOURCES})
-
-# 添加头文件
-include_directories(${INCLUDES})

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

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
 

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})

src/checker.cpp

@@ -2,6 +2,8 @@
 
 #include "circuit.h"
 
+using namespace atpg_ls;
+
 double LUTCircuit::check() {
 
     // static bool init = 0;

src/circuit.cpp

@@ -4,6 +4,8 @@
 #include "circuit.h"
 #include "paras.h"
 
+using namespace atpg_ls;
+
 void LUTCircuit::print() {
 
     std::set<Gate*> 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];

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();
@@ -54,3 +56,5 @@ void init_topo_index();
 void init_avg_dist();
 
 };
+
+}

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) {}
 };
+
+}

src/gate.cpp

@@ -2,6 +2,8 @@
 
 #include "assert.h"
 
+using namespace atpg_ls;
+
 int Gate::cal_propagate_len(bool x) {
 
     int fpl[2];

src/gate.h

@@ -8,6 +8,8 @@
 #include <algorithm>
 #include <assert.h>
 
+namespace atpg_ls {
+
 class LUT;
 
 class Gate {
@@ -58,3 +60,5 @@ public:
     // [ cal_FPLS(~Vx, fanouts) - cal_FPLS(Vx, fanouts) ] * - FPLS_COST(x)
     // [ cal_FDS(~Vx, fanouts) - cal_FDS(Vx, fanouts) ] * - FDS_COST(x)
 };
+
+}

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<std::pair<Gate*, int>> 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<int> 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; i<inputs.size(); i++) {
+            PIs[i]->value = 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; i<lut->fanins.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,12 +255,11 @@ 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();
 
         if(pick == nullptr) {
@@ -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);
         }
     }
 }

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) {

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();
 };
+
+}

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;

src/parse.cpp

@@ -6,6 +6,8 @@
 #include <regex>
 #include <set>
 
+using namespace atpg_ls;
+
 void line2tokens(const std::string &line, std::vector<std::string> &tokens) {
     std::string token;
     for(char c : line) {

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 <fstream>
+#include <algorithm>
+#include <iostream>
+#include <map>
+
+
+CircuitGraph *graph;
+Iscas89Parser *parser;
+FaultManager *fault_manager;
+FaultCnfMaker *fault_cnf_maker;
+std::unique_ptr<SatSolver> solver;
+ProxyCnf *proxy;
+
+std::map<std::string, Fault> fault_map;
+
+bool sat_atpg(const char* name, int stuck_at, std::vector<int> &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);
+}

src/sat_atpg.h

@@ -0,0 +1,6 @@
+#pragma once
+
+#include "circuit.h"
+
+bool sat_atpg(const char* name, int stuck_at, std::vector<int> &input_vector);
+void sat_atpg_init(const char* file);

src/score.cpp

@@ -1,6 +1,8 @@
 #include "lut.h"
 #include "circuit.h"
 
+using namespace atpg_ls;
+
 void LUT::cal_score() {
     
     score = 0;

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);

src/simulator.h

@@ -2,8 +2,12 @@
 
 #include "circuit.h"
 
+namespace atpg_ls {
+
 class Simulator : public Circuit {
 public:
       void simulate(std::vector<LUT*> &inputs, int &score, int** fault_detected);
       int verify(LUTCircuit *lut_circuit, int** fault_detected);
 };
+
+}

tg-pro

@@ -0,0 +1 @@
+Subproject commit 7f0eef881be4d91aef0095e3a889e485a4e42f5d