From: Noah Moroze <noahmoroze@gmail.com>
Date: Thu, 20 Aug 2020 20:00:05 +0000 (-0400)
Subject: Ensure smt2 comments are associated with accessors
X-Git-Tag: working-ls180~304^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=91682d189e55923114726b797968ef939777000c;p=yosys.git

Ensure smt2 comments are associated with accessors
---

diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index a79c0bd99..0423b977a 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -824,38 +824,49 @@ struct Smt2Worker
 					is_register = true;
 			if (wire->port_id || is_register || wire->get_bool_attribute(ID::keep) || (wiresmode && wire->name[0] == '\\')) {
 				RTLIL::SigSpec sig = sigmap(wire);
+				std::vector<std::string> comments;
 				if (wire->port_input)
-					decls.push_back(stringf("; yosys-smt2-input %s %d\n", get_id(wire), wire->width));
+					comments.push_back(stringf("; yosys-smt2-input %s %d\n", get_id(wire), wire->width));
 				if (wire->port_output)
-					decls.push_back(stringf("; yosys-smt2-output %s %d\n", get_id(wire), wire->width));
+					comments.push_back(stringf("; yosys-smt2-output %s %d\n", get_id(wire), wire->width));
 				if (is_register)
-					decls.push_back(stringf("; yosys-smt2-register %s %d\n", get_id(wire), wire->width));
+					comments.push_back(stringf("; yosys-smt2-register %s %d\n", get_id(wire), wire->width));
 				if (wire->get_bool_attribute(ID::keep) || (wiresmode && wire->name[0] == '\\'))
-					decls.push_back(stringf("; yosys-smt2-wire %s %d\n", get_id(wire), wire->width));
+					comments.push_back(stringf("; yosys-smt2-wire %s %d\n", get_id(wire), wire->width));
 				if (GetSize(wire) == 1 && (clock_posedge.count(sig) || clock_negedge.count(sig)))
-					decls.push_back(stringf("; yosys-smt2-clock %s%s%s\n", get_id(wire),
+					comments.push_back(stringf("; yosys-smt2-clock %s%s%s\n", get_id(wire),
 							clock_posedge.count(sig) ? " posedge" : "", clock_negedge.count(sig) ? " negedge" : ""));
 				if (bvmode && GetSize(sig) > 1) {
+					std::string sig_bv = get_bv(sig);
+					if (!comments.empty())
+						decls.insert(decls.end(), comments.begin(), comments.end());
 					decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) (_ BitVec %d) %s)\n",
-							get_id(module), get_id(wire), get_id(module), GetSize(sig), get_bv(sig).c_str()));
+							get_id(module), get_id(wire), get_id(module), GetSize(sig), sig_bv.c_str()));
 					if (wire->port_input)
 						ex_input_eq.push_back(stringf("  (= (|%s_n %s| state) (|%s_n %s| other_state))",
 								get_id(module), get_id(wire), get_id(module), get_id(wire)));
 				} else {
-					for (int i = 0; i < GetSize(sig); i++)
+					std::vector<std::string> sig_bool;
+					for (int i = 0; i < GetSize(sig); i++) {
+						sig_bool.push_back(get_bool(sig[i]));
+					}
+					if (!comments.empty())
+						decls.insert(decls.end(), comments.begin(), comments.end());
+					for (int i = 0; i < GetSize(sig); i++) {
 						if (GetSize(sig) > 1) {
 							decls.push_back(stringf("(define-fun |%s_n %s %d| ((state |%s_s|)) Bool %s)\n",
-									get_id(module), get_id(wire), i, get_id(module), get_bool(sig[i]).c_str()));
+									get_id(module), get_id(wire), i, get_id(module), sig_bool[i].c_str()));
 							if (wire->port_input)
 								ex_input_eq.push_back(stringf("  (= (|%s_n %s %d| state) (|%s_n %s %d| other_state))",
 										get_id(module), get_id(wire), i, get_id(module), get_id(wire), i));
 						} else {
 							decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) Bool %s)\n",
-									get_id(module), get_id(wire), get_id(module), get_bool(sig[i]).c_str()));
+									get_id(module), get_id(wire), get_id(module), sig_bool[i].c_str()));
 							if (wire->port_input)
 								ex_input_eq.push_back(stringf("  (= (|%s_n %s| state) (|%s_n %s| other_state))",
 										get_id(module), get_id(wire), get_id(module), get_id(wire)));
 						}
+					}
 				}
 			}
 		}