1 files changed, 1378 insertions, 87 deletions

diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc
index 4e158da62..8081ffffe 100644
--- a/passes/sat/sim.cc
+++ b/passes/sat/sim.cc
@@ -21,19 +21,76 @@
 #include "kernel/sigtools.h"
 #include "kernel/celltypes.h"
 #include "kernel/mem.h"
+#include "kernel/fstdata.h"
+#include "kernel/ff.h"
 
 #include <ctime>
 
 USING_YOSYS_NAMESPACE
 PRIVATE_NAMESPACE_BEGIN
 
+enum class SimulationMode {
+	sim,
+	cmp,
+	gold,
+	gate,
+};
+
+static const std::map<std::string, int> g_units =
+{
+	{ "",    -9 }, // default is ns
+	{ "s",    0 },
+	{ "ms",  -3 },
+	{ "us",  -6 },
+	{ "ns",  -9 },
+	{ "ps", -12 },
+	{ "fs", -15 },
+	{ "as", -18 },
+	{ "zs", -21 },
+};
+
+static double stringToTime(std::string str)
+{
+	if (str=="END") return -1;
+
+	char *endptr;
+	long value = strtol(str.c_str(), &endptr, 10);
+
+	if (g_units.find(endptr)==g_units.end())
+		log_error("Cannot parse '%s', bad unit '%s'\n", str.c_str(), endptr);
+
+	if (value < 0)
+		log_error("Time value '%s' must be positive\n", str.c_str());
+
+	return value * pow(10.0, g_units.at(endptr));
+}
+
+struct SimWorker;
+struct OutputWriter
+{
+	OutputWriter(SimWorker *w) { worker = w;};
+	virtual ~OutputWriter() {};
+	virtual void write(std::map<int, bool> &use_signal) = 0;
+	SimWorker *worker;
+};
+
 struct SimShared
 {
 	bool debug = false;
+	bool verbose = true;
 	bool hide_internal = true;
 	bool writeback = false;
 	bool zinit = false;
 	int rstlen = 1;
+	FstData *fst = nullptr;
+	double start_time = 0;
+	double stop_time = -1;
+	SimulationMode sim_mode = SimulationMode::sim;
+	bool cycles_set = false;
+	std::vector<std::unique_ptr<OutputWriter>> outputfiles;
+	std::vector<std::pair<int,std::map<int,Const>>> output_data;
+	bool ignore_x = false;
+	bool date = false;
 };
 
 void zinit(State &v)
@@ -51,7 +108,8 @@ void zinit(Const &v)
 struct SimInstance
 {
 	SimShared *shared;
-
+	
+	std::string scope;
 	Module *module;
 	Cell *instance;
 
@@ -70,8 +128,13 @@ struct SimInstance
 
 	struct ff_state_t
 	{
-		State past_clock;
 		Const past_d;
+		Const past_ad;
+		State past_clk;
+		State past_ce;
+		State past_srst;
+		
+		FfData data;
 	};
 
 	struct mem_state_t
@@ -91,10 +154,11 @@ struct SimInstance
 
 	std::vector<Mem> memories;
 
-	dict<Wire*, pair<int, Const>> vcd_database;
+	dict<Wire*, pair<int, Const>> signal_database;
+	dict<Wire*, fstHandle> fst_handles;
 
-	SimInstance(SimShared *shared, Module *module, Cell *instance = nullptr, SimInstance *parent = nullptr) :
-			shared(shared), module(module), instance(instance), parent(parent), sigmap(module)
+	SimInstance(SimShared *shared, std::string scope, Module *module, Cell *instance = nullptr, SimInstance *parent = nullptr) :
+			shared(shared), scope(scope), module(module), instance(instance), parent(parent), sigmap(module)
 	{
 		log_assert(module);
 
@@ -116,6 +180,13 @@ struct SimInstance
 				}
 			}
 
+			if ((shared->fst) && !(shared->hide_internal && wire->name[0] == '$')) {
+				fstHandle id = shared->fst->getHandle(scope + "." + RTLIL::unescape_id(wire->name));
+				if (id==0 && wire->name.isPublic())
+					log_warning("Unable to find wire %s in input file.\n", (scope + "." + RTLIL::unescape_id(wire->name)).c_str());
+				fst_handles[wire] = id;
+			}
+
 			if (wire->attributes.count(ID::init)) {
 				Const initval = wire->attributes.at(ID::init);
 				for (int i = 0; i < GetSize(sig) && i < GetSize(initval); i++)
@@ -144,7 +215,7 @@ struct SimInstance
 			Module *mod = module->design->module(cell->type);
 
 			if (mod != nullptr) {
-				dirty_children.insert(new SimInstance(shared, mod, cell, this));
+				dirty_children.insert(new SimInstance(shared, scope + "." + RTLIL::unescape_id(cell->name), mod, cell, this));
 			}
 
 			for (auto &port : cell->connections()) {
@@ -157,10 +228,15 @@ struct SimInstance
 					}
 			}
 
-			if (cell->type.in(ID($dff))) {
+			if (RTLIL::builtin_ff_cell_types().count(cell->type)) {
+				FfData ff_data(nullptr, cell);
 				ff_state_t ff;
-				ff.past_clock = State::Sx;
-				ff.past_d = Const(State::Sx, cell->getParam(ID::WIDTH).as_int());
+				ff.past_d = Const(State::Sx, ff_data.width);
+				ff.past_ad = Const(State::Sx, ff_data.width);
+				ff.past_clk = State::Sx;
+				ff.past_ce = State::Sx;
+				ff.past_srst = State::Sx;
+				ff.data = ff_data;
 				ff_database[cell] = ff;
 			}
 
@@ -177,11 +253,10 @@ struct SimInstance
 		{
 			for (auto &it : ff_database)
 			{
-				Cell *cell = it.first;
 				ff_state_t &ff = it.second;
 				zinit(ff.past_d);
 
-				SigSpec qsig = cell->getPort(ID::Q);
+				SigSpec qsig = it.second.data.sig_q;
 				Const qdata = get_state(qsig);
 				zinit(qdata);
 				set_state(qsig, qdata);
@@ -253,6 +328,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))
@@ -313,6 +398,12 @@ struct SimInstance
 				return;
 			}
 
+			// (A,S -> Y) cells
+			if (has_a && !has_b && !has_c && !has_d && has_s && has_y) {
+				set_state(sig_y, CellTypes::eval(cell, get_state(sig_a), get_state(sig_s)));
+				return;
+			}
+
 			// (A,B,S -> Y) cells
 			if (has_a && has_b && !has_c && !has_d && has_s && has_y) {
 				set_state(sig_y, CellTypes::eval(cell, get_state(sig_a), get_state(sig_b), get_state(sig_s)));
@@ -408,21 +499,62 @@ struct SimInstance
 
 		for (auto &it : ff_database)
 		{
-			Cell *cell = it.first;
 			ff_state_t &ff = it.second;
-
-			if (cell->type.in(ID($dff)))
-			{
-				bool clkpol = cell->getParam(ID::CLK_POLARITY).as_bool();
-				State current_clock = get_state(cell->getPort(ID::CLK))[0];
-
-				if (clkpol ? (ff.past_clock == State::S1 || current_clock != State::S1) :
-						(ff.past_clock == State::S0 || current_clock != State::S0))
-					continue;
-
-				if (set_state(cell->getPort(ID::Q), ff.past_d))
-					did_something = true;
+			FfData &ff_data = ff.data;
+
+			Const current_q = get_state(ff.data.sig_q);
+
+			if (ff_data.has_clk) {
+				// flip-flops
+				State current_clk = get_state(ff_data.sig_clk)[0];
+				if (ff_data.pol_clk ? (ff.past_clk == State::S0 && current_clk != State::S0) :
+							(ff.past_clk == State::S1 && current_clk != State::S1)) {
+					bool ce = ff.past_ce == (ff_data.pol_ce ? State::S1 : State::S0);
+					// set if no ce, or ce is enabled
+					if (!ff_data.has_ce || (ff_data.has_ce && ce)) {
+						current_q = ff.past_d;
+					}
+					// override if sync reset
+					if ((ff_data.has_srst) && (ff.past_srst == (ff_data.pol_srst ? State::S1 : State::S0)) &&
+						((!ff_data.ce_over_srst) || (ff_data.ce_over_srst && ce))) {
+						current_q = ff_data.val_srst;
+					}
+				}
+			}
+			// async load
+			if (ff_data.has_aload) {
+				State current_aload = get_state(ff_data.sig_aload)[0];
+				if (current_aload == (ff_data.pol_aload ? State::S1 : State::S0)) {
+					current_q = ff_data.has_clk ? ff.past_ad : get_state(ff.data.sig_ad);
+				}
+			}
+			// async reset
+			if (ff_data.has_arst) {
+				State current_arst = get_state(ff_data.sig_arst)[0];
+				if (current_arst == (ff_data.pol_arst ? State::S1 : State::S0)) {
+					current_q = ff_data.val_arst;
+				}
+			}
+			// handle set/reset
+			if (ff.data.has_sr) {
+				Const current_clr = get_state(ff.data.sig_clr);
+				Const current_set = get_state(ff.data.sig_set);
+
+				for(int i=0;i<ff.past_d.size();i++) {
+					if (current_clr[i] == (ff_data.pol_clr ? State::S1 : State::S0)) {
+						current_q[i] = State::S0;
+					}
+					else if (current_set[i] == (ff_data.pol_set ? State::S1 : State::S0)) {
+						current_q[i] = State::S1;
+					}
+				}
+			}
+			if (ff_data.has_gclk) {
+				// $ff
+				current_q = ff.past_d;
 			}
+			if (set_state(ff_data.sig_q, current_q))
+				did_something = true;
 		}
 
 		for (auto &it : mem_database)
@@ -480,13 +612,22 @@ struct SimInstance
 	{
 		for (auto &it : ff_database)
 		{
-			Cell *cell = it.first;
 			ff_state_t &ff = it.second;
 
-			if (cell->type.in(ID($dff))) {
-				ff.past_clock = get_state(cell->getPort(ID::CLK))[0];
-				ff.past_d = get_state(cell->getPort(ID::D));
-			}
+			if (ff.data.has_aload)
+				ff.past_ad = get_state(ff.data.sig_ad);
+
+			if (ff.data.has_clk || ff.data.has_gclk)
+				ff.past_d = get_state(ff.data.sig_d);
+
+			if (ff.data.has_clk)
+				ff.past_clk = get_state(ff.data.sig_clk)[0];
+
+			if (ff.data.has_ce)
+				ff.past_ce = get_state(ff.data.sig_ce)[0];
+
+			if (ff.data.has_srst)
+				ff.past_srst = get_state(ff.data.sig_srst)[0];
 		}
 
 		for (auto &it : mem_database)
@@ -537,8 +678,7 @@ struct SimInstance
 
 		for (auto &it : ff_database)
 		{
-			Cell *cell = it.first;
-			SigSpec sig_q = cell->getPort(ID::Q);
+			SigSpec sig_q = it.second.data.sig_q;
 			Const initval = get_state(sig_q);
 
 			for (int i = 0; i < GetSize(sig_q); i++)
@@ -568,28 +708,51 @@ struct SimInstance
 			it.second->writeback(wbmods);
 	}
 
-	void write_vcd_header(std::ofstream &f, int &id)
+	void register_signals(int &id)
 	{
-		f << stringf("$scope module %s $end\n", log_id(name()));
-
 		for (auto wire : module->wires())
 		{
 			if (shared->hide_internal && wire->name[0] == '$')
 				continue;
 
-			f << stringf("$var wire %d n%d %s%s $end\n", GetSize(wire), id, wire->name[0] == '$' ? "\\" : "", log_id(wire));
-			vcd_database[wire] = make_pair(id++, Const());
+			signal_database[wire] = make_pair(id, Const());
+			id++;
+		}
+
+		for (auto child : children)
+			child.second->register_signals(id);
+	}
+
+	void write_output_header(std::function<void(IdString)> enter_scope, std::function<void()> exit_scope, std::function<void(Wire*, int, bool)> register_signal)
+	{
+		enter_scope(name());
+
+		dict<Wire*,bool> registers;
+		for (auto cell : module->cells())
+		{
+			if (RTLIL::builtin_ff_cell_types().count(cell->type)) {
+				FfData ff_data(nullptr, cell);
+				SigSpec q = sigmap(ff_data.sig_q);
+				if (q.is_wire() && signal_database.count(q.as_wire()) != 0) {
+					registers[q.as_wire()] = true;
+				}
+			}
+		}
+		
+		for (auto signal : signal_database)
+		{
+			register_signal(signal.first, signal.second.first, registers.count(signal.first)!=0);
 		}
 
 		for (auto child : children)
-			child.second->write_vcd_header(f, id);
+			child.second->write_output_header(enter_scope, exit_scope, register_signal);
 
-		f << stringf("$upscope $end\n");
+		exit_scope();
 	}
 
-	void write_vcd_step(std::ofstream &f)
+	void register_output_step_values(std::map<int,Const> *data)
 	{
-		for (auto &it : vcd_database)
+		for (auto &it : signal_database)
 		{
 			Wire *wire = it.first;
 			Const value = get_state(wire);
@@ -599,66 +762,134 @@ struct SimInstance
 				continue;
 
 			it.second.second = value;
+			data->emplace(id, value);
+		}
 
-			f << "b";
-			for (int i = GetSize(value)-1; i >= 0; i--) {
-				switch (value[i]) {
-					case State::S0: f << "0"; break;
-					case State::S1: f << "1"; break;
-					case State::Sx: f << "x"; break;
-					default: f << "z";
+		for (auto child : children)
+			child.second->register_output_step_values(data);
+	}
+
+	void setInitState()
+	{
+		for (auto &it : ff_database)
+		{
+			SigSpec qsig = it.second.data.sig_q;
+			if (qsig.is_wire()) {
+				IdString name = qsig.as_wire()->name;
+				fstHandle id = shared->fst->getHandle(scope + "." + RTLIL::unescape_id(name));
+				if (id==0 && name.isPublic())
+					log_warning("Unable to find wire %s in input file.\n", (scope + "." + RTLIL::unescape_id(name)).c_str());
+				if (id!=0) {
+					Const fst_val = Const::from_string(shared->fst->valueOf(id));
+					set_state(qsig, fst_val);
 				}
 			}
+		}
+		for (auto child : children)
+			child.second->setInitState();
+	}
 
-			f << stringf(" n%d\n", id);
+	void setState(dict<int, std::pair<SigBit,bool>> bits, std::string values)
+	{
+		for(auto bit : bits) {
+			if (bit.first >= GetSize(values))
+				log_error("Too few input data bits in file.\n");
+			switch(values.at(bit.first)) {
+				case '0': set_state(bit.second.first, bit.second.second ? State::S1 : State::S0); break;
+				case '1': set_state(bit.second.first, bit.second.second ? State::S0 : State::S1); break;
+				default: set_state(bit.second.first, State::Sx); break;
+			}
 		}
+	}
 
+	bool checkSignals()
+	{
+		bool retVal = false;
+		for(auto &item : fst_handles) {
+			if (item.second==0) continue; // Ignore signals not found
+			Const fst_val = Const::from_string(shared->fst->valueOf(item.second));
+			Const sim_val = get_state(item.first);
+			if (sim_val.size()!=fst_val.size()) {
+				log_warning("Signal '%s.%s' size is different in gold and gate.\n", scope.c_str(), log_id(item.first));
+				continue;
+			}
+			if (shared->sim_mode == SimulationMode::sim) {
+				// No checks performed when using stimulus
+			} else if (shared->sim_mode == SimulationMode::gate && !fst_val.is_fully_def()) { // FST data contains X
+				for(int i=0;i<fst_val.size();i++) {
+					if (fst_val[i]!=State::Sx && fst_val[i]!=sim_val[i]) {
+						log_warning("Signal '%s.%s' in file %s in simulation %s\n", scope.c_str(), log_id(item.first), log_signal(fst_val), log_signal(sim_val));
+						retVal = true;
+						break;
+					}
+				}
+			} else if (shared->sim_mode == SimulationMode::gold && !sim_val.is_fully_def()) { // sim data contains X
+				for(int i=0;i<sim_val.size();i++) {
+					if (sim_val[i]!=State::Sx && fst_val[i]!=sim_val[i]) {
+						log_warning("Signal '%s.%s' in file %s in simulation %s\n", scope.c_str(), log_id(item.first), log_signal(fst_val), log_signal(sim_val));
+						retVal = true;
+						break;
+					}
+				}
+			} else {
+				if (fst_val!=sim_val) {
+					log_warning("Signal '%s.%s' in file %s in simulation '%s'\n", scope.c_str(), log_id(item.first), log_signal(fst_val), log_signal(sim_val));
+					retVal = true;
+				}
+			}
+		}
 		for (auto child : children)
-			child.second->write_vcd_step(f);
+			retVal |= child.second->checkSignals();
+		return retVal;
 	}
 };
 
 struct SimWorker : SimShared
 {
 	SimInstance *top = nullptr;
-	std::ofstream vcdfile;
 	pool<IdString> clock, clockn, reset, resetn;
 	std::string timescale;
+	std::string sim_filename;
+	std::string map_filename;
+	std::string scope;
 
 	~SimWorker()
 	{
+		outputfiles.clear();
 		delete top;
 	}
 
-	void write_vcd_header()
+	void register_signals()
 	{
-		if (!vcdfile.is_open())
-			return;
-
-		vcdfile << stringf("$version %s $end\n", yosys_version_str);
-
-		std::time_t t = std::time(nullptr);
-		char mbstr[255];
-		if (std::strftime(mbstr, sizeof(mbstr), "%c", std::localtime(&t))) {
-			vcdfile << stringf("$date ") << mbstr << stringf(" $end\n");
-		}
-
-		if (!timescale.empty())
-			vcdfile << stringf("$timescale %s $end\n", timescale.c_str());
-
 		int id = 1;
-		top->write_vcd_header(vcdfile, id);
-
-		vcdfile << stringf("$enddefinitions $end\n");
+		top->register_signals(id);
 	}
 
-	void write_vcd_step(int t)
+	void register_output_step(int t)
 	{
-		if (!vcdfile.is_open())
-			return;
+		std::map<int,Const> data;
+		top->register_output_step_values(&data);
+		output_data.emplace_back(t, data);
+	}
 
-		vcdfile << stringf("#%d\n", t);
-		top->write_vcd_step(vcdfile);
+	void write_output_files()
+	{
+		std::map<int, bool> use_signal;
+		bool first = ignore_x;
+		for(auto& d : output_data)
+		{
+			if (first) {
+				for (auto &data : d.second)
+					use_signal[data.first] = !data.second.is_fully_undef();
+				first = false;
+			} else {
+				for (auto &data : d.second)
+					use_signal[data.first] = true;
+			}
+			if (!ignore_x) break;
+		}
+		for(auto& writer : outputfiles)
+			writer->write(use_signal);
 	}
 
 	void update()
@@ -699,11 +930,12 @@ struct SimWorker : SimShared
 	void run(Module *topmod, int numcycles)
 	{
 		log_assert(top == nullptr);
-		top = new SimInstance(this, topmod);
+		top = new SimInstance(this, scope, topmod);
+		register_signals();
 
 		if (debug)
 			log("\n===== 0 =====\n");
-		else
+		else if (verbose)
 			log("Simulating cycle 0.\n");
 
 		set_inports(reset, State::S1);
@@ -714,24 +946,24 @@ struct SimWorker : SimShared
 
 		update();
 
-		write_vcd_header();
-		write_vcd_step(0);
+		register_output_step(0);
 
 		for (int cycle = 0; cycle < numcycles; cycle++)
 		{
 			if (debug)
 				log("\n===== %d =====\n", 10*cycle + 5);
-
+			else if (verbose)
+				log("Simulating cycle %d.\n", (cycle*2)+1);
 			set_inports(clock, State::S0);
 			set_inports(clockn, State::S1);
 
 			update();
-			write_vcd_step(10*cycle + 5);
+			register_output_step(10*cycle + 5);
 
 			if (debug)
 				log("\n===== %d =====\n", 10*cycle + 10);
-			else
-				log("Simulating cycle %d.\n", cycle+1);
+			else if (verbose)
+				log("Simulating cycle %d.\n", (cycle*2)+2);
 
 			set_inports(clock, State::S1);
 			set_inports(clockn, State::S0);
@@ -742,16 +974,812 @@ struct SimWorker : SimShared
 			}
 
 			update();
-			write_vcd_step(10*cycle + 10);
+			register_output_step(10*cycle + 10);
 		}
 
-		write_vcd_step(10*numcycles + 2);
+		register_output_step(10*numcycles + 2);
+
+		write_output_files();
 
 		if (writeback) {
 			pool<Module*> wbmods;
 			top->writeback(wbmods);
 		}
 	}
+
+	void run_cosim_fst(Module *topmod, int numcycles)
+	{
+		log_assert(top == nullptr);
+		fst = new FstData(sim_filename);
+
+		if (scope.empty())
+			log_error("Scope must be defined for co-simulation.\n");
+
+		top = new SimInstance(this, scope, topmod);
+		register_signals();
+
+		std::vector<fstHandle> fst_clock;
+
+		for (auto portname : clock)
+		{
+			Wire *w = topmod->wire(portname);
+			if (!w)
+				log_error("Can't find port %s on module %s.\n", log_id(portname), log_id(top->module));
+			if (!w->port_input)
+				log_error("Clock port %s on module %s is not input.\n", log_id(portname), log_id(top->module));
+			fstHandle id = fst->getHandle(scope + "." + RTLIL::unescape_id(portname));
+			if (id==0)
+				log_error("Can't find port %s.%s in FST.\n", scope.c_str(), log_id(portname));
+			fst_clock.push_back(id);
+		}
+		for (auto portname : clockn)
+		{
+			Wire *w = topmod->wire(portname);
+			if (!w)
+				log_error("Can't find port %s on module %s.\n", log_id(portname), log_id(top->module));
+			if (!w->port_input)
+				log_error("Clock port %s on module %s is not input.\n", log_id(portname), log_id(top->module));
+			fstHandle id = fst->getHandle(scope + "." + RTLIL::unescape_id(portname));
+			if (id==0)
+				log_error("Can't find port %s.%s in FST.\n", scope.c_str(), log_id(portname));
+			fst_clock.push_back(id);
+		}
+
+		SigMap sigmap(topmod);
+		std::map<Wire*,fstHandle> inputs;
+
+		for (auto wire : topmod->wires()) {
+			if (wire->port_input) {
+				fstHandle id = fst->getHandle(scope + "." + RTLIL::unescape_id(wire->name));
+				if (id==0)
+					log_error("Unable to find required '%s' signal in file\n",(scope + "." + RTLIL::unescape_id(wire->name)).c_str());
+				inputs[wire] = id;
+			}
+		}
+
+		uint64_t startCount = 0;
+		uint64_t stopCount = 0;
+		if (start_time==0) {
+			if (start_time < fst->getStartTime())
+				log_warning("Start time is before simulation file start time\n");
+			startCount = fst->getStartTime();
+		} else if (start_time==-1) 
+			startCount = fst->getEndTime();
+		else {
+			startCount = start_time / fst->getTimescale();
+			if (startCount > fst->getEndTime()) {
+				startCount = fst->getEndTime();
+				log_warning("Start time is after simulation file end time\n");
+			}
+		}
+		if (stop_time==0) {
+			if (stop_time < fst->getStartTime())
+				log_warning("Stop time is before simulation file start time\n");
+			stopCount = fst->getStartTime();
+		} else if (stop_time==-1) 
+			stopCount = fst->getEndTime();
+		else {
+			stopCount = stop_time / fst->getTimescale();
+			if (stopCount > fst->getEndTime()) {
+				stopCount = fst->getEndTime();
+				log_warning("Stop time is after simulation file end time\n");
+			}
+		}
+		if (stopCount<startCount) {
+			log_error("Stop time is before start time\n");
+		}
+
+		bool initial = true;
+		int cycle = 0;
+		log("Co-simulation from %lu%s to %lu%s", (unsigned long)startCount, fst->getTimescaleString(), (unsigned long)stopCount, fst->getTimescaleString());
+		if (cycles_set) 
+			log(" for %d clock cycle(s)",numcycles);
+		log("\n");
+		bool all_samples = fst_clock.empty();
+
+		try {
+			fst->reconstructAllAtTimes(fst_clock, startCount, stopCount, [&](uint64_t time) {
+				if (verbose)
+					log("Co-simulating %s %d [%lu%s].\n", (all_samples ? "sample" : "cycle"), cycle, (unsigned long)time, fst->getTimescaleString());
+				bool did_something = false;
+				for(auto &item : inputs) {
+					std::string v = fst->valueOf(item.second);
+					did_something |= top->set_state(item.first, Const::from_string(v));
+				}
+
+				if (initial) {
+					top->setInitState();
+					initial = false;
+				}
+				if (did_something)
+					update();
+				register_output_step(time);
+
+				bool status = top->checkSignals();
+				if (status)
+					log_error("Signal difference\n");
+				cycle++;
+
+				// Limit to number of cycles if provided
+				if (cycles_set && cycle > numcycles *2)
+					throw fst_end_of_data_exception();
+				if (time==stopCount)
+					throw fst_end_of_data_exception();
+			});
+		} catch(fst_end_of_data_exception) {
+			// end of data detected
+		}
+
+		write_output_files();
+
+		if (writeback) {
+			pool<Module*> wbmods;
+			top->writeback(wbmods);
+		}
+		delete fst;
+	}
+
+	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);
+			if (!w)
+				log_error("Wire %s not present in module %s\n",log_signal(w),log_id(topmod));
+			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") {
+				inputs[variable] = {SigBit(w,index-w->start_offset), false};
+			} else if (type == "init") {
+				inits[variable] = {SigBit(w,index-w->start_offset), false};
+			} else if (type == "latch") {
+				latches[variable] = {SigBit(w,index-w->start_offset), false};
+			} else if (type == "invlatch") {
+				latches[variable] = {SigBit(w,index-w->start_offset), true};
+			}
+		}
+
+		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;
+		std::string status;
+		int cycle = 0;
+		top = new SimInstance(this, scope, topmod);
+		register_signals();
+
+		while (!f.eof())
+		{
+			std::string line;
+			std::getline(f, line);
+			if (line.size()==0 || line[0]=='#') continue;
+			if (line[0]=='.') break;
+			if (state==0 && line.size()!=1) {
+				// old format detected, latch data
+				state = 2;
+			}
+			if (state==1 && line[0]!='b' && line[0]!='c') {
+				// was old format but with 1 bit latch
+				top->setState(latches, status);
+				state = 3;
+			}
+
+			switch(state)
+			{
+				case 0:
+					status = line;
+					state = 1;
+					break;
+				case 1:
+					state = 2;
+					break;
+				case 2:
+					top->setState(latches, line);
+					state = 3;
+					break;
+				default:
+					if (verbose)
+						log("Simulating cycle %d.\n", cycle);
+					top->setState(inputs, line);
+					if (cycle) {
+						set_inports(clock, State::S1);
+						set_inports(clockn, State::S0);
+					} else {
+						top->setState(inits, line);
+						set_inports(clock, State::S0);
+						set_inports(clockn, State::S1);
+					}
+					update();
+					register_output_step(10*cycle);
+					if (cycle) {
+						set_inports(clock, State::S0);
+						set_inports(clockn, State::S1);
+						update();
+						register_output_step(10*cycle + 5);
+					}
+					cycle++;
+					break;
+			}
+		}
+		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) {
+					if (verbose)
+						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();
+	}
+
+	std::string define_signal(Wire *wire)
+	{
+		std::stringstream f;
+
+		if (wire->width==1)
+			f << stringf("%s", RTLIL::unescape_id(wire->name).c_str());
+		else
+			if (wire->upto)
+				f << stringf("[%d:%d] %s", wire->start_offset, wire->width - 1 + wire->start_offset, RTLIL::unescape_id(wire->name).c_str());
+			else
+				f << stringf("[%d:%d] %s", wire->width - 1 + wire->start_offset, wire->start_offset, RTLIL::unescape_id(wire->name).c_str());
+		return f.str();
+	}
+
+	std::string signal_list(std::map<Wire*,fstHandle> &signals)
+	{
+		std::stringstream f;
+		for(auto item=signals.begin();item!=signals.end();item++)
+			f << stringf("%c%s", (item==signals.begin() ? ' ' : ','), RTLIL::unescape_id(item->first->name).c_str());
+		return f.str();
+	}
+
+	void generate_tb(Module *topmod, std::string tb_filename, int numcycles)
+	{
+		fst = new FstData(sim_filename);
+
+		if (scope.empty())
+			log_error("Scope must be defined for co-simulation.\n");
+
+		if ((clock.size()+clockn.size())==0)
+			log_error("Clock signal must be specified.\n");
+
+		std::vector<fstHandle> fst_clock;
+		std::map<Wire*,fstHandle> clocks;
+
+		for (auto portname : clock)
+		{
+			Wire *w = topmod->wire(portname);
+			if (!w)
+				log_error("Can't find port %s on module %s.\n", log_id(portname), log_id(top->module));
+			if (!w->port_input)
+				log_error("Clock port %s on module %s is not input.\n", log_id(portname), log_id(top->module));
+			fstHandle id = fst->getHandle(scope + "." + RTLIL::unescape_id(portname));
+			if (id==0)
+				log_error("Can't find port %s.%s in FST.\n", scope.c_str(), log_id(portname));
+			fst_clock.push_back(id);
+			clocks[w] = id;
+		}
+		for (auto portname : clockn)
+		{
+			Wire *w = topmod->wire(portname);
+			if (!w)
+				log_error("Can't find port %s on module %s.\n", log_id(portname), log_id(top->module));
+			if (!w->port_input)
+				log_error("Clock port %s on module %s is not input.\n", log_id(portname), log_id(top->module));
+			fstHandle id = fst->getHandle(scope + "." + RTLIL::unescape_id(portname));
+			if (id==0)
+				log_error("Can't find port %s.%s in FST.\n", scope.c_str(), log_id(portname));
+			fst_clock.push_back(id);
+			clocks[w] = id;
+		}
+
+		SigMap sigmap(topmod);
+		std::map<Wire*,fstHandle> inputs;
+		std::map<Wire*,fstHandle> outputs;
+
+		for (auto wire : topmod->wires()) {
+			fstHandle id = fst->getHandle(scope + "." + RTLIL::unescape_id(wire->name));
+			if (id==0 && (wire->port_input || wire->port_output))
+				log_error("Unable to find required '%s' signal in file\n",(scope + "." + RTLIL::unescape_id(wire->name)).c_str());
+			if (wire->port_input)
+				if (clocks.find(wire)==clocks.end())
+					inputs[wire] = id;
+			if (wire->port_output)
+				outputs[wire] = id;
+		}
+
+		uint64_t startCount = 0;
+		uint64_t stopCount = 0;
+		if (start_time==0) {
+			if (start_time < fst->getStartTime())
+				log_warning("Start time is before simulation file start time\n");
+			startCount = fst->getStartTime();
+		} else if (start_time==-1) 
+			startCount = fst->getEndTime();
+		else {
+			startCount = start_time / fst->getTimescale();
+			if (startCount > fst->getEndTime()) {
+				startCount = fst->getEndTime();
+				log_warning("Start time is after simulation file end time\n");
+			}
+		}
+		if (stop_time==0) {
+			if (stop_time < fst->getStartTime())
+				log_warning("Stop time is before simulation file start time\n");
+			stopCount = fst->getStartTime();
+		} else if (stop_time==-1) 
+			stopCount = fst->getEndTime();
+		else {
+			stopCount = stop_time / fst->getTimescale();
+			if (stopCount > fst->getEndTime()) {
+				stopCount = fst->getEndTime();
+				log_warning("Stop time is after simulation file end time\n");
+			}
+		}
+		if (stopCount<startCount) {
+			log_error("Stop time is before start time\n");
+		}
+
+		int cycle = 0;
+		log("Generate testbench data from %lu%s to %lu%s", (unsigned long)startCount, fst->getTimescaleString(), (unsigned long)stopCount, fst->getTimescaleString());
+		if (cycles_set) 
+			log(" for %d clock cycle(s)",numcycles);
+		log("\n");
+
+		std::stringstream f;
+		f << stringf("`timescale 1%s/1%s\n", fst->getTimescaleString(),fst->getTimescaleString());
+		f << stringf("module %s();\n",tb_filename.c_str());
+		int clk_len = 0;
+		int inputs_len = 0;
+		int outputs_len = 0;
+		for(auto &item : clocks) {
+			clk_len += item.first->width;
+			f << "\treg " << define_signal(item.first) << ";\n";
+		}
+		for(auto &item : inputs) {
+			inputs_len += item.first->width;
+			f << "\treg " << define_signal(item.first) << ";\n";
+		}
+		for(auto &item : outputs) {
+			outputs_len += item.first->width;
+			f << "\twire " << define_signal(item.first) << ";\n";
+		}
+		int data_len = clk_len + inputs_len + outputs_len + 32;
+		f << "\n";
+		f << stringf("\t%s uut(",RTLIL::unescape_id(topmod->name).c_str());
+		for(auto item=clocks.begin();item!=clocks.end();item++)
+			f << stringf("%c.%s(%s)", (item==clocks.begin() ? ' ' : ','), RTLIL::unescape_id(item->first->name).c_str(), RTLIL::unescape_id(item->first->name).c_str());
+		for(auto &item : inputs)
+			f << stringf(",.%s(%s)", RTLIL::unescape_id(item.first->name).c_str(), RTLIL::unescape_id(item.first->name).c_str());
+		for(auto &item : outputs)
+			f << stringf(",.%s(%s)", RTLIL::unescape_id(item.first->name).c_str(), RTLIL::unescape_id(item.first->name).c_str());
+		f << ");\n";
+		f << "\n";
+		f << "\tinteger i;\n";
+		uint64_t prev_time = startCount;
+		log("Writing data to `%s`\n", (tb_filename+".txt").c_str());
+		std::ofstream data_file(tb_filename+".txt");
+		std::stringstream initstate;
+		try {
+			fst->reconstructAllAtTimes(fst_clock, startCount, stopCount, [&](uint64_t time) {
+				for(auto &item : clocks)
+					data_file << stringf("%s",fst->valueOf(item.second).c_str());
+				for(auto &item : inputs)
+					data_file << stringf("%s",fst->valueOf(item.second).c_str());
+				for(auto &item : outputs)
+					data_file << stringf("%s",fst->valueOf(item.second).c_str());
+				data_file << stringf("%s\n",Const(time-prev_time).as_string().c_str());
+
+				if (time==startCount) {
+					// initial state
+					for(auto var : fst->getVars()) {
+						if (var.is_reg && !Const::from_string(fst->valueOf(var.id).c_str()).is_fully_undef()) {
+							if (var.scope == scope) {
+								initstate << stringf("\t\tuut.%s = %d'b%s;\n", var.name.c_str(), var.width, fst->valueOf(var.id).c_str());
+							} else if (var.scope.find(scope+".")==0) {
+								initstate << stringf("\t\tuut.%s.%s = %d'b%s;\n",var.scope.substr(scope.size()+1).c_str(), var.name.c_str(), var.width, fst->valueOf(var.id).c_str());
+							}
+						}
+					}
+				}
+				cycle++;
+				prev_time = time;
+
+				// Limit to number of cycles if provided
+				if (cycles_set && cycle > numcycles *2)
+					throw fst_end_of_data_exception();
+				if (time==stopCount)
+					throw fst_end_of_data_exception();
+			});
+		} catch(fst_end_of_data_exception) {
+			// end of data detected
+		}
+
+		f << stringf("\treg [0:%d] data [0:%d];\n", data_len-1, cycle-1);
+		f << "\tinitial begin;\n";
+		f << stringf("\t\t$dumpfile(\"%s\");\n",tb_filename.c_str());
+		f << stringf("\t\t$dumpvars(0,%s);\n",tb_filename.c_str());
+		f << initstate.str();
+		f << stringf("\t\t$readmemb(\"%s.txt\", data);\n",tb_filename.c_str());
+
+		f << stringf("\t\t#(data[0][%d:%d]);\n", data_len-32, data_len-1);	
+		f << stringf("\t\t{%s } = data[0][%d:%d];\n", signal_list(clocks).c_str(), 0, clk_len-1);		
+		f << stringf("\t\t{%s } <= data[0][%d:%d];\n", signal_list(inputs).c_str(), clk_len, clk_len+inputs_len-1);
+
+		f << stringf("\t\tfor (i = 1; i < %d; i++) begin\n",cycle);
+
+		f << stringf("\t\t\t#(data[i][%d:%d]);\n", data_len-32, data_len-1);	
+		f << stringf("\t\t\t{%s } = data[i][%d:%d];\n", signal_list(clocks).c_str(), 0, clk_len-1);		
+		f << stringf("\t\t\t{%s } <= data[i][%d:%d];\n", signal_list(inputs).c_str(), clk_len, clk_len+inputs_len-1);
+		
+		f << stringf("\t\t\tif ({%s } != data[i-1][%d:%d]) begin\n", signal_list(outputs).c_str(), clk_len+inputs_len, clk_len+inputs_len+outputs_len-1);
+		f << "\t\t\t\t$error(\"Signal difference detected\\n\");\n";
+		f << "\t\t\tend\n";
+		
+		f << "\t\tend\n";
+		
+		f << "\t\t$finish;\n";
+		f << "\tend\n";
+		f << "endmodule\n";
+
+		log("Writing testbench to `%s`\n", (tb_filename+".v").c_str());
+		std::ofstream tb_file(tb_filename+".v");
+		tb_file << f.str();
+
+		delete fst;
+	}
+};
+
+struct VCDWriter : public OutputWriter
+{
+	VCDWriter(SimWorker *worker, std::string filename) : OutputWriter(worker) {
+		vcdfile.open(filename.c_str());
+	}
+
+	void write(std::map<int, bool> &use_signal) override
+	{
+		if (!vcdfile.is_open()) return;
+		vcdfile << stringf("$version %s $end\n", worker->date ? yosys_version_str : "Yosys");
+
+		if (worker->date) {
+			std::time_t t = std::time(nullptr);
+			char mbstr[255];
+			if (std::strftime(mbstr, sizeof(mbstr), "%c", std::localtime(&t))) {
+				vcdfile << stringf("$date ") << mbstr << stringf(" $end\n");
+			}
+		}
+
+		if (!worker->timescale.empty())
+			vcdfile << stringf("$timescale %s $end\n", worker->timescale.c_str());
+
+		worker->top->write_output_header(
+			[this](IdString name) { vcdfile << stringf("$scope module %s $end\n", log_id(name)); },
+			[this]() { vcdfile << stringf("$upscope $end\n");},
+			[this,use_signal](Wire *wire, int id, bool is_reg) { if (use_signal.at(id)) vcdfile << stringf("$var %s %d n%d %s%s $end\n", is_reg ? "reg" : "wire", GetSize(wire), id, wire->name[0] == '$' ? "\\" : "", log_id(wire)); }
+		);
+
+		vcdfile << stringf("$enddefinitions $end\n");
+
+		for(auto& d : worker->output_data)
+		{
+			vcdfile << stringf("#%d\n", d.first);
+			for (auto &data : d.second)
+			{
+				if (!use_signal.at(data.first)) continue;
+				Const value = data.second;
+				vcdfile << "b";
+				for (int i = GetSize(value)-1; i >= 0; i--) {
+					switch (value[i]) {
+						case State::S0: vcdfile << "0"; break;
+						case State::S1: vcdfile << "1"; break;
+						case State::Sx: vcdfile << "x"; break;
+						default: vcdfile << "z";
+					}
+				}
+				vcdfile << stringf(" n%d\n", data.first);
+			}
+		}
+	}
+
+	std::ofstream vcdfile;
+};
+
+struct FSTWriter : public OutputWriter
+{
+	FSTWriter(SimWorker *worker, std::string filename) : OutputWriter(worker) {
+		fstfile = (struct fstContext *)fstWriterCreate(filename.c_str(),1);
+	}
+
+	virtual ~FSTWriter()
+	{
+		fstWriterClose(fstfile);
+	}
+
+	void write(std::map<int, bool> &use_signal) override
+	{
+		if (!fstfile) return;
+		std::time_t t = std::time(nullptr);
+		fstWriterSetVersion(fstfile, worker->date ? yosys_version_str : "Yosys");
+		if (worker->date)
+			fstWriterSetDate(fstfile, asctime(std::localtime(&t)));
+		else
+			fstWriterSetDate(fstfile, "");
+		if (!worker->timescale.empty())
+			fstWriterSetTimescaleFromString(fstfile, worker->timescale.c_str());
+
+		fstWriterSetPackType(fstfile, FST_WR_PT_FASTLZ);
+		fstWriterSetRepackOnClose(fstfile, 1);
+	   
+	   	worker->top->write_output_header(
+			[this](IdString name) { fstWriterSetScope(fstfile, FST_ST_VCD_MODULE, stringf("%s",log_id(name)).c_str(), nullptr); },
+			[this]() { fstWriterSetUpscope(fstfile); },
+			[this,use_signal](Wire *wire, int id, bool is_reg) {
+				if (!use_signal.at(id)) return;
+				fstHandle fst_id = fstWriterCreateVar(fstfile, is_reg ? FST_VT_VCD_REG : FST_VT_VCD_WIRE, FST_VD_IMPLICIT, GetSize(wire),
+												stringf("%s%s", wire->name[0] == '$' ? "\\" : "", log_id(wire)).c_str(), 0);
+
+				mapping.emplace(id, fst_id);
+			}
+		);
+
+		for(auto& d : worker->output_data)
+		{
+			fstWriterEmitTimeChange(fstfile, d.first);
+			for (auto &data : d.second)
+			{
+				if (!use_signal.at(data.first)) continue;
+				Const value = data.second;
+				std::stringstream ss;
+				for (int i = GetSize(value)-1; i >= 0; i--) {
+					switch (value[i]) {
+						case State::S0: ss << "0"; break;
+						case State::S1: ss << "1"; break;
+						case State::Sx: ss << "x"; break;
+						default: ss << "z";
+					}
+				}
+				fstWriterEmitValueChange(fstfile, mapping[data.first], ss.str().c_str());
+			}
+		}
+	}
+
+	struct fstContext *fstfile = nullptr;
+	std::map<int,fstHandle> mapping;
+};
+
+struct AIWWriter : public OutputWriter
+{
+	AIWWriter(SimWorker *worker, std::string filename) : OutputWriter(worker) {
+		aiwfile.open(filename.c_str());
+	}
+
+	virtual ~AIWWriter()
+	{
+		aiwfile << '.' << '\n';
+	}
+
+	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_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") {
+				aiw_inputs[variable] = SigBit(w,index-w->start_offset);
+			} else if (type == "init") {
+				aiw_inits[variable] = SigBit(w,index-w->start_offset);
+			} else if (type == "latch") {
+				aiw_latches[variable] = {SigBit(w,index-w->start_offset), false};
+			} else if (type == "invlatch") {
+				aiw_latches[variable] = {SigBit(w,index-w->start_offset), true};
+			}
+		}
+
+		worker->top->write_output_header(
+			[](IdString) {},
+			[]() {},
+			[this](Wire *wire, int id, bool) { mapping[wire] = id; }
+		);
+
+		std::map<int, Yosys::RTLIL::Const> current;
+		bool first = true;
+		for(auto& d : worker->output_data)
+		{
+			for (auto &data : d.second)
+			{
+				current[data.first] = data.second;
+			}
+			if (first) {
+				for (int i = 0;; i++)
+				{
+					if (aiw_latches.count(i)) {
+						SigBit bit = aiw_latches.at(i).first;
+						auto v = current[mapping[bit.wire]].bits.at(bit.offset);
+						if (v == State::S1)
+							aiwfile << (aiw_latches.at(i).second ? '0' : '1');
+						else
+							aiwfile << (aiw_latches.at(i).second ? '1' : '0');
+						continue;
+					}
+					aiwfile << '\n';
+					break;
+				}
+				first = false;
+			}
+
+			for (int i = 0;; i++)
+			{
+				if (aiw_inputs.count(i)) {
+					SigBit bit = aiw_inputs.at(i);
+					auto v = current[mapping[bit.wire]].bits.at(bit.offset);
+					if (v == State::S1)
+						aiwfile << '1';
+					else
+						aiwfile << '0';
+					continue;
+				}
+				if (aiw_inits.count(i)) {
+					SigBit bit = aiw_inits.at(i);
+					auto v = current[mapping[bit.wire]].bits.at(bit.offset);
+					if (v == State::S1)
+						aiwfile << '1';
+					else
+						aiwfile << '0';
+					continue;
+				}
+				aiwfile << '\n';
+				break;
+			}
+		} 
+	}
+
+	std::ofstream aiwfile;
+	dict<int, std::pair<SigBit, bool>> aiw_latches;
+	dict<int, SigBit> aiw_inputs, aiw_inits;
+	std::map<Wire*,int> mapping;
 };
 
 struct SimPass : public Pass {
@@ -767,6 +1795,19 @@ struct SimPass : public Pass {
 		log("    -vcd <filename>\n");
 		log("        write the simulation results to the given VCD file\n");
 		log("\n");
+		log("    -fst <filename>\n");
+		log("        write the simulation results to the given FST file\n");
+		log("\n");
+		log("    -aiw <filename>\n");
+		log("        write the simulation results to an AIGER witness file\n");
+		log("        (requires a *.aim file via -map)\n");
+		log("\n");
+		log("    -x\n");
+		log("        ignore constant x outputs in simulation file.\n");
+		log("\n");
+		log("    -date\n");
+		log("        include date and full version info in output.\n");
+		log("\n");
 		log("    -clock <portname>\n");
 		log("        name of top-level clock input\n");
 		log("\n");
@@ -789,22 +1830,64 @@ struct SimPass : public Pass {
 		log("        include the specified timescale declaration in the vcd\n");
 		log("\n");
 		log("    -n <integer>\n");
-		log("        number of cycles to simulate (default: 20)\n");
+		log("        number of clock cycles to simulate (default: 20)\n");
 		log("\n");
 		log("    -a\n");
-		log("        include all nets in VCD output, not just those with public names\n");
+		log("        use all nets in VCD/FST operations, not just those with public names\n");
 		log("\n");
 		log("    -w\n");
 		log("        writeback mode: use final simulation state as new init state\n");
 		log("\n");
+		log("    -r\n");
+		log("        read simulation results file (file formats supported: FST, VCD, AIW and WIT)\n");
+		log("		 VCD support requires vcd2fst external tool to be present\n");
+		log("\n");
+		log("    -map <filename>\n");
+		log("        read file with port and latch symbols, needed for AIGER witness input\n");
+		log("\n");
+		log("    -scope <name>\n");
+		log("        scope of simulation top model\n");
+		log("\n");
+		log("    -at <time>\n");
+		log("        sets start and stop time\n");
+		log("\n");
+		log("    -start <time>\n");
+		log("        start co-simulation in arbitary time (default 0)\n");
+		log("\n");
+		log("    -stop <time>\n");
+		log("        stop co-simulation in arbitary time (default END)\n");
+		log("\n");
+		log("    -sim\n");
+		log("        simulation with stimulus from FST (default)\n");
+		log("\n");
+		log("    -sim-cmp\n");
+		log("        co-simulation expect exact match\n");
+		log("\n");
+		log("    -sim-gold\n");
+		log("        co-simulation, x in simulation can match any value in FST\n");
+		log("\n");
+		log("    -sim-gate\n");
+		log("        co-simulation, x in FST can match any value in simulation\n");
+		log("\n");
+		log("    -q\n");
+		log("        disable per-cycle/sample log message\n");
+		log("\n");
 		log("    -d\n");
 		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;
 		int numcycles = 20;
+		bool start_set = false, stop_set = false, at_set = false;
 
 		log_header(design, "Executing SIM pass (simulate the circuit).\n");
 
@@ -813,11 +1896,24 @@ struct SimPass : public Pass {
 			if (args[argidx] == "-vcd" && argidx+1 < args.size()) {
 				std::string vcd_filename = args[++argidx];
 				rewrite_filename(vcd_filename);
-				worker.vcdfile.open(vcd_filename.c_str());
+				worker.outputfiles.emplace_back(std::unique_ptr<VCDWriter>(new VCDWriter(&worker, vcd_filename.c_str())));
+				continue;
+			}
+			if (args[argidx] == "-fst" && argidx+1 < args.size()) {
+				std::string fst_filename = args[++argidx];
+				rewrite_filename(fst_filename);
+				worker.outputfiles.emplace_back(std::unique_ptr<FSTWriter>(new FSTWriter(&worker, fst_filename.c_str())));
+				continue;
+			}
+			if (args[argidx] == "-aiw" && argidx+1 < args.size()) {
+				std::string aiw_filename = args[++argidx];
+				rewrite_filename(aiw_filename);
+				worker.outputfiles.emplace_back(std::unique_ptr<AIWWriter>(new AIWWriter(&worker, aiw_filename.c_str())));
 				continue;
 			}
 			if (args[argidx] == "-n" && argidx+1 < args.size()) {
 				numcycles = atoi(args[++argidx].c_str());
+				worker.cycles_set = true;
 				continue;
 			}
 			if (args[argidx] == "-rstlen" && argidx+1 < args.size()) {
@@ -848,6 +1944,10 @@ struct SimPass : public Pass {
 				worker.hide_internal = false;
 				continue;
 			}
+			if (args[argidx] == "-q") {
+				worker.verbose = false;
+				continue;
+			}
 			if (args[argidx] == "-d") {
 				worker.debug = true;
 				continue;
@@ -860,9 +1960,69 @@ struct SimPass : public Pass {
 				worker.zinit = true;
 				continue;
 			}
+			if (args[argidx] == "-r" && argidx+1 < args.size()) {
+				std::string sim_filename = args[++argidx];
+				rewrite_filename(sim_filename);
+				worker.sim_filename = sim_filename;
+				continue;
+			}
+			if (args[argidx] == "-map" && argidx+1 < args.size()) {
+				std::string map_filename = args[++argidx];
+				rewrite_filename(map_filename);
+				worker.map_filename = map_filename;
+				continue;
+			}
+			if (args[argidx] == "-scope" && argidx+1 < args.size()) {
+				worker.scope = args[++argidx];
+				continue;
+			}
+			if (args[argidx] == "-start" && argidx+1 < args.size()) {
+				worker.start_time = stringToTime(args[++argidx]);
+				start_set = true;
+				continue;
+			}
+			if (args[argidx] == "-stop" && argidx+1 < args.size()) {
+				worker.stop_time = stringToTime(args[++argidx]);
+				stop_set = true;
+				continue;
+			}
+			if (args[argidx] == "-at" && argidx+1 < args.size()) {
+				worker.start_time = stringToTime(args[++argidx]);
+				worker.stop_time = worker.start_time;
+				at_set = true;
+				continue;
+			}
+			if (args[argidx] == "-sim") {
+				worker.sim_mode = SimulationMode::sim;
+				continue;
+			}
+			if (args[argidx] == "-sim-cmp") {
+				worker.sim_mode = SimulationMode::cmp;
+				continue;
+			}
+			if (args[argidx] == "-sim-gold") {
+				worker.sim_mode = SimulationMode::gold;
+				continue;
+			}
+			if (args[argidx] == "-sim-gate") {
+				worker.sim_mode = SimulationMode::gate;
+				continue;
+			}
+			if (args[argidx] == "-x") {
+				worker.ignore_x = true;
+				continue;
+			}
+			if (args[argidx] == "-date") {
+				worker.date = true;
+				continue;
+			}
 			break;
 		}
 		extra_args(args, argidx, design);
+		if (at_set && (start_set || stop_set || worker.cycles_set))
+			log_error("'at' option can only be defined separate of 'start','stop' and 'n'\n");
+		if (stop_set && worker.cycles_set)
+			log_error("'stop' and 'n' can only be used exclusively'\n");
 
 		Module *top_mod = nullptr;
 
@@ -878,8 +2038,139 @@ struct SimPass : public Pass {
 			top_mod = mods.front();
 		}
 
-		worker.run(top_mod, numcycles);
+		if (worker.sim_filename.empty())
+			worker.run(top_mod, numcycles);
+		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;
 
+struct Fst2TbPass : public Pass {
+	Fst2TbPass() : Pass("fst2tb", "generate testbench out of fst file") { }
+	void help() override
+	{
+		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+		log("\n");
+		log("    fst2tb [options] [top-level]\n");
+		log("\n");
+		log("This command generates testbench for the circuit using the given top-level module\n");
+		log("and simulus signal from FST file\n");
+		log("\n");
+		log("    -tb <name>\n");
+		log("        generated testbench name.\n");
+		log("        files <name>.v and <name>.txt are created as result.\n");
+		log("\n");
+		log("    -r <filename>\n");
+		log("        read simulation FST file\n");
+		log("\n");
+		log("    -clock <portname>\n");
+		log("        name of top-level clock input\n");
+		log("\n");
+		log("    -clockn <portname>\n");
+		log("        name of top-level clock input (inverse polarity)\n");
+		log("\n");
+		log("    -scope <name>\n");
+		log("        scope of simulation top model\n");
+		log("\n");
+		log("    -start <time>\n");
+		log("        start co-simulation in arbitary time (default 0)\n");
+		log("\n");
+		log("    -stop <time>\n");
+		log("        stop co-simulation in arbitary time (default END)\n");
+		log("\n");
+		log("    -n <integer>\n");
+		log("        number of clock cycles to simulate (default: 20)\n");
+		log("\n");		
+	}
+
+	void execute(std::vector<std::string> args, RTLIL::Design *design) override
+	{
+		SimWorker worker;
+		int numcycles = 20;
+		bool stop_set = false;
+		std::string tb_filename;
+
+		log_header(design, "Executing FST2FB pass.\n");
+
+		size_t argidx;
+		for (argidx = 1; argidx < args.size(); argidx++) {
+			if (args[argidx] == "-clock" && argidx+1 < args.size()) {
+				worker.clock.insert(RTLIL::escape_id(args[++argidx]));
+				continue;
+			}
+			if (args[argidx] == "-clockn" && argidx+1 < args.size()) {
+				worker.clockn.insert(RTLIL::escape_id(args[++argidx]));
+				continue;
+			}
+			if (args[argidx] == "-r" && argidx+1 < args.size()) {
+				std::string sim_filename = args[++argidx];
+				rewrite_filename(sim_filename);
+				worker.sim_filename = sim_filename;
+				continue;
+			}
+			if (args[argidx] == "-n" && argidx+1 < args.size()) {
+				numcycles = atoi(args[++argidx].c_str());
+				worker.cycles_set = true;
+				continue;
+			}
+			if (args[argidx] == "-scope" && argidx+1 < args.size()) {
+				worker.scope = args[++argidx];
+				continue;
+			}
+			if (args[argidx] == "-start" && argidx+1 < args.size()) {
+				worker.start_time = stringToTime(args[++argidx]);
+				continue;
+			}
+			if (args[argidx] == "-stop" && argidx+1 < args.size()) {
+				worker.stop_time = stringToTime(args[++argidx]);
+				stop_set = true;
+				continue;
+			}
+			if (args[argidx] == "-tb" && argidx+1 < args.size()) {
+				tb_filename = args[++argidx];
+				continue;
+			}
+			break;
+		}
+		extra_args(args, argidx, design);
+		if (stop_set && worker.cycles_set)
+			log_error("'stop' and 'n' can only be used exclusively'\n");
+
+		Module *top_mod = nullptr;
+
+		if (design->full_selection()) {
+			top_mod = design->top_module();
+
+			if (!top_mod)
+				log_cmd_error("Design has no top module, use the 'hierarchy' command to specify one.\n");
+		} else {
+			auto mods = design->selected_whole_modules();
+			if (GetSize(mods) != 1)
+				log_cmd_error("Only one top module must be selected.\n");
+			top_mod = mods.front();
+		}
+
+		if (tb_filename.empty())
+			log_cmd_error("Testbench name must be defined.\n");
+
+		if (worker.sim_filename.empty())
+			log_cmd_error("Stimulus FST file must be defined.\n");
+
+		worker.generate_tb(top_mod, tb_filename, numcycles);
+	}
+} Fst2TbPass;
+
 PRIVATE_NAMESPACE_END