mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-06-13 09:26:16 +00:00
Code Activity

Merge remote-tracking branch 'upstream/master'

Browse source
This commit is contained in:
Bogdan Vukobratovic 2019-06-27 12:11:47 +02:00
commit 0f32cb4e0a
37 changed files with 1632 additions and 144 deletions
Download patch file Download diff file Expand all files Collapse all files

8
CHANGELOG
View file

@ -17,8 +17,12 @@ Yosys 0.8 .. Yosys 0.8-dev
- Added "rename -src" - Added "rename -src"
- Added "equiv_opt" pass - Added "equiv_opt" pass
- Added "read_aiger" frontend - Added "read_aiger" frontend
- Extended "muxcover -mux{4,8,16}=<cost>" - Added "muxcover -mux{4,8,16}=<cost>"
- Added "muxcover -dmux=<cost>"
- Added "muxcover -nopartial"
- Added "muxpack" pass
- "synth_xilinx" to now infer hard shift registers, using new "shregmap -tech xilinx" - "synth_xilinx" to now infer hard shift registers, using new "shregmap -tech xilinx"
- Fixed sign extension of unsized constants with 'bx and 'bz MSB
Yosys 0.7 .. Yosys 0.8 Yosys 0.7 .. Yosys 0.8
@ -32,7 +36,7 @@ Yosys 0.7 .. Yosys 0.8
- Added "write_verilog -decimal" - Added "write_verilog -decimal"
- Added "scc -set_attr" - Added "scc -set_attr"
- Added "verilog_defines" command - Added "verilog_defines" command
- Remeber defines from one read_verilog to next - Remember defines from one read_verilog to next
- Added support for hierarchical defparam - Added support for hierarchical defparam
- Added FIRRTL back-end - Added FIRRTL back-end
- Improved ABC default scripts - Improved ABC default scripts

3
backends/aiger/aiger.cc
View file

@ -89,7 +89,8 @@ struct AigerWriter
aig_map[bit] = mkgate(a0, a1); aig_map[bit] = mkgate(a0, a1);
} else } else
if (alias_map.count(bit)) { if (alias_map.count(bit)) {
aig_map[bit] = bit2aig(alias_map.at(bit)); int a = bit2aig(alias_map.at(bit));
aig_map[bit] = a;
} }
if (bit == State::Sx || bit == State::Sz) if (bit == State::Sx || bit == State::Sz)

30
backends/btor/btor.cc
View file

@ -17,6 +17,11 @@
* *
*/ */
// [[CITE]] Btor2 , BtorMC and Boolector 3.0
// Aina Niemetz, Mathias Preiner, Clifford Wolf, Armin Biere
// Computer Aided Verification - 30th International Conference, CAV 2018
// https://cs.stanford.edu/people/niemetz/publication/2018/niemetzpreinerwolfbiere-cav18/
#include "kernel/rtlil.h" #include "kernel/rtlil.h"
#include "kernel/register.h" #include "kernel/register.h"
#include "kernel/sigtools.h" #include "kernel/sigtools.h"
@ -875,9 +880,28 @@ struct BtorWorker
else else
{ {
if (bit_cell.count(bit) == 0) if (bit_cell.count(bit) == 0)
log_error("No driver for signal bit %s.\n", log_signal(bit)); {
export_cell(bit_cell.at(bit)); SigSpec s = bit;
log_assert(bit_nid.count(bit));
while (i+GetSize(s) < GetSize(sig) && sig[i+GetSize(s)].wire != nullptr &&
bit_cell.count(sig[i+GetSize(s)]) == 0)
s.append(sig[i+GetSize(s)]);
log_warning("No driver for signal %s.\n", log_signal(s));
int sid = get_bv_sid(GetSize(s));
int nid = next_nid++;
btorf("%d input %d %s\n", nid, sid);
nid_width[nid] = GetSize(s);
i += GetSize(s)-1;
continue;
}
else
{
export_cell(bit_cell.at(bit));
log_assert(bit_nid.count(bit));
}
} }
} }

8
backends/json/json.cc
View file

@ -126,6 +126,10 @@ struct JsonWriter
f << stringf("%s\n", first ? "" : ","); f << stringf("%s\n", first ? "" : ",");
f << stringf(" %s: {\n", get_name(n).c_str()); f << stringf(" %s: {\n", get_name(n).c_str());
f << stringf(" \"direction\": \"%s\",\n", w->port_input ? w->port_output ? "inout" : "input" : "output"); f << stringf(" \"direction\": \"%s\",\n", w->port_input ? w->port_output ? "inout" : "input" : "output");
if (w->start_offset)
f << stringf(" \"offset\": %d,\n", w->start_offset);
if (w->upto)
f << stringf(" \"upto\": 1,\n");
f << stringf(" \"bits\": %s\n", get_bits(w).c_str()); f << stringf(" \"bits\": %s\n", get_bits(w).c_str());
f << stringf(" }"); f << stringf(" }");
first = false; first = false;
@ -189,6 +193,10 @@ struct JsonWriter
f << stringf(" %s: {\n", get_name(w->name).c_str()); f << stringf(" %s: {\n", get_name(w->name).c_str());
f << stringf(" \"hide_name\": %s,\n", w->name[0] == '$' ? "1" : "0"); f << stringf(" \"hide_name\": %s,\n", w->name[0] == '$' ? "1" : "0");
f << stringf(" \"bits\": %s,\n", get_bits(w).c_str()); f << stringf(" \"bits\": %s,\n", get_bits(w).c_str());
if (w->start_offset)
f << stringf(" \"offset\": %d,\n", w->start_offset);
if (w->upto)
f << stringf(" \"upto\": 1,\n");
f << stringf(" \"attributes\": {"); f << stringf(" \"attributes\": {");
write_parameters(w->attributes); write_parameters(w->attributes);
f << stringf("\n }\n"); f << stringf("\n }\n");

5
backends/smt2/smtio.py
View file

@ -1043,7 +1043,10 @@ class MkVcd:
scope = scope[:-1] scope = scope[:-1]
while uipath[:-1] != scope: while uipath[:-1] != scope:
print("$scope module %s $end" % uipath[len(scope)], file=self.f) scopename = uipath[len(scope)]
if scopename.startswith("$"):
scopename = "\\" + scopename
print("$scope module %s $end" % scopename, file=self.f)
scope.append(uipath[len(scope)]) scope.append(uipath[len(scope)])
if path in self.clocks and self.clocks[path][1] == "event": if path in self.clocks and self.clocks[path][1] == "event":

24
frontends/json/jsonparse.cc
View file

@ -292,6 +292,18 @@ void json_import(Design *design, string &modname, JsonNode *node)
if (port_wire == nullptr) if (port_wire == nullptr)
port_wire = module->addWire(port_name, GetSize(port_bits_node->data_array)); port_wire = module->addWire(port_name, GetSize(port_bits_node->data_array));
if (port_node->data_dict.count("upto") != 0) {
JsonNode *val = port_node->data_dict.at("upto");
if (val->type == 'N')
port_wire->upto = val->data_number != 0;
}
if (port_node->data_dict.count("offset") != 0) {
JsonNode *val = port_node->data_dict.at("offset");
if (val->type == 'N')
port_wire->start_offset = val->data_number;
}
if (port_direction_node->data_string == "input") { if (port_direction_node->data_string == "input") {
port_wire->port_input = true; port_wire->port_input = true;
} else } else
@ -372,6 +384,18 @@ void json_import(Design *design, string &modname, JsonNode *node)
if (wire == nullptr) if (wire == nullptr)
wire = module->addWire(net_name, GetSize(bits_node->data_array)); wire = module->addWire(net_name, GetSize(bits_node->data_array));
if (net_node->data_dict.count("upto") != 0) {
JsonNode *val = net_node->data_dict.at("upto");
if (val->type == 'N')
wire->upto = val->data_number != 0;
}
if (net_node->data_dict.count("offset") != 0) {
JsonNode *val = net_node->data_dict.at("offset");
if (val->type == 'N')
wire->start_offset = val->data_number;
}
for (int i = 0; i < GetSize(bits_node->data_array); i++) for (int i = 0; i < GetSize(bits_node->data_array); i++)
{ {
JsonNode *bitval_node = bits_node->data_array.at(i); JsonNode *bitval_node = bits_node->data_array.at(i);

14
frontends/verilog/const2ast.cc
View file

@ -153,7 +153,7 @@ AstNode *VERILOG_FRONTEND::const2ast(std::string code, char case_type, bool warn
{ {
if (warn_z) { if (warn_z) {
AstNode *ret = const2ast(code, case_type); AstNode *ret = const2ast(code, case_type);
if (std::find(ret->bits.begin(), ret->bits.end(), RTLIL::State::Sz) != ret->bits.end()) if (ret != nullptr && std::find(ret->bits.begin(), ret->bits.end(), RTLIL::State::Sz) != ret->bits.end())
log_warning("Yosys has only limited support for tri-state logic at the moment. (%s:%d)\n", log_warning("Yosys has only limited support for tri-state logic at the moment. (%s:%d)\n",
current_filename.c_str(), get_line_num()); current_filename.c_str(), get_line_num());
return ret; return ret;
@ -204,7 +204,7 @@ AstNode *VERILOG_FRONTEND::const2ast(std::string code, char case_type, bool warn
{ {
std::vector<RTLIL::State> data; std::vector<RTLIL::State> data;
bool is_signed = false; bool is_signed = false;
bool is_unsized = false; bool is_unsized = len_in_bits < 0;
if (*(endptr+1) == 's') { if (*(endptr+1) == 's') {
is_signed = true; is_signed = true;
endptr++; endptr++;
@ -213,25 +213,25 @@ AstNode *VERILOG_FRONTEND::const2ast(std::string code, char case_type, bool warn
{ {
case 'b': case 'b':
case 'B': case 'B':
my_strtobin(data, endptr+2, len_in_bits, 2, case_type, false); my_strtobin(data, endptr+2, len_in_bits, 2, case_type, is_unsized);
break; break;
case 'o': case 'o':
case 'O': case 'O':
my_strtobin(data, endptr+2, len_in_bits, 8, case_type, false); my_strtobin(data, endptr+2, len_in_bits, 8, case_type, is_unsized);
break; break;
case 'd': case 'd':
case 'D': case 'D':
my_strtobin(data, endptr+2, len_in_bits, 10, case_type, false); my_strtobin(data, endptr+2, len_in_bits, 10, case_type, is_unsized);
break; break;
case 'h': case 'h':
case 'H': case 'H':
my_strtobin(data, endptr+2, len_in_bits, 16, case_type, false); my_strtobin(data, endptr+2, len_in_bits, 16, case_type, is_unsized);
break; break;
default: default:
char next_char = char(tolower(*(endptr+1))); char next_char = char(tolower(*(endptr+1)));
if (next_char == '0' || next_char == '1' || next_char == 'x' || next_char == 'z') { if (next_char == '0' || next_char == '1' || next_char == 'x' || next_char == 'z') {
my_strtobin(data, endptr+1, 1, 2, case_type, true);
is_unsized = true; is_unsized = true;
my_strtobin(data, endptr+1, 1, 2, case_type, is_unsized);
} else { } else {
return NULL; return NULL;
} }

1
frontends/verilog/verilog_parser.y
View file

@ -517,6 +517,7 @@ wire_type_token:
TOK_GENVAR { TOK_GENVAR {
astbuf3->type = AST_GENVAR; astbuf3->type = AST_GENVAR;
astbuf3->is_reg = true; astbuf3->is_reg = true;
astbuf3->is_signed = true;
astbuf3->range_left = 31; astbuf3->range_left = 31;
astbuf3->range_right = 0; astbuf3->range_right = 0;
} | } |

1
kernel/register.cc
View file

@ -545,6 +545,7 @@ void Backend::extra_args(std::ostream *&f, std::string &filename, std::vector<st
} }
filename = arg; filename = arg;
rewrite_filename(filename);
std::ofstream *ff = new std::ofstream; std::ofstream *ff = new std::ofstream;
ff->open(filename.c_str(), std::ofstream::trunc); ff->open(filename.c_str(), std::ofstream::trunc);
yosys_output_files.insert(filename); yosys_output_files.insert(filename);

2
passes/cmds/write_file.cc
View file

@ -62,7 +62,7 @@ struct WriteFileFrontend : public Frontend {
if (argidx < args.size() && args[argidx].rfind("-", 0) != 0) if (argidx < args.size() && args[argidx].rfind("-", 0) != 0)
output_filename = args[argidx++]; output_filename = args[argidx++];
else else
log_cmd_error("Missing putput filename.\n"); log_cmd_error("Missing output filename.\n");
extra_args(f, filename, args, argidx); extra_args(f, filename, args, argidx);

16
passes/memory/memory_dff.cc
View file

@ -182,11 +182,17 @@ struct MemoryDffWorker
if (mux_cells_a.count(sig_data) || mux_cells_b.count(sig_data)) if (mux_cells_a.count(sig_data) || mux_cells_b.count(sig_data))
{ {
bool enable_invert = mux_cells_a.count(sig_data) != 0; RTLIL::SigSpec en;
Cell *mux = enable_invert ? mux_cells_a.at(sig_data) : mux_cells_b.at(sig_data); RTLIL::SigSpec check_q;
SigSpec check_q = sigmap(mux->getPort(enable_invert ? "\\B" : "\\A"));
do {
bool enable_invert = mux_cells_a.count(sig_data) != 0;
Cell *mux = enable_invert ? mux_cells_a.at(sig_data) : mux_cells_b.at(sig_data);
check_q = sigmap(mux->getPort(enable_invert ? "\\B" : "\\A"));
sig_data = sigmap(mux->getPort("\\Y"));
en.append(enable_invert ? module->LogicNot(NEW_ID, mux->getPort("\\S")) : mux->getPort("\\S"));
} while (mux_cells_a.count(sig_data) || mux_cells_b.count(sig_data));
sig_data = sigmap(mux->getPort("\\Y"));
for (auto bit : sig_data) for (auto bit : sig_data)
if (sigbit_users_count[bit] > 1) if (sigbit_users_count[bit] > 1)
goto skip_ff_after_read_merging; goto skip_ff_after_read_merging;
@ -195,7 +201,7 @@ struct MemoryDffWorker
{ {
disconnect_dff(sig_data); disconnect_dff(sig_data);
cell->setPort("\\CLK", clk_data); cell->setPort("\\CLK", clk_data);
cell->setPort("\\EN", enable_invert ? module->LogicNot(NEW_ID, mux->getPort("\\S")) : mux->getPort("\\S")); cell->setPort("\\EN", en.size() > 1 ? module->ReduceAnd(NEW_ID, en) : en);
cell->setPort("\\DATA", sig_data); cell->setPort("\\DATA", sig_data);
cell->parameters["\\CLK_ENABLE"] = RTLIL::Const(1); cell->parameters["\\CLK_ENABLE"] = RTLIL::Const(1);
cell->parameters["\\CLK_POLARITY"] = RTLIL::Const(clk_polarity); cell->parameters["\\CLK_POLARITY"] = RTLIL::Const(clk_polarity);

1
passes/opt/Makefile.inc
View file

@ -14,5 +14,6 @@ OBJS += passes/opt/opt_demorgan.o
OBJS += passes/opt/rmports.o OBJS += passes/opt/rmports.o
OBJS += passes/opt/opt_lut.o OBJS += passes/opt/opt_lut.o
OBJS += passes/opt/pmux2shiftx.o OBJS += passes/opt/pmux2shiftx.o
OBJS += passes/opt/muxpack.o
endif endif

368
passes/opt/muxpack.cc Normal file
View file

@ -0,0 +1,368 @@
/*
* yosys -- Yosys Open SYnthesis Suite
*
* Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
* 2019 Eddie Hung <eddie@fpgeh.com>
*
* 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/sigtools.h"
USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN
struct ExclusiveDatabase
{
Module *module;
const SigMap &sigmap;
dict<SigBit, std::pair<SigSpec,std::vector<Const>>> sig_cmp_prev;
ExclusiveDatabase(Module *module, const SigMap &sigmap) : module(module), sigmap(sigmap)
{
SigSpec const_sig, nonconst_sig;
SigBit y_port;
pool<Cell*> reduce_or;
for (auto cell : module->cells()) {
if (cell->type == "$eq") {
nonconst_sig = sigmap(cell->getPort("\\A"));
const_sig = sigmap(cell->getPort("\\B"));
if (!const_sig.is_fully_const()) {
if (!nonconst_sig.is_fully_const())
continue;
std::swap(nonconst_sig, const_sig);
}
y_port = sigmap(cell->getPort("\\Y"));
}
else if (cell->type == "$logic_not") {
nonconst_sig = sigmap(cell->getPort("\\A"));
const_sig = Const(RTLIL::S0, GetSize(nonconst_sig));
y_port = sigmap(cell->getPort("\\Y"));
}
else if (cell->type == "$reduce_or") {
reduce_or.insert(cell);
continue;
}
else continue;
log_assert(!nonconst_sig.empty());
log_assert(!const_sig.empty());
sig_cmp_prev[y_port] = std::make_pair(nonconst_sig,std::vector<Const>{const_sig.as_const()});
}
for (auto cell : reduce_or) {
nonconst_sig = SigSpec();
std::vector<Const> values;
SigSpec a_port = sigmap(cell->getPort("\\A"));
for (auto bit : a_port) {
auto it = sig_cmp_prev.find(bit);
if (it == sig_cmp_prev.end()) {
nonconst_sig = SigSpec();
break;
}
if (nonconst_sig.empty())
nonconst_sig = it->second.first;
else if (nonconst_sig != it->second.first) {
nonconst_sig = SigSpec();
break;
}
for (auto value : it->second.second)
values.push_back(value);
}
if (nonconst_sig.empty())
continue;
y_port = sigmap(cell->getPort("\\Y"));
sig_cmp_prev[y_port] = std::make_pair(nonconst_sig,std::move(values));
}
}
bool query(const SigSpec &sig) const
{
SigSpec nonconst_sig;
pool<Const> const_values;
for (auto bit : sig.bits()) {
auto it = sig_cmp_prev.find(bit);
if (it == sig_cmp_prev.end())
return false;
if (nonconst_sig.empty())
nonconst_sig = it->second.first;
else if (nonconst_sig != it->second.first)
return false;
for (auto value : it->second.second)
if (!const_values.insert(value).second)
return false;
}
return true;
}
};
struct MuxpackWorker
{
Module *module;
SigMap sigmap;
int mux_count, pmux_count;
pool<Cell*> remove_cells;
dict<SigSpec, Cell*> sig_chain_next;
dict<SigSpec, Cell*> sig_chain_prev;
pool<SigBit> sigbit_with_non_chain_users;
pool<Cell*> chain_start_cells;
pool<Cell*> candidate_cells;
ExclusiveDatabase excl_db;
void make_sig_chain_next_prev()
{
for (auto wire : module->wires())
{
if (wire->port_output || wire->get_bool_attribute("\\keep")) {
for (auto bit : sigmap(wire))
sigbit_with_non_chain_users.insert(bit);
}
}
for (auto cell : module->cells())
{
if (cell->type.in("$mux", "$pmux") && !cell->get_bool_attribute("\\keep"))
{
SigSpec a_sig = sigmap(cell->getPort("\\A"));
SigSpec b_sig;
if (cell->type == "$mux")
b_sig = sigmap(cell->getPort("\\B"));
SigSpec y_sig = sigmap(cell->getPort("\\Y"));
if (sig_chain_next.count(a_sig))
for (auto a_bit : a_sig.bits())
sigbit_with_non_chain_users.insert(a_bit);
else {
sig_chain_next[a_sig] = cell;
candidate_cells.insert(cell);
}
if (!b_sig.empty()) {
if (sig_chain_next.count(b_sig))
for (auto b_bit : b_sig.bits())
sigbit_with_non_chain_users.insert(b_bit);
else {
sig_chain_next[b_sig] = cell;
candidate_cells.insert(cell);
}
}
sig_chain_prev[y_sig] = cell;
continue;
}
for (auto conn : cell->connections())
if (cell->input(conn.first))
for (auto bit : sigmap(conn.second))
sigbit_with_non_chain_users.insert(bit);
}
}
void find_chain_start_cells()
{
for (auto cell : candidate_cells)
{
log_debug("Considering %s (%s)\n", log_id(cell), log_id(cell->type));
SigSpec a_sig = sigmap(cell->getPort("\\A"));
if (cell->type == "$mux") {
SigSpec b_sig = sigmap(cell->getPort("\\B"));
if (sig_chain_prev.count(a_sig) + sig_chain_prev.count(b_sig) != 1)
goto start_cell;
if (!sig_chain_prev.count(a_sig))
a_sig = b_sig;
}
else if (cell->type == "$pmux") {
if (!sig_chain_prev.count(a_sig))
goto start_cell;
}
else log_abort();
for (auto bit : a_sig.bits())
if (sigbit_with_non_chain_users.count(bit))
goto start_cell;
{
Cell *prev_cell = sig_chain_prev.at(a_sig);
log_assert(prev_cell);
SigSpec s_sig = sigmap(cell->getPort("\\S"));
s_sig.append(sigmap(prev_cell->getPort("\\S")));
if (!excl_db.query(s_sig))
goto start_cell;
}
continue;
start_cell:
chain_start_cells.insert(cell);
}
}
vector<Cell*> create_chain(Cell *start_cell)
{
vector<Cell*> chain;
Cell *c = start_cell;
while (c != nullptr)
{
chain.push_back(c);
SigSpec y_sig = sigmap(c->getPort("\\Y"));
if (sig_chain_next.count(y_sig) == 0)
break;
c = sig_chain_next.at(y_sig);
if (chain_start_cells.count(c) != 0)
break;
}
return chain;
}
void process_chain(vector<Cell*> &chain)
{
if (GetSize(chain) < 2)
return;
int cursor = 0;
while (cursor < GetSize(chain))
{
int cases = GetSize(chain) - cursor;
Cell *first_cell = chain[cursor];
dict<int, SigBit> taps_dict;
if (cases < 2) {
cursor++;
continue;
}
Cell *last_cell = chain[cursor+cases-1];
log("Converting %s.%s ... %s.%s to a pmux with %d cases.\n",
log_id(module), log_id(first_cell), log_id(module), log_id(last_cell), cases);
mux_count += cases;
pmux_count += 1;
first_cell->type = "$pmux";
SigSpec b_sig = first_cell->getPort("\\B");
SigSpec s_sig = first_cell->getPort("\\S");
for (int i = 1; i < cases; i++) {
Cell* prev_cell = chain[cursor+i-1];
Cell* cursor_cell = chain[cursor+i];
if (sigmap(prev_cell->getPort("\\Y")) == sigmap(cursor_cell->getPort("\\A"))) {
b_sig.append(cursor_cell->getPort("\\B"));
s_sig.append(cursor_cell->getPort("\\S"));
}
else {
log_assert(cursor_cell->type == "$mux");
b_sig.append(cursor_cell->getPort("\\A"));
s_sig.append(module->LogicNot(NEW_ID, cursor_cell->getPort("\\S")));
}
remove_cells.insert(cursor_cell);
}
first_cell->setPort("\\B", b_sig);
first_cell->setPort("\\S", s_sig);
first_cell->setParam("\\S_WIDTH", GetSize(s_sig));
first_cell->setPort("\\Y", last_cell->getPort("\\Y"));
cursor += cases;
}
}
void cleanup()
{
for (auto cell : remove_cells)
module->remove(cell);
remove_cells.clear();
sig_chain_next.clear();
sig_chain_prev.clear();
chain_start_cells.clear();
candidate_cells.clear();
}
MuxpackWorker(Module *module) :
module(module), sigmap(module), mux_count(0), pmux_count(0), excl_db(module, sigmap)
{
make_sig_chain_next_prev();
find_chain_start_cells();
for (auto c : chain_start_cells) {
vector<Cell*> chain = create_chain(c);
process_chain(chain);
}
cleanup();
}
};
struct MuxpackPass : public Pass {
MuxpackPass() : Pass("muxpack", "$mux/$pmux cascades to $pmux") { }
void help() YS_OVERRIDE
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n");
log(" muxpack [selection]\n");
log("\n");
log("This pass converts cascaded chains of $pmux cells (e.g. those create from case\n");
log("constructs) and $mux cells (e.g. those created by if-else constructs) into\n");
log("$pmux cells.\n");
log("\n");
log("This optimisation is conservative --- it will only pack $mux or $pmux cells\n");
log("whose select lines are driven by '$eq' cells with other such cells if it can be\n");
log("certain that their select inputs are mutually exclusive.\n");
log("\n");
}
void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
{
log_header(design, "Executing MUXPACK pass ($mux cell cascades to $pmux).\n");
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++)
{
break;
}
extra_args(args, argidx, design);
int mux_count = 0;
int pmux_count = 0;
for (auto module : design->selected_modules()) {
MuxpackWorker worker(module);
mux_count += worker.mux_count;
pmux_count += worker.pmux_count;
}
log("Converted %d (p)mux cells into %d pmux cells.\n", mux_count, pmux_count);
}
} MuxpackPass;
PRIVATE_NAMESPACE_END

6
passes/opt/opt_clean.cc
View file

@ -326,8 +326,8 @@ bool rmunused_module_signals(RTLIL::Module *module, bool purge_mode, bool verbos
if (wire->port_id != 0 || wire->get_bool_attribute("\\keep") || !initval.is_fully_undef()) { if (wire->port_id != 0 || wire->get_bool_attribute("\\keep") || !initval.is_fully_undef()) {
// do not delete anything with "keep" or module ports or initialized wires // do not delete anything with "keep" or module ports or initialized wires
} else } else
if (!purge_mode && check_public_name(wire->name)) { if (!purge_mode && check_public_name(wire->name) && (raw_used_signals.check_any(s1) || used_signals.check_any(s2) || s1 != s2)) {
// do not get rid of public names unless in purge mode // do not get rid of public names unless in purge mode or if the wire is entirely unused, not even aliased
} else } else
if (!raw_used_signals.check_any(s1)) { if (!raw_used_signals.check_any(s1)) {
// delete wires that aren't used by anything directly // delete wires that aren't used by anything directly
@ -480,7 +480,7 @@ void rmunused_module(RTLIL::Module *module, bool purge_mode, bool verbose, bool
std::vector<RTLIL::Cell*> delcells; std::vector<RTLIL::Cell*> delcells;
for (auto cell : module->cells()) for (auto cell : module->cells())
if (cell->type.in("$pos", "$_BUF_")) { if (cell->type.in("$pos", "$_BUF_") && !cell->has_keep_attr()) {
bool is_signed = cell->type == "$pos" && cell->getParam("\\A_SIGNED").as_bool(); bool is_signed = cell->type == "$pos" && cell->getParam("\\A_SIGNED").as_bool();
RTLIL::SigSpec a = cell->getPort("\\A"); RTLIL::SigSpec a = cell->getPort("\\A");
RTLIL::SigSpec y = cell->getPort("\\Y"); RTLIL::SigSpec y = cell->getPort("\\Y");

4
passes/sat/sat.cc
View file

@ -659,6 +659,7 @@ struct SatHelper
void dump_model_to_vcd(std::string vcd_file_name) void dump_model_to_vcd(std::string vcd_file_name)
{ {
rewrite_filename(vcd_file_name);
FILE *f = fopen(vcd_file_name.c_str(), "w"); FILE *f = fopen(vcd_file_name.c_str(), "w");
if (!f) if (!f)
log_cmd_error("Can't open output file `%s' for writing: %s\n", vcd_file_name.c_str(), strerror(errno)); log_cmd_error("Can't open output file `%s' for writing: %s\n", vcd_file_name.c_str(), strerror(errno));
@ -761,6 +762,7 @@ struct SatHelper
void dump_model_to_json(std::string json_file_name) void dump_model_to_json(std::string json_file_name)
{ {
rewrite_filename(json_file_name);
FILE *f = fopen(json_file_name.c_str(), "w"); FILE *f = fopen(json_file_name.c_str(), "w");
if (!f) if (!f)
log_cmd_error("Can't open output file `%s' for writing: %s\n", json_file_name.c_str(), strerror(errno)); log_cmd_error("Can't open output file `%s' for writing: %s\n", json_file_name.c_str(), strerror(errno));
@ -1505,6 +1507,7 @@ struct SatPass : public Pass {
{ {
if (!cnf_file_name.empty()) if (!cnf_file_name.empty())
{ {
rewrite_filename(cnf_file_name);
FILE *f = fopen(cnf_file_name.c_str(), "w"); FILE *f = fopen(cnf_file_name.c_str(), "w");
if (!f) if (!f)
log_cmd_error("Can't open output file `%s' for writing: %s\n", cnf_file_name.c_str(), strerror(errno)); log_cmd_error("Can't open output file `%s' for writing: %s\n", cnf_file_name.c_str(), strerror(errno));
@ -1608,6 +1611,7 @@ struct SatPass : public Pass {
if (!cnf_file_name.empty()) if (!cnf_file_name.empty())
{ {
rewrite_filename(cnf_file_name);
FILE *f = fopen(cnf_file_name.c_str(), "w"); FILE *f = fopen(cnf_file_name.c_str(), "w");
if (!f) if (!f)
log_cmd_error("Can't open output file `%s' for writing: %s\n", cnf_file_name.c_str(), strerror(errno)); log_cmd_error("Can't open output file `%s' for writing: %s\n", cnf_file_name.c_str(), strerror(errno));

146
passes/techmap/muxcover.cc
View file

@ -23,6 +23,7 @@
USING_YOSYS_NAMESPACE USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN PRIVATE_NAMESPACE_BEGIN
#define COST_DMUX 90
#define COST_MUX2 100 #define COST_MUX2 100
#define COST_MUX4 220 #define COST_MUX4 220
#define COST_MUX8 460 #define COST_MUX8 460
@ -57,7 +58,9 @@ struct MuxcoverWorker
bool use_mux8; bool use_mux8;
bool use_mux16; bool use_mux16;
bool nodecode; bool nodecode;
bool nopartial;
int cost_dmux;
int cost_mux2; int cost_mux2;
int cost_mux4; int cost_mux4;
int cost_mux8; int cost_mux8;
@ -69,6 +72,8 @@ struct MuxcoverWorker
use_mux8 = false; use_mux8 = false;
use_mux16 = false; use_mux16 = false;
nodecode = false; nodecode = false;
nopartial = false;
cost_dmux = COST_DMUX;
cost_mux2 = COST_MUX2; cost_mux2 = COST_MUX2;
cost_mux4 = COST_MUX4; cost_mux4 = COST_MUX4;
cost_mux8 = COST_MUX8; cost_mux8 = COST_MUX8;
@ -133,13 +138,20 @@ struct MuxcoverWorker
log(" Finished treeification: Found %d trees.\n", GetSize(tree_list)); log(" Finished treeification: Found %d trees.\n", GetSize(tree_list));
} }
bool follow_muxtree(SigBit &ret_bit, tree_t &tree, SigBit bit, const char *path) bool follow_muxtree(SigBit &ret_bit, tree_t &tree, SigBit bit, const char *path, bool first_layer = true)
{ {
if (*path) { if (*path) {
if (tree.muxes.count(bit) == 0) if (tree.muxes.count(bit) == 0) {
return false; if (first_layer || nopartial)
return false;
if (path[0] == 'S')
ret_bit = State::Sx;
else
ret_bit = bit;
return true;
}
char port_name[3] = {'\\', *path, 0}; char port_name[3] = {'\\', *path, 0};
return follow_muxtree(ret_bit, tree, sigmap(tree.muxes.at(bit)->getPort(port_name)), path+1); return follow_muxtree(ret_bit, tree, sigmap(tree.muxes.at(bit)->getPort(port_name)), path+1, false);
} else { } else {
ret_bit = bit; ret_bit = bit;
return true; return true;
@ -148,7 +160,7 @@ struct MuxcoverWorker
int prepare_decode_mux(SigBit &A, SigBit B, SigBit sel, SigBit bit) int prepare_decode_mux(SigBit &A, SigBit B, SigBit sel, SigBit bit)
{ {
if (A == B) if (A == B || sel == State::Sx)
return 0; return 0;
tuple<SigBit, SigBit, SigBit> key(A, B, sel); tuple<SigBit, SigBit, SigBit> key(A, B, sel);
@ -166,7 +178,10 @@ struct MuxcoverWorker
if (std::get<2>(entry)) if (std::get<2>(entry))
return 0; return 0;
return cost_mux2 / GetSize(std::get<1>(entry)); if (A == State::Sx || B == State::Sx)
return 0;
return cost_dmux / GetSize(std::get<1>(entry));
} }
void implement_decode_mux(SigBit ctrl_bit) void implement_decode_mux(SigBit ctrl_bit)
@ -183,9 +198,32 @@ struct MuxcoverWorker
implement_decode_mux(std::get<0>(key)); implement_decode_mux(std::get<0>(key));
implement_decode_mux(std::get<1>(key)); implement_decode_mux(std::get<1>(key));
module->addMuxGate(NEW_ID, std::get<0>(key), std::get<1>(key), std::get<2>(key), ctrl_bit); if (std::get<0>(key) == State::Sx) {
module->addBufGate(NEW_ID, std::get<1>(key), ctrl_bit);
} else if (std::get<1>(key) == State::Sx) {
module->addBufGate(NEW_ID, std::get<0>(key), ctrl_bit);
} else {
module->addMuxGate(NEW_ID, std::get<0>(key), std::get<1>(key), std::get<2>(key), ctrl_bit);
decode_mux_counter++;
}
std::get<2>(entry) = true; std::get<2>(entry) = true;
decode_mux_counter++; }
void find_best_covers(tree_t &tree, const vector<SigBit> &bits)
{
for (auto bit : bits)
find_best_cover(tree, bit);
}
int sum_best_covers(tree_t &tree, const vector<SigBit> &bits)
{
int sum = 0;
for (auto bit : pool<SigBit>(bits.begin(), bits.end())) {
int cost = tree.newmuxes.at(bit).cost;
log_debug(" Best cost for %s: %d\n", log_signal(bit), cost);
sum += cost;
}
return sum;
} }
int find_best_cover(tree_t &tree, SigBit bit) int find_best_cover(tree_t &tree, SigBit bit)
@ -218,9 +256,13 @@ struct MuxcoverWorker
mux.inputs.push_back(B); mux.inputs.push_back(B);
mux.selects.push_back(S1); mux.selects.push_back(S1);
find_best_covers(tree, mux.inputs);
log_debug(" Decode cost for mux2 at %s: %d\n", log_signal(bit), mux.cost);
mux.cost += cost_mux2; mux.cost += cost_mux2;
mux.cost += find_best_cover(tree, A); mux.cost += sum_best_covers(tree, mux.inputs);
mux.cost += find_best_cover(tree, B);
log_debug(" Cost of mux2 at %s: %d\n", log_signal(bit), mux.cost);
best_mux = mux; best_mux = mux;
} }
@ -256,13 +298,15 @@ struct MuxcoverWorker
mux.selects.push_back(S1); mux.selects.push_back(S1);
mux.selects.push_back(T1); mux.selects.push_back(T1);
mux.cost += cost_mux4; find_best_covers(tree, mux.inputs);
mux.cost += find_best_cover(tree, A); log_debug(" Decode cost for mux4 at %s: %d\n", log_signal(bit), mux.cost);
mux.cost += find_best_cover(tree, B);
mux.cost += find_best_cover(tree, C);
mux.cost += find_best_cover(tree, D);
if (best_mux.cost > mux.cost) mux.cost += cost_mux4;
mux.cost += sum_best_covers(tree, mux.inputs);
log_debug(" Cost of mux4 at %s: %d\n", log_signal(bit), mux.cost);
if (best_mux.cost >= mux.cost)
best_mux = mux; best_mux = mux;
} }
} }
@ -319,17 +363,15 @@ struct MuxcoverWorker
mux.selects.push_back(T1); mux.selects.push_back(T1);
mux.selects.push_back(U1); mux.selects.push_back(U1);
mux.cost += cost_mux8; find_best_covers(tree, mux.inputs);
mux.cost += find_best_cover(tree, A); log_debug(" Decode cost for mux8 at %s: %d\n", log_signal(bit), mux.cost);
mux.cost += find_best_cover(tree, B);
mux.cost += find_best_cover(tree, C);
mux.cost += find_best_cover(tree, D);
mux.cost += find_best_cover(tree, E);
mux.cost += find_best_cover(tree, F);
mux.cost += find_best_cover(tree, G);
mux.cost += find_best_cover(tree, H);
if (best_mux.cost > mux.cost) mux.cost += cost_mux8;
mux.cost += sum_best_covers(tree, mux.inputs);
log_debug(" Cost of mux8 at %s: %d\n", log_signal(bit), mux.cost);
if (best_mux.cost >= mux.cost)
best_mux = mux; best_mux = mux;
} }
} }
@ -423,25 +465,15 @@ struct MuxcoverWorker
mux.selects.push_back(U1); mux.selects.push_back(U1);
mux.selects.push_back(V1); mux.selects.push_back(V1);
mux.cost += cost_mux16; find_best_covers(tree, mux.inputs);
mux.cost += find_best_cover(tree, A); log_debug(" Decode cost for mux16 at %s: %d\n", log_signal(bit), mux.cost);
mux.cost += find_best_cover(tree, B);
mux.cost += find_best_cover(tree, C);
mux.cost += find_best_cover(tree, D);
mux.cost += find_best_cover(tree, E);
mux.cost += find_best_cover(tree, F);
mux.cost += find_best_cover(tree, G);
mux.cost += find_best_cover(tree, H);
mux.cost += find_best_cover(tree, I);
mux.cost += find_best_cover(tree, J);
mux.cost += find_best_cover(tree, K);
mux.cost += find_best_cover(tree, L);
mux.cost += find_best_cover(tree, M);
mux.cost += find_best_cover(tree, N);
mux.cost += find_best_cover(tree, O);
mux.cost += find_best_cover(tree, P);
if (best_mux.cost > mux.cost) mux.cost += cost_mux16;
mux.cost += sum_best_covers(tree, mux.inputs);
log_debug(" Cost of mux16 at %s: %d\n", log_signal(bit), mux.cost);
if (best_mux.cost >= mux.cost)
best_mux = mux; best_mux = mux;
} }
} }
@ -537,6 +569,7 @@ struct MuxcoverWorker
void treecover(tree_t &tree) void treecover(tree_t &tree)
{ {
int count_muxes_by_type[4] = {0, 0, 0, 0}; int count_muxes_by_type[4] = {0, 0, 0, 0};
log_debug(" Searching for best cover for tree at %s.\n", log_signal(tree.root));
find_best_cover(tree, tree.root); find_best_cover(tree, tree.root);
implement_best_cover(tree, tree.root, count_muxes_by_type); implement_best_cover(tree, tree.root, count_muxes_by_type);
log(" Replaced tree at %s: %d MUX2, %d MUX4, %d MUX8, %d MUX16\n", log_signal(tree.root), log(" Replaced tree at %s: %d MUX2, %d MUX4, %d MUX8, %d MUX16\n", log_signal(tree.root),
@ -553,12 +586,13 @@ struct MuxcoverWorker
log(" Covering trees:\n"); log(" Covering trees:\n");
// pre-fill cache of decoder muxes if (!nodecode) {
if (!nodecode) log_debug(" Populating cache of decoder muxes.\n");
for (auto &tree : tree_list) { for (auto &tree : tree_list) {
find_best_cover(tree, tree.root); find_best_cover(tree, tree.root);
tree.newmuxes.clear(); tree.newmuxes.clear();
} }
}
for (auto &tree : tree_list) for (auto &tree : tree_list)
treecover(tree); treecover(tree);
@ -584,11 +618,19 @@ struct MuxcoverPass : public Pass {
log(" Default costs: $_MUX_ = %d, $_MUX4_ = %d,\n", COST_MUX2, COST_MUX4); log(" Default costs: $_MUX_ = %d, $_MUX4_ = %d,\n", COST_MUX2, COST_MUX4);
log(" $_MUX8_ = %d, $_MUX16_ = %d\n", COST_MUX8, COST_MUX16); log(" $_MUX8_ = %d, $_MUX16_ = %d\n", COST_MUX8, COST_MUX16);
log("\n"); log("\n");
log(" -dmux=cost\n");
log(" Use the specified cost for $_MUX_ cells used in decoders.\n");
log(" Default cost: %d\n", COST_DMUX);
log("\n");
log(" -nodecode\n"); log(" -nodecode\n");
log(" Do not insert decoder logic. This reduces the number of possible\n"); log(" Do not insert decoder logic. This reduces the number of possible\n");
log(" substitutions, but guarantees that the resulting circuit is not\n"); log(" substitutions, but guarantees that the resulting circuit is not\n");
log(" less efficient than the original circuit.\n"); log(" less efficient than the original circuit.\n");
log("\n"); log("\n");
log(" -nopartial\n");
log(" Do not consider mappings that use $_MUX<N>_ to select from less\n");
log(" than <N> different signals.\n");
log("\n");
} }
void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
{ {
@ -598,6 +640,8 @@ struct MuxcoverPass : public Pass {
bool use_mux8 = false; bool use_mux8 = false;
bool use_mux16 = false; bool use_mux16 = false;
bool nodecode = false; bool nodecode = false;
bool nopartial = false;
int cost_dmux = COST_DMUX;
int cost_mux4 = COST_MUX4; int cost_mux4 = COST_MUX4;
int cost_mux8 = COST_MUX8; int cost_mux8 = COST_MUX8;
int cost_mux16 = COST_MUX16; int cost_mux16 = COST_MUX16;
@ -630,10 +674,18 @@ struct MuxcoverPass : public Pass {
} }
continue; continue;
} }
if (arg.size() >= 6 && arg.substr(0,6) == "-dmux=") {
cost_dmux = atoi(arg.substr(6).c_str());
continue;
}
if (arg == "-nodecode") { if (arg == "-nodecode") {
nodecode = true; nodecode = true;
continue; continue;
} }
if (arg == "-nopartial") {
nopartial = true;
continue;
}
break; break;
} }
extra_args(args, argidx, design); extra_args(args, argidx, design);
@ -650,10 +702,12 @@ struct MuxcoverPass : public Pass {
worker.use_mux4 = use_mux4; worker.use_mux4 = use_mux4;
worker.use_mux8 = use_mux8; worker.use_mux8 = use_mux8;
worker.use_mux16 = use_mux16; worker.use_mux16 = use_mux16;
worker.cost_dmux = cost_dmux;
worker.cost_mux4 = cost_mux4; worker.cost_mux4 = cost_mux4;
worker.cost_mux8 = cost_mux8; worker.cost_mux8 = cost_mux8;
worker.cost_mux16 = cost_mux16; worker.cost_mux16 = cost_mux16;
worker.nodecode = nodecode; worker.nodecode = nodecode;
worker.nopartial = nopartial;
worker.run(); worker.run();
} }
} }

20
passes/techmap/shregmap.cc
View file

@ -293,10 +293,22 @@ struct ShregmapWorker
if (opts.init || sigbit_init.count(q_bit) == 0) if (opts.init || sigbit_init.count(q_bit) == 0)
{ {
if (sigbit_chain_next.count(d_bit)) { auto r = sigbit_chain_next.insert(std::make_pair(d_bit, cell));
if (!r.second) {
// Insertion not successful means that d_bit is already
// connected to another register, thus mark it as a
// non chain user ...
sigbit_with_non_chain_users.insert(d_bit); sigbit_with_non_chain_users.insert(d_bit);
} else // ... and clone d_bit into another wire, and use that
sigbit_chain_next[d_bit] = cell; // wire as a different key in the d_bit-to-cell dictionary
// so that it can be identified as another chain
// (omitting this common flop)
// Link: https://github.com/YosysHQ/yosys/pull/1085
Wire *wire = module->addWire(NEW_ID);
module->connect(wire, d_bit);
sigmap.add(wire, d_bit);
sigbit_chain_next.insert(std::make_pair(wire, cell));
}
sigbit_chain_prev[q_bit] = cell; sigbit_chain_prev[q_bit] = cell;
continue; continue;
@ -605,9 +617,11 @@ struct ShregmapPass : public Pass {
log("\n"); log("\n");
log(" -tech greenpak4\n"); log(" -tech greenpak4\n");
log(" map to greenpak4 shift registers.\n"); log(" map to greenpak4 shift registers.\n");
log(" this option also implies -clkpol pos -zinit\n");
log("\n"); log("\n");
log(" -tech xilinx\n"); log(" -tech xilinx\n");
log(" map to xilinx dynamic-length shift registers.\n"); log(" map to xilinx dynamic-length shift registers.\n");
log(" this option also implies -params -init\n");
log("\n"); log("\n");
} }
void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE

9
techlibs/ecp5/arith_map.v
View file

@ -50,20 +50,21 @@ module _80_ecp5_alu (A, B, CI, BI, X, Y, CO);
wire [Y_WIDTH2-1:0] AA = A_buf; wire [Y_WIDTH2-1:0] AA = A_buf;
wire [Y_WIDTH2-1:0] BB = BI ? ~B_buf : B_buf; wire [Y_WIDTH2-1:0] BB = BI ? ~B_buf : B_buf;
wire [Y_WIDTH2-1:0] BX = B_buf;
wire [Y_WIDTH2-1:0] C = {CO, CI}; wire [Y_WIDTH2-1:0] C = {CO, CI};
wire [Y_WIDTH2-1:0] FCO, Y1; wire [Y_WIDTH2-1:0] FCO, Y1;
genvar i; genvar i;
generate for (i = 0; i < Y_WIDTH2; i = i + 2) begin:slice generate for (i = 0; i < Y_WIDTH2; i = i + 2) begin:slice
CCU2C #( CCU2C #(
.INIT0(16'b0110011010101010), .INIT0(16'b1001011010101010),
.INIT1(16'b0110011010101010), .INIT1(16'b1001011010101010),
.INJECT1_0("NO"), .INJECT1_0("NO"),
.INJECT1_1("NO") .INJECT1_1("NO")
) ccu2c_i ( ) ccu2c_i (
.CIN(C[i]), .CIN(C[i]),
.A0(AA[i]), .B0(BB[i]), .C0(1'b0), .D0(1'b1), .A0(AA[i]), .B0(BX[i]), .C0(BI), .D0(1'b1),
.A1(AA[i+1]), .B1(BB[i+1]), .C1(1'b0), .D1(1'b1), .A1(AA[i+1]), .B1(BX[i+1]), .C1(BI), .D1(1'b1),
.S0(Y[i]), .S1(Y1[i]), .S0(Y[i]), .S1(Y1[i]),
.COUT(FCO[i]) .COUT(FCO[i])
); );

40
techlibs/ecp5/cells_map.v
View file

@ -47,6 +47,28 @@ module \$__DFFSE_NP1 (input D, C, E, R, output Q); TRELLIS_FF #(.GSR("DISABLED"
module \$__DFFSE_PP0 (input D, C, E, R, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("CE"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("RESET"), .SRMODE("LSR_OVER_CE")) _TECHMAP_REPLACE_ (.CLK(C), .CE(E), .LSR(R), .DI(D), .Q(Q)); endmodule module \$__DFFSE_PP0 (input D, C, E, R, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("CE"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("RESET"), .SRMODE("LSR_OVER_CE")) _TECHMAP_REPLACE_ (.CLK(C), .CE(E), .LSR(R), .DI(D), .Q(Q)); endmodule
module \$__DFFSE_PP1 (input D, C, E, R, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("CE"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("SET"), .SRMODE("LSR_OVER_CE")) _TECHMAP_REPLACE_ (.CLK(C), .CE(E), .LSR(R), .DI(D), .Q(Q)); endmodule module \$__DFFSE_PP1 (input D, C, E, R, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("CE"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("SET"), .SRMODE("LSR_OVER_CE")) _TECHMAP_REPLACE_ (.CLK(C), .CE(E), .LSR(R), .DI(D), .Q(Q)); endmodule
// TODO: Diamond flip-flops
// module FD1P3AX(); endmodule
// module FD1P3AY(); endmodule
// module FD1P3BX(); endmodule
// module FD1P3DX(); endmodule
// module FD1P3IX(); endmodule
// module FD1P3JX(); endmodule
// module FD1S3AX(); endmodule
// module FD1S3AY(); endmodule
module FD1S3BX(input PD, D, CK, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("1"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("SET"), .SRMODE("ASYNC")) _TECHMAP_REPLACE_ (.CLK(CK), .LSR(PD), .DI(D), .Q(Q)); endmodule
module FD1S3DX(input CD, D, CK, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("1"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("RESET"), .SRMODE("ASYNC")) _TECHMAP_REPLACE_ (.CLK(CK), .LSR(CD), .DI(D), .Q(Q)); endmodule
module FD1S3IX(input CD, D, CK, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("1"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("RESET"), .SRMODE("LSR_OVER_CE")) _TECHMAP_REPLACE_ (.CLK(CK), .LSR(CD), .DI(D), .Q(Q)); endmodule
module FD1S3JX(input PD, D, CK, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("1"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("SET"), .SRMODE("LSR_OVER_CE")) _TECHMAP_REPLACE_ (.CLK(CK), .LSR(PD), .DI(D), .Q(Q)); endmodule
// module FL1P3AY(); endmodule
// module FL1P3AZ(); endmodule
// module FL1P3BX(); endmodule
// module FL1P3DX(); endmodule
// module FL1P3IY(); endmodule
// module FL1P3JY(); endmodule
// module FL1S3AX(); endmodule
// module FL1S3AY(); endmodule
// Diamond I/O buffers // Diamond I/O buffers
module IB (input I, output O); (* PULLMODE="NONE" *) TRELLIS_IO #(.DIR("INPUT")) _TECHMAP_REPLACE_ (.B(I), .O(O)); endmodule module IB (input I, output O); (* PULLMODE="NONE" *) TRELLIS_IO #(.DIR("INPUT")) _TECHMAP_REPLACE_ (.B(I), .O(O)); endmodule
module IBPU (input I, output O); (* PULLMODE="UP" *) TRELLIS_IO #(.DIR("INPUT")) _TECHMAP_REPLACE_ (.B(I), .O(O)); endmodule module IBPU (input I, output O); (* PULLMODE="UP" *) TRELLIS_IO #(.DIR("INPUT")) _TECHMAP_REPLACE_ (.B(I), .O(O)); endmodule
@ -62,8 +84,22 @@ module BBPD (input I, T, output O, inout B); (* PULLMODE="DOWN" *) TRELLIS_IO #(
module ILVDS(input A, AN, output Z); TRELLIS_IO #(.DIR("INPUT")) _TECHMAP_REPLACE_ (.B(A), .O(Z)); endmodule module ILVDS(input A, AN, output Z); TRELLIS_IO #(.DIR("INPUT")) _TECHMAP_REPLACE_ (.B(A), .O(Z)); endmodule
module OLVDS(input A, output Z, ZN); TRELLIS_IO #(.DIR("OUTPUT")) _TECHMAP_REPLACE_ (.B(Z), .I(A)); endmodule module OLVDS(input A, output Z, ZN); TRELLIS_IO #(.DIR("OUTPUT")) _TECHMAP_REPLACE_ (.B(Z), .I(A)); endmodule
// For Diamond compatibility, FIXME: add all Diamond flipflop mappings // Diamond I/O registers
module FD1S3BX(input PD, D, CK, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("1"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("SET"), .SRMODE("ASYNC")) _TECHMAP_REPLACE_ (.CLK(CK), .LSR(PD), .DI(D), .Q(Q)); endmodule module IFS1P3BX(input PD, D, SP, SCLK, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("1"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("SET"), .SRMODE("ASYNC")) _TECHMAP_REPLACE_ (.CLK(SCLK), .LSR(PD), .CE(SP), .DI(D), .Q(Q)); endmodule
module IFS1P3DX(input CD, D, SP, SCLK, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("1"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("RESET"), .SRMODE("ASYNC")) _TECHMAP_REPLACE_ (.CLK(SCLK), .LSR(CD), .CE(SP), .DI(D), .Q(Q)); endmodule
module IFS1P3IX(input CD, D, SP, SCLK, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("1"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("RESET"), .SRMODE("LSR_OVER_CE")) _TECHMAP_REPLACE_ (.CLK(SCLK), .LSR(CD), .CE(SP), .DI(D), .Q(Q)); endmodule
module IFS1P3JX(input PD, D, SP, SCLK, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("1"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("SET"), .SRMODE("LSR_OVER_CE")) _TECHMAP_REPLACE_ (.CLK(SCLK), .LSR(PD), .CE(SP), .DI(D), .Q(Q)); endmodule
module OFS1P3BX(input PD, D, SP, SCLK, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("1"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("SET"), .SRMODE("ASYNC")) _TECHMAP_REPLACE_ (.CLK(SCLK), .LSR(PD), .CE(SP), .DI(D), .Q(Q)); endmodule
module OFS1P3DX(input CD, D, SP, SCLK, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("1"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("RESET"), .SRMODE("ASYNC")) _TECHMAP_REPLACE_ (.CLK(SCLK), .LSR(CD), .CE(SP), .DI(D), .Q(Q)); endmodule
module OFS1P3IX(input CD, D, SP, SCLK, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("1"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("RESET"), .SRMODE("LSR_OVER_CE")) _TECHMAP_REPLACE_ (.CLK(SCLK), .LSR(CD), .CE(SP), .DI(D), .Q(Q)); endmodule
module OFS1P3JX(input PD, D, SP, SCLK, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("1"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("SET"), .SRMODE("LSR_OVER_CE")) _TECHMAP_REPLACE_ (.CLK(SCLK), .LSR(PD), .CE(SP), .DI(D), .Q(Q)); endmodule
// TODO: Diamond I/O latches
// module IFS1S1B(input PD, D, SCLK, output Q); endmodule
// module IFS1S1D(input CD, D, SCLK, output Q); endmodule
// module IFS1S1I(input PD, D, SCLK, output Q); endmodule
// module IFS1S1J(input CD, D, SCLK, output Q); endmodule
`ifndef NO_LUT `ifndef NO_LUT
module \$lut (A, Y); module \$lut (A, Y);

94
techlibs/ecp5/cells_sim.v
View file

@ -250,18 +250,6 @@ module TRELLIS_FF(input CLK, LSR, CE, DI, M, output reg Q);
endgenerate endgenerate
endmodule endmodule
// ---------------------------------------
module OBZ(input I, T, output O);
assign O = T ? 1'bz : I;
endmodule
// ---------------------------------------
module IB(input I, output O);
assign O = I;
endmodule
// --------------------------------------- // ---------------------------------------
(* keep *) (* keep *)
module TRELLIS_IO( module TRELLIS_IO(
@ -293,19 +281,6 @@ endmodule
// --------------------------------------- // ---------------------------------------
module OB(input I, output O);
assign O = I;
endmodule
// ---------------------------------------
module BB(input I, T, output O, inout B);
assign B = T ? 1'bz : I;
assign O = B;
endmodule
// ---------------------------------------
module INV(input A, output Z); module INV(input A, output Z);
assign Z = !A; assign Z = !A;
endmodule endmodule
@ -558,19 +533,56 @@ module DP16KD(
parameter INITVAL_3F = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; parameter INITVAL_3F = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000;
endmodule endmodule
// For Diamond compatibility, FIXME: add all Diamond flipflop mappings // TODO: Diamond flip-flops
module FD1S3BX(input PD, D, CK, output Q); // module FD1P3AX(); endmodule
TRELLIS_FF #( // module FD1P3AY(); endmodule
.GSR("DISABLED"), // module FD1P3BX(); endmodule
.CEMUX("1"), // module FD1P3DX(); endmodule
.CLKMUX("CLK"), // module FD1P3IX(); endmodule
.LSRMUX("LSR"), // module FD1P3JX(); endmodule
.REGSET("SET"), // module FD1S3AX(); endmodule
.SRMODE("ASYNC") // module FD1S3AY(); endmodule
) tff_i ( module FD1S3BX(input PD, D, CK, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("1"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("SET"), .SRMODE("ASYNC")) tff (.CLK(CK), .LSR(PD), .DI(D), .Q(Q)); endmodule
.CLK(CK), module FD1S3DX(input CD, D, CK, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("1"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("RESET"), .SRMODE("ASYNC")) tff (.CLK(CK), .LSR(CD), .DI(D), .Q(Q)); endmodule
.LSR(PD), module FD1S3IX(input CD, D, CK, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("1"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("RESET"), .SRMODE("LSR_OVER_CE")) tff (.CLK(CK), .LSR(CD), .DI(D), .Q(Q)); endmodule
.DI(D), module FD1S3JX(input PD, D, CK, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("1"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("SET"), .SRMODE("LSR_OVER_CE")) tff (.CLK(CK), .LSR(PD), .DI(D), .Q(Q)); endmodule
.Q(Q) // module FL1P3AY(); endmodule
); // module FL1P3AZ(); endmodule
endmodule // module FL1P3BX(); endmodule
// module FL1P3DX(); endmodule
// module FL1P3IY(); endmodule
// module FL1P3JY(); endmodule
// module FL1S3AX(); endmodule
// module FL1S3AY(); endmodule
// Diamond I/O buffers
module IB (input I, output O); (* PULLMODE="NONE" *) TRELLIS_IO #(.DIR("INPUT")) tio (.B(I), .O(O)); endmodule
module IBPU (input I, output O); (* PULLMODE="UP" *) TRELLIS_IO #(.DIR("INPUT")) tio (.B(I), .O(O)); endmodule
module IBPD (input I, output O); (* PULLMODE="DOWN" *) TRELLIS_IO #(.DIR("INPUT")) tio (.B(I), .O(O)); endmodule
module OB (input I, output O); (* PULLMODE="NONE" *) TRELLIS_IO #(.DIR("OUTPUT")) tio (.B(O), .I(I)); endmodule
module OBZ (input I, T, output O); (* PULLMODE="NONE" *) TRELLIS_IO #(.DIR("OUTPUT")) tio (.B(O), .I(I), .T(T)); endmodule
module OBZPU(input I, T, output O); (* PULLMODE="UP" *) TRELLIS_IO #(.DIR("OUTPUT")) tio (.B(O), .I(I), .T(T)); endmodule
module OBZPD(input I, T, output O); (* PULLMODE="DOWN" *) TRELLIS_IO #(.DIR("OUTPUT")) tio (.B(O), .I(I), .T(T)); endmodule
module OBCO (input I, output OT, OC); OLVDS olvds (.A(I), .Z(OT), .ZN(OC)); endmodule
module BB (input I, T, output O, inout B); (* PULLMODE="NONE" *) TRELLIS_IO #(.DIR("BIDIR")) tio (.B(B), .I(I), .O(O), .T(T)); endmodule
module BBPU (input I, T, output O, inout B); (* PULLMODE="UP" *) TRELLIS_IO #(.DIR("BIDIR")) tio (.B(B), .I(I), .O(O), .T(T)); endmodule
module BBPD (input I, T, output O, inout B); (* PULLMODE="DOWN" *) TRELLIS_IO #(.DIR("BIDIR")) tio (.B(B), .I(I), .O(O), .T(T)); endmodule
module ILVDS(input A, AN, output Z); TRELLIS_IO #(.DIR("INPUT")) tio (.B(A), .O(Z)); endmodule
module OLVDS(input A, output Z, ZN); TRELLIS_IO #(.DIR("OUTPUT")) tio (.B(Z), .I(A)); endmodule
// Diamond I/O registers
module IFS1P3BX(input PD, D, SP, SCLK, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("1"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("SET"), .SRMODE("ASYNC")) tff (.CLK(SCLK), .LSR(PD), .CE(SP), .DI(D), .Q(Q)); endmodule
module IFS1P3DX(input CD, D, SP, SCLK, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("1"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("RESET"), .SRMODE("ASYNC")) tff (.CLK(SCLK), .LSR(CD), .CE(SP), .DI(D), .Q(Q)); endmodule
module IFS1P3IX(input CD, D, SP, SCLK, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("1"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("RESET"), .SRMODE("LSR_OVER_CE")) tff (.CLK(SCLK), .LSR(CD), .CE(SP), .DI(D), .Q(Q)); endmodule
module IFS1P3JX(input PD, D, SP, SCLK, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("1"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("SET"), .SRMODE("LSR_OVER_CE")) tff (.CLK(SCLK), .LSR(PD), .CE(SP), .DI(D), .Q(Q)); endmodule
module OFS1P3BX(input PD, D, SP, SCLK, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("1"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("SET"), .SRMODE("ASYNC")) tff (.CLK(SCLK), .LSR(PD), .CE(SP), .DI(D), .Q(Q)); endmodule
module OFS1P3DX(input CD, D, SP, SCLK, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("1"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("RESET"), .SRMODE("ASYNC")) tff (.CLK(SCLK), .LSR(CD), .CE(SP), .DI(D), .Q(Q)); endmodule
module OFS1P3IX(input CD, D, SP, SCLK, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("1"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("RESET"), .SRMODE("LSR_OVER_CE")) tff (.CLK(SCLK), .LSR(CD), .CE(SP), .DI(D), .Q(Q)); endmodule
module OFS1P3JX(input PD, D, SP, SCLK, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("1"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("SET"), .SRMODE("LSR_OVER_CE")) tff (.CLK(SCLK), .LSR(PD), .CE(SP), .DI(D), .Q(Q)); endmodule
// TODO: Diamond I/O latches
// module IFS1S1B(input PD, D, SCLK, output Q); endmodule
// module IFS1S1D(input CD, D, SCLK, output Q); endmodule
// module IFS1S1I(input PD, D, SCLK, output Q); endmodule
// module IFS1S1J(input CD, D, SCLK, output Q); endmodule

17
techlibs/xilinx/cells_sim.v
View file

@ -278,6 +278,23 @@ module FDPE_1 (output reg Q, input C, CE, D, PRE);
always @(negedge C, posedge PRE) if (PRE) Q <= 1'b1; else if (CE) Q <= D; always @(negedge C, posedge PRE) if (PRE) Q <= 1'b1; else if (CE) Q <= D;
endmodule endmodule
module RAM32X1D (
output DPO, SPO,
input D, WCLK, WE,
input A0, A1, A2, A3, A4,
input DPRA0, DPRA1, DPRA2, DPRA3, DPRA4
);
parameter INIT = 32'h0;
parameter IS_WCLK_INVERTED = 1'b0;
wire [4:0] a = {A4, A3, A2, A1, A0};
wire [4:0] dpra = {DPRA4, DPRA3, DPRA2, DPRA1, DPRA0};
reg [31:0] mem = INIT;
assign SPO = mem[a];
assign DPO = mem[dpra];
wire clk = WCLK ^ IS_WCLK_INVERTED;
always @(posedge clk) if (WE) mem[a] <= D;
endmodule
module RAM64X1D ( module RAM64X1D (
output DPO, SPO, output DPO, SPO,
input D, WCLK, WE, input D, WCLK, WE,

4
techlibs/xilinx/cells_xtra.sh
View file

@ -116,11 +116,11 @@ function xtract_cell_decl()
xtract_cell_decl PS7 "(* keep *)" xtract_cell_decl PS7 "(* keep *)"
xtract_cell_decl PULLDOWN xtract_cell_decl PULLDOWN
xtract_cell_decl PULLUP xtract_cell_decl PULLUP
xtract_cell_decl RAM128X1D #xtract_cell_decl RAM128X1D
xtract_cell_decl RAM128X1S xtract_cell_decl RAM128X1S
xtract_cell_decl RAM256X1S xtract_cell_decl RAM256X1S
xtract_cell_decl RAM32M xtract_cell_decl RAM32M
xtract_cell_decl RAM32X1D #xtract_cell_decl RAM32X1D
xtract_cell_decl RAM32X1S xtract_cell_decl RAM32X1S
xtract_cell_decl RAM32X1S_1 xtract_cell_decl RAM32X1S_1
xtract_cell_decl RAM32X2S xtract_cell_decl RAM32X2S

18
techlibs/xilinx/cells_xtra.v
View file

@ -3655,17 +3655,6 @@ module PULLUP (...);
output O; output O;
endmodule endmodule
module RAM128X1D (...);
parameter [127:0] INIT = 128'h00000000000000000000000000000000;
parameter [0:0] IS_WCLK_INVERTED = 1'b0;
output DPO, SPO;
input [6:0] A;
input [6:0] DPRA;
input D;
input WCLK;
input WE;
endmodule
module RAM128X1S (...); module RAM128X1S (...);
parameter [127:0] INIT = 128'h00000000000000000000000000000000; parameter [127:0] INIT = 128'h00000000000000000000000000000000;
parameter [0:0] IS_WCLK_INVERTED = 1'b0; parameter [0:0] IS_WCLK_INVERTED = 1'b0;
@ -3705,13 +3694,6 @@ module RAM32M (...);
input WE; input WE;
endmodule endmodule
module RAM32X1D (...);
parameter [31:0] INIT = 32'h00000000;
parameter [0:0] IS_WCLK_INVERTED = 1'b0;
output DPO, SPO;
input A0, A1, A2, A3, A4, D, DPRA0, DPRA1, DPRA2, DPRA3, DPRA4, WCLK, WE;
endmodule
module RAM32X1S (...); module RAM32X1S (...);
parameter [31:0] INIT = 32'h00000000; parameter [31:0] INIT = 32'h00000000;
parameter [0:0] IS_WCLK_INVERTED = 1'b0; parameter [0:0] IS_WCLK_INVERTED = 1'b0;

20
techlibs/xilinx/drams.txt
View file

@ -1,4 +1,17 @@
bram $__XILINX_RAM32X1D
init 1
abits 5
dbits 1
groups 2
ports 1 1
wrmode 0 1
enable 0 1
transp 0 0
clocks 0 1
clkpol 0 2
endbram
bram $__XILINX_RAM64X1D bram $__XILINX_RAM64X1D
init 1 init 1
abits 6 abits 6
@ -25,6 +38,13 @@ bram $__XILINX_RAM128X1D
clkpol 0 2 clkpol 0 2
endbram endbram
match $__XILINX_RAM32X1D
min bits 3
min wports 1
make_outreg
or_next_if_better
endmatch
match $__XILINX_RAM64X1D match $__XILINX_RAM64X1D
min bits 5 min bits 5
min wports 1 min wports 1

34
techlibs/xilinx/drams_map.v
View file

@ -1,4 +1,38 @@
module \$__XILINX_RAM32X1D (CLK1, A1ADDR, A1DATA, B1ADDR, B1DATA, B1EN);
parameter [31:0] INIT = 32'bx;
parameter CLKPOL2 = 1;
input CLK1;
input [4:0] A1ADDR;
output A1DATA;
input [4:0] B1ADDR;
input B1DATA;
input B1EN;
RAM32X1D #(
.INIT(INIT),
.IS_WCLK_INVERTED(!CLKPOL2)
) _TECHMAP_REPLACE_ (
.DPRA0(A1ADDR[0]),
.DPRA1(A1ADDR[1]),
.DPRA2(A1ADDR[2]),
.DPRA3(A1ADDR[3]),
.DPRA4(A1ADDR[4]),
.DPO(A1DATA),
.A0(B1ADDR[0]),
.A1(B1ADDR[1]),
.A2(B1ADDR[2]),
.A3(B1ADDR[3]),
.A4(B1ADDR[4]),
.D(B1DATA),
.WCLK(CLK1),
.WE(B1EN)
);
endmodule
module \$__XILINX_RAM64X1D (CLK1, A1ADDR, A1DATA, B1ADDR, B1DATA, B1EN); module \$__XILINX_RAM64X1D (CLK1, A1ADDR, A1DATA, B1ADDR, B1DATA, B1EN);
parameter [63:0] INIT = 64'bx; parameter [63:0] INIT = 64'bx;
parameter CLKPOL2 = 1; parameter CLKPOL2 = 1;

3
tests/aiger/.gitignore vendored
View file

@ -1,2 +1 @@
*.log /*_ref.v
*.out

28
tests/memories/issue00335.v Normal file
View file

@ -0,0 +1,28 @@
// expect-wr-ports 1
// expect-rd-ports 1
// expect-rd-clk \clk
module ram2 (input clk,
input sel,
input we,
input [SIZE-1:0] adr,
input [63:0] dat_i,
output reg [63:0] dat_o);
parameter SIZE = 5; // Address size
reg [63:0] mem [0:(1 << SIZE)-1];
integer i;
initial begin
for (i = 0; i < (1<<SIZE) - 1; i = i + 1)
mem[i] <= 0;
end
always @(posedge clk)
if (sel) begin
if (~we)
dat_o <= mem[adr];
else
mem[adr] <= dat_i;
end
endmodule

17
tests/memories/issue00710.v Normal file
View file

@ -0,0 +1,17 @@
// expect-wr-ports 1
// expect-rd-ports 1
// expect-rd-clk \clk
module top(input clk, input we, re, reset, input [7:0] addr, wdata, output reg [7:0] rdata);
reg [7:0] bram[0:255];
(* keep *) reg dummy;
always @(posedge clk)
if (reset)
dummy <= 1'b0;
else if (re)
rdata <= bram[addr];
else if (we)
bram[addr] <= wdata;
endmodule

6
tests/memories/run-test.sh
View file

@ -14,7 +14,7 @@ shift "$((OPTIND-1))"
bash ../tools/autotest.sh $seed -G *.v bash ../tools/autotest.sh $seed -G *.v
for f in `egrep -l 'expect-(wr|rd)-ports' *.v`; do for f in `egrep -l 'expect-(wr-ports|rd-ports|rd-clk)' *.v`; do
echo -n "Testing expectations for $f .." echo -n "Testing expectations for $f .."
../../yosys -qp "proc; opt; memory -nomap;; dump -outfile ${f%.v}.dmp t:\$mem" $f ../../yosys -qp "proc; opt; memory -nomap;; dump -outfile ${f%.v}.dmp t:\$mem" $f
if grep -q expect-wr-ports $f; then if grep -q expect-wr-ports $f; then
@ -25,6 +25,10 @@ for f in `egrep -l 'expect-(wr|rd)-ports' *.v`; do
grep -q "parameter \\\\RD_PORTS $(gawk '/expect-rd-ports/ { print $3; }' $f)\$" ${f%.v}.dmp || grep -q "parameter \\\\RD_PORTS $(gawk '/expect-rd-ports/ { print $3; }' $f)\$" ${f%.v}.dmp ||
{ echo " ERROR: Unexpected number of read ports."; false; } { echo " ERROR: Unexpected number of read ports."; false; }
fi fi
if grep -q expect-rd-clk $f; then
grep -q "connect \\\\RD_CLK \\$(gawk '/expect-rd-clk/ { print $3; }' $f)\$" ${f%.v}.dmp ||
{ echo " ERROR: Unexpected read clock."; false; }
fi
echo " ok." echo " ok."
done done

11
tests/simple/generate.v
View file

@ -148,3 +148,14 @@ generate
endgenerate endgenerate
assign out = steps[WIDTH].outer[0].val; assign out = steps[WIDTH].outer[0].val;
endmodule endmodule
// ------------------------------------------
module gen_test6(output [3:0] o);
generate
genvar i;
for (i = 3; i >= 0; i = i-1) begin
assign o[i] = 1'b0;
end
endgenerate
endmodule

3
tests/various/.gitignore vendored
View file

@ -1 +1,2 @@
*.log /*.log
/*.out

141
tests/various/muxcover.ys
View file

@ -13,7 +13,7 @@ read_verilog -formal <<EOT
EOT EOT
## Examle usage for "pmuxtree" and "muxcover" ## Example usage for "pmuxtree" and "muxcover"
proc proc
pmuxtree pmuxtree
@ -49,3 +49,142 @@ hierarchy -top equiv
equiv_simple -undef equiv_simple -undef
equiv_status -assert equiv_status -assert
## Partial matching MUX4
design -reset
read_verilog -formal <<EOT
module mux_if_bal_3_1 #(parameter N=3, parameter W=1) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
always @* begin
o <= {{W{{1'bx}}}};
if (s[0] == 1'b0)
if (s[1] == 1'b0)
o <= i[0*W+:W];
else
o <= i[1*W+:W];
else
if (s[1] == 1'b0)
o <= i[2*W+:W];
end
endmodule
EOT
prep
design -save gold
techmap
muxcover -mux4=150
select -assert-count 0 t:$_MUX_
select -assert-count 1 t:$_MUX4_
select -assert-count 0 t:$_MUX8_
select -assert-count 0 t:$_MUX16_
techmap -map +/simcells.v t:$_MUX4_
design -stash gate
design -import gold -as gold
design -import gate -as gate
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -show-ports miter
## Partial matching MUX8
design -reset
read_verilog -formal <<EOT
module mux_if_bal_5_1 #(parameter N=5, parameter W=1) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
always @* begin
o <= {{W{{1'bx}}}};
if (s[0] == 1'b0)
if (s[1] == 1'b0)
if (s[2] == 1'b0)
o <= i[0*W+:W];
else
o <= i[1*W+:W];
else
if (s[2] == 1'b0)
o <= i[2*W+:W];
else
o <= i[3*W+:W];
else
if (s[1] == 1'b0)
if (s[2] == 1'b0)
o <= i[4*W+:W];
end
endmodule
EOT
prep
design -save gold
techmap
muxcover -mux4=150 -mux8=200
clean
opt_expr -mux_bool
select -assert-count 0 t:$_MUX_
select -assert-count 0 t:$_MUX4_
select -assert-count 1 t:$_MUX8_
select -assert-count 0 t:$_MUX16_
techmap -map +/simcells.v t:$_MUX8_
design -stash gate
design -import gold -as gold
design -import gate -as gate
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -show-ports miter
## Partial matching MUX16
design -reset
read_verilog -formal <<EOT
module mux_if_bal_9_1 #(parameter N=9, parameter W=1) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
always @* begin
o <= {{W{{1'bx}}}};
if (s[0] == 1'b0)
if (s[1] == 1'b0)
if (s[2] == 1'b0)
if (s[3] == 1'b0)
o <= i[0*W+:W];
else
o <= i[1*W+:W];
else
if (s[3] == 1'b0)
o <= i[2*W+:W];
else
o <= i[3*W+:W];
else
if (s[2] == 1'b0)
if (s[3] == 1'b0)
o <= i[4*W+:W];
else
o <= i[5*W+:W];
else
if (s[3] == 1'b0)
o <= i[6*W+:W];
else
o <= i[7*W+:W];
else
if (s[1] == 1'b0)
if (s[2] == 1'b0)
if (s[3] == 1'b0)
o <= i[8*W+:W];
end
endmodule
EOT
prep
design -save gold
techmap
muxcover -mux4=150 -mux8=200 -mux16=250
clean
opt_expr -mux_bool
select -assert-count 0 t:$_MUX_
select -assert-count 0 t:$_MUX4_
select -assert-count 0 t:$_MUX8_
select -assert-count 1 t:$_MUX16_
techmap -map +/simcells.v t:$_MUX16_
design -stash gate
design -import gold -as gold
design -import gate -as gate
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -show-ports miter

259
tests/various/muxpack.v Normal file
View file

@ -0,0 +1,259 @@
module mux_if_unbal_4_1 #(parameter N=4, parameter W=1) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
always @*
if (s == 0) o <= i[0*W+:W];
else if (s == 1) o <= i[1*W+:W];
else if (s == 2) o <= i[2*W+:W];
else if (s == 3) o <= i[3*W+:W];
else o <= {W{1'bx}};
endmodule
module mux_if_unbal_5_3 #(parameter N=5, parameter W=3) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
always @* begin
o <= {W{1'bx}};
if (s == 0) o <= i[0*W+:W];
if (s == 1) o <= i[1*W+:W];
if (s == 2) o <= i[2*W+:W];
if (s == 3) o <= i[3*W+:W];
if (s == 4) o <= i[4*W+:W];
end
endmodule
module mux_if_unbal_5_3_invert #(parameter N=5, parameter W=3) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
always @*
if (s != 0)
if (s != 1)
if (s != 2)
if (s != 3)
if (s != 4) o <= i[4*W+:W];
else o <= i[0*W+:W];
else o <= i[3*W+:W];
else o <= i[2*W+:W];
else o <= i[1*W+:W];
else o <= {W{1'bx}};
endmodule
module mux_if_unbal_5_3_width_mismatch #(parameter N=5, parameter W=3) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
always @* begin
o <= {W{1'bx}};
if (s == 0) o <= i[0*W+:W];
if (s == 1) o <= i[1*W+:W];
if (s == 2) o[W-2:0] <= i[2*W+:W-1];
if (s == 3) o <= i[3*W+:W];
if (s == 4) o <= i[4*W+:W];
end
endmodule
module mux_if_unbal_4_1_missing #(parameter N=5, parameter W=3) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
always @* begin
if (s == 0) o <= i[0*W+:W];
// else if (s == 1) o <= i[1*W+:W];
// else if (s == 2) o <= i[2*W+:W];
else if (s == 3) o <= i[3*W+:W];
else o <= {W{1'bx}};
end
endmodule
module mux_if_unbal_5_3_order #(parameter N=5, parameter W=3) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
always @* begin
o <= {W{1'bx}};
if (s == 3) o <= i[3*W+:W];
if (s == 2) o <= i[2*W+:W];
if (s == 1) o <= i[1*W+:W];
if (s == 4) o <= i[4*W+:W];
if (s == 0) o <= i[0*W+:W];
end
endmodule
module mux_if_unbal_4_1_nonexcl #(parameter N=4, parameter W=1) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
always @*
if (s == 0) o <= i[0*W+:W];
else if (s == 1) o <= i[1*W+:W];
else if (s == 2) o <= i[2*W+:W];
else if (s == 3) o <= i[3*W+:W];
else if (s == 0) o <= {W{1'b0}};
else o <= {W{1'bx}};
endmodule
module mux_if_unbal_5_3_nonexcl #(parameter N=5, parameter W=3) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
always @* begin
o <= {W{1'bx}};
if (s == 0) o <= i[0*W+:W];
if (s == 1) o <= i[1*W+:W];
if (s == 2) o <= i[2*W+:W];
if (s == 3) o <= i[3*W+:W];
if (s == 4) o <= i[4*W+:W];
if (s == 0) o <= i[2*W+:W];
end
endmodule
module mux_case_unbal_8_7#(parameter N=8, parameter W=7) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
always @* begin
o <= {W{1'bx}};
case (s)
0: o <= i[0*W+:W];
default:
case (s)
1: o <= i[1*W+:W];
2: o <= i[2*W+:W];
default:
case (s)
3: o <= i[3*W+:W];
4: o <= i[4*W+:W];
5: o <= i[5*W+:W];
default:
case (s)
6: o <= i[6*W+:W];
default: o <= i[7*W+:W];
endcase
endcase
endcase
endcase
end
endmodule
module mux_if_bal_8_2 #(parameter N=8, parameter W=2) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
always @*
if (s[0] == 1'b0)
if (s[1] == 1'b0)
if (s[2] == 1'b0)
o <= i[0*W+:W];
else
o <= i[1*W+:W];
else
if (s[2] == 1'b0)
o <= i[2*W+:W];
else
o <= i[3*W+:W];
else
if (s[1] == 1'b0)
if (s[2] == 1'b0)
o <= i[4*W+:W];
else
o <= i[5*W+:W];
else
if (s[2] == 1'b0)
o <= i[6*W+:W];
else
o <= i[7*W+:W];
endmodule
module mux_if_bal_5_1 #(parameter N=5, parameter W=1) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
always @*
if (s[0] == 1'b0)
if (s[1] == 1'b0)
if (s[2] == 1'b0)
o <= i[0*W+:W];
else
o <= i[1*W+:W];
else
if (s[2] == 1'b0)
o <= i[2*W+:W];
else
o <= i[3*W+:W];
else
o <= i[4*W+:W];
endmodule
module cliffordwolf_nonexclusive_select (
input wire x, y, z,
input wire a, b, c, d,
output reg o
);
always @* begin
o = a;
if (x) o = b;
if (y) o = c;
if (z) o = d;
end
endmodule
module cliffordwolf_freduce (
input wire [1:0] s,
input wire a, b, c, d,
output reg [3:0] o
);
always @* begin
o = {4{a}};
if (s == 0) o = {3{b}};
if (s == 1) o = {2{c}};
if (s == 2) o = d;
end
endmodule
module case_nonexclusive_select (
input wire [1:0] x, y,
input wire a, b, c, d, e,
output reg o
);
always @* begin
case (x)
0: o = b;
2: o = b;
1: o = c;
default: begin
o = a;
if (y == 0) o = d;
if (y == 1) o = e;
end
endcase
end
endmodule
module case_nonoverlap (
input wire [2:0] x,
input wire a, b, c, d, e,
output reg o
);
always @* begin
case (x)
0, 2: o = b; // Creates $reduce_or
1: o = c;
default:
case (x)
3: o = d; 4: o = d; // Creates $reduce_or
5: o = e;
default: o = 1'b0;
endcase
endcase
end
endmodule
module case_overlap (
input wire [2:0] x,
input wire a, b, c, d, e,
output reg o
);
always @* begin
case (x)
0, 2: o = b; // Creates $reduce_or
1: o = c;
default:
case (x)
0: o = 1'b1; // OVERLAP!
3, 4: o = d; // Creates $reduce_or
5: o = e;
default: o = 1'b0;
endcase
endcase
end
endmodule
module case_overlap2 (
input wire [2:0] x,
input wire a, b, c, d, e,
output reg o
);
always @* begin
case (x)
0: o = b; 2: o = b; // Creates $reduce_or
1: o = c;
default:
case (x)
0: o = d; 2: o = d; // Creates $reduce_or
3: o = d; 4: o = d; // Creates $reduce_or
5: o = e;
default: o = 1'b0;
endcase
endcase
end
endmodule

268
tests/various/muxpack.ys Normal file
View file

@ -0,0 +1,268 @@
read_verilog muxpack.v
design -save read
hierarchy -top mux_if_unbal_4_1
prep
design -save gold
muxpack
opt
stat
select -assert-count 0 t:$mux
select -assert-count 1 t:$pmux
design -stash gate
design -import gold -as gold
design -import gate -as gate
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -show-ports miter
design -load read
hierarchy -top mux_if_unbal_5_3
prep
design -save gold
muxpack
opt
stat
select -assert-count 0 t:$mux
select -assert-count 1 t:$pmux
design -stash gate
design -import gold -as gold
design -import gate -as gate
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -show-ports miter
# TODO: Currently ExclusiveDatabase only analyses $eq cells
#design -load read
#hierarchy -top mux_if_unbal_5_3_invert
#prep
#design -save gold
#muxpack
#opt
#stat
#select -assert-count 0 t:$mux
#select -assert-count 1 t:$pmux
#design -stash gate
#design -import gold -as gold
#design -import gate -as gate
#miter -equiv -flatten -make_assert -make_outputs gold gate miter
#sat -verify -prove-asserts -show-ports miter
design -load read
hierarchy -top mux_if_unbal_5_3_width_mismatch
prep
design -save gold
muxpack
opt
stat
select -assert-count 0 t:$mux
select -assert-count 2 t:$pmux
design -stash gate
design -import gold -as gold
design -import gate -as gate
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -show-ports miter
design -load read
hierarchy -top mux_if_unbal_4_1_missing
prep
design -save gold
muxpack
opt
stat
select -assert-count 0 t:$mux
select -assert-count 1 t:$pmux
design -stash gate
design -import gold -as gold
design -import gate -as gate
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -show-ports miter
design -load read
hierarchy -top mux_if_unbal_5_3_order
prep
design -save gold
muxpack
opt
stat
select -assert-count 0 t:$mux
select -assert-count 1 t:$pmux
design -stash gate
design -import gold -as gold
design -import gate -as gate
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -show-ports miter
design -load read
hierarchy -top mux_if_unbal_4_1_nonexcl
prep
design -save gold
muxpack
opt
stat
select -assert-count 0 t:$mux
select -assert-count 1 t:$pmux
design -stash gate
design -import gold -as gold
design -import gate -as gate
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -show-ports miter
design -load read
hierarchy -top mux_if_unbal_5_3_nonexcl
prep
design -save gold
muxpack
opt
stat
select -assert-count 0 t:$mux
select -assert-count 1 t:$pmux
design -stash gate
design -import gold -as gold
design -import gate -as gate
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -show-ports miter
design -load read
hierarchy -top mux_case_unbal_8_7
prep
design -save gold
muxpack
opt
stat
select -assert-count 0 t:$mux
select -assert-count 1 t:$pmux
design -stash gate
design -import gold -as gold
design -import gate -as gate
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -show-ports miter
design -load read
hierarchy -top mux_if_bal_8_2
prep
design -save gold
muxpack
opt
stat
select -assert-count 7 t:$mux
select -assert-count 0 t:$pmux
design -stash gate
design -import gold -as gold
design -import gate -as gate
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -show-ports miter
design -load read
hierarchy -top mux_if_bal_5_1
prep
design -save gold
muxpack
opt
stat
select -assert-count 4 t:$mux
select -assert-count 0 t:$pmux
design -stash gate
design -import gold -as gold
design -import gate -as gate
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -show-ports miter
design -load read
hierarchy -top cliffordwolf_nonexclusive_select
prep
design -save gold
muxpack
opt
stat
select -assert-count 3 t:$mux
select -assert-count 0 t:$pmux
design -stash gate
design -import gold -as gold
design -import gate -as gate
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -show-ports miter
#design -load read
#hierarchy -top cliffordwolf_freduce
#prep
#design -save gold
#proc; opt; freduce; opt
#show
#muxpack
#opt
#stat
#select -assert-count 0 t:$mux
#select -assert-count 1 t:$pmux
#design -stash gate
#design -import gold -as gold
#design -import gate -as gate
#miter -equiv -flatten -make_assert -make_outputs gold gate miter
#sat -verify -prove-asserts -show-ports miter
design -load read
hierarchy -top case_nonexclusive_select
prep
design -save gold
muxpack
opt
stat
select -assert-count 0 t:$mux
select -assert-count 2 t:$pmux
design -stash gate
design -import gold -as gold
design -import gate -as gate
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -show-ports miter
design -load read
hierarchy -top case_nonoverlap
#prep # Do not prep otherwise $pmux's overlapping entry will get removed
proc
design -save gold
opt -fast -mux_undef
select -assert-count 2 t:$pmux
muxpack
opt
stat
select -assert-count 0 t:$mux
select -assert-count 1 t:$pmux
design -stash gate
design -import gold -as gold
design -import gate -as gate
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -show-ports miter
design -load read
hierarchy -top case_overlap
#prep # Do not prep otherwise $pmux's overlapping entry will get removed
proc
design -save gold
opt -fast -mux_undef
select -assert-count 2 t:$pmux
muxpack
opt
stat
select -assert-count 0 t:$mux
select -assert-count 2 t:$pmux
design -stash gate
design -import gold -as gold
design -import gate -as gate
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -show-ports miter
design -load read
hierarchy -top case_overlap2
#prep # Do not prep otherwise $pmux's overlapping entry will get removed
proc
design -save gold
opt -fast -mux_undef
select -assert-count 2 t:$pmux
muxpack
opt
stat
select -assert-count 0 t:$mux
select -assert-count 2 t:$pmux
design -stash gate
design -import gold -as gold
design -import gate -as gate
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -show-ports miter

48
tests/various/shregmap.v Normal file
View file

@ -0,0 +1,48 @@
module shregmap_static_test(input i, clk, output [1:0] q);
reg head = 1'b0;
reg [3:0] shift1 = 4'b0000;
reg [3:0] shift2 = 4'b0000;
always @(posedge clk) begin
head <= i;
shift1 <= {shift1[2:0], head};
shift2 <= {shift2[2:0], head};
end
assign q = {shift2[3], shift1[3]};
endmodule
module $__SHREG_DFF_P_(input C, D, output Q);
parameter DEPTH = 1;
parameter [DEPTH-1:0] INIT = {DEPTH{1'b0}};
reg [DEPTH-1:0] r = INIT;
always @(posedge C)
r <= { r[DEPTH-2:0], D };
assign Q = r[DEPTH-1];
endmodule
module shregmap_variable_test(input i, clk, input [1:0] l1, l2, output [1:0] q);
reg head = 1'b0;
reg [3:0] shift1 = 4'b0000;
reg [3:0] shift2 = 4'b0000;
always @(posedge clk) begin
head <= i;
shift1 <= {shift1[2:0], head};
shift2 <= {shift2[2:0], head};
end
assign q = {shift2[l2], shift1[l1]};
endmodule
module $__XILINX_SHREG_(input C, D, input [1:0] L, output Q);
parameter CLKPOL = 1;
parameter ENPOL = 1;
parameter DEPTH = 1;
parameter [DEPTH-1:0] INIT = {DEPTH{1'b0}};
reg [DEPTH-1:0] r = INIT;
wire clk = C ^ CLKPOL;
always @(posedge C)
r <= { r[DEPTH-2:0], D };
assign Q = r[L];
endmodule

66
tests/various/shregmap.ys Normal file
View file

@ -0,0 +1,66 @@
read_verilog shregmap.v
design -save read
design -copy-to model $__SHREG_DFF_P_
hierarchy -top shregmap_static_test
prep
design -save gold
techmap
shregmap -init
opt
stat
# show -width
select -assert-count 1 t:$_DFF_P_
select -assert-count 2 t:$__SHREG_DFF_P_
design -stash gate
design -import gold -as gold
design -import gate -as gate
design -copy-from model -as $__SHREG_DFF_P_ \$__SHREG_DFF_P_
prep
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -show-ports -seq 5 miter
design -load gold
stat
design -load gate
stat
##########
design -load read
design -copy-to model $__XILINX_SHREG_
hierarchy -top shregmap_variable_test
prep
design -save gold
simplemap t:$dff t:$dffe
shregmap -tech xilinx
stat
# show -width
write_verilog -noexpr -norename
select -assert-count 1 t:$_DFF_P_
select -assert-count 2 t:$__XILINX_SHREG_
design -stash gate
design -import gold -as gold
design -import gate -as gate
design -copy-from model -as $__XILINX_SHREG_ \$__XILINX_SHREG_
prep
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -show-ports -seq 5 miter
design -load gold
stat
design -load gate
stat

33
tests/various/signext.ys Normal file
View file

@ -0,0 +1,33 @@
read_verilog -formal <<EOT
module gate(input clk, output [32:0] o, p, q, r, s, t, u);
assign o = 'bx;
assign p = 1'bx;
assign q = 'bz;
assign r = 1'bz;
assign s = 1'b0;
assign t = 'b1;
assign u = -'sb1;
endmodule
EOT
proc
## Equivalence checking
read_verilog -formal <<EOT
module gold(input clk, output [32:0] o, p, q, r, s, t, u);
assign o = {33{1'bx}};
assign p = {{32{1'b0}}, 1'bx};
assign q = {33{1'bz}};
assign r = {{32{1'b0}}, 1'bz};
assign s = {33{1'b0}};
assign t = {{32{1'b0}}, 1'b1};
assign u = {33{1'b1}};
endmodule
EOT
proc
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -show-ports -enable_undef miter