aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--backends/smt2/smtbmc.py58
-rw-r--r--backends/smt2/smtio.py24
-rw-r--r--frontends/ast/simplify.cc2
-rw-r--r--frontends/verilog/verilog_lexer.l3
-rw-r--r--frontends/verilog/verilog_parser.y2
-rw-r--r--kernel/rtlil.cc1
-rw-r--r--passes/equiv/equiv_simple.cc4
-rw-r--r--passes/fsm/fsm_expand.cc30
-rw-r--r--passes/hierarchy/hierarchy.cc4
-rw-r--r--passes/opt/opt_rmdff.cc26
10 files changed, 127 insertions, 27 deletions
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index ecee6795e..10875f523 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -29,7 +29,9 @@ num_steps = 20
append_steps = 0
vcdfile = None
cexfile = None
-aigprefix = None
+aimfile = None
+aiwfile = None
+aigheader = True
vlogtbfile = None
inconstr = list()
outconstr = None
@@ -73,6 +75,14 @@ yosys-smtbmc [options] <yosys_smt2_output>
and AIGER witness file. The file names are <prefix>.aim for
the map file and <prefix>.aiw for the witness file.
+ --aig <aim_filename>:<aiw_filename>
+ like above, but for map files and witness files that do not
+ share a filename prefix (or use differen file extensions).
+
+ --aig-noheader
+ the AIGER witness file does not include the status and
+ properties lines.
+
--noinfo
only run the core proof, do not collect and print any
additional information (e.g. which assert failed)
@@ -111,7 +121,7 @@ yosys-smtbmc [options] <yosys_smt2_output>
try:
opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igm:", so.longopts +
- ["final-only", "assume-skipped=", "smtc=", "cex=", "aig=",
+ ["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader",
"dump-vcd=", "dump-vlogtb=", "dump-smtc=", "dump-all", "noinfo", "append="])
except:
usage()
@@ -140,7 +150,13 @@ for o, a in opts:
elif o == "--cex":
cexfile = a
elif o == "--aig":
- aigprefix = a
+ if ":" in a:
+ aimfile, aiwfile = a.split(":")
+ else:
+ aimfile = a + ".aim"
+ aiwfile = a + ".aiw"
+ elif o == "--aig-noheader":
+ aigheader = False
elif o == "--dump-vcd":
vcdfile = a
elif o == "--dump-vlogtb":
@@ -375,7 +391,7 @@ if cexfile is not None:
skip_steps = max(skip_steps, step)
num_steps = max(num_steps, step+1)
-if aigprefix is not None:
+if aimfile is not None:
input_map = dict()
init_map = dict()
latch_map = dict()
@@ -385,7 +401,7 @@ if aigprefix is not None:
skip_steps = 0
num_steps = 0
- with open(aigprefix + ".aim", "r") as f:
+ with open(aimfile, "r") as f:
for entry in f.read().splitlines():
entry = entry.split()
@@ -406,11 +422,14 @@ if aigprefix is not None:
assert False
- with open(aigprefix + ".aiw", "r") as f:
+ with open(aiwfile, "r") as f:
got_state = False
got_ffinit = False
step = 0
+ if not aigheader:
+ got_state = True
+
for entry in f.read().splitlines():
if len(entry) == 0 or entry[0] in "bcjfu.":
continue
@@ -458,13 +477,30 @@ if aigprefix is not None:
bitidx = init_map[i][1]
path = smt.get_path(topmod, name)
- width = smt.net_width(topmod, path)
+
+ if not smt.net_exists(topmod, path):
+ match = re.match(r"(.*)\[(\d+)\]$", path[-1])
+ if match:
+ path[-1] = match.group(1)
+ addr = int(match.group(2))
+
+ if not match or not smt.mem_exists(topmod, path):
+ print_msg("Ignoring init value for unknown net: %s" % (name))
+ continue
+
+ meminfo = smt.mem_info(topmod, path)
+ smtexpr = "(select [%s] #b%s)" % (".".join(path), bin(addr)[2:].zfill(meminfo[0]))
+ width = meminfo[1]
+
+ else:
+ smtexpr = "[%s]" % name
+ width = smt.net_width(topmod, path)
if width == 1:
assert bitidx == 0
- smtexpr = "(= [%s] %s)" % (name, "true" if value else "false")
+ smtexpr = "(= %s %s)" % (smtexpr, "true" if value else "false")
else:
- smtexpr = "(= ((_ extract %d %d) [%s]) #b%d)" % (bitidx, bitidx, name, value)
+ smtexpr = "(= ((_ extract %d %d) %s) #b%d)" % (bitidx, bitidx, smtexpr, value)
constr_assumes[0].append((cexfile, smtexpr))
@@ -569,7 +605,7 @@ def write_vlogtb_trace(steps_start, steps_stop, index):
mems = sorted(smt.hiermems(topmod))
for mempath in mems:
- abits, width, ports = smt.mem_info(topmod, "s%d" % steps_start, mempath)
+ abits, width, ports = smt.mem_info(topmod, mempath)
mem = smt.mem_expr(topmod, "s%d" % steps_start, mempath)
addr_expr_list = list()
@@ -630,7 +666,7 @@ def write_constr_trace(steps_start, steps_stop, index):
mems = sorted(smt.hiermems(topmod))
for mempath in mems:
- abits, width, ports = smt.mem_info(topmod, "s%d" % steps_start, mempath)
+ abits, width, ports = smt.mem_info(topmod, mempath)
mem = smt.mem_expr(topmod, "s%d" % steps_start, mempath)
addr_expr_list = list()
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index 497b72db8..3946c3423 100644
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -567,6 +567,26 @@ class SmtIo:
assert net_path[-1] in self.modinfo[mod].wsize
return self.modinfo[mod].wsize[net_path[-1]]
+ def net_exists(self, mod, net_path):
+ for i in range(len(net_path)-1):
+ if mod not in self.modinfo: return False
+ if net_path[i] not in self.modinfo[mod].cells: return False
+ mod = self.modinfo[mod].cells[net_path[i]]
+
+ if mod not in self.modinfo: return False
+ if net_path[-1] not in self.modinfo[mod].wsize: return False
+ return True
+
+ def mem_exists(self, mod, mem_path):
+ for i in range(len(mem_path)-1):
+ if mod not in self.modinfo: return False
+ if mem_path[i] not in self.modinfo[mod].cells: return False
+ mod = self.modinfo[mod].cells[mem_path[i]]
+
+ if mod not in self.modinfo: return False
+ if mem_path[-1] not in self.modinfo[mod].memories: return False
+ return True
+
def mem_expr(self, mod, base, path, portidx=None, infomode=False):
if len(path) == 1:
assert mod in self.modinfo
@@ -582,8 +602,8 @@ class SmtIo:
nextbase = "(|%s_h %s| %s)" % (mod, path[0], base)
return self.mem_expr(nextmod, nextbase, path[1:], portidx=portidx, infomode=infomode)
- def mem_info(self, mod, base, path):
- return self.mem_expr(mod, base, path, infomode=True)
+ def mem_info(self, mod, path):
+ return self.mem_expr(mod, "", path, infomode=True)
def get_net(self, mod_name, net_path, state_name):
return self.get(self.net_expr(mod_name, state_name, net_path))
diff --git a/frontends/ast/simplify.cc b/frontends/ast/simplify.cc
index de85355b5..c1e77c6ec 100644
--- a/frontends/ast/simplify.cc
+++ b/frontends/ast/simplify.cc
@@ -3079,6 +3079,8 @@ bool AstNode::mem2reg_as_needed_pass2(pool<AstNode*> &mem2reg_set, AstNode *mod,
if (bit_part_sel)
children.push_back(bit_part_sel);
+
+ did_something = true;
}
log_assert(id2ast == NULL || mem2reg_set.count(id2ast) == 0);
diff --git a/frontends/verilog/verilog_lexer.l b/frontends/verilog/verilog_lexer.l
index 405aeb975..c22fdf39c 100644
--- a/frontends/verilog/verilog_lexer.l
+++ b/frontends/verilog/verilog_lexer.l
@@ -192,6 +192,9 @@ YOSYS_NAMESPACE_END
"genvar" { return TOK_GENVAR; }
"real" { return TOK_REAL; }
+"enum" { SV_KEYWORD(TOK_ENUM); }
+"typedef" { SV_KEYWORD(TOK_TYPEDEF); }
+
[0-9][0-9_]* {
frontend_verilog_yylval.string = new std::string(yytext);
return TOK_CONST;
diff --git a/frontends/verilog/verilog_parser.y b/frontends/verilog/verilog_parser.y
index 607c48a81..ba47bf2d3 100644
--- a/frontends/verilog/verilog_parser.y
+++ b/frontends/verilog/verilog_parser.y
@@ -114,7 +114,7 @@ static void free_attr(std::map<std::string, AstNode*> *al)
%token TOK_SYNOPSYS_FULL_CASE TOK_SYNOPSYS_PARALLEL_CASE
%token TOK_SUPPLY0 TOK_SUPPLY1 TOK_TO_SIGNED TOK_TO_UNSIGNED
%token TOK_POS_INDEXED TOK_NEG_INDEXED TOK_ASSERT TOK_ASSUME
-%token TOK_RESTRICT TOK_PROPERTY
+%token TOK_RESTRICT TOK_PROPERTY TOK_ENUM TOK_TYPEDEF
%type <ast> range range_or_multirange non_opt_range non_opt_multirange range_or_signed_int
%type <ast> wire_type expr basic_expr concat_list rvalue lvalue lvalue_concat_list
diff --git a/kernel/rtlil.cc b/kernel/rtlil.cc
index 40ad8ca13..365bfd9f8 100644
--- a/kernel/rtlil.cc
+++ b/kernel/rtlil.cc
@@ -2050,6 +2050,7 @@ RTLIL::Memory::Memory()
hashidx_ = hashidx_count;
width = 1;
+ start_offset = 0;
size = 0;
}
diff --git a/passes/equiv/equiv_simple.cc b/passes/equiv/equiv_simple.cc
index 49963ed68..270200c34 100644
--- a/passes/equiv/equiv_simple.cc
+++ b/passes/equiv/equiv_simple.cc
@@ -59,7 +59,7 @@ struct EquivSimpleWorker
for (auto &conn : cell->connections())
if (yosys_celltypes.cell_input(cell->type, conn.first))
for (auto bit : sigmap(conn.second)) {
- if (cell->type.in("$dff", "$_DFF_P_", "$_DFF_N_")) {
+ if (cell->type.in("$dff", "$_DFF_P_", "$_DFF_N_", "$ff", "$_FF_")) {
if (!conn.first.in("\\CLK", "\\C"))
next_seed.insert(bit);
} else
@@ -329,7 +329,7 @@ struct EquivSimplePass : public Pass {
unproven_cells_counter, GetSize(unproven_equiv_cells), log_id(module));
for (auto cell : module->cells()) {
- if (!ct.cell_known(cell->type) && !cell->type.in("$dff", "$_DFF_P_", "$_DFF_N_"))
+ if (!ct.cell_known(cell->type) && !cell->type.in("$dff", "$_DFF_P_", "$_DFF_N_", "$ff", "$_FF_"))
continue;
for (auto &conn : cell->connections())
if (yosys_celltypes.cell_output(cell->type, conn.first))
diff --git a/passes/fsm/fsm_expand.cc b/passes/fsm/fsm_expand.cc
index e7b9dcf90..2c344a1c1 100644
--- a/passes/fsm/fsm_expand.cc
+++ b/passes/fsm/fsm_expand.cc
@@ -54,13 +54,27 @@ struct FsmExpand
if (cell->getPort("\\A").size() < 2)
return true;
+ int in_bits = 0;
RTLIL::SigSpec new_signals;
- if (cell->hasPort("\\A"))
+
+ if (cell->hasPort("\\A")) {
+ in_bits += GetSize(cell->getPort("\\A"));
new_signals.append(assign_map(cell->getPort("\\A")));
- if (cell->hasPort("\\B"))
+ }
+
+ if (cell->hasPort("\\B")) {
+ in_bits += GetSize(cell->getPort("\\B"));
new_signals.append(assign_map(cell->getPort("\\B")));
- if (cell->hasPort("\\S"))
+ }
+
+ if (cell->hasPort("\\S")) {
+ in_bits += GetSize(cell->getPort("\\S"));
new_signals.append(assign_map(cell->getPort("\\S")));
+ }
+
+ if (in_bits > 8)
+ return false;
+
if (cell->hasPort("\\Y"))
new_signals.append(assign_map(cell->getPort("\\Y")));
@@ -173,6 +187,16 @@ struct FsmExpand
new_ctrl_out.append(output_sig);
fsm_cell->setPort("\\CTRL_OUT", new_ctrl_out);
+ if (GetSize(input_sig) > 10)
+ log_warning("Cell %s.%s (%s) has %d input bits, merging into FSM %s.%s might be problematic.\n",
+ log_id(cell->module), log_id(cell), log_id(cell->type),
+ GetSize(input_sig), log_id(fsm_cell->module), log_id(fsm_cell));
+
+ if (GetSize(fsm_data.transition_table) > 10000)
+ log_warning("Transition table for FSM %s.%s already has %d rows, merging more cells "
+ "into this FSM might be problematic.\n", log_id(fsm_cell->module), log_id(fsm_cell),
+ GetSize(fsm_data.transition_table));
+
std::vector<FsmData::transition_t> new_transition_table;
for (auto &tr : fsm_data.transition_table) {
for (int i = 0; i < (1 << input_sig.size()); i++) {
diff --git a/passes/hierarchy/hierarchy.cc b/passes/hierarchy/hierarchy.cc
index 337af7fd7..f1c4a1d3b 100644
--- a/passes/hierarchy/hierarchy.cc
+++ b/passes/hierarchy/hierarchy.cc
@@ -175,16 +175,12 @@ bool expand_module(RTLIL::Design *design, RTLIL::Module *module, bool flag_check
{
filename = dir + "/" + RTLIL::unescape_id(cell->type) + ".v";
if (check_file_exists(filename)) {
- std::vector<std::string> args;
- args.push_back(filename);
Frontend::frontend_call(design, NULL, filename, "verilog");
goto loaded_module;
}
filename = dir + "/" + RTLIL::unescape_id(cell->type) + ".il";
if (check_file_exists(filename)) {
- std::vector<std::string> args;
- args.push_back(filename);
Frontend::frontend_call(design, NULL, filename, "ilang");
goto loaded_module;
}
diff --git a/passes/opt/opt_rmdff.cc b/passes/opt/opt_rmdff.cc
index 922f086f1..00094738c 100644
--- a/passes/opt/opt_rmdff.cc
+++ b/passes/opt/opt_rmdff.cc
@@ -41,9 +41,27 @@ void remove_init_attr(SigSpec sig)
bool handle_dlatch(RTLIL::Module *mod, RTLIL::Cell *dlatch)
{
- SigSpec sig_e = dlatch->getPort("\\EN");
+ SigSpec sig_e;
+ State on_state, off_state;
+
+ if (dlatch->type == "$dlatch") {
+ sig_e = assign_map(dlatch->getPort("\\EN"));
+ on_state = dlatch->getParam("\\EN_POLARITY").as_bool() ? State::S1 : State::S0;
+ off_state = dlatch->getParam("\\EN_POLARITY").as_bool() ? State::S0 : State::S1;
+ } else
+ if (dlatch->type == "$_DLATCH_P_") {
+ sig_e = assign_map(dlatch->getPort("\\E"));
+ on_state = State::S1;
+ off_state = State::S0;
+ } else
+ if (dlatch->type == "$_DLATCH_N_") {
+ sig_e = assign_map(dlatch->getPort("\\E"));
+ on_state = State::S0;
+ off_state = State::S1;
+ } else
+ log_abort();
- if (sig_e == State::S0)
+ if (sig_e == off_state)
{
RTLIL::Const val_init;
for (auto bit : dff_init_map(dlatch->getPort("\\Q")))
@@ -52,7 +70,7 @@ bool handle_dlatch(RTLIL::Module *mod, RTLIL::Cell *dlatch)
goto delete_dlatch;
}
- if (sig_e == State::S1)
+ if (sig_e == on_state)
{
mod->connect(dlatch->getPort("\\Q"), dlatch->getPort("\\D"));
goto delete_dlatch;
@@ -268,7 +286,7 @@ struct OptRmdffPass : public Pass {
"$ff", "$dff", "$adff"))
dff_list.push_back(cell->name);
- if (cell->type == "$dlatch")
+ if (cell->type.in("$dlatch", "$_DLATCH_P_", "$_DLATCH_N_"))
dlatch_list.push_back(cell->name);
}
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-25 06:24:47 +0000