From 3e816e992224612ace7d43171e8c1993b7e8238d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Emil=20Ji=C5=99=C3=AD=20Tywoniak?= Date: Sun, 9 Oct 2022 18:24:43 +0200 Subject: [PATCH 01/80] experimental temporal induction counterexample loop detection --- backends/smt2/smtbmc.py | 44 ++++++++++++++++++++++++++++++++++++++++- 1 file changed, 43 insertions(+), 1 deletion(-) diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index 5f05287de..4997833f4 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -55,6 +55,7 @@ noinit = False binarymode = False keep_going = False check_witness = False +find_loops = False so = SmtOpts() @@ -175,6 +176,9 @@ def usage(): check that the used witness file contains sufficient constraints to force an assertion failure. + --find-loops + check if states are unique in temporal induction counterexamples + """ + so.helpmsg()) sys.exit(1) @@ -183,7 +187,7 @@ try: opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igcm:", so.longopts + ["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "yw=", "btorwit=", "presat", "dump-vcd=", "dump-yw=", "dump-vlogtb=", "vlogtb-top=", "dump-smtc=", "dump-all", "noinfo", "append=", - "smtc-init", "smtc-top=", "noinit", "binary", "keep-going", "check-witness"]) + "smtc-init", "smtc-top=", "noinit", "binary", "keep-going", "check-witness", "find-loops"]) except: usage() @@ -264,6 +268,8 @@ for o, a in opts: keep_going = True elif o == "--check-witness": check_witness = True + elif o == "--find-loops": + find_loops = True elif so.handle(o, a): pass else: @@ -969,6 +975,38 @@ def write_vcd_trace(steps_start, steps_stop, index): vcd.set_time(steps_stop) +def find_state_loop(steps_start, steps_stop): + print_msg(f"Looking for loops") + + path_list = list() + + for netpath in sorted(smt.hiernets(topmod)): + hidden_net = False + for n in netpath: + if n.startswith("$"): + hidden_net = True + if not hidden_net: + path_list.append(netpath) + + mem_trace_data = collect_mem_trace_data(steps_start, steps_stop) + + states = dict() + path_tupled_list = [tuple(p) for p in path_list] + for i in range(steps_start, steps_stop): + value_list = smt.get_net_bin_list(topmod, path_list, "s%d" % i) + state = tuple(zip(path_tupled_list, value_list)) + if states.get(state): + return (i, states[state]) + else: + states[state] = i + + if i in mem_trace_data: + if mem_trace_data[i]: + print_msg(f"This design contains memory. Searching for counterexample loops will be skipped") + return None + + return None + def char_ok_in_verilog(c,i): if ('A' <= c <= 'Z'): return True if ('a' <= c <= 'z'): return True @@ -1596,6 +1634,10 @@ if tempind: print_anyconsts(num_steps) print_failed_asserts(num_steps) write_trace(step, num_steps+1, '%', allregs=True) + if find_loops: + loop = find_state_loop(step, num_steps+1) + if loop: + print_msg(f"Loop detected, increasing induction depth will not help. Cycle {loop[0]} = cycle {loop[1]}") elif dumpall: print_anyconsts(num_steps) From 0dbebea939ec52dfa2a0d522adfede123405a81c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Emil=20Ji=C5=99=C3=AD=20Tywoniak?= Date: Tue, 11 Oct 2022 19:48:16 +0200 Subject: [PATCH 02/80] include memory in state --- backends/smt2/smtbmc.py | 48 ++++++++++++++++++----------------------- 1 file changed, 21 insertions(+), 27 deletions(-) diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index 4997833f4..fd54622f2 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -55,7 +55,7 @@ noinit = False binarymode = False keep_going = False check_witness = False -find_loops = False +detect_loops = False so = SmtOpts() @@ -176,8 +176,9 @@ def usage(): check that the used witness file contains sufficient constraints to force an assertion failure. - --find-loops - check if states are unique in temporal induction counterexamples + --detect-loops + check if states are unique in temporal induction counter examples + (this feature is experimental and incomplete) """ + so.helpmsg()) sys.exit(1) @@ -187,7 +188,7 @@ try: opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igcm:", so.longopts + ["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "yw=", "btorwit=", "presat", "dump-vcd=", "dump-yw=", "dump-vlogtb=", "vlogtb-top=", "dump-smtc=", "dump-all", "noinfo", "append=", - "smtc-init", "smtc-top=", "noinit", "binary", "keep-going", "check-witness", "find-loops"]) + "smtc-init", "smtc-top=", "noinit", "binary", "keep-going", "check-witness", "detect-loops"]) except: usage() @@ -268,8 +269,8 @@ for o, a in opts: keep_going = True elif o == "--check-witness": check_witness = True - elif o == "--find-loops": - find_loops = True + elif o == "--detect-loops": + detect_loops = True elif so.handle(o, a): pass else: @@ -975,36 +976,29 @@ def write_vcd_trace(steps_start, steps_stop, index): vcd.set_time(steps_stop) -def find_state_loop(steps_start, steps_stop): - print_msg(f"Looking for loops") +def detect_state_loop(steps_start, steps_stop): + print_msg(f"Checking for loops in found induction counter example") + print_msg(f"This feature is experimental and incomplete") - path_list = list() - - for netpath in sorted(smt.hiernets(topmod)): - hidden_net = False - for n in netpath: - if n.startswith("$"): - hidden_net = True - if not hidden_net: - path_list.append(netpath) + path_list = sorted(smt.hiernets(topmod, regs_only=True)) mem_trace_data = collect_mem_trace_data(steps_start, steps_stop) + # Map state to index of step when it occurred states = dict() - path_tupled_list = [tuple(p) for p in path_list] + for i in range(steps_start, steps_stop): value_list = smt.get_net_bin_list(topmod, path_list, "s%d" % i) - state = tuple(zip(path_tupled_list, value_list)) + mem_state = sorted( + [(tuple(path), addr, data) + for path, addr, data in mem_trace_data.get(i, [])] + ) + state = tuple(value_list), tuple(mem_state) if states.get(state): return (i, states[state]) else: states[state] = i - if i in mem_trace_data: - if mem_trace_data[i]: - print_msg(f"This design contains memory. Searching for counterexample loops will be skipped") - return None - return None def char_ok_in_verilog(c,i): @@ -1634,10 +1628,10 @@ if tempind: print_anyconsts(num_steps) print_failed_asserts(num_steps) write_trace(step, num_steps+1, '%', allregs=True) - if find_loops: - loop = find_state_loop(step, num_steps+1) + if detect_loops: + loop = detect_state_loop(step, num_steps+1) if loop: - print_msg(f"Loop detected, increasing induction depth will not help. Cycle {loop[0]} = cycle {loop[1]}") + print_msg(f"Loop detected, increasing induction depth will not help. Step {loop[0]} = step {loop[1]}") elif dumpall: print_anyconsts(num_steps) From 8d4000a9b75dd636e9609b9e6a05d7ae3d7a9dee Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Emil=20Ji=C5=99=C3=AD=20Tywoniak?= Date: Tue, 11 Oct 2022 19:52:44 +0200 Subject: [PATCH 03/80] include memory in state --- backends/smt2/smtbmc.py | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index fd54622f2..c25f529b9 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -991,8 +991,7 @@ def detect_state_loop(steps_start, steps_stop): value_list = smt.get_net_bin_list(topmod, path_list, "s%d" % i) mem_state = sorted( [(tuple(path), addr, data) - for path, addr, data in mem_trace_data.get(i, [])] - ) + for path, addr, data in mem_trace_data.get(i, [])]) state = tuple(value_list), tuple(mem_state) if states.get(state): return (i, states[state]) From 083ca6ab066d01aa33156860bb4e29efe547f834 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Emil=20Ji=C5=99=C3=AD=20Tywoniak?= Date: Tue, 18 Oct 2022 22:58:54 +0200 Subject: [PATCH 04/80] bugfix --- backends/smt2/smtbmc.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index c25f529b9..cc108d52b 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -993,7 +993,7 @@ def detect_state_loop(steps_start, steps_stop): [(tuple(path), addr, data) for path, addr, data in mem_trace_data.get(i, [])]) state = tuple(value_list), tuple(mem_state) - if states.get(state): + if state in states: return (i, states[state]) else: states[state] = i From 2ba435b6bc0a5f0f831c331abdf8d58e0fdae132 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Emil=20Ji=C5=99=C3=AD=20Tywoniak?= Date: Thu, 20 Oct 2022 19:31:16 +0200 Subject: [PATCH 05/80] bugfix for mathsat counterexample vcd dump --- backends/smt2/smtio.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 9af454cca..5cd1a74fb 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -917,7 +917,7 @@ class SmtIo: if len(expr_list) == 0: return [] self.write("(get-value (%s))" % " ".join(expr_list)) - return [n[1] for n in self.parse(self.read())] + return [n[1] for n in self.parse(self.read()) if n] def get_path(self, mod, path): assert mod in self.modinfo From d0e559a34f8be18af195c8eb15324baf28d9c2a5 Mon Sep 17 00:00:00 2001 From: "N. Engelhardt" Date: Mon, 2 Oct 2023 16:06:26 +0200 Subject: [PATCH 06/80] celledges: support shift ops --- kernel/celledges.cc | 46 ++++++++++++++++++++++++++++++++++++++------- 1 file changed, 39 insertions(+), 7 deletions(-) diff --git a/kernel/celledges.cc b/kernel/celledges.cc index c43ba8db3..0288b62e2 100644 --- a/kernel/celledges.cc +++ b/kernel/celledges.cc @@ -172,6 +172,30 @@ void demux_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell) } } +void shift_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell) +{ + int width = GetSize(cell->getPort(ID::A)); + int b_width = GetSize(cell->getPort(ID::B)); + + for (int i = 0; i < width; i++){ + for (int k = 0; k < b_width; k++) + db->add_edge(cell, ID::B, k, ID::Y, i, -1); + + if (cell->type.in(ID($shl), ID($sshl))) { + for (int k = i; k >= 0; k--) + db->add_edge(cell, ID::A, k, ID::Y, i, -1); + } + + if (cell->type.in(ID($shr), ID($sshr))) + for (int k = i; k < width; k++) + db->add_edge(cell, ID::A, k, ID::Y, i, -1); + + if (cell->type.in(ID($shift), ID($shiftx))) + for (int k = 0; k < width; k++) + db->add_edge(cell, ID::A, k, ID::Y, i, -1); + } +} + PRIVATE_NAMESPACE_END bool YOSYS_NAMESPACE_PREFIX AbstractCellEdgesDatabase::add_edges_from_cell(RTLIL::Cell *cell) @@ -201,11 +225,10 @@ bool YOSYS_NAMESPACE_PREFIX AbstractCellEdgesDatabase::add_edges_from_cell(RTLIL return true; } - // FIXME: - // if (cell->type.in(ID($shl), ID($shr), ID($sshl), ID($sshr), ID($shift), ID($shiftx))) { - // shift_op(this, cell); - // return true; - // } + if (cell->type.in(ID($shl), ID($shr), ID($sshl), ID($sshr), ID($shift), ID($shiftx))) { + shift_op(this, cell); + return true; + } if (cell->type.in(ID($lt), ID($le), ID($eq), ID($ne), ID($eqx), ID($nex), ID($ge), ID($gt))) { compare_op(this, cell); @@ -227,8 +250,17 @@ bool YOSYS_NAMESPACE_PREFIX AbstractCellEdgesDatabase::add_edges_from_cell(RTLIL return true; } - // FIXME: $mul $div $mod $divfloor $modfloor $slice $concat - // FIXME: $lut $sop $alu $lcu $macc $fa + // FIXME: $mul $div $mod $divfloor $modfloor $pow $slice $concat $bweqx + // FIXME: $lut $sop $alu $lcu $macc $fa $logic_and $logic_or $bwmux + + // FIXME: $_BUF_ $_NOT_ $_AND_ $_NAND_ $_OR_ $_NOR_ $_XOR_ $_XNOR_ $_ANDNOT_ $_ORNOT_ + // FIXME: $_MUX_ $_NMUX_ $_MUX4_ $_MUX8_ $_MUX16_ $_AOI3_ $_OAI3_ $_AOI4_ $_OAI4_ + + // FIXME: $specify2 $specify3 $specrule ??? + // FIXME: $equiv $set_tag $get_tag $overwrite_tag $original_tag + + if (cell->type.in(ID($assert), ID($assume), ID($live), ID($fair), ID($cover), ID($initstate), ID($anyconst), ID($anyseq), ID($allconst), ID($allseq))) + return true; // no-op: these have either no inputs or no outputs return false; } From 2d6d6a8da1dd89a606bff4099e7b84404deb6e07 Mon Sep 17 00:00:00 2001 From: "N. Engelhardt" Date: Mon, 2 Oct 2023 17:29:09 +0200 Subject: [PATCH 07/80] fix handling a_width != y_width --- kernel/celledges.cc | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/kernel/celledges.cc b/kernel/celledges.cc index 0288b62e2..fc381f35c 100644 --- a/kernel/celledges.cc +++ b/kernel/celledges.cc @@ -174,24 +174,25 @@ void demux_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell) void shift_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell) { - int width = GetSize(cell->getPort(ID::A)); + int a_width = GetSize(cell->getPort(ID::A)); int b_width = GetSize(cell->getPort(ID::B)); + int y_width = GetSize(cell->getPort(ID::Y)); - for (int i = 0; i < width; i++){ + for (int i = 0; i < y_width; i++){ for (int k = 0; k < b_width; k++) db->add_edge(cell, ID::B, k, ID::Y, i, -1); if (cell->type.in(ID($shl), ID($sshl))) { - for (int k = i; k >= 0; k--) + for (int k = min(i, a_width); k >= 0; k--) db->add_edge(cell, ID::A, k, ID::Y, i, -1); } if (cell->type.in(ID($shr), ID($sshr))) - for (int k = i; k < width; k++) + for (int k = i; k < a_width; k++) db->add_edge(cell, ID::A, k, ID::Y, i, -1); if (cell->type.in(ID($shift), ID($shiftx))) - for (int k = 0; k < width; k++) + for (int k = 0; k < a_width; k++) db->add_edge(cell, ID::A, k, ID::Y, i, -1); } } From 6c562c76bc36ea51af25c26abffe7f92ceae77bd Mon Sep 17 00:00:00 2001 From: "N. Engelhardt" Date: Mon, 2 Oct 2023 18:32:53 +0200 Subject: [PATCH 08/80] fix handling right shifts --- kernel/celledges.cc | 61 +++++++++++++++++++++++++++++++++++++-------- passes/sat/eval.cc | 4 +-- 2 files changed, 53 insertions(+), 12 deletions(-) diff --git a/kernel/celledges.cc b/kernel/celledges.cc index fc381f35c..1e5a68db3 100644 --- a/kernel/celledges.cc +++ b/kernel/celledges.cc @@ -174,26 +174,67 @@ void demux_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell) void shift_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell) { + bool is_signed = cell->getParam(ID::A_SIGNED).as_bool(); int a_width = GetSize(cell->getPort(ID::A)); int b_width = GetSize(cell->getPort(ID::B)); int y_width = GetSize(cell->getPort(ID::Y)); - for (int i = 0; i < y_width; i++){ - for (int k = 0; k < b_width; k++) - db->add_edge(cell, ID::B, k, ID::Y, i, -1); + // how far the maximum value of B is able to shift + int b_range = (1<type.in(ID($shl), ID($sshl))) { - for (int k = min(i, a_width); k >= 0; k--) - db->add_edge(cell, ID::A, k, ID::Y, i, -1); + // << and <<< + b_range_upper = a_width + b_range; + if (is_signed) b_range_upper -= 1; + a_range_lower = max(0, i - b_range); + a_range_upper = min(i+1, a_width); + } else if (cell->type.in(ID($shr), ID($sshr))){ + // >> and >>> + b_range_upper = a_width; + a_range_lower = min(i, a_width - 1); // technically the min is unneccessary as b_range_upper check already skips any i >= a_width, but let's leave the logic in since this is hard enough + a_range_upper = min(i+1 + b_range, a_width); + } else if (cell->type.in(ID($shift), ID($shiftx))) { + // can go both ways depending on sign of B + // 2's complement range is different depending on direction + int b_range_left = (1<<(b_width - 1)); + int b_range_right = (1<<(b_width - 1)) - 1; + b_range_upper = a_width + b_range_left; + a_range_lower = max(0, i - b_range_left); + a_range_upper = min(i+1 + b_range_right, a_width); } - if (cell->type.in(ID($shr), ID($sshr))) - for (int k = i; k < a_width; k++) + if (i < b_range_upper) { + for (int k = a_range_lower; k < a_range_upper; k++) db->add_edge(cell, ID::A, k, ID::Y, i, -1); + } else { + // the only possible influence value is sign extension + if (is_signed) + db->add_edge(cell, ID::A, a_width - 1, ID::Y, i, -1); + } + + for (int k = 0; k < b_width; k++) { + if (cell->type.in(ID($shl), ID($sshl)) && a_width == 1 && is_signed) { + int skip = (1<<(k+1)); + int base = skip -1; + if (i % skip != base) + db->add_edge(cell, ID::B, k, ID::Y, i, -1); + } else if (cell->type.in(ID($shr), ID($sshr)) && is_signed) { + int skip = (1<<(k+1)); + int base = 0; + if (i % skip != base || i < a_width - 1) + db->add_edge(cell, ID::B, k, ID::Y, i, -1); + } else { + db->add_edge(cell, ID::B, k, ID::Y, i, -1); + } + } - if (cell->type.in(ID($shift), ID($shiftx))) - for (int k = 0; k < a_width; k++) - db->add_edge(cell, ID::A, k, ID::Y, i, -1); } } diff --git a/passes/sat/eval.cc b/passes/sat/eval.cc index 05879426e..acebea6c5 100644 --- a/passes/sat/eval.cc +++ b/passes/sat/eval.cc @@ -543,13 +543,13 @@ struct EvalPass : public Pass { int pos = 0; for (auto &c : tabsigs.chunks()) { - tab_line.push_back(log_signal(RTLIL::SigSpec(tabvals).extract(pos, c.width))); + tab_line.push_back(log_signal(RTLIL::SigSpec(tabvals).extract(pos, c.width), false)); pos += c.width; } pos = 0; for (auto &c : signal.chunks()) { - tab_line.push_back(log_signal(value.extract(pos, c.width))); + tab_line.push_back(log_signal(value.extract(pos, c.width), false)); pos += c.width; } From bdd74e61aed2297cdd3af76da8f43432e6a0afa7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Povi=C5=A1er?= Date: Mon, 16 Oct 2023 13:29:47 +0200 Subject: [PATCH 09/80] celledges: Account for shift down of x-bits wrt B port --- kernel/celledges.cc | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/kernel/celledges.cc b/kernel/celledges.cc index 1e5a68db3..c6615968f 100644 --- a/kernel/celledges.cc +++ b/kernel/celledges.cc @@ -226,12 +226,16 @@ void shift_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell) if (i % skip != base) db->add_edge(cell, ID::B, k, ID::Y, i, -1); } else if (cell->type.in(ID($shr), ID($sshr)) && is_signed) { - int skip = (1<<(k+1)); - int base = 0; - if (i % skip != base || i < a_width - 1) + bool shift_in_bulk = i < a_width - 1; + // can we jump into the ambient x-bits by toggling B[k]? + bool x_jump = (((y_width - i) & ((1 << (k + 1)) - 1)) != 0 \ + && (((y_width - i) & ~(1 << k)) < (1 << b_width))); + + if (shift_in_bulk || (cell->type == ID($shr) && x_jump)) db->add_edge(cell, ID::B, k, ID::Y, i, -1); } else { - db->add_edge(cell, ID::B, k, ID::Y, i, -1); + if (i < a_width) + db->add_edge(cell, ID::B, k, ID::Y, i, -1); } } From 4cce4916397bcc6ce9e44692f1b31f4edc9369be Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Povi=C5=A1er?= Date: Sun, 10 Dec 2023 00:27:42 +0100 Subject: [PATCH 10/80] celledges: s/x_jump/zpad_jump/ --- kernel/celledges.cc | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/kernel/celledges.cc b/kernel/celledges.cc index c6615968f..2d8177d31 100644 --- a/kernel/celledges.cc +++ b/kernel/celledges.cc @@ -227,11 +227,11 @@ void shift_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell) db->add_edge(cell, ID::B, k, ID::Y, i, -1); } else if (cell->type.in(ID($shr), ID($sshr)) && is_signed) { bool shift_in_bulk = i < a_width - 1; - // can we jump into the ambient x-bits by toggling B[k]? - bool x_jump = (((y_width - i) & ((1 << (k + 1)) - 1)) != 0 \ + // can we jump into the zero-padding by toggling B[k]? + bool zpad_jump = (((y_width - i) & ((1 << (k + 1)) - 1)) != 0 \ && (((y_width - i) & ~(1 << k)) < (1 << b_width))); - if (shift_in_bulk || (cell->type == ID($shr) && x_jump)) + if (shift_in_bulk || (cell->type == ID($shr) && zpad_jump)) db->add_edge(cell, ID::B, k, ID::Y, i, -1); } else { if (i < a_width) From a96c257b3f4860534d7db2b1611c352eceb86161 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Povi=C5=A1er?= Date: Mon, 11 Dec 2023 21:36:00 +0100 Subject: [PATCH 11/80] celledges: Add messy rules that do pass the tests This passes `test_cell -edges` on all the types of shift cells. --- kernel/celledges.cc | 55 +++++++++++++++++++++++++++++++++++++++------ 1 file changed, 48 insertions(+), 7 deletions(-) diff --git a/kernel/celledges.cc b/kernel/celledges.cc index 2d8177d31..a78c1ab83 100644 --- a/kernel/celledges.cc +++ b/kernel/celledges.cc @@ -175,9 +175,16 @@ void demux_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell) void shift_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell) { bool is_signed = cell->getParam(ID::A_SIGNED).as_bool(); + bool is_b_signed = cell->getParam(ID::B_SIGNED).as_bool(); int a_width = GetSize(cell->getPort(ID::A)); int b_width = GetSize(cell->getPort(ID::B)); int y_width = GetSize(cell->getPort(ID::Y)); + int effective_a_width = a_width; + + if (cell->type.in(ID($shift), ID($shiftx)) && is_signed) { + effective_a_width = std::max(y_width, a_width); + //is_signed = false; + } // how far the maximum value of B is able to shift int b_range = (1<type.in(ID($shr), ID($sshr))){ + } else if (cell->type.in(ID($shr), ID($sshr)) || (cell->type.in(ID($shift), ID($shiftx)) && !is_b_signed)){ // >> and >>> b_range_upper = a_width; a_range_lower = min(i, a_width - 1); // technically the min is unneccessary as b_range_upper check already skips any i >= a_width, but let's leave the logic in since this is hard enough a_range_upper = min(i+1 + b_range, a_width); - } else if (cell->type.in(ID($shift), ID($shiftx))) { + } else if (cell->type.in(ID($shift), ID($shiftx)) && is_b_signed) { // can go both ways depending on sign of B // 2's complement range is different depending on direction int b_range_left = (1<<(b_width - 1)); int b_range_right = (1<<(b_width - 1)) - 1; - b_range_upper = a_width + b_range_left; + b_range_upper = effective_a_width + b_range_left; a_range_lower = max(0, i - b_range_left); + if (is_signed) + a_range_lower = min(a_range_lower, a_width - 1); a_range_upper = min(i+1 + b_range_right, a_width); } @@ -223,18 +232,50 @@ void shift_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell) if (cell->type.in(ID($shl), ID($sshl)) && a_width == 1 && is_signed) { int skip = (1<<(k+1)); int base = skip -1; - if (i % skip != base) + if (i % skip != base && i - a_width + 2 < 1 << b_width) db->add_edge(cell, ID::B, k, ID::Y, i, -1); - } else if (cell->type.in(ID($shr), ID($sshr)) && is_signed) { + } else if (true && cell->type.in(ID($shift), ID($shiftx)) && a_width == 1 && is_signed && is_b_signed) { + if (k != b_width - 1) { + // can we jump into the zero-padding by toggling B[k]? + bool zpad_jump = (((y_width - i) & ((1 << (k + 1)) - 1)) != 0 \ + && (((y_width - i) & ~(1 << k)) < (1 << (b_width - 1)))); + if (((~(i - 1) & ((1 << (k + 1)) - 1)) != 0 && i < 1 << (b_width - 1)) || zpad_jump) + db->add_edge(cell, ID::B, k, ID::Y, i, -1); + } else { + if ((y_width - 1 - i < (1 << (b_width - 1)) - 1) || (i < (1 << (b_width - 1)))) + db->add_edge(cell, ID::B, k, ID::Y, i, -1); + } + } else if ((cell->type.in(ID($shr), ID($sshr)) || (cell->type.in(ID($shift), ID($shiftx)) && !is_b_signed)) && is_signed) { bool shift_in_bulk = i < a_width - 1; // can we jump into the zero-padding by toggling B[k]? bool zpad_jump = (((y_width - i) & ((1 << (k + 1)) - 1)) != 0 \ && (((y_width - i) & ~(1 << k)) < (1 << b_width))); - if (shift_in_bulk || (cell->type == ID($shr) && zpad_jump)) + if (shift_in_bulk || (cell->type.in(ID($shr), ID($shift), ID($shiftx)) && zpad_jump)) db->add_edge(cell, ID::B, k, ID::Y, i, -1); + } else if (cell->type.in(ID($sshl), ID($shl)) && is_signed) { + if (i - a_width + 2 < 1 << b_width) + db->add_edge(cell, ID::B, k, ID::Y, i, -1); + } else if (cell->type.in(ID($shl), ID($sshl))) { + if (i - a_width + 1 < 1 << b_width) + db->add_edge(cell, ID::B, k, ID::Y, i, -1); + } else if (cell->type.in(ID($shift), ID($shiftx)) && is_b_signed && !is_signed) { + if (i - a_width < (1 << (b_width - 1))) + db->add_edge(cell, ID::B, k, ID::Y, i, -1); + } else if (cell->type.in(ID($shift), ID($shiftx)) && is_b_signed && is_signed) { + if (k != b_width - 1) { + bool r_shift_in_bulk = i < a_width - 1; + // can we jump into the zero-padding by toggling B[k]? + bool r_zpad_jump = (((y_width - i) & ((1 << (k + 1)) - 1)) != 0 \ + && (((y_width - i) & ~(1 << k)) < (1 << (b_width - 1)))); + if (r_shift_in_bulk || r_zpad_jump || i - a_width + 2 <= 1 << (b_width - 1)) + db->add_edge(cell, ID::B, k, ID::Y, i, -1); + } else { + if ((i - a_width + 2) <= (1 << (b_width - 1)) || (y_width - i) < (1 << (b_width - 1))) + db->add_edge(cell, ID::B, k, ID::Y, i, -1); + } } else { - if (i < a_width) + if (i < effective_a_width) db->add_edge(cell, ID::B, k, ID::Y, i, -1); } } From 134eb15c7e25816aba6570ed78b21398c539c395 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Povi=C5=A1er?= Date: Fri, 19 Jan 2024 11:08:31 +0100 Subject: [PATCH 12/80] celledges: Clean up shift rules --- kernel/celledges.cc | 154 +++++++++++++++++++++++++------------------- 1 file changed, 89 insertions(+), 65 deletions(-) diff --git a/kernel/celledges.cc b/kernel/celledges.cc index a78c1ab83..2ed0d5036 100644 --- a/kernel/celledges.cc +++ b/kernel/celledges.cc @@ -179,107 +179,131 @@ void shift_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell) int a_width = GetSize(cell->getPort(ID::A)); int b_width = GetSize(cell->getPort(ID::B)); int y_width = GetSize(cell->getPort(ID::Y)); - int effective_a_width = a_width; - if (cell->type.in(ID($shift), ID($shiftx)) && is_signed) { - effective_a_width = std::max(y_width, a_width); - //is_signed = false; + // Behavior of the different shift cells: + // + // $shl, $sshl -- shifts left by the amount on B port, B always unsigned + // $shr, $sshr -- ditto right + // $shift, $shiftx -- shifts right by the amount on B port, B optionally signed + // + // Sign extension (if A signed): + // + // $shl, $shr, $shift -- only sign-extends up to size of Y, then shifts in zeroes + // $sshl, $sshr -- fully sign-extends + // $shiftx -- no sign extension + // + // Because $shl, $sshl only shift left, and $shl sign-extens up to size of Y, they + // are effectively the same. + + // the cap below makes sure we don't overflow in the arithmetic further down, though + // it makes the edge data invalid once a_width approaches the order of 2**30 + // (that ever happening is considered improbable) + int b_width_capped = min(b_width, 30); + + int b_high, b_low; + if (!is_b_signed) { + b_high = (1 << b_width_capped) - 1; + b_low = 0; + } else { + b_high = (1 << (b_width_capped - 1)) - 1; + b_low = -(1 << (b_width_capped - 1)); } - // how far the maximum value of B is able to shift - int b_range = (1<type.in(ID($shl), ID($sshl))) { - // << and <<< - b_range_upper = a_width + b_range; + b_range_upper = a_width + b_high; if (is_signed) b_range_upper -= 1; - a_range_lower = max(0, i - b_range); + a_range_lower = max(0, i - b_high); a_range_upper = min(i+1, a_width); - } else if (cell->type.in(ID($shr), ID($sshr)) || (cell->type.in(ID($shift), ID($shiftx)) && !is_b_signed)){ - // >> and >>> + } else if (cell->type.in(ID($shr), ID($sshr)) || (cell->type.in(ID($shift), ID($shiftx)) && !is_b_signed)) { b_range_upper = a_width; - a_range_lower = min(i, a_width - 1); // technically the min is unneccessary as b_range_upper check already skips any i >= a_width, but let's leave the logic in since this is hard enough - a_range_upper = min(i+1 + b_range, a_width); + a_range_lower = min(i, a_width - 1); + a_range_upper = min(i+1 + b_high, a_width); } else if (cell->type.in(ID($shift), ID($shiftx)) && is_b_signed) { // can go both ways depending on sign of B // 2's complement range is different depending on direction - int b_range_left = (1<<(b_width - 1)); - int b_range_right = (1<<(b_width - 1)) - 1; - b_range_upper = effective_a_width + b_range_left; - a_range_lower = max(0, i - b_range_left); + b_range_upper = a_width - b_low; + a_range_lower = max(0, i + b_low); if (is_signed) a_range_lower = min(a_range_lower, a_width - 1); - a_range_upper = min(i+1 + b_range_right, a_width); + a_range_upper = min(i+1 + b_high, a_width); + } else { + log_assert(false && "unreachable"); } if (i < b_range_upper) { for (int k = a_range_lower; k < a_range_upper; k++) db->add_edge(cell, ID::A, k, ID::Y, i, -1); } else { - // the only possible influence value is sign extension + // only influence is through sign extension if (is_signed) db->add_edge(cell, ID::A, a_width - 1, ID::Y, i, -1); } for (int k = 0; k < b_width; k++) { - if (cell->type.in(ID($shl), ID($sshl)) && a_width == 1 && is_signed) { - int skip = (1<<(k+1)); - int base = skip -1; - if (i % skip != base && i - a_width + 2 < 1 << b_width) - db->add_edge(cell, ID::B, k, ID::Y, i, -1); - } else if (true && cell->type.in(ID($shift), ID($shiftx)) && a_width == 1 && is_signed && is_b_signed) { - if (k != b_width - 1) { - // can we jump into the zero-padding by toggling B[k]? - bool zpad_jump = (((y_width - i) & ((1 << (k + 1)) - 1)) != 0 \ - && (((y_width - i) & ~(1 << k)) < (1 << (b_width - 1)))); - if (((~(i - 1) & ((1 << (k + 1)) - 1)) != 0 && i < 1 << (b_width - 1)) || zpad_jump) + // left shifts + if (cell->type.in(ID($shl), ID($sshl))) { + if (a_width == 1 && is_signed) { + int skip = 1 << (k + 1); + int base = skip -1; + if (i % skip != base && i - a_width + 2 < 1 << b_width) + db->add_edge(cell, ID::B, k, ID::Y, i, -1); + } else if (is_signed) { + if (i - a_width + 2 < 1 << b_width) db->add_edge(cell, ID::B, k, ID::Y, i, -1); } else { - if ((y_width - 1 - i < (1 << (b_width - 1)) - 1) || (i < (1 << (b_width - 1)))) + if (i - a_width + 1 < 1 << b_width) db->add_edge(cell, ID::B, k, ID::Y, i, -1); } - } else if ((cell->type.in(ID($shr), ID($sshr)) || (cell->type.in(ID($shift), ID($shiftx)) && !is_b_signed)) && is_signed) { - bool shift_in_bulk = i < a_width - 1; - // can we jump into the zero-padding by toggling B[k]? - bool zpad_jump = (((y_width - i) & ((1 << (k + 1)) - 1)) != 0 \ - && (((y_width - i) & ~(1 << k)) < (1 << b_width))); - - if (shift_in_bulk || (cell->type.in(ID($shr), ID($shift), ID($shiftx)) && zpad_jump)) - db->add_edge(cell, ID::B, k, ID::Y, i, -1); - } else if (cell->type.in(ID($sshl), ID($shl)) && is_signed) { - if (i - a_width + 2 < 1 << b_width) - db->add_edge(cell, ID::B, k, ID::Y, i, -1); - } else if (cell->type.in(ID($shl), ID($sshl))) { - if (i - a_width + 1 < 1 << b_width) - db->add_edge(cell, ID::B, k, ID::Y, i, -1); - } else if (cell->type.in(ID($shift), ID($shiftx)) && is_b_signed && !is_signed) { - if (i - a_width < (1 << (b_width - 1))) - db->add_edge(cell, ID::B, k, ID::Y, i, -1); - } else if (cell->type.in(ID($shift), ID($shiftx)) && is_b_signed && is_signed) { - if (k != b_width - 1) { - bool r_shift_in_bulk = i < a_width - 1; + // right shifts + } else if (cell->type.in(ID($shr), ID($sshr)) || (cell->type.in(ID($shift), ID($shiftx)) && !is_b_signed)) { + if (is_signed) { + bool shift_in_bulk = i < a_width - 1; // can we jump into the zero-padding by toggling B[k]? - bool r_zpad_jump = (((y_width - i) & ((1 << (k + 1)) - 1)) != 0 \ - && (((y_width - i) & ~(1 << k)) < (1 << (b_width - 1)))); - if (r_shift_in_bulk || r_zpad_jump || i - a_width + 2 <= 1 << (b_width - 1)) + bool zpad_jump = (((y_width - i) & ((1 << (k + 1)) - 1)) != 0 \ + && (((y_width - i) & ~(1 << k)) < (1 << b_width))); + + if (shift_in_bulk || (cell->type.in(ID($shr), ID($shift), ID($shiftx)) && zpad_jump)) db->add_edge(cell, ID::B, k, ID::Y, i, -1); } else { - if ((i - a_width + 2) <= (1 << (b_width - 1)) || (y_width - i) < (1 << (b_width - 1))) + if (i < a_width) + db->add_edge(cell, ID::B, k, ID::Y, i, -1); + } + // bidirectional shifts (positive B shifts right, negative left) + } else if (cell->type.in(ID($shift), ID($shiftx)) && is_b_signed) { + if (is_signed) { + if (k != b_width - 1) { + bool r_shift_in_bulk = i < a_width - 1; + // assuming B is positive, can we jump into the upper zero-padding by toggling B[k]? + bool r_zpad_jump = (((y_width - i) & ((1 << (k + 1)) - 1)) != 0 \ + && (((y_width - i) & ~(1 << k)) <= b_high)); + // assuming B is negative, can we influence Y[i] by toggling B[k]? + bool l = a_width - 2 - i >= b_low; + if (a_width == 1) { + // in case of a_width==1 we go into more detailed reasoning + l = l && (~(i - a_width) & ((1 << (k + 1)) - 1)) != 0; + } + if (r_shift_in_bulk || r_zpad_jump || l) + db->add_edge(cell, ID::B, k, ID::Y, i, -1); + } else { + if (y_width - i <= b_high || a_width - 2 - i >= b_low) + db->add_edge(cell, ID::B, k, ID::Y, i, -1); + } + } else { + if (a_width - 1 - i >= b_low) db->add_edge(cell, ID::B, k, ID::Y, i, -1); } } else { - if (i < effective_a_width) - db->add_edge(cell, ID::B, k, ID::Y, i, -1); + log_assert(false && "unreachable"); } } - } } From cb86efa50c69fd8c949c44d50dfbb81056459faa Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Povi=C5=A1er?= Date: Fri, 19 Jan 2024 11:14:10 +0100 Subject: [PATCH 13/80] celledges: Add test of shift cells edge data --- tests/various/celledges_shift.ys | 1 + 1 file changed, 1 insertion(+) create mode 100644 tests/various/celledges_shift.ys diff --git a/tests/various/celledges_shift.ys b/tests/various/celledges_shift.ys new file mode 100644 index 000000000..753c8641e --- /dev/null +++ b/tests/various/celledges_shift.ys @@ -0,0 +1 @@ +test_cell -s 1705659041 -n 100 -edges $shift $shiftx $shl $shr $sshl $sshr From a84fa0a27727490884a8795eaee8f82335b5e2be Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Povi=C5=A1er?= Date: Thu, 1 Feb 2024 10:28:36 +0100 Subject: [PATCH 14/80] connect: Do interpret selection arguments Instead of silently ignoring what would ordinarily be the selection arguments to a pass, interpret those and mark the support in the help message. --- passes/cmds/connect.cc | 29 +++++++++++++++-------------- 1 file changed, 15 insertions(+), 14 deletions(-) diff --git a/passes/cmds/connect.cc b/passes/cmds/connect.cc index 1bd52aab2..65292ef92 100644 --- a/passes/cmds/connect.cc +++ b/passes/cmds/connect.cc @@ -47,7 +47,7 @@ struct ConnectPass : public Pass { { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| log("\n"); - log(" connect [-nomap] [-nounset] -set \n"); + log(" connect [-nomap] [-nounset] -set [selection]\n"); log("\n"); log("Create a connection. This is equivalent to adding the statement 'assign\n"); log(" = ;' to the Verilog input. Per default, all existing\n"); @@ -55,12 +55,12 @@ struct ConnectPass : public Pass { log("the -nounset option.\n"); log("\n"); log("\n"); - log(" connect [-nomap] -unset \n"); + log(" connect [-nomap] -unset [selection]\n"); log("\n"); log("Unconnect all existing drivers for the specified expression.\n"); log("\n"); log("\n"); - log(" connect [-nomap] [-assert] -port \n"); + log(" connect [-nomap] [-assert] -port [selection]\n"); log("\n"); log("Connect the specified cell port to the specified cell port.\n"); log("\n"); @@ -80,17 +80,6 @@ struct ConnectPass : public Pass { } void execute(std::vector args, RTLIL::Design *design) override { - RTLIL::Module *module = nullptr; - for (auto mod : design->selected_modules()) { - if (module != nullptr) - log_cmd_error("Multiple modules selected: %s, %s\n", log_id(module->name), log_id(mod->name)); - module = mod; - } - if (module == nullptr) - log_cmd_error("No modules selected.\n"); - if (!module->processes.empty()) - log_cmd_error("Found processes in selected module.\n"); - bool flag_nounset = false, flag_nomap = false, flag_assert = false; std::string set_lhs, set_rhs, unset_expr; std::string port_cell, port_port, port_expr; @@ -128,6 +117,18 @@ struct ConnectPass : public Pass { } break; } + extra_args(args, argidx, design); + + RTLIL::Module *module = nullptr; + for (auto mod : design->selected_modules()) { + if (module != nullptr) + log_cmd_error("Multiple modules selected: %s, %s\n", log_id(module->name), log_id(mod->name)); + module = mod; + } + if (module == nullptr) + log_cmd_error("No modules selected.\n"); + if (!module->processes.empty()) + log_cmd_error("Found processes in selected module.\n"); SigMap sigmap; if (!flag_nomap) From 862f2fd705a7822c7d5cf30ceab2bc8ff49eb1e1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Povi=C5=A1er?= Date: Thu, 8 Feb 2024 00:07:51 +0100 Subject: [PATCH 15/80] proc_dlatch: Include `$bwmux` among considered mux cells --- passes/proc/proc_dlatch.cc | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) diff --git a/passes/proc/proc_dlatch.cc b/passes/proc/proc_dlatch.cc index 8340e1431..5b392ce51 100644 --- a/passes/proc/proc_dlatch.cc +++ b/passes/proc/proc_dlatch.cc @@ -46,7 +46,7 @@ struct proc_dlatch_db_t for (auto cell : module->cells()) { - if (cell->type.in(ID($mux), ID($pmux))) + if (cell->type.in(ID($mux), ID($pmux), ID($bwmux))) { auto sig_y = sigmap(cell->getPort(ID::Y)); for (int i = 0; i < GetSize(sig_y); i++) @@ -186,6 +186,8 @@ struct proc_dlatch_db_t Cell *cell = it->second.first; int index = it->second.second; + log_assert(cell->type.in(ID($mux), ID($pmux), ID($bwmux))); + bool is_bwmux = (cell->type == ID($bwmux)); SigSpec sig_a = sigmap(cell->getPort(ID::A)); SigSpec sig_b = sigmap(cell->getPort(ID::B)); SigSpec sig_s = sigmap(cell->getPort(ID::S)); @@ -200,12 +202,16 @@ struct proc_dlatch_db_t sig[index] = State::Sx; cell->setPort(ID::A, sig); } - for (int i = 0; i < GetSize(sig_s); i++) - n = make_inner(sig_s[i], State::S0, n); + if (!is_bwmux) { + for (int i = 0; i < GetSize(sig_s); i++) + n = make_inner(sig_s[i], State::S0, n); + } else { + n = make_inner(sig_s[index], State::S0, n); + } children.insert(n); } - for (int i = 0; i < GetSize(sig_s); i++) { + for (int i = 0; i < (is_bwmux ? 1 : GetSize(sig_s)); i++) { n = find_mux_feedback(sig_b[i*width + index], needle, set_undef); if (n != false_node) { if (set_undef && sig_b[i*width + index] == needle) { @@ -213,7 +219,7 @@ struct proc_dlatch_db_t sig[i*width + index] = State::Sx; cell->setPort(ID::B, sig); } - children.insert(make_inner(sig_s[i], State::S1, n)); + children.insert(make_inner(sig_s[is_bwmux ? index : i], State::S1, n)); } } From 8566489d8510af1e3086af9b692490f35db377a8 Mon Sep 17 00:00:00 2001 From: Ethan Mahintorabi Date: Fri, 9 Feb 2024 23:51:00 +0000 Subject: [PATCH 16/80] stat: Add sequential area output to stat -liberty Checks to see if a cell is of type ff in the liberty, and keeps track of an additional area value. ``` Chip area for module '\addr': 92.280720 Sequential area for module '\addr': 38.814720 ``` Signed-off-by: Ethan Mahintorabi --- passes/cmds/stat.cc | 34 ++++++++++++++++++++++++---------- 1 file changed, 24 insertions(+), 10 deletions(-) diff --git a/passes/cmds/stat.cc b/passes/cmds/stat.cc index d34373c1c..9849d2537 100644 --- a/passes/cmds/stat.cc +++ b/passes/cmds/stat.cc @@ -28,6 +28,11 @@ USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN +struct cell_data_t { + double area; + bool is_flip_flop; +}; + struct statdata_t { #define STAT_INT_MEMBERS X(num_wires) X(num_wire_bits) X(num_pub_wires) X(num_pub_wire_bits) \ @@ -39,6 +44,7 @@ struct statdata_t STAT_INT_MEMBERS #undef X double area; + double sequential_area; string tech; std::map techinfo; @@ -74,7 +80,7 @@ struct statdata_t #undef X } - statdata_t(RTLIL::Design *design, RTLIL::Module *mod, bool width_mode, const dict &cell_area, string techname) + statdata_t(RTLIL::Design *design, RTLIL::Module *mod, bool width_mode, const dict &cell_properties, string techname) { tech = techname; @@ -131,11 +137,17 @@ struct statdata_t cell_type = stringf("%s_%d", cell_type.c_str(), GetSize(cell->getPort(ID::Q))); } - if (!cell_area.empty()) { - if (cell_area.count(cell_type)) - area += cell_area.at(cell_type); - else + if (!cell_properties.empty()) { + if (cell_properties.count(cell_type)) { + cell_data_t cell_data = cell_properties.at(cell_type); + if (cell_data.is_flip_flop) { + sequential_area += cell_data.area; + } + area += cell_data.area; + } + else { unknown_cell_area.insert(cell_type); + } } num_cells++; @@ -244,6 +256,7 @@ struct statdata_t if (area != 0) { log("\n"); log(" Chip area for %smodule '%s': %f\n", (top_mod) ? "top " : "", mod_name.c_str(), area); + log(" Sequential area for %smodule '%s': %f\n", (top_mod) ? "top " : "", mod_name.c_str(), sequential_area); } if (tech == "xilinx") @@ -325,7 +338,7 @@ statdata_t hierarchy_worker(std::map &mod_stat, RTL return mod_data; } -void read_liberty_cellarea(dict &cell_area, string liberty_file) +void read_liberty_cellarea(dict &cell_properties, string liberty_file) { std::ifstream f; f.open(liberty_file.c_str()); @@ -341,8 +354,9 @@ void read_liberty_cellarea(dict &cell_area, string liberty_fil continue; LibertyAst *ar = cell->find("area"); + bool is_flip_flop = cell->find("ff") != nullptr; if (ar != nullptr && !ar->value.empty()) - cell_area["\\" + cell->args[0]] = atof(ar->value.c_str()); + cell_properties["\\" + cell->args[0]] = {/*area=*/atof(ar->value.c_str()), is_flip_flop}; } } @@ -383,7 +397,7 @@ struct StatPass : public Pass { bool width_mode = false, json_mode = false; RTLIL::Module *top_mod = nullptr; std::map mod_stat; - dict cell_area; + dict cell_properties; string techname; size_t argidx; @@ -396,7 +410,7 @@ struct StatPass : public Pass { if (args[argidx] == "-liberty" && argidx+1 < args.size()) { string liberty_file = args[++argidx]; rewrite_filename(liberty_file); - read_liberty_cellarea(cell_area, liberty_file); + read_liberty_cellarea(cell_properties, liberty_file); continue; } if (args[argidx] == "-tech" && argidx+1 < args.size()) { @@ -439,7 +453,7 @@ struct StatPass : public Pass { if (mod->get_bool_attribute(ID::top)) top_mod = mod; - statdata_t data(design, mod, width_mode, cell_area, techname); + statdata_t data(design, mod, width_mode, cell_properties, techname); mod_stat[mod->name] = data; if (json_mode) { From 5226d0772125f136a30290e4e3a66c3064d840d7 Mon Sep 17 00:00:00 2001 From: passingglance <75091815+passingglance@users.noreply.github.com> Date: Sun, 11 Feb 2024 23:59:07 -0800 Subject: [PATCH 17/80] Update CHAPTER_CellLib.rst Fix parameter name to \WIDTH for $tribuf cell. --- docs/source/CHAPTER_CellLib.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/source/CHAPTER_CellLib.rst b/docs/source/CHAPTER_CellLib.rst index 3b6f1b4d3..70a0e2150 100644 --- a/docs/source/CHAPTER_CellLib.rst +++ b/docs/source/CHAPTER_CellLib.rst @@ -195,7 +195,7 @@ from ``\S`` is set the output is undefined. Cells of this type are used to model by an optimization). The ``$tribuf`` cell is used to implement tristate logic. Cells of this type -have a ``\B`` parameter and inputs ``\A`` and ``\EN`` and an output ``\Y``. The +have a ``\WIDTH`` parameter and inputs ``\A`` and ``\EN`` and an output ``\Y``. The ``\A`` input and ``\Y`` output are ``\WIDTH`` bits wide, and the ``\EN`` input is one bit wide. When ``\EN`` is 0, the output is not driven. When ``\EN`` is 1, the value from ``\A`` input is sent to the ``\Y`` output. Therefore, the From 353ccc9e58d12b2a9dcf9213bfa02116a754c230 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Mon, 12 Feb 2024 12:58:13 +0100 Subject: [PATCH 18/80] do not override existing shell variable --- tests/gen-tests-makefile.sh | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/gen-tests-makefile.sh b/tests/gen-tests-makefile.sh index 6bf91b4dc..2b26d8c98 100755 --- a/tests/gen-tests-makefile.sh +++ b/tests/gen-tests-makefile.sh @@ -16,8 +16,8 @@ generate_target() { # $ generate_ys_test ys_file [yosys_args] generate_ys_test() { ys_file=$1 - yosys_args=${2:-} - generate_target "$ys_file" "\"$YOSYS_BASEDIR/yosys\" -ql ${ys_file%.*}.log $yosys_args $ys_file" + yosys_args_=${2:-} + generate_target "$ys_file" "\"$YOSYS_BASEDIR/yosys\" -ql ${ys_file%.*}.log $yosys_args_ $ys_file" } # $ generate_bash_test bash_file From d8ce26a5bad847521f09c7d31325c9d63f3e4a69 Mon Sep 17 00:00:00 2001 From: Catherine Date: Tue, 13 Feb 2024 18:20:26 +0000 Subject: [PATCH 19/80] read_verilog: correctly format `hdlname` attribute value. The leading slash is not a part of the attribute as it only concerns public values. --- frontends/ast/ast.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/frontends/ast/ast.cc b/frontends/ast/ast.cc index ead79fd95..996f6715d 100644 --- a/frontends/ast/ast.cc +++ b/frontends/ast/ast.cc @@ -1820,7 +1820,7 @@ std::string AstModule::derive_common(RTLIL::Design *design, const dictclone(); if (!new_ast->attributes.count(ID::hdlname)) - new_ast->set_attribute(ID::hdlname, AstNode::mkconst_str(stripped_name)); + new_ast->set_attribute(ID::hdlname, AstNode::mkconst_str(stripped_name.substr(1))); para_counter = 0; for (auto child : new_ast->children) { From b16f4900fd97308134d27b32adaf09ae6204f801 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Povi=C5=A1er?= Date: Tue, 13 Feb 2024 21:38:41 +0100 Subject: [PATCH 20/80] ast/simplify: Interpret hdlname w/o expecting backslash --- frontends/ast/simplify.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/frontends/ast/simplify.cc b/frontends/ast/simplify.cc index 96296aeb8..43a4e03a2 100644 --- a/frontends/ast/simplify.cc +++ b/frontends/ast/simplify.cc @@ -5662,7 +5662,7 @@ std::string AstNode::try_pop_module_prefix() const if (current_scope.count(new_str)) { std::string prefix = str.substr(0, pos); auto it = current_scope_ast->attributes.find(ID::hdlname); - if ((it != current_scope_ast->attributes.end() && it->second->str == prefix) + if ((it != current_scope_ast->attributes.end() && it->second->str == prefix.substr(1)) || prefix == current_scope_ast->str) return new_str; } From 834276a2f72566cfdeb420f04fd260d87e5c07ec Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Wed, 14 Feb 2024 09:50:53 +0100 Subject: [PATCH 21/80] show: Add option to add cell/wire "src" attribute into graphviz attribute href --- passes/cmds/show.cc | 36 +++++++++++++++++++++++++++--------- 1 file changed, 27 insertions(+), 9 deletions(-) diff --git a/passes/cmds/show.cc b/passes/cmds/show.cc index 8c2695dbe..82b5c6bcf 100644 --- a/passes/cmds/show.cc +++ b/passes/cmds/show.cc @@ -65,6 +65,7 @@ struct ShowWorker bool enumerateIds; bool abbreviateIds; bool notitle; + bool href; int page_counter; const std::vector> &color_selections; @@ -432,9 +433,13 @@ struct ShowWorker if (wire->port_input || wire->port_output) shape = "octagon"; if (wire->name.isPublic()) { - fprintf(f, "n%d [ shape=%s, label=\"%s\", %s ];\n", + std::string src_href; + if (href && wire->attributes.count(ID::src) > 0) + src_href = stringf(", href=\"%s\" ", escape(wire->attributes.at(ID::src).decode_string())); + fprintf(f, "n%d [ shape=%s, label=\"%s\", %s%s];\n", id2num(wire->name), shape, findLabel(wire->name.str()), - nextColor(RTLIL::SigSpec(wire), "color=\"black\", fontcolor=\"black\"").c_str()); + nextColor(RTLIL::SigSpec(wire), "color=\"black\", fontcolor=\"black\"").c_str(), + src_href.c_str()); if (wire->port_input) all_sources.insert(stringf("n%d", id2num(wire->name))); else if (wire->port_output) @@ -496,14 +501,18 @@ struct ShowWorker conn.second, ct.cell_output(cell->type, conn.first)); } + std::string src_href; + if (href && cell->attributes.count(ID::src) > 0) { + src_href = stringf("%shref=\"%s\" ", (findColor(cell->name).empty() ? "" :" , "), escape(cell->attributes.at(ID::src).decode_string())); + } #ifdef CLUSTER_CELLS_AND_PORTBOXES if (!code.empty()) - fprintf(f, "subgraph cluster_c%d {\nc%d [ shape=record, label=\"%s\"%s ];\n%s}\n", - id2num(cell->name), id2num(cell->name), label_string.c_str(), color.c_str(), code.c_str()); + fprintf(f, "subgraph cluster_c%d {\nc%d [ shape=record, label=\"%s\"%s%s ];\n%s}\n", + id2num(cell->name), id2num(cell->name), label_string.c_str(), color.c_str(), src_href.c_str(), code.c_str()); else #endif - fprintf(f, "c%d [ shape=record, label=\"%s\", %s ];\n%s", - id2num(cell->name), label_string.c_str(), findColor(cell->name).c_str(), code.c_str()); + fprintf(f, "c%d [ shape=record, label=\"%s\", %s%s ];\n%s", + id2num(cell->name), label_string.c_str(), findColor(cell->name).c_str(), src_href.c_str(), code.c_str()); } for (auto &it : module->processes) @@ -608,12 +617,12 @@ struct ShowWorker } ShowWorker(FILE *f, RTLIL::Design *design, std::vector &libs, uint32_t colorSeed, bool genWidthLabels, - bool genSignedLabels, bool stretchIO, bool enumerateIds, bool abbreviateIds, bool notitle, + bool genSignedLabels, bool stretchIO, bool enumerateIds, bool abbreviateIds, bool notitle, bool href, const std::vector> &color_selections, const std::vector> &label_selections, RTLIL::IdString colorattr) : f(f), design(design), currentColor(colorSeed), genWidthLabels(genWidthLabels), genSignedLabels(genSignedLabels), stretchIO(stretchIO), enumerateIds(enumerateIds), abbreviateIds(abbreviateIds), - notitle(notitle), color_selections(color_selections), label_selections(label_selections), colorattr(colorattr) + notitle(notitle), href(href), color_selections(color_selections), label_selections(label_selections), colorattr(colorattr) { ct.setup_internals(); ct.setup_internals_mem(); @@ -726,6 +735,10 @@ struct ShowPass : public Pass { log(" don't run viewer in the background, IE wait for the viewer tool to\n"); log(" exit before returning\n"); log("\n"); + log(" -href\n"); + log(" adds href attribute to all items representing cells and wires, using\n"); + log(" src attribute of origin\n"); + log("\n"); log("When no is specified, 'dot' is used. When no and is\n"); log("specified, 'xdot' is used to display the schematic (POSIX systems only).\n"); log("\n"); @@ -763,6 +776,7 @@ struct ShowPass : public Pass { bool flag_enum = false; bool flag_abbreviate = true; bool flag_notitle = false; + bool flag_href = false; bool custom_prefix = false; std::string background = "&"; RTLIL::IdString colorattr; @@ -850,6 +864,10 @@ struct ShowPass : public Pass { background= ""; continue; } + if (arg == "-href") { + flag_href = true; + continue; + } break; } extra_args(args, argidx, design); @@ -894,7 +912,7 @@ struct ShowPass : public Pass { delete lib; log_cmd_error("Can't open dot file `%s' for writing.\n", dot_file.c_str()); } - ShowWorker worker(f, design, libs, colorSeed, flag_width, flag_signed, flag_stretch, flag_enum, flag_abbreviate, flag_notitle, color_selections, label_selections, colorattr); + ShowWorker worker(f, design, libs, colorSeed, flag_width, flag_signed, flag_stretch, flag_enum, flag_abbreviate, flag_notitle, flag_href, color_selections, label_selections, colorattr); fclose(f); for (auto lib : libs) From 2d8343d4234da07e026225682694e4192db75c3a Mon Sep 17 00:00:00 2001 From: Ethan Mahintorabi Date: Thu, 15 Feb 2024 23:59:19 +0000 Subject: [PATCH 22/80] update type and variable names Signed-off-by: Ethan Mahintorabi --- passes/cmds/stat.cc | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/passes/cmds/stat.cc b/passes/cmds/stat.cc index 9849d2537..82ad80779 100644 --- a/passes/cmds/stat.cc +++ b/passes/cmds/stat.cc @@ -28,9 +28,9 @@ USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN -struct cell_data_t { +struct cell_area_t { double area; - bool is_flip_flop; + bool is_sequential; }; struct statdata_t @@ -80,7 +80,7 @@ struct statdata_t #undef X } - statdata_t(RTLIL::Design *design, RTLIL::Module *mod, bool width_mode, const dict &cell_properties, string techname) + statdata_t(RTLIL::Design *design, RTLIL::Module *mod, bool width_mode, const dict &cell_properties, string techname) { tech = techname; @@ -139,8 +139,8 @@ struct statdata_t if (!cell_properties.empty()) { if (cell_properties.count(cell_type)) { - cell_data_t cell_data = cell_properties.at(cell_type); - if (cell_data.is_flip_flop) { + cell_area_t cell_data = cell_properties.at(cell_type); + if (cell_data.is_sequential) { sequential_area += cell_data.area; } area += cell_data.area; @@ -338,7 +338,7 @@ statdata_t hierarchy_worker(std::map &mod_stat, RTL return mod_data; } -void read_liberty_cellarea(dict &cell_properties, string liberty_file) +void read_liberty_cellarea(dict &cell_properties, string liberty_file) { std::ifstream f; f.open(liberty_file.c_str()); @@ -397,7 +397,7 @@ struct StatPass : public Pass { bool width_mode = false, json_mode = false; RTLIL::Module *top_mod = nullptr; std::map mod_stat; - dict cell_properties; + dict cell_properties; string techname; size_t argidx; From f0df0e3912bdc40075a2762530d21add11c7e6d0 Mon Sep 17 00:00:00 2001 From: Ethan Mahintorabi Date: Fri, 16 Feb 2024 00:01:44 +0000 Subject: [PATCH 23/80] update type and variable names Signed-off-by: Ethan Mahintorabi --- passes/cmds/stat.cc | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/passes/cmds/stat.cc b/passes/cmds/stat.cc index 82ad80779..c74aa7c14 100644 --- a/passes/cmds/stat.cc +++ b/passes/cmds/stat.cc @@ -80,7 +80,7 @@ struct statdata_t #undef X } - statdata_t(RTLIL::Design *design, RTLIL::Module *mod, bool width_mode, const dict &cell_properties, string techname) + statdata_t(RTLIL::Design *design, RTLIL::Module *mod, bool width_mode, const dict &cell_area, string techname) { tech = techname; @@ -137,9 +137,9 @@ struct statdata_t cell_type = stringf("%s_%d", cell_type.c_str(), GetSize(cell->getPort(ID::Q))); } - if (!cell_properties.empty()) { - if (cell_properties.count(cell_type)) { - cell_area_t cell_data = cell_properties.at(cell_type); + if (!cell_area.empty()) { + if (cell_area.count(cell_type)) { + cell_area_t cell_data = cell_area.at(cell_type); if (cell_data.is_sequential) { sequential_area += cell_data.area; } @@ -338,7 +338,7 @@ statdata_t hierarchy_worker(std::map &mod_stat, RTL return mod_data; } -void read_liberty_cellarea(dict &cell_properties, string liberty_file) +void read_liberty_cellarea(dict &cell_area, string liberty_file) { std::ifstream f; f.open(liberty_file.c_str()); @@ -356,7 +356,7 @@ void read_liberty_cellarea(dict &cell_properties, string LibertyAst *ar = cell->find("area"); bool is_flip_flop = cell->find("ff") != nullptr; if (ar != nullptr && !ar->value.empty()) - cell_properties["\\" + cell->args[0]] = {/*area=*/atof(ar->value.c_str()), is_flip_flop}; + cell_area["\\" + cell->args[0]] = {/*area=*/atof(ar->value.c_str()), is_flip_flop}; } } @@ -397,7 +397,7 @@ struct StatPass : public Pass { bool width_mode = false, json_mode = false; RTLIL::Module *top_mod = nullptr; std::map mod_stat; - dict cell_properties; + dict cell_area; string techname; size_t argidx; @@ -410,7 +410,7 @@ struct StatPass : public Pass { if (args[argidx] == "-liberty" && argidx+1 < args.size()) { string liberty_file = args[++argidx]; rewrite_filename(liberty_file); - read_liberty_cellarea(cell_properties, liberty_file); + read_liberty_cellarea(cell_area, liberty_file); continue; } if (args[argidx] == "-tech" && argidx+1 < args.size()) { @@ -453,7 +453,7 @@ struct StatPass : public Pass { if (mod->get_bool_attribute(ID::top)) top_mod = mod; - statdata_t data(design, mod, width_mode, cell_properties, techname); + statdata_t data(design, mod, width_mode, cell_area, techname); mod_stat[mod->name] = data; if (json_mode) { From 5a05344d9cd003e5136415fd65a13fd18f28b189 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Povi=C5=A1er?= Date: Fri, 16 Feb 2024 11:41:09 +0100 Subject: [PATCH 24/80] tests: Fix initialization race in xprop tests --- tests/xprop/test.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/xprop/test.py b/tests/xprop/test.py index a275b0d93..b73b4dae7 100644 --- a/tests/xprop/test.py +++ b/tests/xprop/test.py @@ -271,7 +271,7 @@ if "prepare" in steps: for pattern in patterns: print( - f' gclk = 1; #0; A[0] = 1\'b{pattern[-1]}; #0; A = {input_width}\'b{pattern}; #5; gclk = 0; $display("%b %b", A, Y); #5', + f' #0; gclk = 1; #0; A[0] = 1\'b{pattern[-1]}; #0; A = {input_width}\'b{pattern}; #5; gclk = 0; $display("%b %b", A, Y); #5', file=tb_file, ) From e51c77484a6d335e431b8e77aa46f3295365025f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Povi=C5=A1er?= Date: Fri, 16 Feb 2024 11:41:53 +0100 Subject: [PATCH 25/80] tests: Comment on `A[0]` --- tests/xprop/test.py | 1 + 1 file changed, 1 insertion(+) diff --git a/tests/xprop/test.py b/tests/xprop/test.py index b73b4dae7..e2cddf679 100644 --- a/tests/xprop/test.py +++ b/tests/xprop/test.py @@ -270,6 +270,7 @@ if "prepare" in steps: print("initial begin", file=tb_file) for pattern in patterns: + # A[0] might be the clock which requires special sequencing print( f' #0; gclk = 1; #0; A[0] = 1\'b{pattern[-1]}; #0; A = {input_width}\'b{pattern}; #5; gclk = 0; $display("%b %b", A, Y); #5', file=tb_file, From fdda501b587bb1bfc3561979b04a6e323d57677b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Povi=C5=A1er?= Date: Fri, 16 Feb 2024 11:42:56 +0100 Subject: [PATCH 26/80] ci: Stop pinning iverilog revision --- .github/workflows/test-linux.yml | 1 - .github/workflows/test-macos.yml | 1 - 2 files changed, 2 deletions(-) diff --git a/.github/workflows/test-linux.yml b/.github/workflows/test-linux.yml index 28c17a6c0..b3a6bd846 100644 --- a/.github/workflows/test-linux.yml +++ b/.github/workflows/test-linux.yml @@ -86,7 +86,6 @@ jobs: run: | git clone https://github.com/steveicarus/iverilog.git cd iverilog - git checkout 192b6aec96fde982e6ddcb28b346d5893aa8e874 echo "IVERILOG_GIT=$(git rev-parse HEAD)" >> $GITHUB_ENV - name: Cache iverilog diff --git a/.github/workflows/test-macos.yml b/.github/workflows/test-macos.yml index 17e2ae331..9b806a580 100644 --- a/.github/workflows/test-macos.yml +++ b/.github/workflows/test-macos.yml @@ -42,7 +42,6 @@ jobs: run: | git clone https://github.com/steveicarus/iverilog.git cd iverilog - git checkout 192b6aec96fde982e6ddcb28b346d5893aa8e874 echo "IVERILOG_GIT=$(git rev-parse HEAD)" >> $GITHUB_ENV - name: Cache iverilog From b8a1009de98406d6841357954724807bd034176e Mon Sep 17 00:00:00 2001 From: Ethan Mahintorabi Date: Fri, 16 Feb 2024 07:44:09 -0800 Subject: [PATCH 27/80] Update passes/cmds/stat.cc Make reporting line more clear about the non cumulative area of sequential cells Co-authored-by: N. Engelhardt --- passes/cmds/stat.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/passes/cmds/stat.cc b/passes/cmds/stat.cc index c74aa7c14..85107b68f 100644 --- a/passes/cmds/stat.cc +++ b/passes/cmds/stat.cc @@ -256,7 +256,7 @@ struct statdata_t if (area != 0) { log("\n"); log(" Chip area for %smodule '%s': %f\n", (top_mod) ? "top " : "", mod_name.c_str(), area); - log(" Sequential area for %smodule '%s': %f\n", (top_mod) ? "top " : "", mod_name.c_str(), sequential_area); + log(" of which used for sequential elements: %f (%.2f%%)\n", sequential_area, 100.0*sequential_area/area); } if (tech == "xilinx") From f8d4d7128cf72456cc03b0738a8651ac5dbe52e1 Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Sat, 17 Feb 2024 00:15:42 +0000 Subject: [PATCH 28/80] Bump version --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 57e37351c..109721c71 100644 --- a/Makefile +++ b/Makefile @@ -141,7 +141,7 @@ LDLIBS += -lrt endif endif -YOSYS_VER := 0.38+46 +YOSYS_VER := 0.38+54 # Note: We arrange for .gitcommit to contain the (short) commit hash in # tarballs generated with git-archive(1) using .gitattributes. The git repo From bf4a46ccb3b37517f62ac451cf4535630fee365d Mon Sep 17 00:00:00 2001 From: Amelia Cuss Date: Sun, 18 Feb 2024 01:30:28 +1100 Subject: [PATCH 29/80] proc_rom: don't assert on big actionless switch. See the test case. PROC_ROM will consider this for evaluation, even though -- without any actions -- lhs is empty (but still "uniform"). A zero-width memory is constructed, which later fails check with: ERROR: Assert `width != 0' failed in kernel/mem.cc:518. Ensure we don't proceed if there's nothing to encode. --- passes/proc/proc_rom.cc | 5 +++++ tests/proc/proc_rom.ys | 23 +++++++++++++++++++++++ 2 files changed, 28 insertions(+) diff --git a/passes/proc/proc_rom.cc b/passes/proc/proc_rom.cc index b83466ce7..ebc2377aa 100644 --- a/passes/proc/proc_rom.cc +++ b/passes/proc/proc_rom.cc @@ -66,6 +66,11 @@ struct RomWorker } } + if (lhs.empty()) { + log_debug("rejecting switch: lhs empty\n"); + return; + } + int swsigbits = 0; for (int i = 0; i < GetSize(sw->signal); i++) if (sw->signal[i] != State::S0) diff --git a/tests/proc/proc_rom.ys b/tests/proc/proc_rom.ys index 0ef2e2c61..93fd5002b 100644 --- a/tests/proc/proc_rom.ys +++ b/tests/proc/proc_rom.ys @@ -186,4 +186,27 @@ design -stash preopt equiv_opt -assert -run prepare: dummy +design -reset +read_ilang < Date: Tue, 6 Feb 2024 10:22:19 +0100 Subject: [PATCH 30/80] rtlil: Fix `Const` hashing omission --- kernel/rtlil.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kernel/rtlil.h b/kernel/rtlil.h index 928bc0440..40422dce5 100644 --- a/kernel/rtlil.h +++ b/kernel/rtlil.h @@ -712,7 +712,7 @@ struct RTLIL::Const inline unsigned int hash() const { unsigned int h = mkhash_init; for (auto b : bits) - mkhash(h, b); + h = mkhash(h, b); return h; } }; From 689feed012699d55d36327f3b08ba17dc76567b1 Mon Sep 17 00:00:00 2001 From: Austin Rovinski Date: Mon, 19 Feb 2024 13:00:18 -0500 Subject: [PATCH 31/80] dfflibmap: Add a -dont_use flag to ignore cells This is an alternative to setting the dont_use property in lib. This brings dfflibmap in parity with the abc pass for dont_use. Signed-off-by: Austin Rovinski --- passes/techmap/dfflibmap.cc | 92 ++++++++++++++++++++++++++++--------- tests/techmap/dfflibmap.ys | 7 +++ 2 files changed, 78 insertions(+), 21 deletions(-) diff --git a/passes/techmap/dfflibmap.cc b/passes/techmap/dfflibmap.cc index 12c3a95de..312f34be4 100644 --- a/passes/techmap/dfflibmap.cc +++ b/passes/techmap/dfflibmap.cc @@ -23,6 +23,13 @@ #include #include +#ifdef _WIN32 +#include +#pragma comment(lib, "shlwapi.lib") +#else +#include +#endif + USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN @@ -115,7 +122,15 @@ static bool parse_pin(LibertyAst *cell, LibertyAst *attr, std::string &pin_name, return false; } -static void find_cell(LibertyAst *ast, IdString cell_type, bool clkpol, bool has_reset, bool rstpol, bool rstval) +static int glob_match(const char *pattern, const char *string) { + #ifdef _WIN32 + return PathMatchSpec(string, pattern); + #else + return fnmatch(pattern, string, 0) == 0; + #endif +} + +static void find_cell(LibertyAst *ast, IdString cell_type, bool clkpol, bool has_reset, bool rstpol, bool rstval, std::vector &dont_use_cells) { LibertyAst *best_cell = nullptr; std::map best_cell_ports; @@ -135,6 +150,18 @@ static void find_cell(LibertyAst *ast, IdString cell_type, bool clkpol, bool has if (dn != nullptr && dn->value == "true") continue; + bool dont_use = false; + for (std::string &dont_use_cell : dont_use_cells) + { + if (glob_match(dont_use_cell.c_str(), cell->args[0].c_str())) + { + dont_use = true; + break; + } + } + if (dont_use) + continue; + LibertyAst *ff = cell->find("ff"); if (ff == nullptr) continue; @@ -227,7 +254,7 @@ static void find_cell(LibertyAst *ast, IdString cell_type, bool clkpol, bool has } } -static void find_cell_sr(LibertyAst *ast, IdString cell_type, bool clkpol, bool setpol, bool clrpol) +static void find_cell_sr(LibertyAst *ast, IdString cell_type, bool clkpol, bool setpol, bool clrpol, std::vector &dont_use_cells) { LibertyAst *best_cell = nullptr; std::map best_cell_ports; @@ -247,6 +274,18 @@ static void find_cell_sr(LibertyAst *ast, IdString cell_type, bool clkpol, bool if (dn != nullptr && dn->value == "true") continue; + bool dont_use = false; + for (std::string &dont_use_cell : dont_use_cells) + { + if (glob_match(dont_use_cell.c_str(), cell->args[0].c_str())) + { + dont_use = true; + break; + } + } + if (dont_use) + continue; + LibertyAst *ff = cell->find("ff"); if (ff == nullptr) continue; @@ -414,7 +453,7 @@ struct DfflibmapPass : public Pass { void help() override { log("\n"); - log(" dfflibmap [-prepare] [-map-only] [-info] -liberty [selection]\n"); + log(" dfflibmap [-prepare] [-map-only] [-info] [-dont_use ] -liberty [selection]\n"); log("\n"); log("Map internal flip-flop cells to the flip-flop cells in the technology\n"); log("library specified in the given liberty file.\n"); @@ -435,6 +474,11 @@ struct DfflibmapPass : public Pass { log("that would be passed to the dfflegalize pass. The design will not be\n"); log("changed.\n"); log("\n"); + log("When called with -dont_use, this command will not map to the specified cell\n"); + log("name as an alternative to setting the dont_use property in the Liberty file.\n"); + log("This argument can be called multiple times with different cell names. This\n"); + log("argument also supports simple glob patterns in the cell name.\n"); + log("\n"); } void execute(std::vector args, RTLIL::Design *design) override { @@ -446,6 +490,8 @@ struct DfflibmapPass : public Pass { bool map_only_mode = false; bool info_mode = false; + std::vector dont_use_cells; + size_t argidx; for (argidx = 1; argidx < args.size(); argidx++) { @@ -467,6 +513,10 @@ struct DfflibmapPass : public Pass { info_mode = true; continue; } + if (arg == "-dont_use" && argidx+1 < args.size()) { + dont_use_cells.push_back(args[++argidx]); + continue; + } break; } extra_args(args, argidx, design); @@ -491,26 +541,26 @@ struct DfflibmapPass : public Pass { LibertyParser libparser(f); f.close(); - find_cell(libparser.ast, ID($_DFF_N_), false, false, false, false); - find_cell(libparser.ast, ID($_DFF_P_), true, false, false, false); + find_cell(libparser.ast, ID($_DFF_N_), false, false, false, false, dont_use_cells); + find_cell(libparser.ast, ID($_DFF_P_), true, false, false, false, dont_use_cells); - find_cell(libparser.ast, ID($_DFF_NN0_), false, true, false, false); - find_cell(libparser.ast, ID($_DFF_NN1_), false, true, false, true); - find_cell(libparser.ast, ID($_DFF_NP0_), false, true, true, false); - find_cell(libparser.ast, ID($_DFF_NP1_), false, true, true, true); - find_cell(libparser.ast, ID($_DFF_PN0_), true, true, false, false); - find_cell(libparser.ast, ID($_DFF_PN1_), true, true, false, true); - find_cell(libparser.ast, ID($_DFF_PP0_), true, true, true, false); - find_cell(libparser.ast, ID($_DFF_PP1_), true, true, true, true); + find_cell(libparser.ast, ID($_DFF_NN0_), false, true, false, false, dont_use_cells); + find_cell(libparser.ast, ID($_DFF_NN1_), false, true, false, true, dont_use_cells); + find_cell(libparser.ast, ID($_DFF_NP0_), false, true, true, false, dont_use_cells); + find_cell(libparser.ast, ID($_DFF_NP1_), false, true, true, true, dont_use_cells); + find_cell(libparser.ast, ID($_DFF_PN0_), true, true, false, false, dont_use_cells); + find_cell(libparser.ast, ID($_DFF_PN1_), true, true, false, true, dont_use_cells); + find_cell(libparser.ast, ID($_DFF_PP0_), true, true, true, false, dont_use_cells); + find_cell(libparser.ast, ID($_DFF_PP1_), true, true, true, true, dont_use_cells); - find_cell_sr(libparser.ast, ID($_DFFSR_NNN_), false, false, false); - find_cell_sr(libparser.ast, ID($_DFFSR_NNP_), false, false, true); - find_cell_sr(libparser.ast, ID($_DFFSR_NPN_), false, true, false); - find_cell_sr(libparser.ast, ID($_DFFSR_NPP_), false, true, true); - find_cell_sr(libparser.ast, ID($_DFFSR_PNN_), true, false, false); - find_cell_sr(libparser.ast, ID($_DFFSR_PNP_), true, false, true); - find_cell_sr(libparser.ast, ID($_DFFSR_PPN_), true, true, false); - find_cell_sr(libparser.ast, ID($_DFFSR_PPP_), true, true, true); + find_cell_sr(libparser.ast, ID($_DFFSR_NNN_), false, false, false, dont_use_cells); + find_cell_sr(libparser.ast, ID($_DFFSR_NNP_), false, false, true, dont_use_cells); + find_cell_sr(libparser.ast, ID($_DFFSR_NPN_), false, true, false, dont_use_cells); + find_cell_sr(libparser.ast, ID($_DFFSR_NPP_), false, true, true, dont_use_cells); + find_cell_sr(libparser.ast, ID($_DFFSR_PNN_), true, false, false, dont_use_cells); + find_cell_sr(libparser.ast, ID($_DFFSR_PNP_), true, false, true, dont_use_cells); + find_cell_sr(libparser.ast, ID($_DFFSR_PPN_), true, true, false, dont_use_cells); + find_cell_sr(libparser.ast, ID($_DFFSR_PPP_), true, true, true, dont_use_cells); log(" final dff cell mappings:\n"); logmap_all(); diff --git a/tests/techmap/dfflibmap.ys b/tests/techmap/dfflibmap.ys index b0a7d6b7e..e8b125456 100644 --- a/tests/techmap/dfflibmap.ys +++ b/tests/techmap/dfflibmap.ys @@ -58,3 +58,10 @@ select -assert-count 4 t:$_NOT_ select -assert-count 1 t:dffn select -assert-count 4 t:dffsr select -assert-none t:dffn t:dffsr t:$_NOT_ %% %n t:* %i + +design -load orig +dfflibmap -liberty dfflibmap.lib -dont_use *ffn +clean + +select -assert-count 0 t:dffn +select -assert-count 5 t:dffsr From 5059bb1d4fa5e75f0ebc7f2a4a3938b729155fed Mon Sep 17 00:00:00 2001 From: Austin Rovinski Date: Mon, 19 Feb 2024 14:40:46 -0500 Subject: [PATCH 32/80] dfflibmap: force PathMatchSpecA on WIN32 Depending on the WIN32 compilation mode, PathMatchSpec may expect a LPCSTR or LPCWSTR argument. char* is only convertable to LPCSTR, so use that implementation Signed-off-by: Austin Rovinski --- passes/techmap/dfflibmap.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/passes/techmap/dfflibmap.cc b/passes/techmap/dfflibmap.cc index 312f34be4..6caf282bd 100644 --- a/passes/techmap/dfflibmap.cc +++ b/passes/techmap/dfflibmap.cc @@ -124,7 +124,7 @@ static bool parse_pin(LibertyAst *cell, LibertyAst *attr, std::string &pin_name, static int glob_match(const char *pattern, const char *string) { #ifdef _WIN32 - return PathMatchSpec(string, pattern); + return PathMatchSpecA(string, pattern); #else return fnmatch(pattern, string, 0) == 0; #endif From 01d6c12af44953b62b3d6c7d10824cc4c3ba5292 Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Tue, 20 Feb 2024 00:15:14 +0000 Subject: [PATCH 33/80] Bump version --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 109721c71..93d8effca 100644 --- a/Makefile +++ b/Makefile @@ -141,7 +141,7 @@ LDLIBS += -lrt endif endif -YOSYS_VER := 0.38+54 +YOSYS_VER := 0.38+75 # Note: We arrange for .gitcommit to contain the (short) commit hash in # tarballs generated with git-archive(1) using .gitattributes. The git repo From 20dbc860e7f28ec3a07b32973583b46f88dd1254 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Tue, 20 Feb 2024 12:44:55 +0100 Subject: [PATCH 34/80] Add shlwapi lib for mingw builds --- Makefile | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Makefile b/Makefile index 93d8effca..205fe319f 100644 --- a/Makefile +++ b/Makefile @@ -355,7 +355,7 @@ LD = i686-w64-mingw32-g++ CXXFLAGS += -std=$(CXXSTD) -Os -D_POSIX_SOURCE -DYOSYS_WIN32_UNIX_DIR CXXFLAGS := $(filter-out -fPIC,$(CXXFLAGS)) LDFLAGS := $(filter-out -rdynamic,$(LDFLAGS)) -s -LDLIBS := $(filter-out -lrt,$(LDLIBS)) +LDLIBS := $(filter-out -lrt,$(LDLIBS)) -lshlwapi ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H -DWIN32_NO_DLL -DHAVE_STRUCT_TIMESPEC -fpermissive -w" ABCMKARGS += LIBS="-lpthread -lshlwapi -s" ABC_USE_NO_READLINE=0 CC="i686-w64-mingw32-gcc" CXX="$(CXX)" EXE = .exe @@ -366,7 +366,7 @@ LD = x86_64-w64-mingw32-g++ CXXFLAGS += -std=$(CXXSTD) -Os -D_POSIX_SOURCE -DYOSYS_WIN32_UNIX_DIR CXXFLAGS := $(filter-out -fPIC,$(CXXFLAGS)) LDFLAGS := $(filter-out -rdynamic,$(LDFLAGS)) -s -LDLIBS := $(filter-out -lrt,$(LDLIBS)) +LDLIBS := $(filter-out -lrt,$(LDLIBS)) -lshlwapi ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H -DWIN32_NO_DLL -DHAVE_STRUCT_TIMESPEC -fpermissive -w" ABCMKARGS += LIBS="-lpthread -lshlwapi -s" ABC_USE_NO_READLINE=0 CC="x86_64-w64-mingw32-gcc" CXX="$(CXX)" EXE = .exe From 03cadf64748c8027f49f46cab11b33c7addfe46f Mon Sep 17 00:00:00 2001 From: Austin Rovinski Date: Tue, 20 Feb 2024 11:04:55 -0500 Subject: [PATCH 35/80] dfflibmap: use patmatch() from kernel/yosys.cc Replace OS matching functions with yosys kernel function Signed-off-by: Austin Rovinski --- passes/techmap/dfflibmap.cc | 19 ++----------------- 1 file changed, 2 insertions(+), 17 deletions(-) diff --git a/passes/techmap/dfflibmap.cc b/passes/techmap/dfflibmap.cc index 6caf282bd..78bfe1586 100644 --- a/passes/techmap/dfflibmap.cc +++ b/passes/techmap/dfflibmap.cc @@ -23,13 +23,6 @@ #include #include -#ifdef _WIN32 -#include -#pragma comment(lib, "shlwapi.lib") -#else -#include -#endif - USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN @@ -122,14 +115,6 @@ static bool parse_pin(LibertyAst *cell, LibertyAst *attr, std::string &pin_name, return false; } -static int glob_match(const char *pattern, const char *string) { - #ifdef _WIN32 - return PathMatchSpecA(string, pattern); - #else - return fnmatch(pattern, string, 0) == 0; - #endif -} - static void find_cell(LibertyAst *ast, IdString cell_type, bool clkpol, bool has_reset, bool rstpol, bool rstval, std::vector &dont_use_cells) { LibertyAst *best_cell = nullptr; @@ -153,7 +138,7 @@ static void find_cell(LibertyAst *ast, IdString cell_type, bool clkpol, bool has bool dont_use = false; for (std::string &dont_use_cell : dont_use_cells) { - if (glob_match(dont_use_cell.c_str(), cell->args[0].c_str())) + if (patmatch(dont_use_cell.c_str(), cell->args[0].c_str())) { dont_use = true; break; @@ -277,7 +262,7 @@ static void find_cell_sr(LibertyAst *ast, IdString cell_type, bool clkpol, bool bool dont_use = false; for (std::string &dont_use_cell : dont_use_cells) { - if (glob_match(dont_use_cell.c_str(), cell->args[0].c_str())) + if (patmatch(dont_use_cell.c_str(), cell->args[0].c_str())) { dont_use = true; break; From d5934357f3e4c9030a2d2287047aa40975801ca3 Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Wed, 21 Feb 2024 00:15:24 +0000 Subject: [PATCH 36/80] Bump version --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 205fe319f..a1185515c 100644 --- a/Makefile +++ b/Makefile @@ -141,7 +141,7 @@ LDLIBS += -lrt endif endif -YOSYS_VER := 0.38+75 +YOSYS_VER := 0.38+88 # Note: We arrange for .gitcommit to contain the (short) commit hash in # tarballs generated with git-archive(1) using .gitattributes. The git repo From 4c96546717546e5e0327559235c2a990c9cd980c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Povi=C5=A1er?= Date: Wed, 21 Feb 2024 12:03:37 +0100 Subject: [PATCH 37/80] equiv_simple: Take FFs into account for driver map This fixes an issue introduced in commit 26644ea due to which flip-flops are inadvertently ignored when building up driver map. The mentioned commit wasn't without functional change after all. --- passes/equiv/equiv_simple.cc | 2 ++ 1 file changed, 2 insertions(+) diff --git a/passes/equiv/equiv_simple.cc b/passes/equiv/equiv_simple.cc index 2c9d82914..59974a1e6 100644 --- a/passes/equiv/equiv_simple.cc +++ b/passes/equiv/equiv_simple.cc @@ -339,6 +339,8 @@ struct EquivSimplePass : public Pass { CellTypes ct; ct.setup_internals(); ct.setup_stdcells(); + ct.setup_internals_ff(); + ct.setup_stdcells_mem(); for (auto module : design->selected_modules()) { From 38f1b0b12d27d0a9c14e540b7907579d26a3f454 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Wed, 21 Feb 2024 20:23:49 +0100 Subject: [PATCH 38/80] Revert "Add shlwapi lib for mingw builds" This reverts commit 20dbc860e7f28ec3a07b32973583b46f88dd1254. --- Makefile | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Makefile b/Makefile index a1185515c..4b978ae20 100644 --- a/Makefile +++ b/Makefile @@ -355,7 +355,7 @@ LD = i686-w64-mingw32-g++ CXXFLAGS += -std=$(CXXSTD) -Os -D_POSIX_SOURCE -DYOSYS_WIN32_UNIX_DIR CXXFLAGS := $(filter-out -fPIC,$(CXXFLAGS)) LDFLAGS := $(filter-out -rdynamic,$(LDFLAGS)) -s -LDLIBS := $(filter-out -lrt,$(LDLIBS)) -lshlwapi +LDLIBS := $(filter-out -lrt,$(LDLIBS)) ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H -DWIN32_NO_DLL -DHAVE_STRUCT_TIMESPEC -fpermissive -w" ABCMKARGS += LIBS="-lpthread -lshlwapi -s" ABC_USE_NO_READLINE=0 CC="i686-w64-mingw32-gcc" CXX="$(CXX)" EXE = .exe @@ -366,7 +366,7 @@ LD = x86_64-w64-mingw32-g++ CXXFLAGS += -std=$(CXXSTD) -Os -D_POSIX_SOURCE -DYOSYS_WIN32_UNIX_DIR CXXFLAGS := $(filter-out -fPIC,$(CXXFLAGS)) LDFLAGS := $(filter-out -rdynamic,$(LDFLAGS)) -s -LDLIBS := $(filter-out -lrt,$(LDLIBS)) -lshlwapi +LDLIBS := $(filter-out -lrt,$(LDLIBS)) ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H -DWIN32_NO_DLL -DHAVE_STRUCT_TIMESPEC -fpermissive -w" ABCMKARGS += LIBS="-lpthread -lshlwapi -s" ABC_USE_NO_READLINE=0 CC="x86_64-w64-mingw32-gcc" CXX="$(CXX)" EXE = .exe From 84116c9a38546d549c9b122983441d69544854ab Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Thu, 22 Feb 2024 00:15:36 +0000 Subject: [PATCH 39/80] Bump version --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 4b978ae20..3f5c787fd 100644 --- a/Makefile +++ b/Makefile @@ -141,7 +141,7 @@ LDLIBS += -lrt endif endif -YOSYS_VER := 0.38+88 +YOSYS_VER := 0.38+92 # Note: We arrange for .gitcommit to contain the (short) commit hash in # tarballs generated with git-archive(1) using .gitattributes. The git repo From d77b792156b439ce7ae6a8900d0166fb1c849ee5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Povi=C5=A1er?= Date: Thu, 22 Feb 2024 17:22:56 +0100 Subject: [PATCH 40/80] synth: Put in missing bounds check for `-lut` --- techlibs/common/synth.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/techlibs/common/synth.cc b/techlibs/common/synth.cc index e5013678a..f604b67c9 100644 --- a/techlibs/common/synth.cc +++ b/techlibs/common/synth.cc @@ -151,7 +151,7 @@ struct SynthPass : public ScriptPass { flatten = true; continue; } - if (args[argidx] == "-lut") { + if (args[argidx] == "-lut" && argidx + 1 < args.size()) { lut = atoi(args[++argidx].c_str()); continue; } From ba07cba6ce73a979e4ce25a027fbf9cb8723a8c8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Povi=C5=A1er?= Date: Thu, 22 Feb 2024 17:23:28 +0100 Subject: [PATCH 41/80] synth: Introduce `-inject` for amending techmap --- techlibs/common/synth.cc | 23 +++++++++++++++++++++-- 1 file changed, 21 insertions(+), 2 deletions(-) diff --git a/techlibs/common/synth.cc b/techlibs/common/synth.cc index f604b67c9..7da9ba666 100644 --- a/techlibs/common/synth.cc +++ b/techlibs/common/synth.cc @@ -88,6 +88,10 @@ struct SynthPass : public ScriptPass { log(" read/write collision\" (same result as setting the no_rw_check\n"); log(" attribute on all memories).\n"); log("\n"); + log(" -inject filename\n"); + log(" inject rules from the given file to complement the default\n"); + log(" mapping library in the `techmap` step. this option can be\n"); + log(" repeated.\n"); log("\n"); log("The following commands are executed by this synthesis command:\n"); help_script(); @@ -96,8 +100,8 @@ struct SynthPass : public ScriptPass { string top_module, fsm_opts, memory_opts, abc; bool autotop, flatten, noalumacc, nofsm, noabc, noshare, flowmap, booth; - int lut; + std::vector techmap_inject; void clear_flags() override { @@ -115,6 +119,7 @@ struct SynthPass : public ScriptPass { flowmap = false; booth = false; abc = "abc"; + techmap_inject.clear(); } void execute(std::vector args, RTLIL::Design *design) override @@ -192,6 +197,10 @@ struct SynthPass : public ScriptPass { memory_opts += " -no-rw-check"; continue; } + if (args[argidx] == "-inject" && argidx + 1 < args.size()) { + techmap_inject.push_back(args[++argidx]); + continue; + } break; } extra_args(args, argidx, design); @@ -261,7 +270,17 @@ struct SynthPass : public ScriptPass { run("opt -fast -full"); run("memory_map"); run("opt -full"); - run("techmap"); + if (help_mode) { + run("techmap", " (unless -inject)"); + run("techmap -map +/techmap.v -map ", " (if -inject)"); + } else { + std::string techmap_opts; + if (!techmap_inject.empty()) + techmap_opts += " -map +/techmap.v"; + for (auto fn : techmap_inject) + techmap_opts += stringf(" -map %s", fn.c_str()); + run("techmap" + techmap_opts); + } if (help_mode) { run("techmap -map +/gate2lut.v", "(if -noabc and -lut)"); run("clean; opt_lut", " (if -noabc and -lut)"); From 53ca7b48f86fd3d5bc9ed0f319e24d0086dc12bc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Povi=C5=A1er?= Date: Thu, 22 Feb 2024 22:00:56 +0100 Subject: [PATCH 42/80] techmap: Fix help message wording --- passes/techmap/techmap.cc | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/passes/techmap/techmap.cc b/passes/techmap/techmap.cc index 144f596c8..db395315c 100644 --- a/passes/techmap/techmap.cc +++ b/passes/techmap/techmap.cc @@ -1041,8 +1041,8 @@ struct TechmapPass : public Pass { log("\n"); log("When a port on a module in the map file has the 'techmap_autopurge' attribute\n"); log("set, and that port is not connected in the instantiation that is mapped, then\n"); - log("then a cell port connected only to such wires will be omitted in the mapped\n"); - log("version of the circuit.\n"); + log("a cell port connected only to such wires will be omitted in the mapped version\n"); + log("of the circuit.\n"); log("\n"); log("All wires in the modules from the map file matching the pattern _TECHMAP_*\n"); log("or *._TECHMAP_* are special wires that are used to pass instructions from\n"); From 173f4b5fbd4cc7841698846816c595889dff2db0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Povi=C5=A1er?= Date: Thu, 22 Feb 2024 22:03:44 +0100 Subject: [PATCH 43/80] Bump Claire's notices --- README.md | 2 +- kernel/yosys.cc | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index 3be1b4c2e..660bd5c6d 100644 --- a/README.md +++ b/README.md @@ -1,7 +1,7 @@ ``` yosys -- Yosys Open SYnthesis Suite -Copyright (C) 2012 - 2020 Claire Xenia Wolf +Copyright (C) 2012 - 2024 Claire Xenia Wolf Permission to use, copy, modify, and/or distribute this software for any purpose with or without fee is hereby granted, provided that the above diff --git a/kernel/yosys.cc b/kernel/yosys.cc index c7f5bebda..6d33ad96c 100644 --- a/kernel/yosys.cc +++ b/kernel/yosys.cc @@ -141,7 +141,7 @@ void yosys_banner() log(" | |\n"); log(" | yosys -- Yosys Open SYnthesis Suite |\n"); log(" | |\n"); - log(" | Copyright (C) 2012 - 2020 Claire Xenia Wolf |\n"); + log(" | Copyright (C) 2012 - 2024 Claire Xenia Wolf |\n"); log(" | |\n"); log(" | Permission to use, copy, modify, and/or distribute this software for any |\n"); log(" | purpose with or without fee is hereby granted, provided that the above |\n"); From f7737a12ca8fc0d9d53bf070332e3cc22d2ed82f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Povi=C5=A1er?= Date: Thu, 22 Feb 2024 22:14:32 +0100 Subject: [PATCH 44/80] Cut down startup banner --- kernel/register.cc | 40 ++++++++++++++++++++++++++++++++++++++++ kernel/yosys.cc | 14 +------------- 2 files changed, 41 insertions(+), 13 deletions(-) diff --git a/kernel/register.cc b/kernel/register.cc index 1853e94d5..b5485e06d 100644 --- a/kernel/register.cc +++ b/kernel/register.cc @@ -992,4 +992,44 @@ struct MinisatSatSolver : public SatSolver { } } MinisatSatSolver; +struct LicensePass : public Pass { + LicensePass() : Pass("license", "print license terms") { } + void help() override + { + log("\n"); + log(" license\n"); + log("\n"); + log("This command produces the following notice.\n"); + notice(); + } + void execute(std::vector args, RTLIL::Design*) override + { + notice(); + } + void notice() + { + log("\n"); + log(" /----------------------------------------------------------------------------\\\n"); + log(" | |\n"); + log(" | yosys -- Yosys Open SYnthesis Suite |\n"); + log(" | |\n"); + log(" | Copyright (C) 2012 - 2024 Claire Xenia Wolf |\n"); + log(" | |\n"); + log(" | Permission to use, copy, modify, and/or distribute this software for any |\n"); + log(" | purpose with or without fee is hereby granted, provided that the above |\n"); + log(" | copyright notice and this permission notice appear in all copies. |\n"); + log(" | |\n"); + log(" | THE SOFTWARE IS PROVIDED \"AS IS\" AND THE AUTHOR DISCLAIMS ALL WARRANTIES |\n"); + log(" | WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF |\n"); + log(" | MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR |\n"); + log(" | ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES |\n"); + log(" | WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN |\n"); + log(" | ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF |\n"); + log(" | OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. |\n"); + log(" | |\n"); + log(" \\----------------------------------------------------------------------------/\n"); + log("\n"); + } +} LicensePass; + YOSYS_NAMESPACE_END diff --git a/kernel/yosys.cc b/kernel/yosys.cc index 6d33ad96c..fe158bc87 100644 --- a/kernel/yosys.cc +++ b/kernel/yosys.cc @@ -140,20 +140,8 @@ void yosys_banner() log(" /----------------------------------------------------------------------------\\\n"); log(" | |\n"); log(" | yosys -- Yosys Open SYnthesis Suite |\n"); - log(" | |\n"); log(" | Copyright (C) 2012 - 2024 Claire Xenia Wolf |\n"); - log(" | |\n"); - log(" | Permission to use, copy, modify, and/or distribute this software for any |\n"); - log(" | purpose with or without fee is hereby granted, provided that the above |\n"); - log(" | copyright notice and this permission notice appear in all copies. |\n"); - log(" | |\n"); - log(" | THE SOFTWARE IS PROVIDED \"AS IS\" AND THE AUTHOR DISCLAIMS ALL WARRANTIES |\n"); - log(" | WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF |\n"); - log(" | MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR |\n"); - log(" | ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES |\n"); - log(" | WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN |\n"); - log(" | ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF |\n"); - log(" | OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. |\n"); + log(" | Distributed under an ISC-like license, type \"license\" to see terms |\n"); log(" | |\n"); log(" \\----------------------------------------------------------------------------/\n"); log("\n"); From b5b737de3887d77f117d99d3fad21a4eeb97953e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Povi=C5=A1er?= Date: Thu, 22 Feb 2024 22:20:35 +0100 Subject: [PATCH 45/80] Shrink a bit more --- kernel/yosys.cc | 2 -- 1 file changed, 2 deletions(-) diff --git a/kernel/yosys.cc b/kernel/yosys.cc index fe158bc87..444f597ca 100644 --- a/kernel/yosys.cc +++ b/kernel/yosys.cc @@ -138,11 +138,9 @@ void yosys_banner() { log("\n"); log(" /----------------------------------------------------------------------------\\\n"); - log(" | |\n"); log(" | yosys -- Yosys Open SYnthesis Suite |\n"); log(" | Copyright (C) 2012 - 2024 Claire Xenia Wolf |\n"); log(" | Distributed under an ISC-like license, type \"license\" to see terms |\n"); - log(" | |\n"); log(" \\----------------------------------------------------------------------------/\n"); log("\n"); log(" %s\n", yosys_version_str); From 975517b022afc8ec74491c77304a91862ce59dd0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Povi=C5=A1er?= Date: Fri, 23 Feb 2024 12:20:05 +0100 Subject: [PATCH 46/80] memory_memx: Fix log header --- passes/memory/memory_memx.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/passes/memory/memory_memx.cc b/passes/memory/memory_memx.cc index 7edc26caa..22aebb43f 100644 --- a/passes/memory/memory_memx.cc +++ b/passes/memory/memory_memx.cc @@ -50,7 +50,7 @@ struct MemoryMemxPass : public Pass { } void execute(std::vector args, RTLIL::Design *design) override { - log_header(design, "Executing MEMORY_MEMX pass (converting $mem cells to logic and flip-flops).\n"); + log_header(design, "Executing MEMORY_MEMX pass (emit soft logic for out-of-bounds handling).\n"); extra_args(args, 1, design); for (auto module : design->selected_modules()) From 030d639201a36ace29122d8e57acde44c0fdc16c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Povi=C5=A1er?= Date: Fri, 23 Feb 2024 12:26:47 +0100 Subject: [PATCH 47/80] opt_mem, memory_*: Refuse to operate in presence of processes Processes can contain `MemWriteAction` entries which are invisible to most passes operating on memories but which will be lowered to write ports later on by `proc_memwr`. For that reason we can get corrupted RTLIL if we sequence the memory passes before `proc`. Address that by making the affected memory passes ignore modules with processes. --- passes/memory/memory_collect.cc | 3 +++ passes/memory/memory_libmap.cc | 3 +++ passes/memory/memory_map.cc | 3 +++ passes/memory/memory_narrow.cc | 3 +++ passes/memory/memory_share.cc | 6 +++++- passes/opt/opt_mem.cc | 3 +++ 6 files changed, 20 insertions(+), 1 deletion(-) diff --git a/passes/memory/memory_collect.cc b/passes/memory/memory_collect.cc index bf3bb34f8..157042c9c 100644 --- a/passes/memory/memory_collect.cc +++ b/passes/memory/memory_collect.cc @@ -39,6 +39,9 @@ struct MemoryCollectPass : public Pass { log_header(design, "Executing MEMORY_COLLECT pass (generating $mem cells).\n"); extra_args(args, 1, design); for (auto module : design->selected_modules()) { + if (module->has_processes_warn()) + continue; + for (auto &mem : Mem::get_selected_memories(module)) { if (!mem.packed) { mem.packed = true; diff --git a/passes/memory/memory_libmap.cc b/passes/memory/memory_libmap.cc index 2e683b8eb..77a4eb81b 100644 --- a/passes/memory/memory_libmap.cc +++ b/passes/memory/memory_libmap.cc @@ -2229,6 +2229,9 @@ struct MemoryLibMapPass : public Pass { Library lib = parse_library(lib_files, defines); for (auto module : design->selected_modules()) { + if (module->has_processes_warn()) + continue; + MapWorker worker(module); auto mems = Mem::get_selected_memories(module); for (auto &mem : mems) diff --git a/passes/memory/memory_map.cc b/passes/memory/memory_map.cc index e2f74c2e1..cafc0aaf3 100644 --- a/passes/memory/memory_map.cc +++ b/passes/memory/memory_map.cc @@ -493,6 +493,9 @@ struct MemoryMapPass : public Pass { extra_args(args, argidx, design); for (auto mod : design->selected_modules()) { + if (mod->has_processes_warn()) + continue; + MemoryMapWorker worker(design, mod); worker.attr_icase = attr_icase; worker.attributes = attributes; diff --git a/passes/memory/memory_narrow.cc b/passes/memory/memory_narrow.cc index cf5e43465..46c538bab 100644 --- a/passes/memory/memory_narrow.cc +++ b/passes/memory/memory_narrow.cc @@ -46,6 +46,9 @@ struct MemoryNarrowPass : public Pass { extra_args(args, argidx, design); for (auto module : design->selected_modules()) { + if (module->has_processes_warn()) + continue; + for (auto &mem : Mem::get_selected_memories(module)) { bool wide = false; diff --git a/passes/memory/memory_share.cc b/passes/memory/memory_share.cc index 8b2354ef8..e06989f4a 100644 --- a/passes/memory/memory_share.cc +++ b/passes/memory/memory_share.cc @@ -558,8 +558,12 @@ struct MemorySharePass : public Pass { extra_args(args, argidx, design); MemoryShareWorker msw(design, flag_widen, flag_sat); - for (auto module : design->selected_modules()) + for (auto module : design->selected_modules()) { + if (module->has_processes_warn()) + continue; + msw(module); + } } } MemorySharePass; diff --git a/passes/opt/opt_mem.cc b/passes/opt/opt_mem.cc index 885b6f97d..9a2d8e6a5 100644 --- a/passes/opt/opt_mem.cc +++ b/passes/opt/opt_mem.cc @@ -52,6 +52,9 @@ struct OptMemPass : public Pass { int total_count = 0; for (auto module : design->selected_modules()) { + if (module->has_processes_warn()) + continue; + SigMap sigmap(module); FfInitVals initvals(&sigmap, module); for (auto &mem : Mem::get_selected_memories(module)) { From fe34abab3a22babfbc87d15c0c2a0e7a85a1f50b Mon Sep 17 00:00:00 2001 From: Roland Coeurjoly Date: Fri, 23 Feb 2024 14:03:12 +0100 Subject: [PATCH 48/80] =?UTF-8?q?=C2=B4Use=20g++=20and=20clang++=20instead?= =?UTF-8?q?=20of=20gcc=20and=20clang=20as=20C++=20compilers?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Makefile | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/Makefile b/Makefile index 3f5c787fd..fa5440ac5 100644 --- a/Makefile +++ b/Makefile @@ -215,7 +215,7 @@ ABC_ARCHFLAGS += "-DABC_NO_RLIMIT" endif ifeq ($(CONFIG),clang) -CXX = clang +CXX = clang++ LD = clang++ CXXFLAGS += -std=$(CXXSTD) -Os ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H -Wno-c++11-narrowing $(ABC_ARCHFLAGS)" @@ -238,8 +238,8 @@ endif endif else ifeq ($(CONFIG),gcc) -CXX = gcc -LD = gcc +CXX = g++ +LD = g++ CXXFLAGS += -std=$(CXXSTD) -Os ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H $(ABC_ARCHFLAGS)" @@ -262,8 +262,8 @@ CXXFLAGS += -std=$(CXXSTD) -Os ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H" else ifeq ($(CONFIG),cygwin) -CXX = gcc -LD = gcc +CXX = g++ +LD = g++ CXXFLAGS += -std=gnu++11 -Os ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H" @@ -309,13 +309,13 @@ yosys.html: misc/yosys.html else ifeq ($(CONFIG),wasi) ifeq ($(WASI_SDK),) -CXX = clang +CXX = clang++ LD = clang++ AR = llvm-ar RANLIB = llvm-ranlib WASIFLAGS := -target wasm32-wasi --sysroot $(WASI_SYSROOT) $(WASIFLAGS) else -CXX = $(WASI_SDK)/bin/clang +CXX = $(WASI_SDK)/bin/clang++ LD = $(WASI_SDK)/bin/clang++ AR = $(WASI_SDK)/bin/ar RANLIB = $(WASI_SDK)/bin/ranlib From a69a89f2e50690e281ae16e58e072c4a5bd5435c Mon Sep 17 00:00:00 2001 From: Roland Coeurjoly Date: Sun, 25 Feb 2024 16:43:55 +0100 Subject: [PATCH 49/80] LD is removed, we use CXX instead --- Makefile | 21 +++++---------------- 1 file changed, 5 insertions(+), 16 deletions(-) diff --git a/Makefile b/Makefile index fa5440ac5..80f929447 100644 --- a/Makefile +++ b/Makefile @@ -216,7 +216,6 @@ endif ifeq ($(CONFIG),clang) CXX = clang++ -LD = clang++ CXXFLAGS += -std=$(CXXSTD) -Os ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H -Wno-c++11-narrowing $(ABC_ARCHFLAGS)" @@ -239,17 +238,15 @@ endif else ifeq ($(CONFIG),gcc) CXX = g++ -LD = g++ CXXFLAGS += -std=$(CXXSTD) -Os ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H $(ABC_ARCHFLAGS)" else ifeq ($(CONFIG),gcc-static) -LD = $(CXX) LDFLAGS := $(filter-out -rdynamic,$(LDFLAGS)) -static LDLIBS := $(filter-out -lrt,$(LDLIBS)) CXXFLAGS := $(filter-out -fPIC,$(CXXFLAGS)) CXXFLAGS += -std=$(CXXSTD) -Os -ABCMKARGS = CC="$(CC)" CXX="$(CXX)" LD="$(LD)" ABC_USE_LIBSTDCXX=1 LIBS="-lm -lpthread -static" OPTFLAGS="-O" \ +ABCMKARGS = CC="$(CC)" CXX="$(CXX)" LD="$(CXX)" ABC_USE_LIBSTDCXX=1 LIBS="-lm -lpthread -static" OPTFLAGS="-O" \ ARCHFLAGS="-DABC_USE_STDINT_H -DABC_NO_DYNAMIC_LINKING=1 -Wno-unused-but-set-variable $(ARCHFLAGS)" ABC_USE_NO_READLINE=1 ifeq ($(DISABLE_ABC_THREADS),1) ABCMKARGS += "ABC_USE_NO_PTHREADS=1" @@ -257,19 +254,16 @@ endif else ifeq ($(CONFIG),afl-gcc) CXX = AFL_QUIET=1 AFL_HARDEN=1 afl-gcc -LD = AFL_QUIET=1 AFL_HARDEN=1 afl-gcc CXXFLAGS += -std=$(CXXSTD) -Os ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H" else ifeq ($(CONFIG),cygwin) CXX = g++ -LD = g++ CXXFLAGS += -std=gnu++11 -Os ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H" else ifeq ($(CONFIG),emcc) CXX = emcc -LD = emcc CXXFLAGS := -std=$(CXXSTD) $(filter-out -fPIC -ggdb,$(CXXFLAGS)) ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H -DABC_MEMALIGN=8 -Wno-c++11-narrowing" EMCC_CXXFLAGS := -Os -Wno-warn-absolute-paths @@ -310,13 +304,11 @@ yosys.html: misc/yosys.html else ifeq ($(CONFIG),wasi) ifeq ($(WASI_SDK),) CXX = clang++ -LD = clang++ AR = llvm-ar RANLIB = llvm-ranlib WASIFLAGS := -target wasm32-wasi --sysroot $(WASI_SYSROOT) $(WASIFLAGS) else CXX = $(WASI_SDK)/bin/clang++ -LD = $(WASI_SDK)/bin/clang++ AR = $(WASI_SDK)/bin/ar RANLIB = $(WASI_SDK)/bin/ranlib WASIFLAGS := --sysroot $(WASI_SDK)/share/wasi-sysroot $(WASIFLAGS) @@ -339,7 +331,6 @@ endif else ifeq ($(CONFIG),mxe) PKG_CONFIG = /usr/local/src/mxe/usr/bin/i686-w64-mingw32.static-pkg-config CXX = /usr/local/src/mxe/usr/bin/i686-w64-mingw32.static-g++ -LD = /usr/local/src/mxe/usr/bin/i686-w64-mingw32.static-g++ CXXFLAGS += -std=$(CXXSTD) -Os -D_POSIX_SOURCE -DYOSYS_MXE_HACKS -Wno-attributes CXXFLAGS := $(filter-out -fPIC,$(CXXFLAGS)) LDFLAGS := $(filter-out -rdynamic,$(LDFLAGS)) -s @@ -351,7 +342,6 @@ EXE = .exe else ifeq ($(CONFIG),msys2-32) CXX = i686-w64-mingw32-g++ -LD = i686-w64-mingw32-g++ CXXFLAGS += -std=$(CXXSTD) -Os -D_POSIX_SOURCE -DYOSYS_WIN32_UNIX_DIR CXXFLAGS := $(filter-out -fPIC,$(CXXFLAGS)) LDFLAGS := $(filter-out -rdynamic,$(LDFLAGS)) -s @@ -362,7 +352,6 @@ EXE = .exe else ifeq ($(CONFIG),msys2-64) CXX = x86_64-w64-mingw32-g++ -LD = x86_64-w64-mingw32-g++ CXXFLAGS += -std=$(CXXSTD) -Os -D_POSIX_SOURCE -DYOSYS_WIN32_UNIX_DIR CXXFLAGS := $(filter-out -fPIC,$(CXXFLAGS)) LDFLAGS := $(filter-out -rdynamic,$(LDFLAGS)) -s @@ -752,13 +741,13 @@ yosys.js: $(filter-out yosysjs-$(YOSYS_VER).zip,$(EXTRA_TARGETS)) endif $(PROGRAM_PREFIX)yosys$(EXE): $(OBJS) - $(P) $(LD) -o $(PROGRAM_PREFIX)yosys$(EXE) $(EXE_LDFLAGS) $(LDFLAGS) $(OBJS) $(LDLIBS) $(LDLIBS_VERIFIC) + $(P) $(CXX) -o $(PROGRAM_PREFIX)yosys$(EXE) $(EXE_LDFLAGS) $(LDFLAGS) $(OBJS) $(LDLIBS) $(LDLIBS_VERIFIC) libyosys.so: $(filter-out kernel/driver.o,$(OBJS)) ifeq ($(OS), Darwin) - $(P) $(LD) -o libyosys.so -shared -Wl,-install_name,$(LIBDIR)/libyosys.so $(LDFLAGS) $^ $(LDLIBS) $(LDLIBS_VERIFIC) + $(P) $(CXX) -o libyosys.so -shared -Wl,-install_name,$(LIBDIR)/libyosys.so $(LDFLAGS) $^ $(LDLIBS) $(LDLIBS_VERIFIC) else - $(P) $(LD) -o libyosys.so -shared -Wl,-soname,$(LIBDIR)/libyosys.so $(LDFLAGS) $^ $(LDLIBS) $(LDLIBS_VERIFIC) + $(P) $(CXX) -o libyosys.so -shared -Wl,-soname,$(LIBDIR)/libyosys.so $(LDFLAGS) $^ $(LDLIBS) $(LDLIBS_VERIFIC) endif %.o: %.cc @@ -767,7 +756,7 @@ endif %.pyh: %.h $(Q) mkdir -p $(dir $@) - $(P) cat $< | grep -E -v "#[ ]*(include|error)" | $(LD) $(CXXFLAGS) -x c++ -o $@ -E -P - + $(P) cat $< | grep -E -v "#[ ]*(include|error)" | $(CXX) $(CXXFLAGS) -x c++ -o $@ -E -P - ifeq ($(ENABLE_PYOSYS),1) $(PY_WRAPPER_FILE).cc: misc/$(PY_GEN_SCRIPT).py $(PY_WRAP_INCLUDES) From 033fa103078b07fad19c5e2f39000b312a13bf7a Mon Sep 17 00:00:00 2001 From: Roland Coeurjoly Date: Sun, 25 Feb 2024 16:49:28 +0100 Subject: [PATCH 50/80] We use CXX instead of LD for linking yosys-filterlib --- passes/techmap/Makefile.inc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/passes/techmap/Makefile.inc b/passes/techmap/Makefile.inc index 97d8b76f3..ed2f1c0bf 100644 --- a/passes/techmap/Makefile.inc +++ b/passes/techmap/Makefile.inc @@ -56,5 +56,5 @@ EXTRA_OBJS += passes/techmap/filterlib.o $(PROGRAM_PREFIX)yosys-filterlib$(EXE): passes/techmap/filterlib.o $(Q) mkdir -p $(dir $@) - $(P) $(LD) -o $(PROGRAM_PREFIX)yosys-filterlib$(EXE) $(LDFLAGS) $^ $(LDLIBS) + $(P) $(CXX) -o $(PROGRAM_PREFIX)yosys-filterlib$(EXE) $(LDFLAGS) $^ $(LDLIBS) endif From dea4aeae56a7b46246fff05f6d48909b9dc8c454 Mon Sep 17 00:00:00 2001 From: Roland Coeurjoly Date: Sun, 25 Feb 2024 17:02:35 +0100 Subject: [PATCH 51/80] LDLIBS -> LIBS. LDFLAGS -> LINKFLAGS --- Makefile | 122 +++++++++++++++++++++++++++---------------------------- 1 file changed, 61 insertions(+), 61 deletions(-) diff --git a/Makefile b/Makefile index 80f929447..e55388159 100644 --- a/Makefile +++ b/Makefile @@ -92,14 +92,14 @@ VPATH := $(YOSYS_SRC) CXXSTD ?= c++11 CXXFLAGS := $(CXXFLAGS) -Wall -Wextra -ggdb -I. -I"$(YOSYS_SRC)" -MD -MP -D_YOSYS_ -fPIC -I$(PREFIX)/include -LDLIBS := $(LDLIBS) -lstdc++ -lm -PLUGIN_LDFLAGS := -PLUGIN_LDLIBS := -EXE_LDFLAGS := +LIBS := $(LIBS) -lstdc++ -lm +PLUGIN_LINKFLAGS := +PLUGIN_LIBS := +EXE_LINKFLAGS := ifeq ($(OS), MINGW) -EXE_LDFLAGS := -Wl,--export-all-symbols -Wl,--out-implib,libyosys_exe.a -PLUGIN_LDFLAGS += -L"$(LIBDIR)" -PLUGIN_LDLIBS := -lyosys_exe +EXE_LINKFLAGS := -Wl,--export-all-symbols -Wl,--out-implib,libyosys_exe.a +PLUGIN_LINKFLAGS += -L"$(LIBDIR)" +PLUGIN_LIBS := -lyosys_exe endif PKG_CONFIG ?= pkg-config @@ -109,7 +109,7 @@ STRIP ?= strip AWK ?= awk ifeq ($(OS), Darwin) -PLUGIN_LDFLAGS += -undefined dynamic_lookup +PLUGIN_LINKFLAGS += -undefined dynamic_lookup # homebrew search paths ifneq ($(shell :; command -v brew),) @@ -117,10 +117,10 @@ BREW_PREFIX := $(shell brew --prefix)/opt $(info $$BREW_PREFIX is [${BREW_PREFIX}]) ifeq ($(ENABLE_PYOSYS),1) CXXFLAGS += -I$(BREW_PREFIX)/boost/include/boost -LDFLAGS += -L$(BREW_PREFIX)/boost/lib +LINKFLAGS += -L$(BREW_PREFIX)/boost/lib endif CXXFLAGS += -I$(BREW_PREFIX)/readline/include -LDFLAGS += -L$(BREW_PREFIX)/readline/lib +LINKFLAGS += -L$(BREW_PREFIX)/readline/lib PKG_CONFIG_PATH := $(BREW_PREFIX)/libffi/lib/pkgconfig:$(PKG_CONFIG_PATH) PKG_CONFIG_PATH := $(BREW_PREFIX)/tcl-tk/lib/pkgconfig:$(PKG_CONFIG_PATH) export PATH := $(BREW_PREFIX)/bison/bin:$(BREW_PREFIX)/gettext/bin:$(BREW_PREFIX)/flex/bin:$(PATH) @@ -129,15 +129,15 @@ export PATH := $(BREW_PREFIX)/bison/bin:$(BREW_PREFIX)/gettext/bin:$(BREW_PREFIX else ifneq ($(shell :; command -v port),) PORT_PREFIX := $(patsubst %/bin/port,%,$(shell :; command -v port)) CXXFLAGS += -I$(PORT_PREFIX)/include -LDFLAGS += -L$(PORT_PREFIX)/lib +LINKFLAGS += -L$(PORT_PREFIX)/lib PKG_CONFIG_PATH := $(PORT_PREFIX)/lib/pkgconfig:$(PKG_CONFIG_PATH) export PATH := $(PORT_PREFIX)/bin:$(PATH) endif else -LDFLAGS += -rdynamic +LINKFLAGS += -rdynamic ifneq ($(OS), OpenBSD) -LDLIBS += -lrt +LIBS += -lrt endif endif @@ -222,17 +222,17 @@ ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H -Wno-c++11-narrowing $(ABC_ARCHFLAGS) ifneq ($(SANITIZER),) $(info [Clang Sanitizer] $(SANITIZER)) CXXFLAGS += -g -O1 -fno-omit-frame-pointer -fno-optimize-sibling-calls -fsanitize=$(SANITIZER) -LDFLAGS += -g -fsanitize=$(SANITIZER) +LINKFLAGS += -g -fsanitize=$(SANITIZER) ifneq ($(findstring address,$(SANITIZER)),) ENABLE_COVER := 0 endif ifneq ($(findstring memory,$(SANITIZER)),) CXXFLAGS += -fPIE -fsanitize-memory-track-origins -LDFLAGS += -fPIE -fsanitize-memory-track-origins +LINKFLAGS += -fPIE -fsanitize-memory-track-origins endif ifneq ($(findstring cfi,$(SANITIZER)),) CXXFLAGS += -flto -LDFLAGS += -flto +LINKFLAGS += -flto endif endif @@ -242,8 +242,8 @@ CXXFLAGS += -std=$(CXXSTD) -Os ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H $(ABC_ARCHFLAGS)" else ifeq ($(CONFIG),gcc-static) -LDFLAGS := $(filter-out -rdynamic,$(LDFLAGS)) -static -LDLIBS := $(filter-out -lrt,$(LDLIBS)) +LINKFLAGS := $(filter-out -rdynamic,$(LINKFLAGS)) -static +LIBS := $(filter-out -lrt,$(LIBS)) CXXFLAGS := $(filter-out -fPIC,$(CXXFLAGS)) CXXFLAGS += -std=$(CXXSTD) -Os ABCMKARGS = CC="$(CC)" CXX="$(CXX)" LD="$(CXX)" ABC_USE_LIBSTDCXX=1 LIBS="-lm -lpthread -static" OPTFLAGS="-O" \ @@ -267,15 +267,15 @@ CXX = emcc CXXFLAGS := -std=$(CXXSTD) $(filter-out -fPIC -ggdb,$(CXXFLAGS)) ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H -DABC_MEMALIGN=8 -Wno-c++11-narrowing" EMCC_CXXFLAGS := -Os -Wno-warn-absolute-paths -EMCC_LDFLAGS := --memory-init-file 0 --embed-file share -EMCC_LDFLAGS += -s NO_EXIT_RUNTIME=1 -EMCC_LDFLAGS += -s EXPORTED_FUNCTIONS="['_main','_run','_prompt','_errmsg','_memset']" -EMCC_LDFLAGS += -s TOTAL_MEMORY=134217728 -EMCC_LDFLAGS += -s EXPORTED_RUNTIME_METHODS='["ccall", "cwrap"]' +EMCC_LINKFLAGS := --memory-init-file 0 --embed-file share +EMCC_LINKFLAGS += -s NO_EXIT_RUNTIME=1 +EMCC_LINKFLAGS += -s EXPORTED_FUNCTIONS="['_main','_run','_prompt','_errmsg','_memset']" +EMCC_LINKFLAGS += -s TOTAL_MEMORY=134217728 +EMCC_LINKFLAGS += -s EXPORTED_RUNTIME_METHODS='["ccall", "cwrap"]' # https://github.com/kripken/emscripten/blob/master/src/settings.js CXXFLAGS += $(EMCC_CXXFLAGS) -LDFLAGS += $(EMCC_LDFLAGS) -LDLIBS = +LINKFLAGS += $(EMCC_LINKFLAGS) +LIBS = EXE = .js DISABLE_SPAWN := 1 @@ -314,8 +314,8 @@ RANLIB = $(WASI_SDK)/bin/ranlib WASIFLAGS := --sysroot $(WASI_SDK)/share/wasi-sysroot $(WASIFLAGS) endif CXXFLAGS := $(WASIFLAGS) -std=$(CXXSTD) -Os -D_WASI_EMULATED_PROCESS_CLOCKS $(filter-out -fPIC,$(CXXFLAGS)) -LDFLAGS := $(WASIFLAGS) -Wl,-z,stack-size=1048576 $(filter-out -rdynamic,$(LDFLAGS)) -LDLIBS := -lwasi-emulated-process-clocks $(filter-out -lrt,$(LDLIBS)) +LINKFLAGS := $(WASIFLAGS) -Wl,-z,stack-size=1048576 $(filter-out -rdynamic,$(LINKFLAGS)) +LIBS := -lwasi-emulated-process-clocks $(filter-out -lrt,$(LIBS)) ABCMKARGS += AR="$(AR)" RANLIB="$(RANLIB)" ABCMKARGS += ARCHFLAGS="$(WASIFLAGS) -D_WASI_EMULATED_PROCESS_CLOCKS -DABC_USE_STDINT_H -DABC_NO_DYNAMIC_LINKING -DABC_NO_RLIMIT -Wno-c++11-narrowing" ABCMKARGS += OPTFLAGS="-Os" @@ -333,19 +333,19 @@ PKG_CONFIG = /usr/local/src/mxe/usr/bin/i686-w64-mingw32.static-pkg-config CXX = /usr/local/src/mxe/usr/bin/i686-w64-mingw32.static-g++ CXXFLAGS += -std=$(CXXSTD) -Os -D_POSIX_SOURCE -DYOSYS_MXE_HACKS -Wno-attributes CXXFLAGS := $(filter-out -fPIC,$(CXXFLAGS)) -LDFLAGS := $(filter-out -rdynamic,$(LDFLAGS)) -s -LDLIBS := $(filter-out -lrt,$(LDLIBS)) +LINKFLAGS := $(filter-out -rdynamic,$(LINKFLAGS)) -s +LIBS := $(filter-out -lrt,$(LIBS)) ABCMKARGS += ARCHFLAGS="-DWIN32_NO_DLL -DHAVE_STRUCT_TIMESPEC -fpermissive -w" # TODO: Try to solve pthread linking issue in more appropriate way -ABCMKARGS += LIBS="lib/x86/pthreadVC2.lib -s" LDFLAGS="-Wl,--allow-multiple-definition" ABC_USE_NO_READLINE=1 CC="/usr/local/src/mxe/usr/bin/i686-w64-mingw32.static-gcc" +ABCMKARGS += LIBS="lib/x86/pthreadVC2.lib -s" LINKFLAGS="-Wl,--allow-multiple-definition" ABC_USE_NO_READLINE=1 CC="/usr/local/src/mxe/usr/bin/i686-w64-mingw32.static-gcc" EXE = .exe else ifeq ($(CONFIG),msys2-32) CXX = i686-w64-mingw32-g++ CXXFLAGS += -std=$(CXXSTD) -Os -D_POSIX_SOURCE -DYOSYS_WIN32_UNIX_DIR CXXFLAGS := $(filter-out -fPIC,$(CXXFLAGS)) -LDFLAGS := $(filter-out -rdynamic,$(LDFLAGS)) -s -LDLIBS := $(filter-out -lrt,$(LDLIBS)) +LINKFLAGS := $(filter-out -rdynamic,$(LINKFLAGS)) -s +LIBS := $(filter-out -lrt,$(LIBS)) ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H -DWIN32_NO_DLL -DHAVE_STRUCT_TIMESPEC -fpermissive -w" ABCMKARGS += LIBS="-lpthread -lshlwapi -s" ABC_USE_NO_READLINE=0 CC="i686-w64-mingw32-gcc" CXX="$(CXX)" EXE = .exe @@ -354,8 +354,8 @@ else ifeq ($(CONFIG),msys2-64) CXX = x86_64-w64-mingw32-g++ CXXFLAGS += -std=$(CXXSTD) -Os -D_POSIX_SOURCE -DYOSYS_WIN32_UNIX_DIR CXXFLAGS := $(filter-out -fPIC,$(CXXFLAGS)) -LDFLAGS := $(filter-out -rdynamic,$(LDFLAGS)) -s -LDLIBS := $(filter-out -lrt,$(LDLIBS)) +LINKFLAGS := $(filter-out -rdynamic,$(LINKFLAGS)) -s +LIBS := $(filter-out -lrt,$(LIBS)) ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H -DWIN32_NO_DLL -DHAVE_STRUCT_TIMESPEC -fpermissive -w" ABCMKARGS += LIBS="-lpthread -lshlwapi -s" ABC_USE_NO_READLINE=0 CC="x86_64-w64-mingw32-gcc" CXX="$(CXX)" EXE = .exe @@ -382,9 +382,9 @@ ifeq ($(BOOST_PYTHON_LIB),) $(error BOOST_PYTHON_LIB could not be detected. Please define manually) endif -LDLIBS += $(shell $(PYTHON_CONFIG) --libs) $(BOOST_PYTHON_LIB) -lboost_system -lboost_filesystem -# python-config --ldflags includes LDLIBS for some reason -LDFLAGS += $(filter-out -l%,$(shell $(PYTHON_CONFIG) --ldflags)) +LIBS += $(shell $(PYTHON_CONFIG) --libs) $(BOOST_PYTHON_LIB) -lboost_system -lboost_filesystem +# python-config --ldflags includes LIBS for some reason +LINKFLAGS += $(filter-out -l%,$(shell $(PYTHON_CONFIG) --ldflags)) CXXFLAGS += $(shell $(PYTHON_CONFIG) --includes) -DWITH_PYTHON PY_WRAPPER_FILE = kernel/python_wrappers @@ -398,22 +398,22 @@ CXXFLAGS += -DYOSYS_ENABLE_READLINE ifeq ($(OS), $(filter $(OS),FreeBSD OpenBSD NetBSD)) CXXFLAGS += -I/usr/local/include endif -LDLIBS += -lreadline +LIBS += -lreadline ifeq ($(LINK_CURSES),1) -LDLIBS += -lcurses +LIBS += -lcurses ABCMKARGS += "ABC_READLINE_LIBRARIES=-lcurses -lreadline" endif ifeq ($(LINK_TERMCAP),1) -LDLIBS += -ltermcap +LIBS += -ltermcap ABCMKARGS += "ABC_READLINE_LIBRARIES=-lreadline -ltermcap" endif ifeq ($(CONFIG),mxe) -LDLIBS += -ltermcap +LIBS += -ltermcap endif else ifeq ($(ENABLE_EDITLINE),1) CXXFLAGS += -DYOSYS_ENABLE_EDITLINE -LDLIBS += -ledit -ltinfo -lbsd +LIBS += -ledit -ltinfo -lbsd else ABCMKARGS += "ABC_USE_NO_READLINE=1" endif @@ -432,9 +432,9 @@ CXXFLAGS += $(shell PKG_CONFIG_PATH=$(PKG_CONFIG_PATH) $(PKG_CONFIG) --silence-e ifeq ($(OS), MINGW) CXXFLAGS += -Ilibs/dlfcn-win32 endif -LDLIBS += $(shell PKG_CONFIG_PATH=$(PKG_CONFIG_PATH) $(PKG_CONFIG) --silence-errors --libs libffi || echo -lffi) +LIBS += $(shell PKG_CONFIG_PATH=$(PKG_CONFIG_PATH) $(PKG_CONFIG) --silence-errors --libs libffi || echo -lffi) ifneq ($(OS), $(filter $(OS),FreeBSD OpenBSD NetBSD MINGW)) -LDLIBS += -ldl +LIBS += -ldl endif endif @@ -444,7 +444,7 @@ endif ifeq ($(ENABLE_ZLIB),1) CXXFLAGS += -DYOSYS_ENABLE_ZLIB -LDLIBS += -lz +LIBS += -lz endif @@ -461,21 +461,21 @@ endif ifeq ($(CONFIG),mxe) CXXFLAGS += -DYOSYS_ENABLE_TCL -LDLIBS += -ltcl86 -lwsock32 -lws2_32 -lnetapi32 -lz -luserenv +LIBS += -ltcl86 -lwsock32 -lws2_32 -lnetapi32 -lz -luserenv else CXXFLAGS += $(shell PKG_CONFIG_PATH=$(PKG_CONFIG_PATH) $(PKG_CONFIG) --silence-errors --cflags tcl || echo -I$(TCL_INCLUDE)) -DYOSYS_ENABLE_TCL -LDLIBS += $(shell PKG_CONFIG_PATH=$(PKG_CONFIG_PATH) $(PKG_CONFIG) --silence-errors --libs tcl || echo $(TCL_LIBS)) +LIBS += $(shell PKG_CONFIG_PATH=$(PKG_CONFIG_PATH) $(PKG_CONFIG) --silence-errors --libs tcl || echo $(TCL_LIBS)) endif endif ifeq ($(ENABLE_GCOV),1) CXXFLAGS += --coverage -LDFLAGS += --coverage +LINKFLAGS += --coverage endif ifeq ($(ENABLE_GPROF),1) CXXFLAGS += -pg -LDFLAGS += -pg +LINKFLAGS += -pg endif ifeq ($(ENABLE_NDEBUG),1) @@ -495,7 +495,7 @@ CXXFLAGS += -DYOSYS_ENABLE_ABC ifeq ($(LINK_ABC),1) CXXFLAGS += -DYOSYS_LINK_ABC ifeq ($(DISABLE_ABC_THREADS),0) -LDLIBS += -lpthread +LIBS += -lpthread endif else ifeq ($(ABCEXTERNAL),) @@ -509,10 +509,10 @@ GHDL_PREFIX ?= $(PREFIX) GHDL_INCLUDE_DIR ?= $(GHDL_PREFIX)/include GHDL_LIB_DIR ?= $(GHDL_PREFIX)/lib CXXFLAGS += -I$(GHDL_INCLUDE_DIR) -DYOSYS_ENABLE_GHDL -LDLIBS += $(GHDL_LIB_DIR)/libghdl.a $(file <$(GHDL_LIB_DIR)/libghdl.link) +LIBS += $(GHDL_LIB_DIR)/libghdl.a $(file <$(GHDL_LIB_DIR)/libghdl.link) endif -LDLIBS_VERIFIC = +LIBS_VERIFIC = ifeq ($(ENABLE_VERIFIC),1) VERIFIC_DIR ?= /usr/local/src/verific_lib VERIFIC_COMPONENTS ?= verilog database util containers hier_tree @@ -538,9 +538,9 @@ CXXFLAGS += -DYOSYSHQ_VERIFIC_EXTENSIONS endif CXXFLAGS += $(patsubst %,-I$(VERIFIC_DIR)/%,$(VERIFIC_COMPONENTS)) -DYOSYS_ENABLE_VERIFIC ifeq ($(OS), Darwin) -LDLIBS_VERIFIC += $(foreach comp,$(patsubst %,$(VERIFIC_DIR)/%/*-mac.a,$(VERIFIC_COMPONENTS)),-Wl,-force_load $(comp)) -lz +LIBS_VERIFIC += $(foreach comp,$(patsubst %,$(VERIFIC_DIR)/%/*-mac.a,$(VERIFIC_COMPONENTS)),-Wl,-force_load $(comp)) -lz else -LDLIBS_VERIFIC += -Wl,--whole-archive $(patsubst %,$(VERIFIC_DIR)/%/*-linux.a,$(VERIFIC_COMPONENTS)) -Wl,--no-whole-archive -lz +LIBS_VERIFIC += -Wl,--whole-archive $(patsubst %,$(VERIFIC_DIR)/%/*-linux.a,$(VERIFIC_COMPONENTS)) -Wl,--no-whole-archive -lz endif endif @@ -741,13 +741,13 @@ yosys.js: $(filter-out yosysjs-$(YOSYS_VER).zip,$(EXTRA_TARGETS)) endif $(PROGRAM_PREFIX)yosys$(EXE): $(OBJS) - $(P) $(CXX) -o $(PROGRAM_PREFIX)yosys$(EXE) $(EXE_LDFLAGS) $(LDFLAGS) $(OBJS) $(LDLIBS) $(LDLIBS_VERIFIC) + $(P) $(CXX) -o $(PROGRAM_PREFIX)yosys$(EXE) $(EXE_LINKFLAGS) $(LINKFLAGS) $(OBJS) $(LIBS) $(LIBS_VERIFIC) libyosys.so: $(filter-out kernel/driver.o,$(OBJS)) ifeq ($(OS), Darwin) - $(P) $(CXX) -o libyosys.so -shared -Wl,-install_name,$(LIBDIR)/libyosys.so $(LDFLAGS) $^ $(LDLIBS) $(LDLIBS_VERIFIC) + $(P) $(CXX) -o libyosys.so -shared -Wl,-install_name,$(LIBDIR)/libyosys.so $(LINKFLAGS) $^ $(LIBS) $(LIBS_VERIFIC) else - $(P) $(CXX) -o libyosys.so -shared -Wl,-soname,$(LIBDIR)/libyosys.so $(LDFLAGS) $^ $(LDLIBS) $(LDLIBS_VERIFIC) + $(P) $(CXX) -o libyosys.so -shared -Wl,-soname,$(LIBDIR)/libyosys.so $(LINKFLAGS) $^ $(LIBS) $(LIBS_VERIFIC) endif %.o: %.cc @@ -777,15 +777,15 @@ kernel/version_$(GIT_REV).cc: $(YOSYS_SRC)/Makefile ifeq ($(ENABLE_VERIFIC),1) CXXFLAGS_NOVERIFIC = $(foreach v,$(CXXFLAGS),$(if $(findstring $(VERIFIC_DIR),$(v)),,$(v))) -LDLIBS_NOVERIFIC = $(foreach v,$(LDLIBS),$(if $(findstring $(VERIFIC_DIR),$(v)),,$(v))) +LIBS_NOVERIFIC = $(foreach v,$(LIBS),$(if $(findstring $(VERIFIC_DIR),$(v)),,$(v))) else CXXFLAGS_NOVERIFIC = $(CXXFLAGS) -LDLIBS_NOVERIFIC = $(LDLIBS) +LIBS_NOVERIFIC = $(LIBS) endif $(PROGRAM_PREFIX)yosys-config: misc/yosys-config.in $(P) $(SED) -e 's#@CXXFLAGS@#$(subst -Ilibs/dlfcn-win32,,$(subst -I. -I"$(YOSYS_SRC)",-I"$(DATDIR)/include",$(strip $(CXXFLAGS_NOVERIFIC))))#;' \ - -e 's#@CXX@#$(strip $(CXX))#;' -e 's#@LDFLAGS@#$(strip $(LDFLAGS) $(PLUGIN_LDFLAGS))#;' -e 's#@LDLIBS@#$(strip $(LDLIBS_NOVERIFIC) $(PLUGIN_LDLIBS))#;' \ + -e 's#@CXX@#$(strip $(CXX))#;' -e 's#@LINKFLAGS@#$(strip $(LINKFLAGS) $(PLUGIN_LINKFLAGS))#;' -e 's#@LIBS@#$(strip $(LIBS_NOVERIFIC) $(PLUGIN_LIBS))#;' \ -e 's#@BINDIR@#$(strip $(BINDIR))#;' -e 's#@DATDIR@#$(strip $(DATDIR))#;' < $< > $(PROGRAM_PREFIX)yosys-config $(Q) chmod +x $(PROGRAM_PREFIX)yosys-config @@ -924,7 +924,7 @@ ystests: $(TARGETS) $(EXTRA_TARGETS) # Unit test unit-test: libyosys.so @$(MAKE) -C $(UNITESTPATH) CXX="$(CXX)" CPPFLAGS="$(CPPFLAGS)" \ - CXXFLAGS="$(CXXFLAGS)" LDLIBS="$(LDLIBS)" ROOTPATH="$(CURDIR)" + CXXFLAGS="$(CXXFLAGS)" LIBS="$(LIBS)" ROOTPATH="$(CURDIR)" clean-unit-test: @$(MAKE) -C $(UNITESTPATH) clean From 4a2fb187188ad25d557df43850372dc798dcff69 Mon Sep 17 00:00:00 2001 From: Roland Coeurjoly Date: Sun, 25 Feb 2024 17:23:56 +0100 Subject: [PATCH 52/80] Changes in libs, passes and tests Makefiles. LDLIBS -> LIBS. LDFLAGS -> LINKFLAGS. CXX is clang++ or g++, not clang and gcc --- libs/ezsat/Makefile | 5 ++--- libs/subcircuit/Makefile | 11 +++++------ passes/techmap/Makefile.inc | 2 +- tests/unit/Makefile | 2 +- 4 files changed, 9 insertions(+), 11 deletions(-) diff --git a/libs/ezsat/Makefile b/libs/ezsat/Makefile index b1f864160..c41038dc9 100644 --- a/libs/ezsat/Makefile +++ b/libs/ezsat/Makefile @@ -1,9 +1,9 @@ CC = clang -CXX = clang +CXX = clang++ CXXFLAGS = -MD -Wall -Wextra -ggdb CXXFLAGS += -std=c++11 -O0 -LDLIBS = ../minisat/Options.cc ../minisat/SimpSolver.cc ../minisat/Solver.cc ../minisat/System.cc -lm -lstdc++ +LIBS = ../minisat/Options.cc ../minisat/SimpSolver.cc ../minisat/Solver.cc ../minisat/System.cc -lm -lstdc++ all: demo_vec demo_bit demo_cmp testbench puzzle3d @@ -27,4 +27,3 @@ clean: .PHONY: all test clean -include *.d - diff --git a/libs/subcircuit/Makefile b/libs/subcircuit/Makefile index f81085b5b..3d93ad0a2 100644 --- a/libs/subcircuit/Makefile +++ b/libs/subcircuit/Makefile @@ -5,9 +5,9 @@ CONFIG := clang-debug # CONFIG := release CC = clang -CXX = clang +CXX = clang++ CXXFLAGS = -MD -Wall -Wextra -ggdb -LDLIBS = -lstdc++ +LIBS = -lstdc++ ifeq ($(CONFIG),clang-debug) CXXFLAGS += -std=c++11 -O0 @@ -15,19 +15,19 @@ endif ifeq ($(CONFIG),gcc-debug) CC = gcc -CXX = gcc +CXX = g++ CXXFLAGS += -std=gnu++0x -O0 endif ifeq ($(CONFIG),profile) CC = gcc -CXX = gcc +CXX = g++ CXXFLAGS += -std=gnu++0x -Os -DNDEBUG endif ifeq ($(CONFIG),release) CC = gcc -CXX = gcc +CXX = g++ CXXFLAGS += -std=gnu++0x -march=native -O3 -DNDEBUG endif @@ -50,4 +50,3 @@ clean: .PHONY: all test clean -include *.d - diff --git a/passes/techmap/Makefile.inc b/passes/techmap/Makefile.inc index ed2f1c0bf..9d57e3d71 100644 --- a/passes/techmap/Makefile.inc +++ b/passes/techmap/Makefile.inc @@ -56,5 +56,5 @@ EXTRA_OBJS += passes/techmap/filterlib.o $(PROGRAM_PREFIX)yosys-filterlib$(EXE): passes/techmap/filterlib.o $(Q) mkdir -p $(dir $@) - $(P) $(CXX) -o $(PROGRAM_PREFIX)yosys-filterlib$(EXE) $(LDFLAGS) $^ $(LDLIBS) + $(P) $(CXX) -o $(PROGRAM_PREFIX)yosys-filterlib$(EXE) $(LINKFLAGS) $^ $(LIBS) endif diff --git a/tests/unit/Makefile b/tests/unit/Makefile index 9f1e5c99e..b4a752f8f 100644 --- a/tests/unit/Makefile +++ b/tests/unit/Makefile @@ -15,7 +15,7 @@ TESTS := $(addprefix $(BINTEST)/, $(basename $(ALLTESTFILE:%Test.cc=%Test.o))) all: prepare $(TESTS) run-tests $(BINTEST)/%: $(OBJTEST)/%.o - $(CXX) -L$(ROOTPATH) $(RPATH)=$(ROOTPATH) -o $@ $^ $(LDLIBS) \ + $(CXX) -L$(ROOTPATH) $(RPATH)=$(ROOTPATH) -o $@ $^ $(LIBS) \ $(GTESTFLAG) $(EXTRAFLAGS) $(OBJTEST)/%.o: $(basename $(subst $(OBJTEST),.,%)).cc From cf7b6c66f0d2a4b43f2d2d0ac64872969d128dc1 Mon Sep 17 00:00:00 2001 From: Roland Coeurjoly Date: Sun, 25 Feb 2024 18:35:43 +0100 Subject: [PATCH 53/80] Changes in misc/yosys-config.in. LDLIBS -> LIBS. LDFLAGS -> LINKFLAGS. --- misc/yosys-config.in | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) mode change 100644 => 100755 misc/yosys-config.in diff --git a/misc/yosys-config.in b/misc/yosys-config.in old mode 100644 new mode 100755 index f0f0f7552..04d391dbe --- a/misc/yosys-config.in +++ b/misc/yosys-config.in @@ -9,8 +9,8 @@ help() { echo "Replacement args:" echo " --cxx @CXX@" echo " --cxxflags $( echo '@CXXFLAGS@' | fmt -w60 | sed ':a;N;$!ba;s/\n/ \\\n /g' )" - echo " --ldflags @LDFLAGS@" - echo " --ldlibs @LDLIBS@" + echo " --ldflags @LINKFLAGS@" + echo " --ldlibs @LIBS@" echo " --bindir @BINDIR@" echo " --datdir @DATDIR@" echo "" @@ -64,9 +64,9 @@ for opt; do "$prefix"cxxflags) tokens=( "${tokens[@]}" @CXXFLAGS@ ) ;; "$prefix"ldflags) - tokens=( "${tokens[@]}" @LDFLAGS@ ) ;; + tokens=( "${tokens[@]}" @LINKFLAGS@ ) ;; "$prefix"ldlibs) - tokens=( "${tokens[@]}" @LDLIBS@ ) ;; + tokens=( "${tokens[@]}" @LIBS@ ) ;; "$prefix"bindir) tokens=( "${tokens[@]}" '@BINDIR@' ) ;; "$prefix"datdir) @@ -104,4 +104,3 @@ fi echo "${tokens[@]}" exit 0 - From 5fa609b6bfb3689bad7e6f78d04a2f31b8160db2 Mon Sep 17 00:00:00 2001 From: Roland Coeurjoly Date: Sun, 25 Feb 2024 18:48:21 +0100 Subject: [PATCH 54/80] Fix help of yosys-config.in and provide backward compatibility --- misc/yosys-config.in | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/misc/yosys-config.in b/misc/yosys-config.in index 04d391dbe..dd42b7c87 100755 --- a/misc/yosys-config.in +++ b/misc/yosys-config.in @@ -9,8 +9,10 @@ help() { echo "Replacement args:" echo " --cxx @CXX@" echo " --cxxflags $( echo '@CXXFLAGS@' | fmt -w60 | sed ':a;N;$!ba;s/\n/ \\\n /g' )" - echo " --ldflags @LINKFLAGS@" - echo " --ldlibs @LIBS@" + echo " --linkflags @LINKFLAGS@" + echo " --ldflags (alias of --linkflags)" + echo " --libs @LIBS@" + echo " --ldlibs (alias of --libs)" echo " --bindir @BINDIR@" echo " --datdir @DATDIR@" echo "" @@ -18,7 +20,7 @@ help() { echo "" echo "Use --exec to call a command instead of generating output. Example usage:" echo "" - echo " $0 --exec --cxx --cxxflags --ldflags -o plugin.so -shared plugin.cc --ldlibs" + echo " $0 --exec --cxx --cxxflags --ldflags -o plugin.so -shared plugin.cc --libs" echo "" echo "The above command can be abbreviated as:" echo "" @@ -44,7 +46,7 @@ fi if [ "$1" == "--build" ]; then modname="$2"; shift 2 - set -- --exec --cxx --cxxflags --ldflags -o "$modname" -shared "$@" --ldlibs + set -- --exec --cxx --cxxflags --ldflags -o "$modname" -shared "$@" --libs fi prefix="--" @@ -63,6 +65,10 @@ for opt; do tokens=( "${tokens[@]}" @CXX@ ) ;; "$prefix"cxxflags) tokens=( "${tokens[@]}" @CXXFLAGS@ ) ;; + "$prefix"linkflags) + tokens=( "${tokens[@]}" @LINKFLAGS@ ) ;; + "$prefix"libs) + tokens=( "${tokens[@]}" @LIBS@ ) ;; "$prefix"ldflags) tokens=( "${tokens[@]}" @LINKFLAGS@ ) ;; "$prefix"ldlibs) From 569a6d7fea424eae1e0331d1a0cd0c0ff1e75cd6 Mon Sep 17 00:00:00 2001 From: Catherine Date: Mon, 26 Feb 2024 09:52:12 +0000 Subject: [PATCH 55/80] cxxrtl: make blackbox `commit()` possible to override. This fixes a regression introduced when commit observers were added. --- backends/cxxrtl/cxxrtl_backend.cc | 8 +++----- backends/cxxrtl/runtime/cxxrtl/cxxrtl_replay.h | 6 ++++-- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/backends/cxxrtl/cxxrtl_backend.cc b/backends/cxxrtl/cxxrtl_backend.cc index c60b43d3f..865f0ec69 100644 --- a/backends/cxxrtl/cxxrtl_backend.cc +++ b/backends/cxxrtl/cxxrtl_backend.cc @@ -2511,14 +2511,13 @@ struct CxxrtlWorker { dump_eval_method(module); f << indent << "}\n"; f << "\n"; - f << indent << "template\n"; - f << indent << "bool commit(ObserverT &observer) {\n"; + f << indent << "virtual bool commit(observer &observer) {\n"; dump_commit_method(module); f << indent << "}\n"; f << "\n"; f << indent << "bool commit() override {\n"; f << indent << indent << "observer observer;\n"; - f << indent << indent << "return commit<>(observer);\n"; + f << indent << indent << "return commit(observer);\n"; f << indent << "}\n"; if (debug_info) { f << "\n"; @@ -3421,8 +3420,7 @@ struct CxxrtlBackend : public Backend { log(" wire<8> p_o_data;\n"); log("\n"); log(" bool eval(performer *performer) override;\n"); - log(" template\n"); - log(" bool commit(ObserverT &observer);\n"); + log(" virtual bool commit(observer &observer);\n"); log(" bool commit() override;\n"); log("\n"); log(" static std::unique_ptr\n"); diff --git a/backends/cxxrtl/runtime/cxxrtl/cxxrtl_replay.h b/backends/cxxrtl/runtime/cxxrtl/cxxrtl_replay.h index b1cd9d9a1..00d938454 100644 --- a/backends/cxxrtl/runtime/cxxrtl/cxxrtl_replay.h +++ b/backends/cxxrtl/runtime/cxxrtl/cxxrtl_replay.h @@ -556,7 +556,7 @@ public: bool record_incremental(ModuleT &module) { assert(streaming); - struct { + struct : observer { std::unordered_map *ident_lookup; spool::writer *writer; @@ -569,7 +569,9 @@ public: void on_update(size_t chunks, const chunk_t *base, const chunk_t *value, size_t index) { writer->write_change(ident_lookup->at(base), chunks, value, index); } - } record_observer = { &ident_lookup, &writer }; + } record_observer; + record_observer.ident_lookup = &ident_lookup; + record_observer.writer = &writer; writer.write_sample(/*incremental=*/true, pointer++, timestamp); for (auto input_index : inputs) { From d903f47d41cad38ab80c74095ece198afb947ae7 Mon Sep 17 00:00:00 2001 From: Catherine Date: Tue, 13 Feb 2024 18:35:15 +0000 Subject: [PATCH 56/80] write_cxxrtl: don't assert on `-noflatten` with `-g4`. --- backends/cxxrtl/cxxrtl_backend.cc | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/backends/cxxrtl/cxxrtl_backend.cc b/backends/cxxrtl/cxxrtl_backend.cc index 865f0ec69..1bd876bbc 100644 --- a/backends/cxxrtl/cxxrtl_backend.cc +++ b/backends/cxxrtl/cxxrtl_backend.cc @@ -1518,8 +1518,9 @@ struct CxxrtlWorker { } else if (is_internal_cell(cell->type)) { log_cmd_error("Unsupported internal cell `%s'.\n", cell->type.c_str()); // User cells + } else if (for_debug) { + // Outlines are called on demand when computing the value of a debug item. Nothing to do here. } else { - log_assert(!for_debug); log_assert(cell->known()); bool buffered_inputs = false; const char *access = is_cxxrtl_blackbox_cell(cell) ? "->" : "."; From 1a44645aeffac998204a05e6d12b34073f8d5ad4 Mon Sep 17 00:00:00 2001 From: Catherine Date: Tue, 13 Feb 2024 17:43:53 +0000 Subject: [PATCH 57/80] cxxrtl: expose scope information in the C++ API. This commit adds a `debug_scopes` container, which can collect metadata about scopes in a design. Currently the only scope is that of a module. A module scope can be represented either by a module and cell pair, or a `$scopeinfo` cell in a flattened netlist. The metadata produced by the C++ API is identical between these two cases, so flattening remains transparent to a netlist with CXXRTL. The existing `debug_items` method is deprecated. This isn't strictly necessary, but the user experience is better if the path is provided as e.g. `"top "` (as some VCD viewers make it awkward to select topmost anonymous scope), and the upgrade flow encourages that, which should reduce frustration later. While the new `debug_items` method could still be broken in the future as the C++ API permits, this seems unlikely since the debug information can now capture all common netlist aspects and includes several extension points (via `debug_item`, `debug_scope` types). Also, naming of scope paths was normalized to `path` or `top_path`, as applicable. --- backends/cxxrtl/cxxrtl_backend.cc | 314 ++++++++++-------- .../cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi.cc | 12 +- .../cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi.h | 4 +- backends/cxxrtl/runtime/cxxrtl/cxxrtl.h | 70 +++- .../cxxrtl/runtime/cxxrtl/cxxrtl_replay.h | 9 +- 5 files changed, 247 insertions(+), 162 deletions(-) diff --git a/backends/cxxrtl/cxxrtl_backend.cc b/backends/cxxrtl/cxxrtl_backend.cc index 1bd876bbc..877a829d3 100644 --- a/backends/cxxrtl/cxxrtl_backend.cc +++ b/backends/cxxrtl/cxxrtl_backend.cc @@ -25,6 +25,7 @@ #include "kernel/mem.h" #include "kernel/log.h" #include "kernel/fmt.h" +#include "kernel/scopeinfo.h" USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN @@ -2311,11 +2312,14 @@ struct CxxrtlWorker { dict attributes = object->attributes; // Inherently necessary to get access to the object, so a waste of space to emit. attributes.erase(ID::hdlname); + // Internal Yosys attribute that should be removed but isn't. + attributes.erase(ID::module_not_derived); dump_metadata_map(attributes); } void dump_debug_info_method(RTLIL::Module *module) { + size_t count_scopes = 0; size_t count_public_wires = 0; size_t count_member_wires = 0; size_t count_undriven = 0; @@ -2328,153 +2332,188 @@ struct CxxrtlWorker { size_t count_skipped_wires = 0; inc_indent(); f << indent << "assert(path.empty() || path[path.size() - 1] == ' ');\n"; - for (auto wire : module->wires()) { - const auto &debug_wire_type = debug_wire_types[wire]; - if (!wire->name.isPublic()) - continue; - count_public_wires++; - switch (debug_wire_type.type) { - case WireType::BUFFERED: - case WireType::MEMBER: { - // Member wire - std::vector flags; - - if (wire->port_input && wire->port_output) - flags.push_back("INOUT"); - else if (wire->port_output) - flags.push_back("OUTPUT"); - else if (wire->port_input) - flags.push_back("INPUT"); - - bool has_driven_sync = false; - bool has_driven_comb = false; - bool has_undriven = false; - if (!module->get_bool_attribute(ID(cxxrtl_blackbox))) { - for (auto bit : SigSpec(wire)) - if (!bit_has_state.count(bit)) - has_undriven = true; - else if (bit_has_state[bit]) - has_driven_sync = true; - else - has_driven_comb = true; - } else if (wire->port_output) { - switch (cxxrtl_port_type(module, wire->name)) { - case CxxrtlPortType::SYNC: - has_driven_sync = true; - break; - case CxxrtlPortType::COMB: - has_driven_comb = true; - break; - case CxxrtlPortType::UNKNOWN: - has_driven_sync = has_driven_comb = true; - break; - } - } else { - has_undriven = true; - } - if (has_undriven) - flags.push_back("UNDRIVEN"); - if (!has_driven_sync && !has_driven_comb && has_undriven) - count_undriven++; - if (has_driven_sync) - flags.push_back("DRIVEN_SYNC"); - if (has_driven_sync && !has_driven_comb && !has_undriven) - count_driven_sync++; - if (has_driven_comb) - flags.push_back("DRIVEN_COMB"); - if (!has_driven_sync && has_driven_comb && !has_undriven) - count_driven_comb++; - if (has_driven_sync + has_driven_comb + has_undriven > 1) - count_mixed_driver++; - - f << indent << "items.add(path + " << escape_cxx_string(get_hdl_name(wire)); - f << ", debug_item(" << mangle(wire) << ", " << wire->start_offset; - bool first = true; - for (auto flag : flags) { - if (first) { - first = false; - f << ", "; - } else { - f << "|"; - } - f << "debug_item::" << flag; - } - f << "), "; - dump_debug_attrs(wire); + f << indent << "if (scopes) {\n"; + inc_indent(); + // The module is responsible for adding its own scope. + f << indent << "scopes->add(path.empty() ? path : path.substr(0, path.size() - 1), "; + f << escape_cxx_string(get_hdl_name(module)) << ", "; + dump_debug_attrs(module); + f << ", std::move(cell_attrs));\n"; + count_scopes++; + // If there were any submodules that were flattened, the module is also responsible for adding them. + for (auto cell : module->cells()) { + if (cell->type != ID($scopeinfo)) continue; + if (cell->getParam(ID::TYPE).decode_string() == "module") { + auto module_attrs = scopeinfo_attributes(cell, ScopeinfoAttrs::Module); + auto cell_attrs = scopeinfo_attributes(cell, ScopeinfoAttrs::Cell); + cell_attrs.erase(ID::module_not_derived); + f << indent << "scopes->add(path + " << escape_cxx_string(get_hdl_name(cell)) << ", "; + f << escape_cxx_string(cell->get_string_attribute(ID(module))) << ", "; + dump_metadata_map(module_attrs); + f << ", "; + dump_metadata_map(cell_attrs); f << ");\n"; - count_member_wires++; - break; - } - case WireType::ALIAS: { - // Alias of a member wire - const RTLIL::Wire *aliasee = debug_wire_type.sig_subst.as_wire(); - f << indent << "items.add(path + " << escape_cxx_string(get_hdl_name(wire)); - f << ", debug_item("; - // If the aliasee is an outline, then the alias must be an outline, too; otherwise downstream - // tooling has no way to find out about the outline. - if (debug_wire_types[aliasee].is_outline()) - f << "debug_eval_outline"; - else - f << "debug_alias()"; - f << ", " << mangle(aliasee) << ", " << wire->start_offset << "), "; - dump_debug_attrs(aliasee); - f << ");\n"; - count_alias_wires++; - break; - } - case WireType::CONST: { - // Wire tied to a constant - f << indent << "static const value<" << wire->width << "> const_" << mangle(wire) << " = "; - dump_const(debug_wire_type.sig_subst.as_const()); - f << ";\n"; - f << indent << "items.add(path + " << escape_cxx_string(get_hdl_name(wire)); - f << ", debug_item(const_" << mangle(wire) << ", " << wire->start_offset << "), "; - dump_debug_attrs(wire); - f << ");\n"; - count_const_wires++; - break; - } - case WireType::OUTLINE: { - // Localized or inlined, but rematerializable wire - f << indent << "items.add(path + " << escape_cxx_string(get_hdl_name(wire)); - f << ", debug_item(debug_eval_outline, " << mangle(wire) << ", " << wire->start_offset << "), "; - dump_debug_attrs(wire); - f << ");\n"; - count_inline_wires++; - break; - } - default: { - // Localized or inlined wire with no debug information - count_skipped_wires++; - break; - } + } else log_assert(false && "Unknown $scopeinfo type"); + count_scopes++; } - } - if (!module->get_bool_attribute(ID(cxxrtl_blackbox))) { - for (auto &mem : mod_memories[module]) { - if (!mem.memid.isPublic()) + dec_indent(); + f << indent << "}\n"; + f << indent << "if (items) {\n"; + inc_indent(); + for (auto wire : module->wires()) { + const auto &debug_wire_type = debug_wire_types[wire]; + if (!wire->name.isPublic()) continue; - f << indent << "items.add(path + " << escape_cxx_string(mem.packed ? get_hdl_name(mem.cell) : get_hdl_name(mem.mem)); - f << ", debug_item(" << mangle(&mem) << ", "; - f << mem.start_offset << "), "; - if (mem.packed) { - dump_debug_attrs(mem.cell); - } else { - dump_debug_attrs(mem.mem); + count_public_wires++; + switch (debug_wire_type.type) { + case WireType::BUFFERED: + case WireType::MEMBER: { + // Member wire + std::vector flags; + + if (wire->port_input && wire->port_output) + flags.push_back("INOUT"); + else if (wire->port_output) + flags.push_back("OUTPUT"); + else if (wire->port_input) + flags.push_back("INPUT"); + + bool has_driven_sync = false; + bool has_driven_comb = false; + bool has_undriven = false; + if (!module->get_bool_attribute(ID(cxxrtl_blackbox))) { + for (auto bit : SigSpec(wire)) + if (!bit_has_state.count(bit)) + has_undriven = true; + else if (bit_has_state[bit]) + has_driven_sync = true; + else + has_driven_comb = true; + } else if (wire->port_output) { + switch (cxxrtl_port_type(module, wire->name)) { + case CxxrtlPortType::SYNC: + has_driven_sync = true; + break; + case CxxrtlPortType::COMB: + has_driven_comb = true; + break; + case CxxrtlPortType::UNKNOWN: + has_driven_sync = has_driven_comb = true; + break; + } + } else { + has_undriven = true; + } + if (has_undriven) + flags.push_back("UNDRIVEN"); + if (!has_driven_sync && !has_driven_comb && has_undriven) + count_undriven++; + if (has_driven_sync) + flags.push_back("DRIVEN_SYNC"); + if (has_driven_sync && !has_driven_comb && !has_undriven) + count_driven_sync++; + if (has_driven_comb) + flags.push_back("DRIVEN_COMB"); + if (!has_driven_sync && has_driven_comb && !has_undriven) + count_driven_comb++; + if (has_driven_sync + has_driven_comb + has_undriven > 1) + count_mixed_driver++; + + f << indent << "items->add(path + " << escape_cxx_string(get_hdl_name(wire)); + f << ", debug_item(" << mangle(wire) << ", " << wire->start_offset; + bool first = true; + for (auto flag : flags) { + if (first) { + first = false; + f << ", "; + } else { + f << "|"; + } + f << "debug_item::" << flag; + } + f << "), "; + dump_debug_attrs(wire); + f << ");\n"; + count_member_wires++; + break; + } + case WireType::ALIAS: { + // Alias of a member wire + const RTLIL::Wire *aliasee = debug_wire_type.sig_subst.as_wire(); + f << indent << "items->add(path + " << escape_cxx_string(get_hdl_name(wire)); + f << ", debug_item("; + // If the aliasee is an outline, then the alias must be an outline, too; otherwise downstream + // tooling has no way to find out about the outline. + if (debug_wire_types[aliasee].is_outline()) + f << "debug_eval_outline"; + else + f << "debug_alias()"; + f << ", " << mangle(aliasee) << ", " << wire->start_offset << "), "; + dump_debug_attrs(aliasee); + f << ");\n"; + count_alias_wires++; + break; + } + case WireType::CONST: { + // Wire tied to a constant + f << indent << "static const value<" << wire->width << "> const_" << mangle(wire) << " = "; + dump_const(debug_wire_type.sig_subst.as_const()); + f << ";\n"; + f << indent << "items->add(path + " << escape_cxx_string(get_hdl_name(wire)); + f << ", debug_item(const_" << mangle(wire) << ", " << wire->start_offset << "), "; + dump_debug_attrs(wire); + f << ");\n"; + count_const_wires++; + break; + } + case WireType::OUTLINE: { + // Localized or inlined, but rematerializable wire + f << indent << "items->add(path + " << escape_cxx_string(get_hdl_name(wire)); + f << ", debug_item(debug_eval_outline, " << mangle(wire) << ", " << wire->start_offset << "), "; + dump_debug_attrs(wire); + f << ");\n"; + count_inline_wires++; + break; + } + default: { + // Localized or inlined wire with no debug information + count_skipped_wires++; + break; + } } - f << ");\n"; } + if (!module->get_bool_attribute(ID(cxxrtl_blackbox))) { + for (auto &mem : mod_memories[module]) { + if (!mem.memid.isPublic()) + continue; + f << indent << "items->add(path + " << escape_cxx_string(mem.packed ? get_hdl_name(mem.cell) : get_hdl_name(mem.mem)); + f << ", debug_item(" << mangle(&mem) << ", "; + f << mem.start_offset << "), "; + if (mem.packed) { + dump_debug_attrs(mem.cell); + } else { + dump_debug_attrs(mem.mem); + } + f << ");\n"; + } + } + dec_indent(); + f << indent << "}\n"; + if (!module->get_bool_attribute(ID(cxxrtl_blackbox))) { for (auto cell : module->cells()) { if (is_internal_cell(cell->type)) continue; const char *access = is_cxxrtl_blackbox_cell(cell) ? "->" : "."; - f << indent << mangle(cell) << access << "debug_info(items, "; - f << "path + " << escape_cxx_string(get_hdl_name(cell) + ' ') << ");\n"; + f << indent << mangle(cell) << access; + f << "debug_info(items, scopes, path + " << escape_cxx_string(get_hdl_name(cell) + ' ') << ", "; + dump_debug_attrs(cell); + f << ");\n"; } } dec_indent(); log_debug("Debug information statistics for module `%s':\n", log_id(module)); + log_debug(" Scopes: %zu", count_scopes); log_debug(" Public wires: %zu, of which:\n", count_public_wires); log_debug(" Member wires: %zu, of which:\n", count_member_wires); log_debug(" Undriven: %zu (incl. inputs)\n", count_undriven); @@ -2522,7 +2561,8 @@ struct CxxrtlWorker { f << indent << "}\n"; if (debug_info) { f << "\n"; - f << indent << "void debug_info(debug_items &items, std::string path = \"\") override {\n"; + f << indent << "void debug_info(debug_items *items, debug_scopes *scopes, " + << "std::string path, metadata_map &&cell_attrs = {}) override {\n"; dump_debug_info_method(module); f << indent << "}\n"; } @@ -2631,7 +2671,8 @@ struct CxxrtlWorker { } } f << "\n"; - f << indent << "void debug_info(debug_items &items, std::string path = \"\") override;\n"; + f << indent << "void debug_info(debug_items *items, debug_scopes *scopes, " + << "std::string path, metadata_map &&cell_attrs = {}) override;\n"; } dec_indent(); f << indent << "}; // struct " << mangle(module) << "\n"; @@ -2659,7 +2700,8 @@ struct CxxrtlWorker { } f << "\n"; f << indent << "CXXRTL_EXTREMELY_COLD\n"; - f << indent << "void " << mangle(module) << "::debug_info(debug_items &items, std::string path) {\n"; + f << indent << "void " << mangle(module) << "::debug_info(debug_items *items, debug_scopes *scopes, " + << "std::string path, metadata_map &&cell_attrs) {\n"; dump_debug_info_method(module); f << indent << "}\n"; } diff --git a/backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi.cc b/backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi.cc index 593e067a1..3c62401dd 100644 --- a/backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi.cc +++ b/backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi.cc @@ -35,19 +35,19 @@ cxxrtl_handle cxxrtl_create(cxxrtl_toplevel design) { return cxxrtl_create_at(design, ""); } -cxxrtl_handle cxxrtl_create_at(cxxrtl_toplevel design, const char *root) { - std::string path = root; - if (!path.empty()) { +cxxrtl_handle cxxrtl_create_at(cxxrtl_toplevel design, const char *top_path_) { + std::string top_path = top_path_; + if (!top_path.empty()) { // module::debug_info() accepts either an empty path, or a path ending in space to simplify // the logic in generated code. While this is sketchy at best to expose in the C++ API, this // would be a lot worse in the C API, so don't expose it here. - assert(path.back() != ' '); - path += ' '; + assert(top_path.back() != ' '); + top_path += ' '; } cxxrtl_handle handle = new _cxxrtl_handle; handle->module = std::move(design->module); - handle->module->debug_info(handle->objects, path); + handle->module->debug_info(handle->objects, top_path); delete design; return handle; } diff --git a/backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi.h b/backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi.h index c2a9d37e1..ae42733ad 100644 --- a/backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi.h +++ b/backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi.h @@ -55,8 +55,8 @@ cxxrtl_handle cxxrtl_create(cxxrtl_toplevel design); // Create a design handle at a given hierarchy position from a design toplevel. // // This operation is similar to `cxxrtl_create`, except the full hierarchical name of every object -// is prepended with `root`. -cxxrtl_handle cxxrtl_create_at(cxxrtl_toplevel design, const char *root); +// is prepended with `top_path`. +cxxrtl_handle cxxrtl_create_at(cxxrtl_toplevel design, const char *top_path); // Release all resources used by a design and its handle. void cxxrtl_destroy(cxxrtl_handle handle); diff --git a/backends/cxxrtl/runtime/cxxrtl/cxxrtl.h b/backends/cxxrtl/runtime/cxxrtl/cxxrtl.h index f9d22ff9b..b834cd120 100644 --- a/backends/cxxrtl/runtime/cxxrtl/cxxrtl.h +++ b/backends/cxxrtl/runtime/cxxrtl/cxxrtl.h @@ -1331,14 +1331,15 @@ struct debug_items { std::map> table; std::map> attrs_table; - void add(const std::string &name, debug_item &&item, metadata_map &&item_attrs = {}) { - std::unique_ptr &attrs = attrs_table[name]; + void add(const std::string &path, debug_item &&item, metadata_map &&item_attrs = {}) { + assert((path.empty() || path[path.size() - 1] != ' ') && path.find(" ") == std::string::npos); + std::unique_ptr &attrs = attrs_table[path]; if (attrs.get() == nullptr) attrs = std::unique_ptr(new debug_attrs); for (auto attr : item_attrs) attrs->map.insert(attr); item.attrs = attrs.get(); - std::vector &parts = table[name]; + std::vector &parts = table[path]; parts.emplace_back(item); std::sort(parts.begin(), parts.end(), [](const debug_item &a, const debug_item &b) { @@ -1346,25 +1347,58 @@ struct debug_items { }); } - size_t count(const std::string &name) const { - if (table.count(name) == 0) + size_t count(const std::string &path) const { + if (table.count(path) == 0) return 0; - return table.at(name).size(); + return table.at(path).size(); } - const std::vector &at(const std::string &name) const { - return table.at(name); + const std::vector &at(const std::string &path) const { + return table.at(path); } // Like `at()`, but operates only on single-part debug items. - const debug_item &operator [](const std::string &name) const { - const std::vector &parts = table.at(name); + const debug_item &operator [](const std::string &path) const { + const std::vector &parts = table.at(path); assert(parts.size() == 1); return parts.at(0); } - const metadata_map &attrs(const std::string &name) const { - return attrs_table.at(name)->map; + bool is_memory(const std::string &path) const { + return at(path).at(0).type == debug_item::MEMORY; + } + + const metadata_map &attrs(const std::string &path) const { + return attrs_table.at(path)->map; + } +}; + +// Only `module` scopes are defined. The type is implicit, since Yosys does not currently support +// any other scope types. +struct debug_scope { + std::string module_name; + std::unique_ptr module_attrs; + std::unique_ptr cell_attrs; +}; + +struct debug_scopes { + std::map table; + + void add(const std::string &path, const std::string &module_name, metadata_map &&module_attrs, metadata_map &&cell_attrs) { + assert((path.empty() || path[path.size() - 1] != ' ') && path.find(" ") == std::string::npos); + assert(table.count(path) == 0); + debug_scope &scope = table[path]; + scope.module_name = module_name; + scope.module_attrs = std::unique_ptr(new debug_attrs { module_attrs }); + scope.cell_attrs = std::unique_ptr(new debug_attrs { cell_attrs }); + } + + size_t contains(const std::string &path) const { + return table.count(path); + } + + const debug_scope &operator [](const std::string &path) const { + return table.at(path); } }; @@ -1412,8 +1446,16 @@ struct module { return deltas; } - virtual void debug_info(debug_items &items, std::string path = "") { - (void)items, (void)path; + virtual void debug_info(debug_items *items, debug_scopes *scopes, std::string path, metadata_map &&cell_attrs = {}) { + (void)items, (void)scopes, (void)path, (void)cell_attrs; + } + + // Compatibility method. +#if __has_attribute(deprecated) + __attribute__((deprecated("Use `debug_info(path, &items, /*scopes=*/nullptr);` instead. (`path` could be \"top \".)"))) +#endif + void debug_info(debug_items &items, std::string path) { + debug_info(&items, /*scopes=*/nullptr, path); } }; diff --git a/backends/cxxrtl/runtime/cxxrtl/cxxrtl_replay.h b/backends/cxxrtl/runtime/cxxrtl/cxxrtl_replay.h index 00d938454..454895a1f 100644 --- a/backends/cxxrtl/runtime/cxxrtl/cxxrtl_replay.h +++ b/backends/cxxrtl/runtime/cxxrtl/cxxrtl_replay.h @@ -491,9 +491,9 @@ public: template recorder(Args &&...args) : writer(std::forward(args)...) {} - void start(module &module) { + void start(module &module, std::string top_path = "") { debug_items items; - module.debug_info(items); + module.debug_info(&items, /*scopes=*/nullptr, top_path); start(items); } @@ -621,9 +621,10 @@ public: template player(Args &&...args) : reader(std::forward(args)...) {} - void start(module &module) { + // The `top_path` must match the one given to the recorder. + void start(module &module, std::string top_path = "") { debug_items items; - module.debug_info(items); + module.debug_info(&items, /*scopes=*/nullptr, top_path); start(items); } From dd11a5a37c8f000dadddb5ea778289408f43dd0f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Povi=C5=A1er?= Date: Mon, 26 Feb 2024 16:25:46 +0100 Subject: [PATCH 58/80] Shrink further --- kernel/yosys.cc | 2 -- 1 file changed, 2 deletions(-) diff --git a/kernel/yosys.cc b/kernel/yosys.cc index 444f597ca..20f9791c6 100644 --- a/kernel/yosys.cc +++ b/kernel/yosys.cc @@ -142,9 +142,7 @@ void yosys_banner() log(" | Copyright (C) 2012 - 2024 Claire Xenia Wolf |\n"); log(" | Distributed under an ISC-like license, type \"license\" to see terms |\n"); log(" \\----------------------------------------------------------------------------/\n"); - log("\n"); log(" %s\n", yosys_version_str); - log("\n"); } int ceil_log2(int x) From da2e9386f02913fb8f15618f790242973ceed809 Mon Sep 17 00:00:00 2001 From: Catherine Date: Mon, 26 Feb 2024 16:06:25 +0000 Subject: [PATCH 59/80] cxxrtl: install `cxxrtl_time.h` and `cxxrtl_replay.h`. --- Makefile | 6 ------ backends/cxxrtl/Makefile.inc | 9 +++++++++ 2 files changed, 9 insertions(+), 6 deletions(-) diff --git a/Makefile b/Makefile index e55388159..8fdaa0ee7 100644 --- a/Makefile +++ b/Makefile @@ -637,12 +637,6 @@ $(eval $(call add_include_file,frontends/ast/ast.h)) $(eval $(call add_include_file,frontends/ast/ast_binding.h)) $(eval $(call add_include_file,frontends/blif/blifparse.h)) $(eval $(call add_include_file,backends/rtlil/rtlil_backend.h)) -$(eval $(call add_include_file,backends/cxxrtl/runtime/cxxrtl/cxxrtl.h)) -$(eval $(call add_include_file,backends/cxxrtl/runtime/cxxrtl/cxxrtl_vcd.h)) -$(eval $(call add_include_file,backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi.cc)) -$(eval $(call add_include_file,backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi.h)) -$(eval $(call add_include_file,backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi_vcd.cc)) -$(eval $(call add_include_file,backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi_vcd.h)) OBJS += kernel/driver.o kernel/register.o kernel/rtlil.o kernel/log.o kernel/calc.o kernel/yosys.o OBJS += kernel/binding.o diff --git a/backends/cxxrtl/Makefile.inc b/backends/cxxrtl/Makefile.inc index aaa304502..dd77d2ad3 100644 --- a/backends/cxxrtl/Makefile.inc +++ b/backends/cxxrtl/Makefile.inc @@ -1,2 +1,11 @@ OBJS += backends/cxxrtl/cxxrtl_backend.o + +$(eval $(call add_include_file,backends/cxxrtl/runtime/cxxrtl/cxxrtl.h)) +$(eval $(call add_include_file,backends/cxxrtl/runtime/cxxrtl/cxxrtl_vcd.h)) +$(eval $(call add_include_file,backends/cxxrtl/runtime/cxxrtl/cxxrtl_time.h)) +$(eval $(call add_include_file,backends/cxxrtl/runtime/cxxrtl/cxxrtl_replay.h)) +$(eval $(call add_include_file,backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi.cc)) +$(eval $(call add_include_file,backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi.h)) +$(eval $(call add_include_file,backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi_vcd.cc)) +$(eval $(call add_include_file,backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi_vcd.h)) From 91fbd58980e87ad5dc0a5d37c049ffaf5ab243dd Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Tue, 27 Feb 2024 00:15:58 +0000 Subject: [PATCH 60/80] Bump version --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 8fdaa0ee7..c4b46cc13 100644 --- a/Makefile +++ b/Makefile @@ -141,7 +141,7 @@ LIBS += -lrt endif endif -YOSYS_VER := 0.38+92 +YOSYS_VER := 0.38+113 # Note: We arrange for .gitcommit to contain the (short) commit hash in # tarballs generated with git-archive(1) using .gitattributes. The git repo From d2a7ce04ea5a5bd6d3324e3ec81c3ede0ceab5d9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Povi=C5=A1er?= Date: Fri, 1 Mar 2024 10:54:51 +0100 Subject: [PATCH 61/80] synth: Rename `-inject` to `-extra-map` --- techlibs/common/synth.cc | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/techlibs/common/synth.cc b/techlibs/common/synth.cc index 7da9ba666..68be34f20 100644 --- a/techlibs/common/synth.cc +++ b/techlibs/common/synth.cc @@ -88,8 +88,8 @@ struct SynthPass : public ScriptPass { log(" read/write collision\" (same result as setting the no_rw_check\n"); log(" attribute on all memories).\n"); log("\n"); - log(" -inject filename\n"); - log(" inject rules from the given file to complement the default\n"); + log(" -extra-map filename\n"); + log(" source extra rules from the given file to complement the default\n"); log(" mapping library in the `techmap` step. this option can be\n"); log(" repeated.\n"); log("\n"); @@ -101,7 +101,7 @@ struct SynthPass : public ScriptPass { string top_module, fsm_opts, memory_opts, abc; bool autotop, flatten, noalumacc, nofsm, noabc, noshare, flowmap, booth; int lut; - std::vector techmap_inject; + std::vector techmap_maps; void clear_flags() override { @@ -119,7 +119,7 @@ struct SynthPass : public ScriptPass { flowmap = false; booth = false; abc = "abc"; - techmap_inject.clear(); + techmap_maps.clear(); } void execute(std::vector args, RTLIL::Design *design) override @@ -197,8 +197,8 @@ struct SynthPass : public ScriptPass { memory_opts += " -no-rw-check"; continue; } - if (args[argidx] == "-inject" && argidx + 1 < args.size()) { - techmap_inject.push_back(args[++argidx]); + if (args[argidx] == "-extra-map" && argidx + 1 < args.size()) { + techmap_maps.push_back(args[++argidx]); continue; } break; @@ -275,9 +275,9 @@ struct SynthPass : public ScriptPass { run("techmap -map +/techmap.v -map ", " (if -inject)"); } else { std::string techmap_opts; - if (!techmap_inject.empty()) + if (!techmap_maps.empty()) techmap_opts += " -map +/techmap.v"; - for (auto fn : techmap_inject) + for (auto fn : techmap_maps) techmap_opts += stringf(" -map %s", fn.c_str()); run("techmap" + techmap_opts); } From a02d4e78531550b4ff658aa6fff8806f05715330 Mon Sep 17 00:00:00 2001 From: Jason Thorpe Date: Sun, 3 Mar 2024 07:54:39 -0800 Subject: [PATCH 62/80] Tweak the FreeBSD version of proc_self_dirname() to work on NetBSD use it. --- kernel/yosys.cc | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/kernel/yosys.cc b/kernel/yosys.cc index 20f9791c6..57433d0d9 100644 --- a/kernel/yosys.cc +++ b/kernel/yosys.cc @@ -55,7 +55,7 @@ # include #endif -#ifdef __FreeBSD__ +#if defined(__FreeBSD__) || defined(__NetBSD__) # include #endif @@ -901,10 +901,14 @@ std::string proc_self_dirname() buflen--; return std::string(path, buflen); } -#elif defined(__FreeBSD__) +#elif defined(__FreeBSD__) || defined(__NetBSD__) std::string proc_self_dirname() { +#ifdef __NetBSD__ + int mib[4] = {CTL_KERN, KERN_PROC_ARGS, getpid(), KERN_PROC_PATHNAME}; +#else int mib[4] = {CTL_KERN, KERN_PROC, KERN_PROC_PATHNAME, -1}; +#endif size_t buflen; char *buffer; std::string path; From 9b47f3204ee349650d3cb9fb894efe9d9b9cea48 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Mon, 4 Mar 2024 12:28:41 +1300 Subject: [PATCH 63/80] Makefile: Fix emcc build Remove deprecated (and unnecessary?) `--memory-init-file 0` from `EMCC_LINKFLAGS`. --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index c4b46cc13..9e9cc7116 100644 --- a/Makefile +++ b/Makefile @@ -267,7 +267,7 @@ CXX = emcc CXXFLAGS := -std=$(CXXSTD) $(filter-out -fPIC -ggdb,$(CXXFLAGS)) ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H -DABC_MEMALIGN=8 -Wno-c++11-narrowing" EMCC_CXXFLAGS := -Os -Wno-warn-absolute-paths -EMCC_LINKFLAGS := --memory-init-file 0 --embed-file share +EMCC_LINKFLAGS := --embed-file share EMCC_LINKFLAGS += -s NO_EXIT_RUNTIME=1 EMCC_LINKFLAGS += -s EXPORTED_FUNCTIONS="['_main','_run','_prompt','_errmsg','_memset']" EMCC_LINKFLAGS += -s TOTAL_MEMORY=134217728 From 6469d90293b465201c9903f2dc1d02045cc33bcd Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Wed, 7 Feb 2024 18:39:32 +0100 Subject: [PATCH 64/80] write_aiger: Include `$assert` and `$assume` cells in -ywmap output --- backends/aiger/aiger.cc | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc index fe4f7681d..f2cb5d9bc 100644 --- a/backends/aiger/aiger.cc +++ b/backends/aiger/aiger.cc @@ -67,6 +67,8 @@ struct AigerWriter int initstate_ff = 0; dict ywmap_clocks; + vector ywmap_asserts; + vector ywmap_assumes; int mkgate(int a0, int a1) { @@ -269,6 +271,7 @@ struct AigerWriter unused_bits.erase(A); unused_bits.erase(EN); asserts.push_back(make_pair(A, EN)); + ywmap_asserts.push_back(cell); continue; } @@ -279,6 +282,7 @@ struct AigerWriter unused_bits.erase(A); unused_bits.erase(EN); assumes.push_back(make_pair(A, EN)); + ywmap_assumes.push_back(cell); continue; } @@ -852,6 +856,19 @@ struct AigerWriter for (auto &it : init_lines) json.value(it.second); json.end_array(); + + json.name("asserts"); + json.begin_array(); + for (Cell *cell : ywmap_asserts) + json.value(witness_path(cell)); + json.end_array(); + + json.name("assumes"); + json.begin_array(); + for (Cell *cell : ywmap_assumes) + json.value(witness_path(cell)); + json.end_array(); + json.end_object(); } From d8cdc213a64de682952af6f5dc9a12bb2d3f54a4 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 27 Feb 2024 19:56:47 +0100 Subject: [PATCH 65/80] rename -witness: Bug fix and rename formal cells Rename formal cells in addition to witness signals. This is required to reliably track individual property states for the non-smtbmc flows. Also removes a misplced `break` which resulted in only partial witness renaming. --- backends/smt2/smt2.cc | 13 ++++++++++++- passes/cmds/rename.cc | 15 ++++++++++++++- 2 files changed, 26 insertions(+), 2 deletions(-) diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index 5e63e6237..c702d5e7e 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -1117,7 +1117,18 @@ struct Smt2Worker string name_a = get_bool(cell->getPort(ID::A)); string name_en = get_bool(cell->getPort(ID::EN)); - if (cell->name[0] == '$' && cell->attributes.count(ID::src)) + bool private_name = cell->name[0] == '$'; + + if (!private_name && cell->has_attribute(ID::hdlname)) { + for (auto const &part : cell->get_hdlname_attribute()) { + if (part == "_witness_") { + private_name = true; + break; + } + } + } + + if (private_name && cell->attributes.count(ID::src)) decls.push_back(stringf("; yosys-smt2-%s %d %s %s\n", cell->type.c_str() + 1, id, get_id(cell), cell->attributes.at(ID::src).decode_string().c_str())); else decls.push_back(stringf("; yosys-smt2-%s %d %s\n", cell->type.c_str() + 1, id, get_id(cell))); diff --git a/passes/cmds/rename.cc b/passes/cmds/rename.cc index da4ba2f17..3f8d807b3 100644 --- a/passes/cmds/rename.cc +++ b/passes/cmds/rename.cc @@ -134,7 +134,6 @@ static bool rename_witness(RTLIL::Design *design, dict &ca cell->set_hdlname_attribute({ "_witness_", strstr(new_id.c_str(), ".") + 1 }); renames.emplace_back(cell, new_id); } - break; } if (cell->type.in(ID($anyconst), ID($anyseq), ID($anyinit), ID($allconst), ID($allseq))) { @@ -165,6 +164,20 @@ static bool rename_witness(RTLIL::Design *design, dict &ca } } } + + + if (cell->type.in(ID($assert), ID($assume), ID($cover), ID($live), ID($fair), ID($check))) { + has_witness_signals = true; + if (cell->name.isPublic()) + continue; + std::string name = stringf("%s_%s", cell->type.c_str() + 1, cell->name.c_str() + 1); + for (auto &c : name) + if ((c < 'a' || c > 'z') && (c < 'A' || c > 'Z') && (c < '0' || c > '9') && c != '_') + c = '_'; + auto new_id = module->uniquify("\\_witness_." + name); + renames.emplace_back(cell, new_id); + cell->set_hdlname_attribute({ "_witness_", strstr(new_id.c_str(), ".") + 1 }); + } } for (auto rename : renames) { module->rename(rename.first, rename.second); From d03c5e2a00fc1fbb485bdd99bdb264658e316058 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Wed, 21 Feb 2024 16:35:17 +0100 Subject: [PATCH 66/80] smtbmc: Break dependency recursion during unrolling Previously `unroll_stmt` would recurse over the smtlib expressions as well as recursively follow not-yet-emitted definitions the current expression depends on. While the depth of smtlib expressions generated by yosys seems to be reasonably bounded, the dependency chain of not-yet-emitted definitions can grow linearly with the size of the design and linearly in the BMC depth. This makes `unroll_stmt` use a `list` as stack, using python generators and `recursion_helper` function to keep the overall code structure of the previous recursive implementation. --- backends/smt2/smtio.py | 45 ++++++++++++++++++++++++++++++++++++------ 1 file changed, 39 insertions(+), 6 deletions(-) diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index ebf364f06..c904aea95 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -79,6 +79,20 @@ def except_hook(exctype, value, traceback): sys.excepthook = except_hook +def recursion_helper(iteration, *request): + stack = [iteration(*request)] + + while stack: + top = stack.pop() + try: + request = next(top) + except StopIteration: + continue + + stack.append(top) + stack.append(iteration(*request)) + + hex_dict = { "0": "0000", "1": "0001", "2": "0010", "3": "0011", "4": "0100", "5": "0101", "6": "0110", "7": "0111", @@ -298,10 +312,22 @@ class SmtIo: return stmt def unroll_stmt(self, stmt): - if not isinstance(stmt, list): - return stmt + result = [] + recursion_helper(self._unroll_stmt_into, stmt, result) + return result.pop() - stmt = [self.unroll_stmt(s) for s in stmt] + def _unroll_stmt_into(self, stmt, output, depth=128): + if not isinstance(stmt, list): + output.append(stmt) + return + + new_stmt = [] + for s in stmt: + if depth: + yield from self._unroll_stmt_into(s, new_stmt, depth - 1) + else: + yield s, new_stmt + stmt = new_stmt if len(stmt) >= 2 and not isinstance(stmt[0], list) and stmt[0] in self.unroll_decls: assert stmt[1] in self.unroll_objs @@ -330,12 +356,19 @@ class SmtIo: decl[2] = list() if len(decl) > 0: - decl = self.unroll_stmt(decl) + tmp = [] + if depth: + yield from self._unroll_stmt_into(decl, tmp, depth - 1) + else: + yield decl, tmp + + decl = tmp.pop() self.write(self.unparse(decl), unroll=False) - return self.unroll_cache[key] + output.append(self.unroll_cache[key]) + return - return stmt + output.append(stmt) def p_thread_main(self): while True: From 97db1cb7459af0b07dc8d074b2344c35ef1cc570 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Wed, 21 Feb 2024 16:33:14 +0100 Subject: [PATCH 67/80] smtbmc: Cache hierarchy for loading multiple yw files This will be used by sby/tools/cexenum via the incremental interface. --- backends/smt2/smtbmc.py | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index 34657be26..cc47bc376 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -649,14 +649,20 @@ if aimfile is not None: num_steps = max(num_steps, step+2) step += 1 +ywfile_hierwitness_cache = None + def ywfile_constraints(inywfile, constr_assumes, map_steps=None, skip_x=False): + global ywfile_hierwitness_cache if map_steps is None: map_steps = {} with open(inywfile, "r") as f: inyw = ReadWitness(f) - inits, seqs, clocks, mems = smt.hierwitness(topmod, allregs=True, blackbox=True) + if ywfile_hierwitness_cache is None: + ywfile_hierwitness_cache = smt.hierwitness(topmod, allregs=True, blackbox=True) + + inits, seqs, clocks, mems = ywfile_hierwitness_cache smt_wires = defaultdict(list) smt_mems = defaultdict(list) From ff6c29ab1e97c28e5d734d85b14901b0b42a02a1 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Mon, 4 Mar 2024 16:52:11 +0100 Subject: [PATCH 68/80] Update abc revision --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index e55388159..6375f116a 100644 --- a/Makefile +++ b/Makefile @@ -165,7 +165,7 @@ bumpversion: # is just a symlink to your actual ABC working directory, as 'make mrproper' # will remove the 'abc' directory and you do not want to accidentally # delete your work on ABC.. -ABCREV = 896e5e7 +ABCREV = 0cd90d0 ABCPULL = 1 ABCURL ?= https://github.com/YosysHQ/abc ABCMKARGS = CC="$(CXX)" CXX="$(CXX)" ABC_USE_LIBSTDCXX=1 ABC_USE_NAMESPACE=abc VERBOSE=$(Q) From 1e42b4f0f9cc1d2f4097ea632a93be3473b0c2f7 Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Tue, 5 Mar 2024 00:15:21 +0000 Subject: [PATCH 69/80] Bump version --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 9e9cc7116..2539d5caa 100644 --- a/Makefile +++ b/Makefile @@ -141,7 +141,7 @@ LIBS += -lrt endif endif -YOSYS_VER := 0.38+113 +YOSYS_VER := 0.38+120 # Note: We arrange for .gitcommit to contain the (short) commit hash in # tarballs generated with git-archive(1) using .gitattributes. The git repo From 0db76c6ec40cea5c8071f7e0fbda88dc21e824a2 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 5 Mar 2024 14:37:33 +0100 Subject: [PATCH 70/80] tests/sva: Skip sva tests that use SBY until SBY is compatible again This commit is part of a PR that requires corresponding changes in SBY. To prevent CI failures, detect whether those changes already landed and skip the SBY using tests until then. --- tests/sva/runtest.sh | 25 +++++++++++++++++++++---- 1 file changed, 21 insertions(+), 4 deletions(-) diff --git a/tests/sva/runtest.sh b/tests/sva/runtest.sh index 84e797390..7692a5f9a 100644 --- a/tests/sva/runtest.sh +++ b/tests/sva/runtest.sh @@ -1,6 +1,6 @@ #!/usr/bin/env bash -set -ex +set -e prefix=${1%.ok} prefix=${prefix%.sv} @@ -58,16 +58,33 @@ generate_sby() { } if [ -f $prefix.ys ]; then + set -x $PWD/../../yosys -q -e "Assert .* failed." -s $prefix.ys elif [ -f $prefix.sv ]; then generate_sby pass > ${prefix}_pass.sby generate_sby fail > ${prefix}_fail.sby - sby --yosys $PWD/../../yosys -f ${prefix}_pass.sby - sby --yosys $PWD/../../yosys -f ${prefix}_fail.sby + + # Check that SBY is up to date enough for this yosys version + if sby --help | grep -q -e '--status'; then + set -x + sby --yosys $PWD/../../yosys -f ${prefix}_pass.sby + sby --yosys $PWD/../../yosys -f ${prefix}_fail.sby + else + echo "sva test '${prefix}' requires an up to date SBY, skipping" + fi else generate_sby pass > ${prefix}.sby - sby --yosys $PWD/../../yosys -f ${prefix}.sby + + # Check that SBY is up to date enough for this yosys version + if sby --help | grep -q -e '--status'; then + set -x + sby --yosys $PWD/../../yosys -f ${prefix}.sby + else + echo "sva test '${prefix}' requires an up to date SBY, skipping" + fi fi +{ set +x; } &>/dev/null + touch $prefix.ok From f60b77a7f01ebffe57a5d74e2e7a42e0dbf449e3 Mon Sep 17 00:00:00 2001 From: Catherine Date: Tue, 5 Mar 2024 16:21:12 +0000 Subject: [PATCH 71/80] cxxrtl: add ability to record/replay diagnostics. Note that this functionality is only used by diagnostics emitted by the C++ testbench; diagnostics emitted by the RTL in `eval()` do not need to be recorded since they will be emitted again during replay. --- .../cxxrtl/runtime/cxxrtl/cxxrtl_replay.h | 128 +++++++++++++++--- 1 file changed, 107 insertions(+), 21 deletions(-) diff --git a/backends/cxxrtl/runtime/cxxrtl/cxxrtl_replay.h b/backends/cxxrtl/runtime/cxxrtl/cxxrtl_replay.h index 454895a1f..b8233b007 100644 --- a/backends/cxxrtl/runtime/cxxrtl/cxxrtl_replay.h +++ b/backends/cxxrtl/runtime/cxxrtl/cxxrtl_replay.h @@ -49,11 +49,16 @@ // ::= + // ::= 0x52585843 0x00004c54 // ::= * -// ::= * +// ::= ( | )* // ::= 0xc0000000 ... // ::= 0xc0000001 ... // ::= 0x0??????? + | 0x1??????? + | 0x2??????? | 0x3??????? // , ::= 0x???????? +// ::= | | | +// ::= 0xc0000010 +// ::= 0xc0000011 +// ::= 0xc0000012 +// ::= 0xc0000013 // ::= 0xFFFFFFFF // // The replay log contains sample data, however, it does not cover the entire design. Rather, it only contains sample @@ -61,6 +66,10 @@ // a minimum, and recording speed to a maximum. The player samples any missing data by setting the design state items // to the same values they had during recording, and re-evaluating the design. // +// Packets for diagnostics (prints, breakpoints, assertions, and assumptions) are used solely for diagnostics emitted +// by the C++ testbench driving the simulation, and are not recorded while evaluating the design. (Diagnostics emitted +// by the RTL can be reconstructed at replay time, so recording them would be a waste of space.) +// // Limits // ------ // @@ -109,6 +118,33 @@ namespace cxxrtl { +// A single diagnostic that can be manipulated as an object (including being written to and read from a file). +// This differs from the base CXXRTL interface, where diagnostics can only be emitted via a procedure call, and are +// not materialized as objects. +struct diagnostic { + // The `BREAK` flavor corresponds to a breakpoint, which is a diagnostic type that can currently only be emitted + // by the C++ testbench code. + enum flavor { + BREAK = 0, + PRINT = 1, + ASSERT = 2, + ASSUME = 3, + }; + + flavor type; + std::string message; + std::string location; // same format as the `src` attribute of `$print` or `$check` cell + + diagnostic() + : type(BREAK) {} + + diagnostic(flavor type, const std::string &message, const std::string &location) + : type(type), message(message), location(location) {} + + diagnostic(flavor type, const std::string &message, const char *file, unsigned line) + : type(type), message(message), location(std::string(file) + ':' + std::to_string(line)) {} +}; + // A spool stores CXXRTL design state changes in a file. class spool { public: @@ -127,7 +163,7 @@ public: static constexpr uint32_t PACKET_SAMPLE = 0xc0000001; enum sample_flag : uint32_t { - EMPTY = 0, + EMPTY = 0, INCREMENTAL = 1, }; @@ -139,6 +175,9 @@ public: static constexpr uint32_t PACKET_CHANGEL = 0x20000000/* | ident */; static constexpr uint32_t PACKET_CHANGEH = 0x30000000/* | ident */; + static constexpr uint32_t PACKET_DIAGNOSTIC = 0xc0000010/* | diagnostic::flavor */; + static constexpr uint32_t DIAGNOSTIC_MASK = 0x0000000f; + static constexpr uint32_t PACKET_END = 0xffffffff; // Writing spools. @@ -281,6 +320,12 @@ public: emit_word(data[offset]); } + void write_diagnostic(const diagnostic &diagnostic) { + emit_word(PACKET_DIAGNOSTIC | diagnostic.type); + emit_string(diagnostic.message); + emit_string(diagnostic.location); + } + void write_end() { emit_word(PACKET_END); } @@ -397,11 +442,16 @@ public: return true; } - bool read_change_header(uint32_t &header, ident_t &ident) { + bool read_header(uint32_t &header) { header = absorb_word(); - if (header == PACKET_END) - return false; - assert((header & ~(CHANGE_MASK | MAXIMUM_IDENT)) == 0); + return header != PACKET_END; + } + + // This method must be separate from `read_change_data` because `chunks` and `depth` can only be looked up + // if `ident` is known. + bool read_change_ident(uint32_t header, ident_t &ident) { + if ((header & ~(CHANGE_MASK | MAXIMUM_IDENT)) != 0) + return false; // some other packet ident = header & MAXIMUM_IDENT; return true; } @@ -427,6 +477,18 @@ public: for (size_t offset = 0; offset < chunks; offset++) data[chunks * index + offset] = absorb_word(); } + + bool read_diagnostic(uint32_t header, diagnostic &diagnostic) { + if ((header & ~DIAGNOSTIC_MASK) != PACKET_DIAGNOSTIC) + return false; // some other packet + uint32_t type = header & DIAGNOSTIC_MASK; + assert(type == diagnostic::BREAK || type == diagnostic::PRINT || + type == diagnostic::ASSERT || type == diagnostic::ASSUME); + diagnostic.type = (diagnostic::flavor)type; + diagnostic.message = absorb_string(); + diagnostic.location = absorb_string(); + return true; + } }; // Opening spools. For certain uses of the record/replay mechanism, two distinct open files (two open files, i.e. @@ -584,6 +646,18 @@ public: return changed; } + void record_diagnostic(const diagnostic &diagnostic) { + assert(streaming); + + // Emit an incremental delta cycle per diagnostic to simplify the logic of the recorder. This is inefficient, but + // diagnostics should be rare enough that this inefficiency does not matter. If it turns out to be an issue, this + // code should be changed to accumulate diagnostics to a buffer that is flushed in `record_{complete,incremental}` + // and also in `advance_time` before the timestamp is changed. (Right now `advance_time` never writes to the spool.) + writer.write_sample(/*incremental=*/true, pointer++, timestamp); + writer.write_diagnostic(diagnostic); + writer.write_end(); + } + void flush() { writer.flush(); } @@ -657,8 +731,9 @@ public: streaming = true; // Establish the initial state of the design. - initialized = replay(); - assert(initialized); + std::vector diagnostics; + initialized = replay(&diagnostics); + assert(initialized && diagnostics.empty()); } // Returns the pointer of the current sample. @@ -690,8 +765,8 @@ public: // If this function returns `true`, then `current_pointer() == at_pointer`, and the module contains values that // correspond to this pointer in the replay log. To obtain a valid pointer, call `current_pointer()`; while pointers // are monotonically increasing for each consecutive sample, using arithmetic operations to create a new pointer is - // not allowed. - bool rewind_to(spool::pointer_t at_pointer) { + // not allowed. The `diagnostics` argument, if not `nullptr`, receives the diagnostics recorded in this sample. + bool rewind_to(spool::pointer_t at_pointer, std::vector *diagnostics) { assert(initialized); // The pointers in the replay log start from one that is greater than `at_pointer`. In this case the pointer will @@ -707,9 +782,12 @@ public: reader.rewind(position_it->second); // Replay samples until eventually arriving to `at_pointer` or encountering end of file. - while(replay()) { + while(replay(diagnostics)) { if (pointer == at_pointer) return true; + + if (diagnostics) + diagnostics->clear(); } return false; } @@ -717,8 +795,8 @@ public: // If this function returns `true`, then `current_time() <= at_or_before_timestamp`, and the module contains values // that correspond to `current_time()` in the replay log. If `current_time() == at_or_before_timestamp` and there // are several consecutive samples with the same time, the module contains values that correspond to the first of - // these samples. - bool rewind_to_or_before(const time &at_or_before_timestamp) { + // these samples. The `diagnostics` argument, if not `nullptr`, receives the diagnostics recorded in this sample. + bool rewind_to_or_before(const time &at_or_before_timestamp, std::vector *diagnostics) { assert(initialized); // The timestamps in the replay log start from one that is greater than `at_or_before_timestamp`. In this case @@ -734,7 +812,7 @@ public: reader.rewind(position_it->second); // Replay samples until eventually arriving to or past `at_or_before_timestamp` or encountering end of file. - while (replay()) { + while (replay(diagnostics)) { if (timestamp == at_or_before_timestamp) break; @@ -743,14 +821,17 @@ public: break; if (next_timestamp > at_or_before_timestamp) break; + + if (diagnostics) + diagnostics->clear(); } return true; } // If this function returns `true`, then `current_pointer()` and `current_time()` are updated for the next sample // and the module now contains values that correspond to that sample. If it returns `false`, there was no next sample - // to read. - bool replay() { + // to read. The `diagnostics` argument, if not `nullptr`, receives the diagnostics recorded in the next sample. + bool replay(std::vector *diagnostics) { assert(streaming); bool incremental; @@ -771,11 +852,16 @@ public: } uint32_t header; - spool::ident_t ident; - variable var; - while (reader.read_change_header(header, ident)) { - variable &var = variables.at(ident); - reader.read_change_data(header, var.chunks, var.depth, var.curr); + while (reader.read_header(header)) { + spool::ident_t ident; + diagnostic diag; + if (reader.read_change_ident(header, ident)) { + variable &var = variables.at(ident); + reader.read_change_data(header, var.chunks, var.depth, var.curr); + } else if (reader.read_diagnostic(header, diag)) { + if (diagnostics) + diagnostics->push_back(diag); + } else assert(false && "Unrecognized packet header"); } return true; } From e9cd6ca9e8f9c8c729044e83811762ce13e84a12 Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Wed, 6 Mar 2024 00:16:02 +0000 Subject: [PATCH 72/80] Bump version --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 35290fbd8..81715ded5 100644 --- a/Makefile +++ b/Makefile @@ -141,7 +141,7 @@ LIBS += -lrt endif endif -YOSYS_VER := 0.38+120 +YOSYS_VER := 0.38+129 # Note: We arrange for .gitcommit to contain the (short) commit hash in # tarballs generated with git-archive(1) using .gitattributes. The git repo From 570a8f12b58e4cfbd10deb042b217165c2103bc4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Povi=C5=A1er?= Date: Wed, 6 Mar 2024 14:55:43 +0100 Subject: [PATCH 73/80] synth: Fix out-of-sync help message Co-authored-by: N. Engelhardt --- techlibs/common/synth.cc | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/techlibs/common/synth.cc b/techlibs/common/synth.cc index 68be34f20..74a484d59 100644 --- a/techlibs/common/synth.cc +++ b/techlibs/common/synth.cc @@ -271,8 +271,8 @@ struct SynthPass : public ScriptPass { run("memory_map"); run("opt -full"); if (help_mode) { - run("techmap", " (unless -inject)"); - run("techmap -map +/techmap.v -map ", " (if -inject)"); + run("techmap", " (unless -extra-map)"); + run("techmap -map +/techmap.v -map ", " (if -extra-map)"); } else { std::string techmap_opts; if (!techmap_maps.empty()) From b4da6b80f894514979e62230ff8df86b3e38290e Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Fri, 8 Mar 2024 11:56:01 +1300 Subject: [PATCH 74/80] ci: Fix mac builds --- .github/workflows/test-macos.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/test-macos.yml b/.github/workflows/test-macos.yml index 9b806a580..8ca658c39 100644 --- a/.github/workflows/test-macos.yml +++ b/.github/workflows/test-macos.yml @@ -16,7 +16,7 @@ jobs: steps: - name: Install Dependencies run: | - brew install bison flex gawk libffi pkg-config bash + HOMEBREW_NO_INSTALLED_DEPENDENTS_CHECK=1 brew install bison flex gawk libffi pkg-config bash - name: Runtime environment shell: bash From 078b876f505647c992479c2afcf50f0850ea6fac Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Sat, 9 Mar 2024 00:14:37 +0000 Subject: [PATCH 75/80] Bump version --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 81715ded5..90b4e674a 100644 --- a/Makefile +++ b/Makefile @@ -141,7 +141,7 @@ LIBS += -lrt endif endif -YOSYS_VER := 0.38+129 +YOSYS_VER := 0.38+141 # Note: We arrange for .gitcommit to contain the (short) commit hash in # tarballs generated with git-archive(1) using .gitattributes. The git repo From 5e05300e7b56ef9f4c91e4be6c4906051544b98b Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Mon, 11 Mar 2024 10:55:09 +0100 Subject: [PATCH 76/80] fix compile warning --- kernel/register.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kernel/register.cc b/kernel/register.cc index b5485e06d..3ccb5ee78 100644 --- a/kernel/register.cc +++ b/kernel/register.cc @@ -1002,7 +1002,7 @@ struct LicensePass : public Pass { log("This command produces the following notice.\n"); notice(); } - void execute(std::vector args, RTLIL::Design*) override + void execute(std::vector, RTLIL::Design*) override { notice(); } From 42122e240e293f5d01775546448f5f7e2fa0fcd1 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Thu, 7 Mar 2024 13:27:03 +0100 Subject: [PATCH 77/80] smtbmc: Add --track-assumes and --minimize-assumes options The --track-assumes option makes smtbmc keep track of which assumptions were used by the solver when reaching an unsat case and to output that set of assumptions. This is particularly useful to debug PREUNSAT failures. The --minimize-assumes option can be used in addition to --track-assumes which will cause smtbmc to spend additional solving effort to produce a minimal set of assumptions that are sufficient to cause the unsat result. --- backends/smt2/smtbmc.py | 87 +++++++++++++++++++++++--- backends/smt2/smtbmc_incremental.py | 95 +++++++++++++++++++++++++---- backends/smt2/smtio.py | 61 +++++++++++++++++- 3 files changed, 219 insertions(+), 24 deletions(-) diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index cc47bc376..e6b4088db 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -57,6 +57,8 @@ keep_going = False check_witness = False detect_loops = False incremental = None +track_assumes = False +minimize_assumes = False so = SmtOpts() @@ -189,6 +191,15 @@ def help(): --incremental run in incremental mode (experimental) + --track-assumes + track individual assumptions and report a subset of used + assumptions that are sufficient for the reported outcome. This + can be used to debug PREUNSAT failures as well as to find a + smaller set of sufficient assumptions. + + --minimize-assumes + when using --track-assumes, solve for a minimal set of sufficient assumptions. + """ + so.helpmsg()) def usage(): @@ -200,7 +211,8 @@ try: opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:higcm:", so.longopts + ["help", "final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "yw=", "btorwit=", "presat", "dump-vcd=", "dump-yw=", "dump-vlogtb=", "vlogtb-top=", "dump-smtc=", "dump-all", "noinfo", "append=", - "smtc-init", "smtc-top=", "noinit", "binary", "keep-going", "check-witness", "detect-loops", "incremental"]) + "smtc-init", "smtc-top=", "noinit", "binary", "keep-going", "check-witness", "detect-loops", "incremental", + "track-assumes", "minimize-assumes"]) except: usage() @@ -289,6 +301,10 @@ for o, a in opts: elif o == "--incremental": from smtbmc_incremental import Incremental incremental = Incremental() + elif o == "--track-assumes": + track_assumes = True + elif o == "--minimize-assumes": + minimize_assumes = True elif so.handle(o, a): pass else: @@ -447,6 +463,9 @@ def get_constr_expr(db, state, final=False, getvalues=False, individual=False): smt = SmtIo(opts=so) +if track_assumes: + smt.smt2_options[':produce-unsat-assumptions'] = 'true' + if noinfo and vcdfile is None and vlogtbfile is None and outconstr is None: smt.produce_models = False @@ -1497,6 +1516,44 @@ def get_active_assert_map(step, active): return assert_map +assume_enables = {} + +def declare_assume_enables(): + def recurse(mod, path, key_base=()): + for expr, desc in smt.modinfo[mod].assumes.items(): + enable = f"|assume_enable {len(assume_enables)}|" + smt.smt2_assumptions[(expr, key_base)] = enable + smt.write(f"(declare-const {enable} Bool)") + assume_enables[(expr, key_base)] = (enable, path, desc) + + for cell, submod in smt.modinfo[mod].cells.items(): + recurse(submod, f"{path}.{cell}", (mod, cell, key_base)) + + recurse(topmod, topmod) + +if track_assumes: + declare_assume_enables() + +def smt_assert_design_assumes(step): + if not track_assumes: + smt_assert_consequent("(|%s_u| s%d)" % (topmod, step)) + return + + if not assume_enables: + return + + def expr_for_assume(assume_key, base=None): + expr, key_base = assume_key + expr_prefix = f"(|{expr}| " + expr_suffix = ")" + while key_base: + mod, cell, key_base = key_base + expr_prefix += f"(|{mod}_h {cell}| " + expr_suffix += ")" + return f"{expr_prefix} s{step}{expr_suffix}" + + for assume_key, (enable, path, desc) in assume_enables.items(): + smt_assert_consequent(f"(=> {enable} {expr_for_assume(assume_key)})") states = list() asserts_antecedent_cache = [list()] @@ -1651,6 +1708,13 @@ def smt_check_sat(expected=["sat", "unsat"]): smt_forall_assert() return smt.check_sat(expected=expected) +def report_tracked_assumptions(msg): + if track_assumes: + print_msg(msg) + for key in smt.get_unsat_assumptions(minimize=minimize_assumes): + enable, path, descr = assume_enables[key] + print_msg(f" In {path}: {descr}") + if incremental: incremental.mainloop() @@ -1664,7 +1728,7 @@ elif tempind: break smt_state(step) - smt_assert_consequent("(|%s_u| s%d)" % (topmod, step)) + smt_assert_design_assumes(step) smt_assert_antecedent("(|%s_h| s%d)" % (topmod, step)) smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, step)) smt_assert_consequent(get_constr_expr(constr_assumes, step)) @@ -1707,6 +1771,7 @@ elif tempind: else: print_msg("Temporal induction successful.") + report_tracked_assumptions("Used assumptions:") retstatus = "PASSED" break @@ -1732,7 +1797,7 @@ elif covermode: while step < num_steps: smt_state(step) - smt_assert_consequent("(|%s_u| s%d)" % (topmod, step)) + smt_assert_design_assumes(step) smt_assert_antecedent("(|%s_h| s%d)" % (topmod, step)) smt_assert_consequent(get_constr_expr(constr_assumes, step)) @@ -1753,6 +1818,7 @@ elif covermode: smt_assert("(distinct (covers_%d s%d) #b%s)" % (coveridx, step, "0" * len(cover_desc))) if smt_check_sat() == "unsat": + report_tracked_assumptions("Used assumptions:") smt_pop() break @@ -1761,13 +1827,14 @@ elif covermode: print_msg("Appending additional step %d." % i) smt_state(i) smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, i)) - smt_assert_consequent("(|%s_u| s%d)" % (topmod, i)) + smt_assert_design_assumes(i) smt_assert_antecedent("(|%s_h| s%d)" % (topmod, i)) smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, i-1, i)) smt_assert_consequent(get_constr_expr(constr_assumes, i)) print_msg("Re-solving with appended steps..") if smt_check_sat() == "unsat": print("%s Cannot appended steps without violating assumptions!" % smt.timestamp()) + report_tracked_assumptions("Conflicting assumptions:") found_failed_assert = True retstatus = "FAILED" break @@ -1823,7 +1890,7 @@ else: # not tempind, covermode retstatus = "PASSED" while step < num_steps: smt_state(step) - smt_assert_consequent("(|%s_u| s%d)" % (topmod, step)) + smt_assert_design_assumes(step) smt_assert_antecedent("(|%s_h| s%d)" % (topmod, step)) smt_assert_consequent(get_constr_expr(constr_assumes, step)) @@ -1853,7 +1920,7 @@ else: # not tempind, covermode if step+i < num_steps: smt_state(step+i) smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, step+i)) - smt_assert_consequent("(|%s_u| s%d)" % (topmod, step+i)) + smt_assert_design_assumes(step + i) smt_assert_antecedent("(|%s_h| s%d)" % (topmod, step+i)) smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, step+i-1, step+i)) smt_assert_consequent(get_constr_expr(constr_assumes, step+i)) @@ -1867,7 +1934,8 @@ else: # not tempind, covermode print_msg("Checking assumptions in steps %d to %d.." % (step, last_check_step)) if smt_check_sat() == "unsat": - print("%s Assumptions are unsatisfiable!" % smt.timestamp()) + print_msg("Assumptions are unsatisfiable!") + report_tracked_assumptions("Conficting assumptions:") retstatus = "PREUNSAT" break @@ -1920,13 +1988,14 @@ else: # not tempind, covermode print_msg("Appending additional step %d." % i) smt_state(i) smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, i)) - smt_assert_consequent("(|%s_u| s%d)" % (topmod, i)) + smt_assert_design_assumes(i) smt_assert_antecedent("(|%s_h| s%d)" % (topmod, i)) smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, i-1, i)) smt_assert_consequent(get_constr_expr(constr_assumes, i)) print_msg("Re-solving with appended steps..") if smt_check_sat() == "unsat": - print("%s Cannot append steps without violating assumptions!" % smt.timestamp()) + print_msg("Cannot append steps without violating assumptions!") + report_tracked_assumptions("Conflicting assumptions:") retstatus = "FAILED" break print_anyconsts(step) diff --git a/backends/smt2/smtbmc_incremental.py b/backends/smt2/smtbmc_incremental.py index 1a2a45703..f43e878f3 100644 --- a/backends/smt2/smtbmc_incremental.py +++ b/backends/smt2/smtbmc_incremental.py @@ -15,6 +15,14 @@ class InteractiveError(Exception): pass +def mkkey(data): + if isinstance(data, list): + return tuple(map(mkkey, data)) + elif isinstance(data, dict): + raise InteractiveError(f"JSON objects found in assumption key: {data!r}") + return data + + class Incremental: def __init__(self): self.traceidx = 0 @@ -73,17 +81,17 @@ class Incremental: if min_len is not None and arg_len < min_len: if min_len == max_len: - raise ( + raise InteractiveError( f"{json.dumps(expr[0])} expression must have " f"{min_len} argument{'s' if min_len != 1 else ''}" ) else: - raise ( + raise InteractiveError( f"{json.dumps(expr[0])} expression must have at least " f"{min_len} argument{'s' if min_len != 1 else ''}" ) if max_len is not None and arg_len > max_len: - raise ( + raise InteractiveError( f"{json.dumps(expr[0])} expression can have at most " f"{min_len} argument{'s' if max_len != 1 else ''}" ) @@ -96,14 +104,31 @@ class Incremental: smt_out.append(f"s{step}") return "module", smtbmc.topmod - def expr_mod_constraint(self, expr, smt_out): - self.expr_arg_len(expr, 1) + def expr_cell(self, expr, smt_out): + self.expr_arg_len(expr, 2) position = len(smt_out) smt_out.append(None) - arg_sort = self.expr(expr[1], smt_out, required_sort=["module", None]) + arg_sort = self.expr(expr[2], smt_out, required_sort=["module", None]) + smt_out.append(")") module = arg_sort[1] + cell = expr[1] + submod = smtbmc.smt.modinfo[module].cells.get(cell) + if submod is None: + raise InteractiveError(f"module {module!r} has no cell {cell!r}") + smt_out[position] = f"(|{module}_h {cell}| " + return ("module", submod) + + def expr_mod_constraint(self, expr, smt_out): suffix = expr[0][3:] - smt_out[position] = f"(|{module}{suffix}| " + self.expr_arg_len(expr, 1, 2 if suffix in ["_a", "_u", "_c"] else 1) + position = len(smt_out) + smt_out.append(None) + arg_sort = self.expr(expr[-1], smt_out, required_sort=["module", None]) + module = arg_sort[1] + if len(expr) == 3: + smt_out[position] = f"(|{module}{suffix} {expr[1]}| " + else: + smt_out[position] = f"(|{module}{suffix}| " smt_out.append(")") return "Bool" @@ -223,20 +248,19 @@ class Incremental: subexpr = expr[2] if not isinstance(label, str): - raise InteractiveError(f"expression label has to be a string") + raise InteractiveError("expression label has to be a string") smt_out.append("(! ") - smt_out.appedd(label) - smt_out.append(" ") - sort = self.expr(subexpr, smt_out) - + smt_out.append(" :named ") + smt_out.append(label) smt_out.append(")") return sort expr_handlers = { "step": expr_step, + "cell": expr_cell, "mod_h": expr_mod_constraint, "mod_is": expr_mod_constraint, "mod_i": expr_mod_constraint, @@ -302,6 +326,30 @@ class Incremental: assert_fn(self.expr_smt(cmd.get("expr"), "Bool")) + def cmd_assert_design_assumes(self, cmd): + step = self.arg_step(cmd) + smtbmc.smt_assert_design_assumes(step) + + def cmd_get_design_assume(self, cmd): + key = mkkey(cmd.get("key")) + return smtbmc.assume_enables.get(key) + + def cmd_update_assumptions(self, cmd): + expr = cmd.get("expr") + key = cmd.get("key") + + + key = mkkey(key) + + result = smtbmc.smt.smt2_assumptions.pop(key, None) + if expr is not None: + expr = self.expr_smt(expr, "Bool") + smtbmc.smt.smt2_assumptions[key] = expr + return result + + def cmd_get_unsat_assumptions(self, cmd): + return smtbmc.smt.get_unsat_assumptions(minimize=bool(cmd.get('minimize'))) + def cmd_push(self, cmd): smtbmc.smt_push() @@ -313,11 +361,14 @@ class Incremental: def cmd_smtlib(self, cmd): command = cmd.get("command") + response = cmd.get("response", False) if not isinstance(command, str): raise InteractiveError( f"raw SMT-LIB command must be a string, found {json.dumps(command)}" ) smtbmc.smt.write(command) + if response: + return smtbmc.smt.read() def cmd_design_hierwitness(self, cmd=None): allregs = (cmd is None) or bool(cmd.get("allreges", False)) @@ -369,6 +420,21 @@ class Incremental: return dict(last_step=last_step) + def cmd_modinfo(self, cmd): + fields = cmd.get("fields", []) + + mod = cmd.get("mod") + if mod is None: + mod = smtbmc.topmod + modinfo = smtbmc.smt.modinfo.get(mod) + if modinfo is None: + return None + + result = dict(name=mod) + for field in fields: + result[field] = getattr(modinfo, field, None) + return result + def cmd_ping(self, cmd): return cmd @@ -377,6 +443,10 @@ class Incremental: "assert": cmd_assert, "assert_antecedent": cmd_assert, "assert_consequent": cmd_assert, + "assert_design_assumes": cmd_assert_design_assumes, + "get_design_assume": cmd_get_design_assume, + "update_assumptions": cmd_update_assumptions, + "get_unsat_assumptions": cmd_get_unsat_assumptions, "push": cmd_push, "pop": cmd_pop, "check": cmd_check, @@ -384,6 +454,7 @@ class Incremental: "design_hierwitness": cmd_design_hierwitness, "write_yw_trace": cmd_write_yw_trace, "read_yw_trace": cmd_read_yw_trace, + "modinfo": cmd_modinfo, "ping": cmd_ping, } diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index c904aea95..e32f43c60 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -114,6 +114,7 @@ class SmtModInfo: self.clocks = dict() self.cells = dict() self.asserts = dict() + self.assumes = dict() self.covers = dict() self.maximize = set() self.minimize = set() @@ -141,6 +142,7 @@ class SmtIo: self.recheck = False self.smt2cache = [list()] self.smt2_options = dict() + self.smt2_assumptions = dict() self.p = None self.p_index = solvers_index solvers_index += 1 @@ -602,6 +604,12 @@ class SmtIo: else: self.modinfo[self.curmod].covers["%s_c %s" % (self.curmod, fields[2])] = fields[3] + if fields[1] == "yosys-smt2-assume": + if len(fields) > 4: + self.modinfo[self.curmod].assumes["%s_u %s" % (self.curmod, fields[2])] = f'{fields[4]} ({fields[3]})' + else: + self.modinfo[self.curmod].assumes["%s_u %s" % (self.curmod, fields[2])] = fields[3] + if fields[1] == "yosys-smt2-maximize": self.modinfo[self.curmod].maximize.add(fields[2]) @@ -785,8 +793,13 @@ class SmtIo: return stmt def check_sat(self, expected=["sat", "unsat", "unknown", "timeout", "interrupted"]): + if self.smt2_assumptions: + assume_exprs = " ".join(self.smt2_assumptions.values()) + check_stmt = f"(check-sat-assuming ({assume_exprs}))" + else: + check_stmt = "(check-sat)" if self.debug_print: - print("> (check-sat)") + print(f"> {check_stmt}") if self.debug_file and not self.nocomments: print("; running check-sat..", file=self.debug_file) self.debug_file.flush() @@ -800,7 +813,7 @@ class SmtIo: for cache_stmt in cache_ctx: self.p_write(cache_stmt + "\n", False) - self.p_write("(check-sat)\n", True) + self.p_write(f"{check_stmt}\n", True) if self.timeinfo: i = 0 @@ -868,7 +881,7 @@ class SmtIo: if self.debug_file: print("(set-info :status %s)" % result, file=self.debug_file) - print("(check-sat)", file=self.debug_file) + print(check_stmt, file=self.debug_file) self.debug_file.flush() if result not in expected: @@ -945,6 +958,48 @@ class SmtIo: def bv2int(self, v): return int(self.bv2bin(v), 2) + def get_raw_unsat_assumptions(self): + self.write("(get-unsat-assumptions)") + exprs = set(self.unparse(part) for part in self.parse(self.read())) + unsat_assumptions = [] + for key, value in self.smt2_assumptions.items(): + # normalize expression + value = self.unparse(self.parse(value)) + if value in exprs: + exprs.remove(value) + unsat_assumptions.append(key) + return unsat_assumptions + + def get_unsat_assumptions(self, minimize=False): + if not minimize: + return self.get_raw_unsat_assumptions() + required_assumptions = {} + + while True: + candidate_assumptions = {} + for key in self.get_raw_unsat_assumptions(): + if key not in required_assumptions: + candidate_assumptions[key] = self.smt2_assumptions[key] + + while candidate_assumptions: + + candidate_key, candidate_assume = candidate_assumptions.popitem() + + self.smt2_assumptions = {} + for key, assume in candidate_assumptions.items(): + self.smt2_assumptions[key] = assume + for key, assume in required_assumptions.items(): + self.smt2_assumptions[key] = assume + result = self.check_sat() + + if result == 'unsat': + candidate_assumptions = None + else: + required_assumptions[candidate_key] = candidate_assume + + if candidate_assumptions is not None: + return list(required_assumptions) + def get(self, expr): self.write("(get-value (%s))" % (expr)) return self.parse(self.read())[0][1] From 0944664e60b0c2db98006dcb9e0afde42875cbed Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Tue, 12 Mar 2024 00:15:21 +0000 Subject: [PATCH 78/80] Bump version --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 90b4e674a..f8b79c6c7 100644 --- a/Makefile +++ b/Makefile @@ -141,7 +141,7 @@ LIBS += -lrt endif endif -YOSYS_VER := 0.38+141 +YOSYS_VER := 0.38+152 # Note: We arrange for .gitcommit to contain the (short) commit hash in # tarballs generated with git-archive(1) using .gitattributes. The git repo From 00338082b00983e562de8d175329652b46d28c32 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Tue, 12 Mar 2024 08:55:10 +0100 Subject: [PATCH 79/80] Release version 0.39 --- CHANGELOG | 20 +++++++++++++++++++- Makefile | 4 ++-- 2 files changed, 21 insertions(+), 3 deletions(-) diff --git a/CHANGELOG b/CHANGELOG index ed91d5e7c..119fe35f6 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -2,8 +2,26 @@ List of major changes and improvements between releases ======================================================= -Yosys 0.38 .. Yosys 0.39-dev +Yosys 0.38 .. Yosys 0.39 -------------------------- + * New commands and options + - Added option "-extra-map" to "synth" pass. + - Added option "-dont_use" to "dfflibmap" pass. + - Added option "-href" to "show" command. + - Added option "-noscopeinfo" to "flatten" pass. + - Added option "-scopename" to "flatten" pass. + + * SystemVerilog + - Added support for packed multidimensional arrays. + + * Various + - Added "$scopeinfo" cells to preserve information about + the hierarchy during flattening. + - Added sequential area output to "stat -liberty". + - Added ability to record/replay diagnostics in cxxrtl backend. + + * Verific support + - Added attributes to module instantiation. Yosys 0.37 .. Yosys 0.38 -------------------------- diff --git a/Makefile b/Makefile index f8b79c6c7..00fd26bb1 100644 --- a/Makefile +++ b/Makefile @@ -141,7 +141,7 @@ LIBS += -lrt endif endif -YOSYS_VER := 0.38+152 +YOSYS_VER := 0.39 # Note: We arrange for .gitcommit to contain the (short) commit hash in # tarballs generated with git-archive(1) using .gitattributes. The git repo @@ -157,7 +157,7 @@ endif OBJS = kernel/version_$(GIT_REV).o bumpversion: - sed -i "/^YOSYS_VER := / s/+[0-9][0-9]*$$/+`git log --oneline 543faed.. | wc -l`/;" Makefile +# sed -i "/^YOSYS_VER := / s/+[0-9][0-9]*$$/+`git log --oneline 543faed.. | wc -l`/;" Makefile # set 'ABCREV = default' to use abc/ as it is # From 18cec2d9a926c98bfadeffc47d38213139e188a7 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Tue, 12 Mar 2024 08:57:48 +0100 Subject: [PATCH 80/80] Next dev cycle --- CHANGELOG | 3 +++ Makefile | 4 ++-- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/CHANGELOG b/CHANGELOG index 119fe35f6..b172988d5 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -2,6 +2,9 @@ List of major changes and improvements between releases ======================================================= +Yosys 0.39 .. Yosys 0.40-dev +-------------------------- + Yosys 0.38 .. Yosys 0.39 -------------------------- * New commands and options diff --git a/Makefile b/Makefile index 00fd26bb1..55941c8c3 100644 --- a/Makefile +++ b/Makefile @@ -141,7 +141,7 @@ LIBS += -lrt endif endif -YOSYS_VER := 0.39 +YOSYS_VER := 0.39+0 # Note: We arrange for .gitcommit to contain the (short) commit hash in # tarballs generated with git-archive(1) using .gitattributes. The git repo @@ -157,7 +157,7 @@ endif OBJS = kernel/version_$(GIT_REV).o bumpversion: -# sed -i "/^YOSYS_VER := / s/+[0-9][0-9]*$$/+`git log --oneline 543faed.. | wc -l`/;" Makefile + sed -i "/^YOSYS_VER := / s/+[0-9][0-9]*$$/+`git log --oneline 0033808.. | wc -l`/;" Makefile # set 'ABCREV = default' to use abc/ as it is #