mirror of https://github.com/YosysHQ/yosys.git
Progress in SMV back-end
This commit is contained in:
parent
99100f367d
commit
8e84418225
|
@ -166,7 +166,7 @@ struct SmvWorker
|
|||
f << stringf(" VAR\n");
|
||||
|
||||
for (auto wire : module->wires())
|
||||
f << stringf(" %s : unsigned word[%d];\n", cid(wire->name), wire->width);
|
||||
f << stringf(" %s : unsigned word[%d]; -- %s\n", cid(wire->name), wire->width, log_id(wire));
|
||||
|
||||
for (auto cell : module->cells())
|
||||
{
|
||||
|
@ -374,8 +374,65 @@ struct SmvWorker
|
|||
continue;
|
||||
}
|
||||
|
||||
// FIXME: $_BUF_, $_NOT_, $_AND_, $_NAND_, $_OR_, $_NOR_,
|
||||
// $_XOR_, $_XNOR_, $_MUX_, $_AOI3_, $_OAI3_, $_AOI4_, $_OAI4_
|
||||
if (cell->type.in("$_BUF_", "$_NOT_"))
|
||||
{
|
||||
string op = cell->type == "$_NOT_" ? "!" : "";
|
||||
assignments.push_back(stringf("%s := %s%s;", lvalue(cell->getPort("\\Y")), op.c_str(), rvalue(cell->getPort("\\A"))));
|
||||
continue;
|
||||
}
|
||||
|
||||
if (cell->type.in("$_AND_", "$_NAND_", "$_OR_", "$_NOR_", "$_XOR_", "$_XNOR_"))
|
||||
{
|
||||
string op;
|
||||
|
||||
if (cell->type.in("$_AND_", "$_NAND_")) op = "&";
|
||||
if (cell->type.in("$_OR_", "$_NOR_")) op = "|";
|
||||
if (cell->type.in("$_XOR_")) op = "xor";
|
||||
if (cell->type.in("$_XNOR_")) op = "xnor";
|
||||
|
||||
if (cell->type.in("$_NAND_", "$_NOR_"))
|
||||
assignments.push_back(stringf("%s := !(%s %s %s);", lvalue(cell->getPort("\\Y")),
|
||||
rvalue(cell->getPort("\\A")), op.c_str(), rvalue(cell->getPort("\\B"))));
|
||||
else
|
||||
assignments.push_back(stringf("%s := %s %s %s;", lvalue(cell->getPort("\\Y")),
|
||||
rvalue(cell->getPort("\\A")), op.c_str(), rvalue(cell->getPort("\\B"))));
|
||||
continue;
|
||||
}
|
||||
|
||||
if (cell->type == "$_MUX_")
|
||||
{
|
||||
assignments.push_back(stringf("%s := %s ? %s : %s;", lvalue(cell->getPort("\\Y")),
|
||||
rvalue(cell->getPort("\\S")), rvalue(cell->getPort("\\B")), rvalue(cell->getPort("\\A"))));
|
||||
continue;
|
||||
}
|
||||
|
||||
if (cell->type == "$_AOI3_")
|
||||
{
|
||||
assignments.push_back(stringf("%s := !((%s & %s) | %s);", lvalue(cell->getPort("\\Y")),
|
||||
rvalue(cell->getPort("\\A")), rvalue(cell->getPort("\\B")), rvalue(cell->getPort("\\C"))));
|
||||
continue;
|
||||
}
|
||||
|
||||
if (cell->type == "$_OAI3_")
|
||||
{
|
||||
assignments.push_back(stringf("%s := !((%s | %s) & %s);", lvalue(cell->getPort("\\Y")),
|
||||
rvalue(cell->getPort("\\A")), rvalue(cell->getPort("\\B")), rvalue(cell->getPort("\\C"))));
|
||||
continue;
|
||||
}
|
||||
|
||||
if (cell->type == "$_AOI4_")
|
||||
{
|
||||
assignments.push_back(stringf("%s := !((%s & %s) | (%s & %s));", lvalue(cell->getPort("\\Y")),
|
||||
rvalue(cell->getPort("\\A")), rvalue(cell->getPort("\\B")), rvalue(cell->getPort("\\C")), rvalue(cell->getPort("\\D"))));
|
||||
continue;
|
||||
}
|
||||
|
||||
if (cell->type == "$_OAI4_")
|
||||
{
|
||||
assignments.push_back(stringf("%s := !((%s | %s) & (%s | %s));", lvalue(cell->getPort("\\Y")),
|
||||
rvalue(cell->getPort("\\A")), rvalue(cell->getPort("\\B")), rvalue(cell->getPort("\\C")), rvalue(cell->getPort("\\D"))));
|
||||
continue;
|
||||
}
|
||||
|
||||
if (cell->type[0] == '$')
|
||||
log_error("Found currently unsupported cell type %s (%s.%s).\n", log_id(cell->type), log_id(module), log_id(cell));
|
||||
|
@ -473,7 +530,7 @@ struct SmvBackend : public Backend {
|
|||
while (indent < GetSize(line) && (line[indent] == ' ' || line[indent] == '\t'))
|
||||
indent++;
|
||||
|
||||
if (line[indent] == '$')
|
||||
if (line[indent] == '%')
|
||||
{
|
||||
vector<string> stmt = split_tokens(line);
|
||||
|
||||
|
@ -483,6 +540,7 @@ struct SmvBackend : public Backend {
|
|||
if (GetSize(stmt) == 2 && stmt[0] == "%module")
|
||||
{
|
||||
Module *module = design->module(RTLIL::escape_id(stmt[1]));
|
||||
modules.erase(module);
|
||||
|
||||
if (module == nullptr)
|
||||
log_error("Module '%s' not found.\n", stmt[1].c_str());
|
||||
|
@ -504,16 +562,19 @@ struct SmvBackend : public Backend {
|
|||
}
|
||||
}
|
||||
|
||||
*f << stringf("-- SMV description generated by %s\n", yosys_version_str);
|
||||
if (!modules.empty())
|
||||
{
|
||||
*f << stringf("-- SMV description generated by %s\n", yosys_version_str);
|
||||
|
||||
for (auto module : modules) {
|
||||
log("Creating SMV representation of module %s.\n", log_id(module));
|
||||
SmvWorker worker(module, verbose, *f);
|
||||
worker.run();
|
||||
for (auto module : modules) {
|
||||
log("Creating SMV representation of module %s.\n", log_id(module));
|
||||
SmvWorker worker(module, verbose, *f);
|
||||
worker.run();
|
||||
}
|
||||
|
||||
*f << stringf("-- end of yosys output\n");
|
||||
}
|
||||
|
||||
*f << stringf("-- end of yosys output\n");
|
||||
|
||||
if (template_f.is_open()) {
|
||||
std::string line;
|
||||
while (std::getline(template_f, line))
|
||||
|
|
Loading…
Reference in New Issue