diff options
| author | Clifford Wolf <clifford@clifford.at> | 2013-06-09 18:07:05 +0200 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2013-06-09 18:07:05 +0200 |
| commit | a75b249427923c7f3ea604c5748291bdba25d1d0 (patch) | |
| tree | 35620b13ce3aa5b85936575c95b2841aac0fba90 /kernel/satgen.h | |
| parent | b210234612beb3e20d5338d03debf084c9b6c7b9 (diff) | |
| download | yosys-a75b249427923c7f3ea604c5748291bdba25d1d0.tar.gz yosys-a75b249427923c7f3ea604c5748291bdba25d1d0.tar.bz2 yosys-a75b249427923c7f3ea604c5748291bdba25d1d0.zip | |
Implemented temporal induction proofs in sat_solve
Diffstat (limited to 'kernel/satgen.h')
| -rw-r--r-- | kernel/satgen.h | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/satgen.h b/kernel/satgen.h index 7b7a07707..b7bd87dd4 100644 --- a/kernel/satgen.h +++ b/kernel/satgen.h @@ -38,7 +38,7 @@ struct SatGen RTLIL::Design *design; SigMap *sigmap; std::string prefix; - SigPool initial_signals; + SigPool initial_state; SatGen(ezSAT *ez, RTLIL::Design *design, SigMap *sigmap, std::string prefix = std::string()) : ez(ez), design(design), sigmap(sigmap), prefix(prefix) @@ -241,7 +241,7 @@ struct SatGen if (timestep > 0 && (cell->type == "$dff" || cell->type == "$_DFF_N_" || cell->type == "$_DFF_P_")) { if (timestep == 1) { - initial_signals.add((*sigmap)(cell->connections.at("\\Q"))); + initial_state.add((*sigmap)(cell->connections.at("\\Q"))); } else { std::vector<int> d = importSigSpec(cell->connections.at("\\D"), timestep-1); std::vector<int> q = importSigSpec(cell->connections.at("\\Q"), timestep); |