Merge pull request #3226 from YosysHQ/micko/btor2witness

Sim support for btor2 witness files

2 files changed, 171 insertions, 10 deletions

diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index d62cc4c3d..73e88c049 100644
--- a/backends/btor/btor.cc
+++ b/backends/btor/btor.cc
@@ -678,7 +678,7 @@ struct BtorWorker
 			int sid = get_bv_sid(GetSize(sig_y));
 			int nid = next_nid++;
 
-			btorf("%d state %d\n", nid, sid);
+			btorf("%d state %d%s\n", nid, sid, getinfo(cell).c_str());
 
 			if (cell->type == ID($anyconst)) {
 				int nid2 = next_nid++;
@@ -699,7 +699,7 @@ struct BtorWorker
 				int one_nid = get_sig_nid(State::S1);
 				int zero_nid = get_sig_nid(State::S0);
 				initstate_nid = next_nid++;
-				btorf("%d state %d\n", initstate_nid, sid);
+				btorf("%d state %d%s\n", initstate_nid, sid, getinfo(cell).c_str());
 				btorf("%d init %d %d %d\n", next_nid++, sid, initstate_nid, one_nid);
 				btorf("%d next %d %d %d\n", next_nid++, sid, initstate_nid, zero_nid);
 			}
diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc
index d15ae9b57..02b859bcc 100644
--- a/passes/sat/sim.cc
+++ b/passes/sat/sim.cc
@@ -326,6 +326,16 @@ struct SimInstance
 		return did_something;
 	}
 
+	void set_memory_state(IdString memid, Const addr, Const data)
+	{
+		auto &state = mem_database[memid];
+
+		int offset = (addr.as_int() - state.mem->start_offset) * state.mem->width;
+		for (int i = 0; i < GetSize(data); i++)
+			if (0 <= i+offset && i+offset < GetSize(data))
+				state.data.bits[i+offset] = data.bits[i];
+	}
+
 	void update_cell(Cell *cell)
 	{
 		if (ff_database.count(cell))
@@ -961,7 +971,7 @@ struct SimWorker : SimShared
 		}
 	}
 
-	void run_cosim(Module *topmod, int numcycles)
+	void run_cosim_fst(Module *topmod, int numcycles)
 	{
 		log_assert(top == nullptr);
 		fst = new FstData(sim_filename);
@@ -1092,13 +1102,17 @@ struct SimWorker : SimShared
 		delete fst;
 	}
 
-	void run_cosim_witness(Module *topmod)
+	void run_cosim_aiger_witness(Module *topmod)
 	{
 		log_assert(top == nullptr);
+		if ((clock.size()+clockn.size())==0)
+			log_error("Clock signal must be specified.\n");
 		std::ifstream mf(map_filename);
 		std::string type, symbol;
 		int variable, index;
 		dict<int, std::pair<SigBit,bool>> inputs, inits, latches;
+		if (mf.fail())
+			log_cmd_error("Not able to read AIGER witness map file.\n");
 		while (mf >> type >> variable >> index >> symbol) {
 			RTLIL::IdString escaped_s = RTLIL::escape_id(symbol);
 			Wire *w = topmod->wire(escaped_s);
@@ -1183,6 +1197,131 @@ struct SimWorker : SimShared
 		register_output_step(10*cycle);
 		write_output_files();
 	}
+
+	std::vector<std::string> split(std::string text, const char *delim)
+	{
+		std::vector<std::string> list;
+		char *p = strdup(text.c_str());
+		char *t = strtok(p, delim);
+		while (t != NULL) {
+			list.push_back(t);
+			t = strtok(NULL, delim);
+		}
+		free(p);
+		return list;
+	}
+
+	std::string signal_name(std::string const & name)
+	{
+		size_t pos = name.find_first_of("@");
+		if (pos==std::string::npos) {
+			pos = name.find_first_of("#");
+			if (pos==std::string::npos)
+				log_error("Line does not contain proper signal name `%s`\n", name.c_str());
+		}
+		return name.substr(0, pos);
+	}
+
+	void run_cosim_btor2_witness(Module *topmod)
+	{
+		log_assert(top == nullptr);
+		if ((clock.size()+clockn.size())==0)
+			log_error("Clock signal must be specified.\n");
+		std::ifstream f;
+		f.open(sim_filename.c_str());
+		if (f.fail() || GetSize(sim_filename) == 0)
+			log_error("Can not open file `%s`\n", sim_filename.c_str());
+
+		int state = 0;
+		int cycle = 0;
+		top = new SimInstance(this, scope, topmod);
+		register_signals();
+		int prev_cycle = 0;
+		int curr_cycle = 0;
+		std::vector<std::string> parts;
+		size_t len = 0;
+		while (!f.eof())
+		{
+			std::string line;
+			std::getline(f, line);
+			if (line.size()==0) continue;
+
+			if (line[0]=='#' || line[0]=='@' || line[0]=='.') { 
+				if (line[0]!='.')
+					curr_cycle = atoi(line.c_str()+1); 
+				else
+					curr_cycle = -1; // force detect change
+
+				if (curr_cycle != prev_cycle) {
+					log("Simulating cycle %d.\n", cycle);
+					set_inports(clock, State::S1);
+					set_inports(clockn, State::S0);
+					update();
+					register_output_step(10*cycle+0);
+					set_inports(clock, State::S0);
+					set_inports(clockn, State::S1);
+					update();
+					register_output_step(10*cycle+5);
+					cycle++;
+					prev_cycle = curr_cycle;
+				}
+				if (line[0]=='.') break;
+				continue;
+			}
+
+			switch(state)
+			{
+				case 0:
+					if (line=="sat")
+						state = 1;
+					break;
+				case 1:
+					if (line[0]=='b' || line[0]=='j')
+						state = 2;
+					else
+						log_error("Line does not contain property.\n");
+					break;
+				default: // set state or inputs
+					parts = split(line, " ");
+					len = parts.size();
+					if (len<3 || len>4)
+						log_error("Invalid set state line content.\n");
+
+					RTLIL::IdString escaped_s = RTLIL::escape_id(signal_name(parts[len-1]));
+					if (len==3) {
+						Wire *w = topmod->wire(escaped_s);
+						if (!w) {
+							Cell *c = topmod->cell(escaped_s);
+							if (!c)
+								log_warning("Wire/cell %s not present in module %s\n",log_id(escaped_s),log_id(topmod));
+							else if (c->type.in(ID($anyconst), ID($anyseq))) {
+								SigSpec sig_y= c->getPort(ID::Y);
+								if ((int)parts[1].size() != GetSize(sig_y))
+									log_error("Size of wire %s is different than provided data.\n", log_signal(sig_y));
+								top->set_state(sig_y, Const::from_string(parts[1]));
+							}
+						} else {
+							if ((int)parts[1].size() != w->width)
+								log_error("Size of wire %s is different than provided data.\n", log_signal(w));
+							top->set_state(w, Const::from_string(parts[1]));
+						}
+					} else {
+						Cell *c = topmod->cell(escaped_s);
+						if (!c)
+							log_error("Cell %s not present in module %s\n",log_id(escaped_s),log_id(topmod));
+						if (!c->is_mem_cell())
+							log_error("Cell %s is not memory cell in module %s\n",log_id(escaped_s),log_id(topmod));
+						
+						Const addr = Const::from_string(parts[1].substr(1,parts[1].size()-2));
+						Const data = Const::from_string(parts[2]);
+						top->set_memory_state(c->parameters.at(ID::MEMID).decode_string(), addr, data);
+					}
+					break;
+			}
+		}
+		register_output_step(10*cycle);
+		write_output_files();
+	}
 };
 
 struct VCDWriter : public OutputWriter
@@ -1311,14 +1450,19 @@ struct AIWWriter : public OutputWriter
 	void write(std::map<int, bool> &) override
 	{
 		if (!aiwfile.is_open()) return;
+		if (worker->map_filename.empty())
+			log_cmd_error("For AIGER witness file map parameter is mandatory.\n");
+
 		std::ifstream mf(worker->map_filename);
 		std::string type, symbol;
 		int variable, index;
+		if (mf.fail())
+			log_cmd_error("Not able to read AIGER witness map file.\n");
 		while (mf >> type >> variable >> index >> symbol) {
 			RTLIL::IdString escaped_s = RTLIL::escape_id(symbol);
 			Wire *w = worker->top->module->wire(escaped_s);
 			if (!w)
-				log_error("Wire %s not present in module %s\n",log_signal(w),log_id(worker->top->module));
+				log_error("Wire %s not present in module %s\n",log_id(escaped_s),log_id(worker->top->module));
 			if (index < w->start_offset || index > w->start_offset + w->width)
 				log_error("Index %d for wire %s is out of range\n", index, log_signal(w));
 			if (type == "input") {
@@ -1483,6 +1627,13 @@ struct SimPass : public Pass {
 		log("        enable debug output\n");
 		log("\n");
 	}
+
+
+	static std::string file_base_name(std::string const & path)
+	{
+		return path.substr(path.find_last_of("/\\") + 1);
+	}
+
 	void execute(std::vector<std::string> args, RTLIL::Design *design) override
 	{
 		SimWorker worker;
@@ -1632,11 +1783,21 @@ struct SimPass : public Pass {
 
 		if (worker.sim_filename.empty())
 			worker.run(top_mod, numcycles);
-		else
-			if (worker.map_filename.empty())
-				worker.run_cosim(top_mod, numcycles);
-			else
-				worker.run_cosim_witness(top_mod);
+		else {
+			std::string filename_trim = file_base_name(worker.sim_filename);
+			if (filename_trim.size() > 4 && ((filename_trim.compare(filename_trim.size()-4, std::string::npos, ".fst") == 0) ||
+				filename_trim.compare(filename_trim.size()-4, std::string::npos, ".vcd") == 0)) {
+				worker.run_cosim_fst(top_mod, numcycles);
+			} else if (filename_trim.size() > 4 && filename_trim.compare(filename_trim.size()-4, std::string::npos, ".aiw") == 0) {
+				if (worker.map_filename.empty())
+					log_cmd_error("For AIGER witness file map parameter is mandatory.\n");
+				worker.run_cosim_aiger_witness(top_mod);
+			} else if (filename_trim.size() > 4 && filename_trim.compare(filename_trim.size()-4, std::string::npos, ".wit") == 0) {
+				worker.run_cosim_btor2_witness(top_mod);
+			} else {
+				log_cmd_error("Unhandled extension for simulation input file `%s`.\n", worker.sim_filename.c_str());
+			}
+		}
 	}
 } SimPass;