From a75b249427923c7f3ea604c5748291bdba25d1d0 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sun, 9 Jun 2013 18:07:05 +0200 Subject: Implemented temporal induction proofs in sat_solve --- kernel/satgen.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'kernel') 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 d = importSigSpec(cell->connections.at("\\D"), timestep-1); std::vector q = importSigSpec(cell->connections.at("\\Q"), timestep); -- cgit v1.2.3