mirror of
				https://github.com/YosysHQ/yosys
				synced 2025-10-31 03:32:29 +00:00 
			
		
		
		
	
		
			
				
	
	
		
			291 lines
		
	
	
	
		
			7.8 KiB
		
	
	
	
		
			C++
		
	
	
	
	
	
			
		
		
	
	
			291 lines
		
	
	
	
		
			7.8 KiB
		
	
	
	
		
			C++
		
	
	
	
	
	
| /*
 | |
|  *  yosys -- Yosys Open SYnthesis Suite
 | |
|  *
 | |
|  *  Copyright (C) 2014  Claire Xenia Wolf <claire@yosyshq.com>
 | |
|  *  Copyright (C) 2014  Johann Glaser <Johann.Glaser@gmx.at>
 | |
|  *
 | |
|  *  Permission to use, copy, modify, and/or distribute this software for any
 | |
|  *  purpose with or without fee is hereby granted, provided that the above
 | |
|  *  copyright notice and this permission notice appear in all copies.
 | |
|  *
 | |
|  *  THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
 | |
|  *  WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
 | |
|  *  MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
 | |
|  *  ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
 | |
|  *  WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
 | |
|  *  ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
 | |
|  *  OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 | |
|  *
 | |
|  */
 | |
| 
 | |
| #include "kernel/yosys.h"
 | |
| #include "kernel/satgen.h"
 | |
| 
 | |
| USING_YOSYS_NAMESPACE
 | |
| PRIVATE_NAMESPACE_BEGIN
 | |
| 
 | |
| static uint32_t xorshift32_state = 123456789;
 | |
| 
 | |
| static uint32_t xorshift32(uint32_t limit) {
 | |
| 	xorshift32_state ^= xorshift32_state << 13;
 | |
| 	xorshift32_state ^= xorshift32_state >> 17;
 | |
| 	xorshift32_state ^= xorshift32_state << 5;
 | |
| 	return xorshift32_state % limit;
 | |
| }
 | |
| 
 | |
| static RTLIL::Wire *getw(std::vector<RTLIL::Wire*> &wires, RTLIL::Wire *w)
 | |
| {
 | |
| 	while (1) {
 | |
| 		int idx = xorshift32(GetSize(wires));
 | |
| 		if (wires[idx] != w && !wires[idx]->port_output)
 | |
| 			return wires[idx];
 | |
| 	}
 | |
| }
 | |
| 
 | |
| static void test_abcloop()
 | |
| {
 | |
| 	log("Rng seed value: %u\n", int(xorshift32_state));
 | |
| 
 | |
| 	RTLIL::Design *design = new RTLIL::Design;
 | |
| 	RTLIL::Module *module = nullptr;
 | |
| 	RTLIL::SigSpec in_sig, out_sig;
 | |
| 
 | |
| 	bool truthtab[16][4];
 | |
| 	int create_cycles = 0;
 | |
| 
 | |
| 	while (1)
 | |
| 	{
 | |
| 		module = design->addModule(ID(UUT));
 | |
| 		create_cycles++;
 | |
| 
 | |
| 		in_sig = {};
 | |
| 		out_sig = {};
 | |
| 
 | |
| 		std::vector<RTLIL::Wire*> wires;
 | |
| 
 | |
| 		for (int i = 0; i < 4; i++) {
 | |
| 			RTLIL::Wire *w = module->addWire(stringf("\\i%d", i));
 | |
| 			w->port_input = true;
 | |
| 			wires.push_back(w);
 | |
| 			in_sig.append(w);
 | |
| 		}
 | |
| 
 | |
| 		for (int i = 0; i < 4; i++) {
 | |
| 			RTLIL::Wire *w = module->addWire(stringf("\\o%d", i));
 | |
| 			w->port_output = true;
 | |
| 			wires.push_back(w);
 | |
| 			out_sig.append(w);
 | |
| 		}
 | |
| 
 | |
| 		for (int i = 0; i < 16; i++) {
 | |
| 			RTLIL::Wire *w = module->addWire(stringf("\\t%d", i));
 | |
| 			wires.push_back(w);
 | |
| 		}
 | |
| 
 | |
| 		for (auto w : wires)
 | |
| 			if (!w->port_input)
 | |
| 				switch (xorshift32(12))
 | |
| 				{
 | |
| 				case 0:
 | |
| 					module->addNotGate(w->name.str() + "g", getw(wires, w), w);
 | |
| 					break;
 | |
| 				case 1:
 | |
| 					module->addAndGate(w->name.str() + "g", getw(wires, w), getw(wires, w), w);
 | |
| 					break;
 | |
| 				case 2:
 | |
| 					module->addNandGate(w->name.str() + "g", getw(wires, w), getw(wires, w), w);
 | |
| 					break;
 | |
| 				case 3:
 | |
| 					module->addOrGate(w->name.str() + "g", getw(wires, w), getw(wires, w), w);
 | |
| 					break;
 | |
| 				case 4:
 | |
| 					module->addNorGate(w->name.str() + "g", getw(wires, w), getw(wires, w), w);
 | |
| 					break;
 | |
| 				case 5:
 | |
| 					module->addXorGate(w->name.str() + "g", getw(wires, w), getw(wires, w), w);
 | |
| 					break;
 | |
| 				case 6:
 | |
| 					module->addXnorGate(w->name.str() + "g", getw(wires, w), getw(wires, w), w);
 | |
| 					break;
 | |
| 				case 7:
 | |
| 					module->addMuxGate(w->name.str() + "g", getw(wires, w), getw(wires, w), getw(wires, w), w);
 | |
| 					break;
 | |
| 				case 8:
 | |
| 					module->addAoi3Gate(w->name.str() + "g", getw(wires, w), getw(wires, w), getw(wires, w), w);
 | |
| 					break;
 | |
| 				case 9:
 | |
| 					module->addOai3Gate(w->name.str() + "g", getw(wires, w), getw(wires, w), getw(wires, w), w);
 | |
| 					break;
 | |
| 				case 10:
 | |
| 					module->addAoi4Gate(w->name.str() + "g", getw(wires, w), getw(wires, w), getw(wires, w), getw(wires, w), w);
 | |
| 					break;
 | |
| 				case 11:
 | |
| 					module->addOai4Gate(w->name.str() + "g", getw(wires, w), getw(wires, w), getw(wires, w), getw(wires, w), w);
 | |
| 					break;
 | |
| 				}
 | |
| 
 | |
| 		module->fixup_ports();
 | |
| 		Pass::call(design, "clean");
 | |
| 
 | |
| 		ezSatPtr ez;
 | |
| 		SigMap sigmap(module);
 | |
| 		SatGen satgen(ez.get(), &sigmap);
 | |
| 
 | |
| 		for (auto c : module->cells()) {
 | |
| 			bool ok = satgen.importCell(c);
 | |
| 			log_assert(ok);
 | |
| 		}
 | |
| 
 | |
| 		std::vector<int> in_vec = satgen.importSigSpec(in_sig);
 | |
| 		std::vector<int> inverse_in_vec = ez->vec_not(in_vec);
 | |
| 
 | |
| 		std::vector<int> out_vec = satgen.importSigSpec(out_sig);
 | |
| 
 | |
| 		for (int i = 0; i < 16; i++)
 | |
| 		{
 | |
| 			std::vector<int> assumptions;
 | |
| 			for (int j = 0; j < GetSize(in_vec); j++)
 | |
| 				assumptions.push_back((i & (1 << j)) ? in_vec.at(j) : inverse_in_vec.at(j));
 | |
| 
 | |
| 			std::vector<bool> results;
 | |
| 			if (!ez->solve(out_vec, results, assumptions)) {
 | |
| 				log("No stable solution for input %d found -> recreate module.\n", i);
 | |
| 				goto recreate_module;
 | |
| 			}
 | |
| 
 | |
| 			for (int j = 0; j < 4; j++)
 | |
| 				truthtab[i][j] = results[j];
 | |
| 
 | |
| 			assumptions.push_back(ez->vec_ne(out_vec, ez->vec_const(results)));
 | |
| 
 | |
| 			std::vector<bool> results2;
 | |
| 			if (ez->solve(out_vec, results2, assumptions)) {
 | |
| 				log("Two stable solutions for input %d found -> recreate module.\n", i);
 | |
| 				goto recreate_module;
 | |
| 			}
 | |
| 		}
 | |
| 		break;
 | |
| 
 | |
| 	recreate_module:
 | |
| 		design->remove(module);
 | |
| 	}
 | |
| 
 | |
| 	log("Found viable UUT after %d cycles:\n", create_cycles);
 | |
| 	Pass::call(design, "write_rtlil");
 | |
| 	Pass::call(design, "abc");
 | |
| 
 | |
| 	log("\n");
 | |
| 	log("Pre- and post-abc truth table:\n");
 | |
| 
 | |
| 	ezSatPtr ez;
 | |
| 	SigMap sigmap(module);
 | |
| 	SatGen satgen(ez.get(), &sigmap);
 | |
| 
 | |
| 	for (auto c : module->cells()) {
 | |
| 		bool ok = satgen.importCell(c);
 | |
| 		log_assert(ok);
 | |
| 	}
 | |
| 
 | |
| 	std::vector<int> in_vec = satgen.importSigSpec(in_sig);
 | |
| 	std::vector<int> inverse_in_vec = ez->vec_not(in_vec);
 | |
| 
 | |
| 	std::vector<int> out_vec = satgen.importSigSpec(out_sig);
 | |
| 
 | |
| 	bool found_error = false;
 | |
| 	bool truthtab2[16][4];
 | |
| 
 | |
| 	for (int i = 0; i < 16; i++)
 | |
| 	{
 | |
| 		std::vector<int> assumptions;
 | |
| 		for (int j = 0; j < GetSize(in_vec); j++)
 | |
| 			assumptions.push_back((i & (1 << j)) ? in_vec.at(j) : inverse_in_vec.at(j));
 | |
| 
 | |
| 		for (int j = 0; j < 4; j++)
 | |
| 			truthtab2[i][j] = truthtab[i][j];
 | |
| 
 | |
| 		std::vector<bool> results;
 | |
| 		if (!ez->solve(out_vec, results, assumptions)) {
 | |
| 			log("No stable solution for input %d found.\n", i);
 | |
| 			found_error = true;
 | |
| 			continue;
 | |
| 		}
 | |
| 
 | |
| 		for (int j = 0; j < 4; j++)
 | |
| 			truthtab2[i][j] = results[j];
 | |
| 
 | |
| 		assumptions.push_back(ez->vec_ne(out_vec, ez->vec_const(results)));
 | |
| 
 | |
| 		std::vector<bool> results2;
 | |
| 		if (ez->solve(out_vec, results2, assumptions)) {
 | |
| 			log("Two stable solutions for input %d found -> recreate module.\n", i);
 | |
| 			found_error = true;
 | |
| 		}
 | |
| 	}
 | |
| 
 | |
| 	for (int i = 0; i < 16; i++) {
 | |
| 		log("%3d ", i);
 | |
| 		for (int j = 0; j < 4; j++)
 | |
| 			log("%c", truthtab[i][j] ? '1' : '0');
 | |
| 		log(" ");
 | |
| 		for (int j = 0; j < 4; j++)
 | |
| 			log("%c", truthtab2[i][j] ? '1' : '0');
 | |
| 		for (int j = 0; j < 4; j++)
 | |
| 			if (truthtab[i][j] != truthtab2[i][j]) {
 | |
| 				found_error = true;
 | |
| 				log(" !");
 | |
| 				break;
 | |
| 			}
 | |
| 		log("\n");
 | |
| 	}
 | |
| 
 | |
| 	log_assert(found_error == false);
 | |
| 	log("\n");
 | |
| }
 | |
| 
 | |
| struct TestAbcloopPass : public Pass {
 | |
| 	TestAbcloopPass() : Pass("test_abcloop", "automatically test handling of loops in abc command") {
 | |
| 		internal();
 | |
| 	}
 | |
| 	void help() override
 | |
| 	{
 | |
| 		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
 | |
| 		log("\n");
 | |
| 		log("    test_abcloop [options]\n");
 | |
| 		log("\n");
 | |
| 		log("Test handling of logic loops in ABC.\n");
 | |
| 		log("\n");
 | |
| 		log("    -n {integer}\n");
 | |
| 		log("        create this number of circuits and test them (default = 100).\n");
 | |
| 		log("\n");
 | |
| 		log("    -s {positive_integer}\n");
 | |
| 		log("        use this value as rng seed value (default = unix time).\n");
 | |
| 		log("\n");
 | |
| 	}
 | |
| 	void execute(std::vector<std::string> args, RTLIL::Design*) override
 | |
| 	{
 | |
| 		int num_iter = 100;
 | |
| 		xorshift32_state = 0;
 | |
| 
 | |
| 		int argidx;
 | |
| 		for (argidx = 1; argidx < GetSize(args); argidx++)
 | |
| 		{
 | |
| 			if (args[argidx] == "-n" && argidx+1 < GetSize(args)) {
 | |
| 				num_iter = atoi(args[++argidx].c_str());
 | |
| 				continue;
 | |
| 			}
 | |
| 			if (args[argidx] == "-s" && argidx+1 < GetSize(args)) {
 | |
| 				xorshift32_state = atoi(args[++argidx].c_str());
 | |
| 				continue;
 | |
| 			}
 | |
| 			break;
 | |
| 		}
 | |
| 
 | |
| 		if (xorshift32_state == 0)
 | |
| 			xorshift32_state = time(NULL) & 0x7fffffff;
 | |
| 
 | |
| 		for (int i = 0; i < num_iter; i++)
 | |
| 			test_abcloop();
 | |
| 	}
 | |
| } TestAbcloopPass;
 | |
| 
 | |
| PRIVATE_NAMESPACE_END
 |