From d0e559a34f8be18af195c8eb15324baf28d9c2a5 Mon Sep 17 00:00:00 2001
From: "N. Engelhardt" <nak@yosyshq.com>
Date: Mon, 2 Oct 2023 16:06:26 +0200
Subject: [PATCH 01/32] 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" <nak@yosyshq.com>
Date: Mon, 2 Oct 2023 17:29:09 +0200
Subject: [PATCH 02/32] 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" <nak@yosyshq.com>
Date: Mon, 2 Oct 2023 18:32:53 +0200
Subject: [PATCH 03/32] 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<<b_width) - 1;
+ // highest position of Y that can change with the value of B
+ int b_range_upper;
+ // 1 + highest position of A that can be moved to Y[i]
+ int a_range_upper;
+ // lowest position of A that can be moved to Y[i]
+ int a_range_lower;
+ for (int i = 0; i < y_width; i++){
if (cell->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?= <povik@cutebit.org>
Date: Mon, 16 Oct 2023 13:29:47 +0200
Subject: [PATCH 04/32] 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?= <povik@cutebit.org>
Date: Sun, 10 Dec 2023 00:27:42 +0100
Subject: [PATCH 05/32] 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?= <povik@cutebit.org>
Date: Mon, 11 Dec 2023 21:36:00 +0100
Subject: [PATCH 06/32] 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<<b_width) - 1;
@@ -195,18 +202,20 @@ void shift_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell)
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))){
+ } 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?= <povik@cutebit.org>
Date: Fri, 19 Jan 2024 11:08:31 +0100
Subject: [PATCH 07/32] 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<<b_width) - 1;
- // highest position of Y that can change with the value of B
- int b_range_upper;
- // 1 + highest position of A that can be moved to Y[i]
- int a_range_upper;
- // lowest position of A that can be moved to Y[i]
- int a_range_lower;
-
for (int i = 0; i < y_width; i++){
+ // highest position of Y that can change with the value of B
+ int b_range_upper = 0;
+ // 1 + highest position of A that can be moved to Y[i]
+ int a_range_upper;
+ // lowest position of A that can be moved to Y[i]
+ int a_range_lower;
+
if (cell->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?= <povik@cutebit.org>
Date: Fri, 19 Jan 2024 11:14:10 +0100
Subject: [PATCH 08/32] 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 d77b792156b439ce7ae6a8900d0166fb1c849ee5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Martin=20Povi=C5=A1er?= <povik@cutebit.org>
Date: Thu, 22 Feb 2024 17:22:56 +0100
Subject: [PATCH 09/32] 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?= <povik@cutebit.org>
Date: Thu, 22 Feb 2024 17:23:28 +0100
Subject: [PATCH 10/32] 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<std::string> 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<std::string> 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 <inject>", " (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?= <povik@cutebit.org>
Date: Thu, 22 Feb 2024 22:00:56 +0100
Subject: [PATCH 11/32] 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 d2a7ce04ea5a5bd6d3324e3ec81c3ede0ceab5d9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Martin=20Povi=C5=A1er?= <povik@cutebit.org>
Date: Fri, 1 Mar 2024 10:54:51 +0100
Subject: [PATCH 12/32] 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<std::string> techmap_inject;
+ std::vector<std::string> 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<std::string> 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 <inject>", " (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 6469d90293b465201c9903f2dc1d02045cc33bcd Mon Sep 17 00:00:00 2001
From: Jannis Harder <me@jix.one>
Date: Wed, 7 Feb 2024 18:39:32 +0100
Subject: [PATCH 13/32] 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<SigBit, int> ywmap_clocks;
+ vector<Cell *> ywmap_asserts;
+ vector<Cell *> 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 <me@jix.one>
Date: Tue, 27 Feb 2024 19:56:47 +0100
Subject: [PATCH 14/32] 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<RTLIL::Module *, int> &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<RTLIL::Module *, int> &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 <me@jix.one>
Date: Wed, 21 Feb 2024 16:35:17 +0100
Subject: [PATCH 15/32] 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 <me@jix.one>
Date: Wed, 21 Feb 2024 16:33:14 +0100
Subject: [PATCH 16/32] 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 <me@jix.one>
Date: Mon, 4 Mar 2024 16:52:11 +0100
Subject: [PATCH 17/32] 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 18/32] 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 <me@jix.one>
Date: Tue, 5 Mar 2024 14:37:33 +0100
Subject: [PATCH 19/32] 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 <whitequark@whitequark.org>
Date: Tue, 5 Mar 2024 16:21:12 +0000
Subject: [PATCH 20/32] 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 @@
// <file> ::= <file-header> <definitions> <sample>+
// <file-header> ::= 0x52585843 0x00004c54
// <definitions> ::= <packet-define>* <packet-end>
-// <sample> ::= <packet-sample> <packet-change>* <packet-end>
+// <sample> ::= <packet-sample> (<packet-change> | <packet-diag>)* <packet-end>
// <packet-define> ::= 0xc0000000 ...
// <packet-sample> ::= 0xc0000001 ...
// <packet-change> ::= 0x0??????? <chunk>+ | 0x1??????? <index> <chunk>+ | 0x2??????? | 0x3???????
// <chunk>, <index> ::= 0x????????
+// <packet-diag> ::= <packet-break> | <packet-print> | <packet-assert> | <packet-assume>
+// <packet-break> ::= 0xc0000010 <message> <source-location>
+// <packet-print> ::= 0xc0000011 <message> <source-location>
+// <packet-assert> ::= 0xc0000012 <message> <source-location>
+// <packet-assume> ::= 0xc0000013 <message> <source-location>
// <packet-end> ::= 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<diagnostic> 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<diagnostic> *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<diagnostic> *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<diagnostic> *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 21/32] 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?= <povik@cutebit.org>
Date: Wed, 6 Mar 2024 14:55:43 +0100
Subject: [PATCH 22/32] synth: Fix out-of-sync help message
Co-authored-by: N. Engelhardt <nakengelhardt@gmail.com>
---
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 <inject>", " (if -inject)");
+ run("techmap", " (unless -extra-map)");
+ run("techmap -map +/techmap.v -map <inject>", " (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 23/32] 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 24/32] 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 <mmicko@gmail.com>
Date: Mon, 11 Mar 2024 10:55:09 +0100
Subject: [PATCH 25/32] 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<std::string> args, RTLIL::Design*) override
+ void execute(std::vector<std::string>, RTLIL::Design*) override
{
notice();
}
From 42122e240e293f5d01775546448f5f7e2fa0fcd1 Mon Sep 17 00:00:00 2001
From: Jannis Harder <me@jix.one>
Date: Thu, 7 Mar 2024 13:27:03 +0100
Subject: [PATCH 26/32] 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 27/32] 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 <mmicko@gmail.com>
Date: Tue, 12 Mar 2024 08:55:10 +0100
Subject: [PATCH 28/32] 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 <mmicko@gmail.com>
Date: Tue, 12 Mar 2024 08:57:48 +0100
Subject: [PATCH 29/32] 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
#
From b3124f30e42cb0f0f8d8216f39d69e522270833b Mon Sep 17 00:00:00 2001
From: "github-actions[bot]"
<41898282+github-actions[bot]@users.noreply.github.com>
Date: Wed, 13 Mar 2024 00:15:33 +0000
Subject: [PATCH 30/32] Bump version
---
Makefile | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/Makefile b/Makefile
index 55941c8c3..e55165f46 100644
--- a/Makefile
+++ b/Makefile
@@ -141,7 +141,7 @@ LIBS += -lrt
endif
endif
-YOSYS_VER := 0.39+0
+YOSYS_VER := 0.39+1
# Note: We arrange for .gitcommit to contain the (short) commit hash in
# tarballs generated with git-archive(1) using .gitattributes. The git repo
From 29e3e10378c32cc5c51ccc65afe5dd0c0d7951aa Mon Sep 17 00:00:00 2001
From: Catherine <whitequark@whitequark.org>
Date: Wed, 13 Mar 2024 10:04:13 +0000
Subject: [PATCH 31/32] Add WebAssembly as a platform to
ISSUE_TEMPLATE/bug_report.yml.
---
.github/ISSUE_TEMPLATE/bug_report.yml | 1 +
1 file changed, 1 insertion(+)
diff --git a/.github/ISSUE_TEMPLATE/bug_report.yml b/.github/ISSUE_TEMPLATE/bug_report.yml
index 27cfd09b7..66c0b1971 100644
--- a/.github/ISSUE_TEMPLATE/bug_report.yml
+++ b/.github/ISSUE_TEMPLATE/bug_report.yml
@@ -34,6 +34,7 @@ body:
- macOS
- Windows
- BSD
+ - WebAssembly
multiple: true
validations:
required: true
From 3231c1cd932b9cffba9651c3264d337093eaed32 Mon Sep 17 00:00:00 2001
From: "github-actions[bot]"
<41898282+github-actions[bot]@users.noreply.github.com>
Date: Sat, 16 Mar 2024 00:14:56 +0000
Subject: [PATCH 32/32] Bump version
---
Makefile | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/Makefile b/Makefile
index e55165f46..ff7b141a4 100644
--- a/Makefile
+++ b/Makefile
@@ -141,7 +141,7 @@ LIBS += -lrt
endif
endif
-YOSYS_VER := 0.39+1
+YOSYS_VER := 0.39+4
# Note: We arrange for .gitcommit to contain the (short) commit hash in
# tarballs generated with git-archive(1) using .gitattributes. The git repo