Merge remote-tracking branch 'upstream/main' into xilinx-transparent-memory

This commit is contained in:
Jakub Janeczko 2026-07-23 01:54:24 +02:00
commit 4d6c133944
No known key found for this signature in database
GPG Key ID: D68C3D5A75B4C697
31 changed files with 2010 additions and 1805 deletions

View File

@ -15,7 +15,7 @@ jobs:
steps:
- id: skip_check
if: ${{ github.event_name != 'merge_group' }}
uses: mmicko/skip-duplicate-actions@master
uses: fkirc/skip-duplicate-actions@v5.3.2
with:
# don't run on documentation changes
paths_ignore: '["**/README.md", "docs/**", "guidelines/**"]'

View File

@ -18,7 +18,7 @@ jobs:
docs_export: ${{ github.ref == 'refs/heads/main' || startsWith(github.ref, 'refs/heads/docs-preview') || startsWith(github.ref, 'refs/tags/') }}
steps:
- id: skip_check
uses: mmicko/skip-duplicate-actions@master
uses: fkirc/skip-duplicate-actions@v5.3.2
with:
paths_ignore: '["**/README.md"]'
# don't cancel in case we're updating docs

View File

@ -15,7 +15,7 @@ jobs:
steps:
- id: skip_check
if: ${{ github.event_name != 'merge_group' }}
uses: mmicko/skip-duplicate-actions@master
uses: fkirc/skip-duplicate-actions@v5.3.2
with:
# don't run on documentation changes
paths_ignore: '["**/README.md", "docs/**", "guidelines/**"]'
@ -38,7 +38,7 @@ jobs:
steps:
- id: skip_check
if: ${{ github.event_name != 'merge_group' }}
uses: mmicko/skip-duplicate-actions@master
uses: fkirc/skip-duplicate-actions@v5.3.2
with:
# don't run on readme changes
paths_ignore: '["**/README.md"]'

View File

@ -15,7 +15,7 @@ jobs:
steps:
- id: skip_check
if: ${{ github.event_name != 'merge_group' }}
uses: mmicko/skip-duplicate-actions@master
uses: fkirc/skip-duplicate-actions@v5.3.2
with:
# don't run on documentation changes
paths_ignore: '["**/README.md", "docs/**", "guidelines/**"]'

View File

@ -15,7 +15,7 @@ jobs:
steps:
- id: skip_check
if: ${{ github.event_name != 'merge_group' }}
uses: mmicko/skip-duplicate-actions@master
uses: fkirc/skip-duplicate-actions@v5.3.2
with:
# don't run on documentation changes
paths_ignore: '["**/README.md", "docs/**", "guidelines/**"]'

View File

@ -15,7 +15,7 @@ jobs:
steps:
- id: skip_check
if: ${{ github.event_name != 'merge_group' && github.event_name != 'push' }}
uses: mmicko/skip-duplicate-actions@master
uses: fkirc/skip-duplicate-actions@v5.3.2
with:
# don't run on documentation changes
paths_ignore: '["**/README.md", "docs/**", "guidelines/**"]'

4
.gitmodules vendored
View File

@ -20,3 +20,7 @@
[submodule "sv-elab"]
path = frontends/slang/lib
url = https://github.com/povik/sv-elab
[submodule "symfpu"]
path = libs/symfpu
url = https://github.com/YosysHQ/symfpu
branch = floatWithStatusFlags

View File

@ -535,6 +535,7 @@ if (NOT YOSYS_BUILD_PYTHON_ONLY)
add_custom_target(test-unit
COMMAND ${CMAKE_CTEST_COMMAND} --test-dir tests/unit --output-on-failure
WORKING_DIRECTORY ${CMAKE_BINARY_DIR}
DEPENDS $<$<TARGET_EXISTS:yosys-gtest-all>:yosys-gtest-all>
)
add_custom_target(test-vanilla

View File

@ -15,7 +15,6 @@ passes/cmds/scratchpad.cc @nakengelhardt
frontends/rpc/ @whitequark
backends/cxxrtl/ @whitequark
passes/cmds/bugpoint.cc @whitequark
passes/techmap/flowmap.cc @whitequark
passes/opt/opt_lut.cc @whitequark
passes/techmap/abc9*.cc @eddiehung @Ravenslofty
backends/aiger/xaiger.cc @eddiehung

View File

@ -71,7 +71,6 @@ map_luts:
techmap
simplemap
techmap
flowmap
read_verilog
abc9
ice40_wrapcarry -unwrap

View File

@ -448,6 +448,7 @@ X(DST_EN)
X(DST_PEN)
X(DST_POL)
X(DST_WIDTH)
X(DZ)
X(D_ARST_N)
X(D_BYPASS)
X(D_EN)
@ -580,11 +581,14 @@ X(NMUX)
X(NOR)
X(NOT)
X(NPRODUCTS)
X(NV)
X(NX)
X(NX_CY)
X(NX_CY_1BIT)
X(O)
X(OAI3)
X(OAI4)
X(OF)
X(OFFSET)
X(OHOLDBOT)
X(OHOLDTOP)
@ -779,6 +783,7 @@ X(T_RISE_MAX)
X(T_RISE_MIN)
X(T_RISE_TYP)
X(U)
X(UF)
X(UP)
X(USE_DPORT)
X(USE_MULT)
@ -882,6 +887,9 @@ X(f_mode)
X(feedback)
X(feedback_i)
X(first)
X(flags_ff)
X(flags_fi)
X(flags_if)
X(force_downto)
X(force_upto)
X(fsm_encoding)
@ -898,6 +906,7 @@ X(gold)
X(hdlname)
X(hierconn)
X(i)
X(ieee754Equal)
X(init)
X(initial_top)
X(interface_modport)
@ -905,11 +914,22 @@ X(interface_type)
X(interfaces_replaced_in_module)
X(invertible_pin)
X(iopad_external_pin)
X(isFinite)
X(isInfinite)
X(isNaN)
X(isNegative)
X(isNormal)
X(isPositive)
X(isSubnormal)
X(isZero)
X(is_inferred)
X(is_interface)
X(is_signed)
X(it)
X(keep)
X(keep_hierarchy)
X(lessThan)
X(lessThanOrEqual)
X(lib_whitebox)
X(library)
X(load_acc)
@ -938,6 +958,9 @@ X(nomeminit)
X(nosync)
X(nowrshmsk)
X(o)
X(o_ff)
X(o_fi)
X(o_if)
X(offset)
X(onehot)
X(output_select)
@ -946,6 +969,7 @@ X(p_class)
X(parallel_case)
X(parameter)
X(promoted_if)
X(qNV)
X(raise_error)
X(ram_block)
X(ram_style)
@ -957,12 +981,14 @@ X(replaced_by_gclk)
X(reprocess_after)
X(reset)
X(reset_i)
X(rm)
X(rom_block)
X(rom_style)
X(romstyle)
X(round)
X(round_i)
X(rtlil)
X(sNV)
X(saturate_enable)
X(saturate_enable_i)
X(scopename)
@ -972,11 +998,16 @@ X(shift_right_i)
X(single_bit_vector)
X(smtlib2_comb_expr)
X(smtlib2_module)
X(smtlibEqual)
X(src)
X(sta_arrival)
X(submod)
X(subtract)
X(subtract_i)
X(symfpu)
X(symfpu_inv)
X(symfpu_post)
X(symfpu_pre)
X(syn_ramstyle)
X(syn_romstyle)
X(techmap_autopurge)
@ -996,6 +1027,7 @@ X(unsigned_a)
X(unsigned_a_i)
X(unsigned_b)
X(unsigned_b_i)
X(unsupported_sva)
X(unused_bits)
X(use_dsp)
X(value)

View File

@ -7,6 +7,12 @@ add_subdirectory(json11)
add_subdirectory(minisat)
add_subdirectory(sha1)
add_subdirectory(subcircuit)
add_library(symfpu INTERFACE)
target_include_directories(symfpu INTERFACE
${CMAKE_CURRENT_SOURCE_DIR}
)
block()
set(BUILD_SHARED_LIBS OFF)
include(FetchContent)

1
libs/symfpu Submodule

@ -0,0 +1 @@
Subproject commit 5d5e50867437fe5cabd6ab5aad3b3808ec86701f

View File

@ -211,3 +211,8 @@ yosys_pass(sort
yosys_pass(icell_liberty
icell_liberty.cc
)
yosys_pass(symfpu
symfpu.cc
LIBRARIES
symfpu
)

View File

@ -17,95 +17,246 @@
*
*/
#include "kernel/yosys.h"
#include <functional>
#include <queue>
#include <ranges>
USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN
typedef struct name_proposal {
string name;
// An "object" is a cell or a wire.
// An object is "private" if its name starts with a '$'.
//
// The "autoname" pass renames private objects based on public object names,
// with suffixes added to show the relationship to the public objects.
// The pass chooses the "best" names based on minimizing their "cost".
// The cost of a new name for a private object is the cost along a path
// to a publicly named object.
struct cost {
// score is a property of one "edge", not of the entire path.
// 0 if the neighbour drives the object, and the wire's fanout otherwise
unsigned int score = UINT_MAX;
// New name length
size_t length = SIZE_MAX;
// Earlier discovered connection wins
int edge_pos = 0;
auto operator<=>(const cost &) const = default;
};
// Endpoints of an "edge" are always a cell index and a wire index. Goofy, I know.
// SigSig connections (module->connections()) don't count
// as neighbors. This means that the equivalent of `assign $w1 = \w2;` won't lead
// to $w1 being renamed.
struct Edge {
// Cell port name at which the wire connects to the cell
IdString port;
int cell;
int wire;
bool cell_is_output;
unsigned int score;
name_proposal() : name(""), score(-1) { }
name_proposal(string name, unsigned int score) : name(name), score(score) { }
bool operator<(const name_proposal &other) const {
if (score != other.score)
return score < other.score;
else
return name.length() < other.name.length();
}
} name_proposal;
// Edge's position in the edge list
int pos_in_cell;
int pos_in_wire;
};
int autoname_worker(Module *module, const dict<Wire*, unsigned int>& wire_score)
// decide() finds shortest names for every object reachable from a public name,
// cheapest-first. It doesn't apply the renames to the objects yet.
//
// commit() then renames in decide() order, which is topological, so a source
// neighbour always already carries its final uniquify()d name.
// A selected cell or wire
struct node {
// Exactly one of cell/wire is set
Cell *cell = nullptr;
Wire *wire = nullptr;
vector<Edge> edges;
// Ignores module->connections() just as the rest of the code
unsigned int fanout = 0;
bool is_public = false;
bool renameable = false;
bool selected = false;
size_t name_length = 0;
// Node index from which we want to construct the rename
int from_node = -1;
// Cost for the edge from that node
cost c;
// Suffix to append to the name of that node
string suffix;
// Is this name final?
bool decided = false;
const IdString& name() const { return cell ? cell->name : wire->name; }
};
// Decides the order of exploring neighbors
struct queue_item {
unsigned int score;
size_t length;
int index;
auto operator<=>(const queue_item &) const = default;
};
struct ModuleAutonamer
{
dict<Cell*, name_proposal> proposed_cell_names;
dict<Wire*, name_proposal> proposed_wire_names;
name_proposal best_name;
Module *module;
for (auto cell : module->selected_cells()) {
if (cell->name[0] == '$') {
// Cells in module order, then wires in the order that they're seen from cells.
// The index doubles as the tie-break between equally good
// proposals for different nodes
vector<node> nodes;
vector<int> decided;
std::priority_queue<queue_item, std::vector<queue_item>, std::greater<>> queue;
int renamed = 0;
ModuleAutonamer(Module *module) : module(module) { build_adjacency(); }
void build_adjacency()
{
vector<Cell*> cells(module->cells().begin(), module->cells().end());
// Arbitrary. Kinda just for passing tests without modifying them
for (auto cell : cells | std::views::reverse)
nodes.emplace_back().cell = cell;
int ncells = GetSize(nodes);
idict<Wire*> wire_ids;
for (int ci = 0; ci < ncells; ci++) {
Cell *cell = nodes[ci].cell;
for (auto &conn : cell->connections()) {
string suffix;
for (auto bit : conn.second)
if (bit.wire != nullptr && bit.wire->name[0] != '$') {
if (suffix.empty())
suffix = stringf("_%s_%s", cell->type.unescape(), conn.first.unescape());
name_proposal proposed_name(
bit.wire->name.str() + suffix,
cell->output(conn.first) ? 0 : wire_score.at(bit.wire)
);
if (!proposed_cell_names.count(cell) || proposed_name < proposed_cell_names.at(cell)) {
if (proposed_name < best_name)
best_name = proposed_name;
proposed_cell_names[cell] = proposed_name;
}
}
}
} else {
for (auto &conn : cell->connections()) {
string suffix;
for (auto bit : conn.second)
if (bit.wire != nullptr && bit.wire->name[0] == '$' && !bit.wire->port_id) {
if (suffix.empty())
suffix = stringf("_%s", conn.first.unescape());
name_proposal proposed_name(
cell->name.str() + suffix,
cell->output(conn.first) ? 0 : wire_score.at(bit.wire)
);
if (!proposed_wire_names.count(bit.wire) || proposed_name < proposed_wire_names.at(bit.wire)) {
if (proposed_name < best_name)
best_name = proposed_name;
proposed_wire_names[bit.wire] = proposed_name;
}
}
bool cell_is_output = cell->output(conn.first);
pool<Wire*> seen_in_this_port;
for (auto bit : conn.second) {
if (bit.wire == nullptr)
continue;
int wi = ncells + wire_ids(bit.wire);
if (wi == GetSize(nodes))
nodes.emplace_back().wire = bit.wire;
nodes[wi].fanout++;
if (!seen_in_this_port.insert(bit.wire).second)
continue;
Edge edge{
.port = conn.first,
.cell = ci,
.wire = wi,
.cell_is_output = cell_is_output,
.score = 0, // no fanouts are final yet
.pos_in_cell = GetSize(nodes[ci].edges),
.pos_in_wire = GetSize(nodes[wi].edges),
};
nodes[ci].edges.push_back(edge);
nodes[wi].edges.push_back(edge);
}
}
}
// Resolve selection before renaming
for (auto &nd : nodes) {
IdString name = nd.name();
nd.selected = nd.cell ? module->selected(nd.cell) : module->selected(nd.wire);
nd.is_public = (name[0] != '$');
nd.renameable = !nd.is_public && (nd.cell || nd.wire->port_id == 0);
if (nd.is_public)
nd.name_length = name.str().size();
}
// Only possible once every fanout is known
for (auto &nd : nodes)
for (auto &edge : nd.edges)
edge.score = edge.cell_is_output ? 0 : nodes[edge.wire].fanout;
}
void offer(int from, int to, const Edge &edge, int edge_pos)
{
node &nd = nodes[to];
if (!nd.renameable || nd.decided)
return;
string suffix = nd.cell
? stringf("_%s_%s", nd.cell->type.unescape(), edge.port.unescape())
: stringf("_%s", edge.port.unescape());
cost c{edge.score, nodes[from].name_length + suffix.length(), edge_pos};
if (c >= nd.c)
return;
nd.c = c;
nd.from_node = from;
nd.name_length = c.length;
nd.suffix = std::move(suffix);
queue.push(queue_item{c.score, c.length, to});
}
// Expand a public (or newly decided) node. The name it lends
// is already settled and the neighbour can keep what offer() built
void expand(int n)
{
const node &nd = nodes[n];
for (auto &edge : nd.edges)
if (nd.cell)
offer(n, edge.wire, edge, edge.pos_in_wire);
else
offer(n, edge.cell, edge, edge.pos_in_cell);
}
void decide()
{
for (int n = 0; n < GetSize(nodes); n++)
if (nodes[n].is_public)
expand(n);
while (!queue.empty()) {
int n = queue.top().index;
queue.pop();
if (nodes[n].decided)
continue;
nodes[n].decided = true;
decided.push_back(n);
expand(n);
}
}
int count = 0;
// compare against double best score for following comparisons so we don't
// pre-empt a future iteration
best_name.score *= 2;
for (auto &it : proposed_cell_names) {
if (best_name < it.second)
continue;
IdString n = module->uniquify(IdString(it.second.name));
log_debug("Rename cell %s in %s to %s.\n", it.first, module, n.unescape());
module->rename(it.first, n);
count++;
void append_name(int n, string &out)
{
const node &nd = nodes[n];
if (nd.is_public || nd.selected)
return nd.name().append_to(&out);
append_name(nd.from_node, out);
out += nd.suffix;
}
for (auto &it : proposed_wire_names) {
if (best_name < it.second)
continue;
IdString n = module->uniquify(IdString(it.second.name));
log_debug("Rename wire %s in %s to %s.\n", it.first, module, n.unescape());
module->rename(it.first, n);
count++;
void commit(int n)
{
node &nd = nodes[n];
if (!nd.selected)
return;
string full;
full.reserve(nd.name_length);
append_name(nd.from_node, full);
full += nd.suffix;
IdString name = module->uniquify(IdString(full));
if (nd.cell) {
log_debug("Rename cell %s in %s to %s.\n", nd.cell, module, name.unescape());
module->rename(nd.cell, name);
} else {
log_debug("Rename wire %s in %s to %s.\n", nd.wire, module, name.unescape());
module->rename(nd.wire, name);
}
renamed++;
}
return count;
}
void run()
{
decide();
for (int n : decided)
commit(n);
if (renamed > 0)
log("Renamed %d objects in module %s.\n", renamed, module);
}
};
struct AutonamePass : public Pass {
AutonamePass() : Pass("autoname", "automatically assign names to objects") { }
@ -135,24 +286,7 @@ struct AutonamePass : public Pass {
log_header(design, "Executing AUTONAME pass.\n");
for (auto module : design->selected_modules())
{
dict<Wire*, unsigned int> wire_score;
for (auto cell : module->selected_cells())
for (auto &conn : cell->connections())
for (auto bit : conn.second)
if (bit.wire != nullptr)
wire_score[bit.wire]++;
int count = 0, iter = 0;
while (1) {
iter++;
int n = autoname_worker(module, wire_score);
if (!n) break;
count += n;
}
if (count > 0)
log("Renamed %d objects in module %s (%d iterations).\n", count, module, iter);
}
ModuleAutonamer(module).run();
}
} AutonamePass;

799
passes/cmds/symfpu.cc Normal file
View File

@ -0,0 +1,799 @@
/*
* yosys -- Yosys Open SYnthesis Suite
*
* Copyright (C) 2025 Jannis Harder <jix@yosyshq.com> <me@jix.one>
*
* Permission to use, copy, modify, and/or distribute this software for any
* purpose with or without fee is hereby granted, provided that the above
* copyright notice and this permission notice appear in all copies.
*
* THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
* WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
* MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
* ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
* WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
* ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
* OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
*
*/
#include "kernel/log_help.h"
#include "kernel/yosys.h"
#include "symfpu/baseTypes/shared.h"
#include "symfpu/core/add.h"
#include "symfpu/core/divide.h"
#include "symfpu/core/fma.h"
#include "symfpu/core/ite.h"
#include "symfpu/core/multiply.h"
#include "symfpu/core/packing.h"
#include "symfpu/core/sqrt.h"
#include "symfpu/core/unpackedFloat.h"
#include "symfpu/core/classify.h"
#include "symfpu/core/compare.h"
USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN
struct prop;
template <bool is_signed> struct bv;
struct rm {
enum class mode { RNE, RNA, RTP, RTN, RTZ };
mode mode;
prop operator==(rm op) const;
};
thread_local Module *symfpu_mod = nullptr;
struct rtlil_traits {
using bwt = uint64_t;
using rm = struct rm;
using fpt = symfpu::shared::floatingPointTypeInfo;
using prop = struct prop;
using sbv = bv<true>;
using ubv = bv<false>;
// Return an instance of each rounding mode.
static rm RNE(void) { return {rm::mode::RNE}; };
static rm RNA(void) { return {rm::mode::RNA}; };
static rm RTP(void) { return {rm::mode::RTP}; };
static rm RTN(void) { return {rm::mode::RTN}; };
static rm RTZ(void) { return {rm::mode::RTZ}; };
// Handle various invariants.
// These can be empty to start with.
static void precondition(const bool b) { assert(b); }
static void postcondition(const bool b) { assert(b); }
static void invariant(const bool b) { assert(b); }
static void precondition(const prop &p);
static void postcondition(const prop &p);
static void invariant(const prop &p);
static void setflag(const string &name, const prop &p);
};
rm parse_rounding(std::string rounding) {
if (rounding.compare("RNE") == 0)
return rtlil_traits::RNE();
else if (rounding.compare("RNA") == 0)
return rtlil_traits::RNA();
else if (rounding.compare("RTP") == 0)
return rtlil_traits::RTP();
else if (rounding.compare("RTN") == 0)
return rtlil_traits::RTN();
else if (rounding.compare("RTZ") == 0)
return rtlil_traits::RTZ();
else if (rounding.compare("DYN") == 0)
return {};
else
log_cmd_error("Unknown rounding mode '%s'. Call help sympfpu for available rounding modes.\n", rounding);
}
using bwt = rtlil_traits::bwt;
using fpt = rtlil_traits::fpt;
using ubv = rtlil_traits::ubv;
using sbv = rtlil_traits::sbv;
using symfpu::ite;
using uf = symfpu::unpackedFloat<rtlil_traits>;
using uf_flagged = symfpu::floatWithStatusFlags<rtlil_traits>;
using uf_flagged_ite = symfpu::ite<prop, uf_flagged>;
using ubv_flagged = symfpu::bvWithStatusFlags<rtlil_traits, ubv>;
using sbv_flagged = symfpu::bvWithStatusFlags<rtlil_traits, sbv>;
PRIVATE_NAMESPACE_END
namespace symfpu
{
template <> struct ite<prop, prop> {
static prop iteOp(const prop &cond, const prop &t, const prop &e);
};
template <bool is_signed> struct ite<prop, bv<is_signed>> {
static bv<is_signed> iteOp(const prop &cond, const bv<is_signed> &t, const bv<is_signed> &e);
};
template <> struct ite<bool, prop> {
static prop iteOp(bool cond, const prop &t, const prop &e);
};
template <bool is_signed> struct ite<bool, bv<is_signed>> {
static bv<is_signed> iteOp(bool cond, const bv<is_signed> &t, const bv<is_signed> &e);
};
} // namespace symfpu
PRIVATE_NAMESPACE_BEGIN
struct prop {
SigBit bit;
explicit prop(SigBit bit) : bit(bit) {}
prop(bool v) : bit(v) {}
prop operator&&(const prop &op) const { return prop{symfpu_mod->And(NEW_ID, bit, op.bit)}; }
prop operator||(const prop &op) const { return prop{symfpu_mod->Or(NEW_ID, bit, op.bit)}; }
prop operator^(const prop &op) const { return prop{symfpu_mod->Xor(NEW_ID, bit, op.bit)}; }
prop operator!() const { return prop{symfpu_mod->Not(NEW_ID, bit)}; }
prop operator==(const prop &op) const { return prop{symfpu_mod->Eq(NEW_ID, bit, op.bit)}; }
const prop &named(std::string_view s) const
{
symfpu_mod->connect(symfpu_mod->addWire(symfpu_mod->uniquify(stringf("\\%s", s))), bit);
return *this;
}
};
template <bool is_signed> struct bv {
SigSpec bits;
const bv &named(std::string_view s) const
{
symfpu_mod->connect(symfpu_mod->addWire(symfpu_mod->uniquify(stringf("\\%s", s)), bits.size()), bits);
return *this;
}
friend ite<prop, bv<is_signed>>;
explicit bv(SigSpec bits) : bits(bits) {}
explicit bv(prop prop) : bits(prop.bit) {}
explicit bv(bwt w, unsigned v) { bits = Const((long long)v, w); }
bv(bv<!is_signed> const &other) : bits(other.bits) {}
bwt getWidth() const { return bits.size(); }
static bv<is_signed> one(bwt w) { return bv{SigSpec(1, w)}; }
static bv<is_signed> zero(bwt w) { return bv{SigSpec(0, w)}; }
static bv<is_signed> allOnes(bwt w) { return bv{SigSpec(State::S1, w)}; }
static bv<is_signed> maxValue(bwt w)
{
if (!is_signed)
return allOnes(w);
log_assert(w > 0);
Const value = Const(State::S1, w);
value.set(w - 1, State::S0);
return bv{SigSpec(value)};
}
static bv<is_signed> minValue(bwt w)
{
if (!is_signed)
return zero(w);
log_assert(w > 0);
Const value = Const(State::S0, w);
value.set(w - 1, State::S1);
return bv{SigSpec(value)};
}
bv<true> toSigned(void) const { return bv<true>(*this); }
bv<false> toUnsigned(void) const { return bv<false>(*this); }
bv<is_signed> extract(bwt upper, bwt lower) const
{
return bv{bits.extract(lower, upper + 1 - lower)};
}
bv<is_signed> extend(bwt extension) const
{
auto extended_bits = bits;
extended_bits.extend_u0(bits.size() + extension, is_signed);
return bv{extended_bits};
}
inline bv<is_signed> matchWidth(const bv<is_signed> &op) const
{
log_assert(this->getWidth() <= op.getWidth());
return this->extend(op.getWidth() - this->getWidth());
}
inline bv<is_signed> resize(bwt newSize) const
{
bwt width = this->getWidth();
if (newSize > width) {
return this->extend(newSize - width);
} else if (newSize < width) {
return this->extract(newSize - 1, 0);
} else {
return *this;
}
}
inline bv<is_signed> contract(bwt reduction) const
{
log_assert(getWidth() > reduction);
return resize(getWidth() - reduction);
}
bv<is_signed> append(const bv<is_signed> &op) const { return bv{SigSpec({bits, op.bits})}; }
prop isAllOnes() const { return prop{symfpu_mod->ReduceAnd(NEW_ID, bits)}; }
prop isAllZeros() const { return prop{symfpu_mod->ReduceAnd(NEW_ID, symfpu_mod->Not(NEW_ID, bits))}; }
bv<is_signed> operator-() const { return bv{symfpu_mod->Neg(NEW_ID, bits, is_signed)}; }
bv<is_signed> operator~() const { return bv{symfpu_mod->Not(NEW_ID, bits, is_signed)}; }
bv<is_signed> operator+(const bv<is_signed> &op) const
{
log_assert(getWidth() == op.getWidth());
return bv{symfpu_mod->Add(NEW_ID, bits, op.bits, is_signed)};
}
bv<is_signed> operator-(const bv<is_signed> &op) const
{
log_assert(getWidth() == op.getWidth());
return bv{symfpu_mod->Sub(NEW_ID, bits, op.bits, is_signed)};
}
bv<is_signed> operator*(const bv<is_signed> &op) const
{
log_assert(getWidth() == op.getWidth());
log_assert(!is_signed);
return bv{symfpu_mod->Mul(NEW_ID, bits, op.bits, is_signed)};
}
bv<is_signed> operator%(const bv<is_signed> &op) const
{
log_assert(getWidth() == op.getWidth());
log_assert(!is_signed);
return bv{symfpu_mod->Mod(NEW_ID, bits, op.bits, is_signed)};
}
bv<is_signed> operator/(const bv<is_signed> &op) const
{
log_assert(getWidth() == op.getWidth());
log_assert(!is_signed);
return bv{symfpu_mod->Div(NEW_ID, bits, op.bits, is_signed)};
}
bv<is_signed> operator|(const bv<is_signed> &op) const
{
log_assert(getWidth() == op.getWidth());
return bv{symfpu_mod->Or(NEW_ID, bits, op.bits, is_signed)};
}
bv<is_signed> operator&(const bv<is_signed> &op) const
{
log_assert(getWidth() == op.getWidth());
return bv{symfpu_mod->And(NEW_ID, bits, op.bits, is_signed)};
}
bv<is_signed> operator<<(const bv<is_signed> &op) const
{
log_assert(getWidth() == op.getWidth());
return bv{symfpu_mod->Shl(NEW_ID, bits, op.bits, is_signed)};
}
bv<is_signed> operator>>(const bv<is_signed> &op) const
{
log_assert(getWidth() == op.getWidth());
if (is_signed)
return bv{symfpu_mod->Sshr(NEW_ID, bits, op.bits, is_signed)};
else
return bv{symfpu_mod->Shr(NEW_ID, bits, op.bits, is_signed)};
}
prop operator!=(const bv<is_signed> &op) const
{
log_assert(getWidth() == op.getWidth());
return prop{symfpu_mod->Ne(NEW_ID, bits, op.bits, is_signed)};
}
prop operator==(const bv<is_signed> &op) const
{
log_assert(getWidth() == op.getWidth());
return prop{symfpu_mod->Eq(NEW_ID, bits, op.bits, is_signed)};
}
prop operator<=(const bv<is_signed> &op) const
{
log_assert(getWidth() == op.getWidth());
return prop{symfpu_mod->Le(NEW_ID, bits, op.bits, is_signed)};
}
prop operator>=(const bv<is_signed> &op) const
{
log_assert(getWidth() == op.getWidth());
return prop{symfpu_mod->Ge(NEW_ID, bits, op.bits, is_signed)};
}
prop operator<(const bv<is_signed> &op) const
{
log_assert(getWidth() == op.getWidth());
return prop{symfpu_mod->Lt(NEW_ID, bits, op.bits, is_signed)};
}
prop operator>(const bv<is_signed> &op) const
{
log_assert(getWidth() == op.getWidth());
return prop{symfpu_mod->Gt(NEW_ID, bits, op.bits, is_signed)};
}
inline bv<is_signed> increment() const { return *this + one(getWidth()); }
inline bv<is_signed> decrement() const { return *this - one(getWidth()); }
inline bv<is_signed> modularLeftShift(const bv<is_signed> &op) const { return *this << op; }
inline bv<is_signed> modularRightShift(const bv<is_signed> &op) const { return *this >> op; }
inline bv<is_signed> modularIncrement() const { return this->increment(); }
inline bv<is_signed> modularDecrement() const { return this->decrement(); }
inline bv<is_signed> modularAdd(const bv<is_signed> &op) const { return *this + op; }
inline bv<is_signed> modularSubtract(const bv<is_signed> &op) const { return *this - op; }
inline bv<is_signed> modularNegate() const { return -(*this); }
inline bv<is_signed> signExtendRightShift(const bv<is_signed> &op) const { return bv{sbv(sbv(*this) >> sbv(op))}; }
};
PRIVATE_NAMESPACE_END
prop symfpu::ite<prop, prop>::iteOp(const prop &cond, const prop &t, const prop &e) { return prop{symfpu_mod->Mux(NEW_ID, e.bit, t.bit, cond.bit)}; }
template <bool is_signed> bv<is_signed> symfpu::ite<prop, bv<is_signed>>::iteOp(const prop &cond, const bv<is_signed> &t, const bv<is_signed> &e)
{
log_assert(t.getWidth() == e.getWidth());
return bv<is_signed>{symfpu_mod->Mux(NEW_ID, e.bits, t.bits, cond.bit)};
}
[[maybe_unused]] prop symfpu::ite<bool, prop>::iteOp(bool cond, const prop &t, const prop &e) { return cond ? t : e; }
template <bool is_signed> bv<is_signed> symfpu::ite<bool, bv<is_signed>>::iteOp(bool cond, const bv<is_signed> &t, const bv<is_signed> &e)
{
log_assert(t.getWidth() == e.getWidth());
return cond ? t : e;
}
PRIVATE_NAMESPACE_BEGIN
prop rm::operator==(rm op) const { return mode == op.mode; }
void rtlil_traits::precondition(const prop &cond)
{
Cell *cell = symfpu_mod->addAssert(NEW_ID, cond.bit, State::S1);
cell->set_bool_attribute(ID(symfpu_pre));
}
void rtlil_traits::postcondition(const prop &cond)
{
Cell *cell = symfpu_mod->addAssert(NEW_ID, cond.bit, State::S1);
cell->set_bool_attribute(ID(symfpu_post));
}
void rtlil_traits::invariant(const prop &cond)
{
Cell *cell = symfpu_mod->addAssert(NEW_ID, cond.bit, State::S1);
cell->set_bool_attribute(ID(symfpu_inv));
}
ubv input_ubv(IdString name, int width)
{
auto input = symfpu_mod->addWire(name, width);
input->port_input = true;
return ubv(SigSpec(input));
}
prop input_prop(IdString name)
{
auto input = symfpu_mod->addWire(name);
input->port_input = true;
return prop(SigBit(input));
}
void output_ubv(IdString name, const ubv &value)
{
auto output = symfpu_mod->addWire(name, value.getWidth());
symfpu_mod->connect(output, value.bits);
output->port_output = true;
}
void output_prop(IdString name, const prop &value)
{
auto output = symfpu_mod->addWire(name);
symfpu_mod->connect(output, value.bit);
output->port_output = true;
}
// unpacked floats don't track NaN signalling, so we need to check the
// raw bitvector
template <bool is_signed> prop is_sNaN(bv<is_signed> bitvector, int sb) {
return bitvector.extract(sb-2, sb-2).isAllZeros();
}
struct SymFpuPass : public Pass {
SymFpuPass() : Pass("symfpu", "SymFPU based floating point netlist generator") {}
bool formatted_help() override
{
auto *help = PrettyHelp::get_current();
help->set_group("formal");
auto content_root = help->get_root();
content_root->usage("symfpu [size] [-op <OP>] [-rm <RM>]");
content_root->paragraph(
"Generates netlist for given floating point operation with floating point inputs "
"a, b, c, floating point output o, 5-bit input rm (rounding mode), and "
"5 single-bit outputs NV (invalid operation), DZ (divide by zero), OF (overflow), "
"UF (underflow), and NX (inexact)."
);
content_root->paragraph(
"Operations use single precision float unless [size] options are provided:"
);
content_root->option("-eb <N>", "use <N> bits for exponent; default=8");
content_root->option("-sb <N>", "use <N> bits for significand, including hidden bit; default=24");
// conversions could be useful, but for targeting Sail we don't need them
auto op_option = content_root->open_option("-op <OP>");
op_option->paragraph("floating point operation to generate, must be one of the below; default=mul");
op_option->codeblock(
"<OP> | description | equation\n"
"-------+--------------------------------+------------\n"
"sqrt | one input square root | o = sqrt(a)\n"
"add | two input addition | o = a+b\n"
"sub | two input subtraction | o = a-b\n"
"mul | two input multiplication | o = a*b\n"
"div | two input divison | o = a/b\n"
"min | two input minimum | o = min(a,b)\n"
"max | two input maximum | o = max(a,b)\n"
"muladd | three input fused multiple-add | o = (a*b)+c\n"
);
auto rm_option = content_root->open_option("-rm <RM>");
rm_option->paragraph("rounding mode to generate, must be one of the below; default=DYN");
rm_option->codeblock(
"<RM> | rm | description\n"
"-----+--------+----------------------\n"
"RNE | 00001 | round ties to even\n"
"RNA | 00010 | round ties to away\n"
"RTP | 00100 | round toward positive\n"
"RTN | 01000 | round toward negative\n"
"RTZ | 10000 | round toward zero\n"
"DYN | xxxxx | round based on 'rm' input signal\n"
);
rm_option->paragraph("Note: when not using DYN mode, the 'rm' input is ignored.");
content_root->usage("symfpu -classify [size]");
content_root->paragraph(
"Generates netlist for floating point classification of input a. Outputs "
"8 single-bit signals, isNormal, isSubnormal, isZero, isInfinite, isNaN, "
"isPositive, isNegative, and isFinite."
);
content_root->usage("symfpu -compare [size]");
content_root->paragraph(
"Generates netlist for floating point comparison of inputs a and b. Outputs "
"6 single-bit signals, smtlibEqual, ieee754Equal, lessThan, lessThanOrEqual, "
"sNV (invalid signaling comparison), and qNV (invalid quiet comparison)."
);
return true;
}
void execute(std::vector<std::string> args, RTLIL::Design *design) override
{
//TODO: fix multiple calls to symfpu in single Yosys instance
int eb = 8, sb = 24;
string op = "mul", rounding = "DYN";
int inputs = 2;
bool classify = false, compare = false;
log_header(design, "Executing SYMFPU pass.\n");
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++) {
if (args[argidx] == "-eb" && argidx+1 < args.size()) {
eb = atoi(args[++argidx].c_str());
continue;
}
if (args[argidx] == "-sb" && argidx+1 < args.size()) {
sb = atoi(args[++argidx].c_str());
continue;
}
if (args[argidx] == "-op" && argidx+1 < args.size()) {
op = args[++argidx];
if (op.compare("sqrt") == 0
|| op.compare("altsqrt") == 0) // currently undocumented
inputs = 1;
else if (op.compare("add") == 0
|| op.compare("sub") == 0
|| op.compare("mul") == 0
|| op.compare("altdiv") == 0 // currently undocumented
|| op.compare("alt2div") == 0 // currently undocumented
|| op.compare("min") == 0
|| op.compare("max") == 0
|| op.compare("div") == 0)
inputs = 2;
else if (op.compare("muladd") == 0)
inputs = 3;
else
log_cmd_error("Unknown operation '%s'. Call help symfpu for available operations.\n", op);
log("Generating '%s'\n", op);
continue;
}
if (args[argidx] == "-rm" && argidx+1 < args.size()) {
rounding = args[++argidx];
continue;
}
if (args[argidx] == "-classify") {
classify = true;
continue;
}
if (args[argidx] == "-compare") {
compare = true;
continue;
}
break;
}
extra_args(args, argidx, design);
if (compare && classify)
log_cmd_error("-classify and -compare flags are incompatible.\n");
if (rounding.compare("DYN") != 0) {
if (compare)
log_cmd_error("symfpu -compare does not support rounding modes.\n");
if (classify)
log_cmd_error("symfpu -classify does not support rounding modes.\n");
if (op.compare("min") == 0 || op.compare("max") == 0)
log_cmd_error("min/max operations do not support rounding modes.\n");
}
if (op.compare("mul") != 0) {
if (compare)
log_cmd_error("symfpu -compare does not support operator selection.\n");
if (classify)
log_cmd_error("symfpu -classify does not support operator selection.\n");
}
rm rounding_mode = parse_rounding(rounding);
fpt format(eb, sb);
auto mod = design->addModule(ID(symfpu));
symfpu_mod = mod;
auto a_bv = input_ubv(ID(a), eb+sb);
uf a = symfpu::unpack<rtlil_traits>(format, a_bv);
if (classify) {
output_prop(ID(isNormal), symfpu::isNormal(format, a));
output_prop(ID(isSubnormal), symfpu::isSubnormal(format, a));
output_prop(ID(isZero), symfpu::isZero(format, a));
output_prop(ID(isInfinite), symfpu::isInfinite(format, a));
output_prop(ID(isNaN), symfpu::isNaN(format, a));
output_prop(ID(isPositive), symfpu::isPositive(format, a));
output_prop(ID(isNegative), symfpu::isNegative(format, a));
output_prop(ID(isFinite), symfpu::isFinite(format, a));
} else if (compare) {
auto b_bv = input_ubv(ID(b), eb+sb);
uf b = symfpu::unpack<rtlil_traits>(format, b_bv);
output_prop(ID(smtlibEqual), symfpu::smtlibEqual(format, a, b));
output_prop(ID(ieee754Equal), symfpu::ieee754Equal(format, a, b));
output_prop(ID(lessThan), symfpu::lessThan(format, a, b));
output_prop(ID(lessThanOrEqual), symfpu::lessThanOrEqual(format, a, b));
output_prop(ID(sNV), a.getNaN() || b.getNaN());
output_prop(ID(qNV), (a.getNaN() && is_sNaN(a_bv, sb)) || (b.getNaN() && is_sNaN(b_bv, sb)));
} else {
auto b_bv = input_ubv(ID(b), eb+sb);
auto c_bv = input_ubv(ID(c), eb+sb);
uf b = symfpu::unpack<rtlil_traits>(format, b_bv);
uf c = symfpu::unpack<rtlil_traits>(format, c_bv);
auto rm_wire = symfpu_mod->addWire(ID(rm), 5);
rm_wire->port_input = true;
SigSpec rm_sig(rm_wire);
prop rm_RNE(rm_sig[0]);
prop rm_RNA(rm_sig[1]);
prop rm_RTP(rm_sig[2]);
prop rm_RTN(rm_sig[3]);
prop rm_RTZ(rm_sig[4]);
// signaling NaN inputs raise NV
prop signals_invalid((a.getNaN() && is_sNaN(a_bv, sb))
|| (b.getNaN() && is_sNaN(b_bv, sb) && inputs >= 2)
|| (c.getNaN() && is_sNaN(c_bv, sb) && inputs >= 3)
);
auto make_op = [&op, &format, &a, &b, &c](rm rounding_mode) {
if (op.compare("add") == 0)
return symfpu::add_flagged(format, rounding_mode, a, b, prop(true));
else if (op.compare("sub") == 0)
return symfpu::add_flagged(format, rounding_mode, a, b, prop(false));
else if (op.compare("mul") == 0)
return symfpu::multiply_flagged(format, rounding_mode, a, b);
else if (op.compare("div") == 0)
return symfpu::divide_flagged(format, rounding_mode, a, b);
else if (op.compare("sqrt") == 0)
return symfpu::sqrt_flagged(format, rounding_mode, a);
else if (op.compare("muladd") == 0)
return symfpu::fma_flagged(format, rounding_mode, a, b, c);
else if (op.compare("altdiv") == 0)
return symfpu::falseDivide_flagged(format, rounding_mode, a, b, prop(true));
else if (op.compare("alt2div") == 0)
return symfpu::falseDivide_flagged(format, rounding_mode, a, b, prop(false));
else if (op.compare("altsqrt") == 0)
return symfpu::falseSqrt_flagged(format, rounding_mode, a);
else if (op.compare("min") == 0)
// setting zeroCase=a.getSign() makes +0 > -0, as per IEEE 754-2019
return uf_flagged(symfpu::min(format, a, b, a.getSign()));
else if (op.compare("max") == 0)
return uf_flagged(symfpu::max(format, a, b, a.getSign()));
else
log_abort();
};
// calling this more than once will fail
auto output_fpu = [&signals_invalid, &format](const uf_flagged &o_flagged) {
output_prop(ID(NV), o_flagged.nv || signals_invalid);
output_prop(ID(DZ), o_flagged.dz);
output_prop(ID(OF), o_flagged.of);
output_prop(ID(UF), o_flagged.uf);
output_prop(ID(NX), o_flagged.nx);
output_ubv(ID(o), symfpu::pack<rtlil_traits>(format, o_flagged.val));
};
if (rounding.compare("DYN") != 0)
output_fpu(make_op(rounding_mode));
else {
auto out_RNE = make_op(rtlil_traits::RNE());
auto out_RNA = make_op(rtlil_traits::RNA());
auto out_RTP = make_op(rtlil_traits::RTP());
auto out_RTN = make_op(rtlil_traits::RTN());
auto out_RTZ = make_op(rtlil_traits::RTZ());
output_fpu(
uf_flagged_ite::iteOp(rm_RNE, out_RNE,
uf_flagged_ite::iteOp(rm_RNA, out_RNA,
uf_flagged_ite::iteOp(rm_RTP, out_RTP,
uf_flagged_ite::iteOp(rm_RTN, out_RTN,
uf_flagged_ite::iteOp(rm_RTZ, out_RTZ,
uf_flagged::makeNaN(format, prop(true)))))))
);
}
}
symfpu_mod->fixup_ports();
}
} SymFpuPass;
struct SymFpuConvertPass : public Pass {
SymFpuConvertPass() : Pass("symfpu_convert", "SymFPU based floating point conversion netlist generator") {}
bool formatted_help() override
{
auto *help = PrettyHelp::get_current();
help->set_group("formal");
auto content_root = help->get_root();
content_root->usage("symfpu_convert <insize> <outsize> [-rm <RM>]");
content_root->paragraph(
"Generates netlist for converting given input size to given output size. "
"Generated module has one input `i`, and three outputs, `o_if`, `o_fi`, and `o_ff`, "
"performing int -> float, float -> int, and float -> float conversions respectively. "
);
content_root->option("-isize <iN>", "input port is <iN> bits wide; default=32");
content_root->option("-osize <oN>", "output ports are <oN> bits wide; default=32");
content_root->option("-iexp <iM>", "input port uses <iM> bits for exponent; default=8");
content_root->option("-oexp <oM>", "output ports use <oM> bits for exponent; default=8");
content_root->paragraph(
"<M> bits of exponent implies <N-M> bits of significand (including hidden bit), "
"e.g. the default is single precision float with N=32 and M=8 (and 24 bits of significand). "
);
auto rm_option = content_root->open_option("-rm <RM>");
rm_option->paragraph("rounding mode to generate, must be one of the below; default=DYN");
rm_option->codeblock(
"<RM> | rm | description\n"
"-----+--------+----------------------\n"
"RNE | 00001 | round ties to even\n"
"RNA | 00010 | round ties to away\n"
"RTP | 00100 | round toward positive\n"
"RTN | 01000 | round toward negative\n"
"RTZ | 10000 | round toward zero\n"
"DYN | xxxxx | round based on 'rm' input signal\n"
);
rm_option->paragraph("Note: when not using DYN mode, the 'rm' input is ignored.");
return true;
}
void execute(std::vector<std::string> args, RTLIL::Design *design) override
{
//TODO: fix multiple calls to symfpu in single Yosys instance
//TODO: signed integers
int i_size = 32, o_size = 32, i_exp = 8, o_exp = 8;
string rounding = "DYN";
log_header(design, "Executing SYMFPU_CONVERT pass.\n");
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++) {
// all args take a value
if (argidx+1 >= args.size())
break;
if (args[argidx] == "-isize") {
i_size = atoi(args[++argidx].c_str());
continue;
}
if (args[argidx] == "-osize") {
o_size = atoi(args[++argidx].c_str());
continue;
}
if (args[argidx] == "-iexp") {
i_exp = atoi(args[++argidx].c_str());
continue;
}
if (args[argidx] == "-oexp") {
o_exp = atoi(args[++argidx].c_str());
continue;
}
if (args[argidx] == "-rm") {
rounding = args[++argidx];
continue;
}
break;
}
extra_args(args, argidx, design);
if (o_exp >= o_size || o_exp <= 0)
log_cmd_error("-oexp value (%d) must be in range: 0 < oM < oN (oN=%d)!\n", o_exp, o_size);
if (i_exp >= i_size || i_exp <= 0)
log_cmd_error("-iexp value (%d) must be in range: 0 < iM < iN (iN=%d)!\n", i_exp, i_size);
if (rounding.compare("DYN") == 0)
log_cmd_error("rm must be set to a single rounding mode!\n");
rm rounding_mode = parse_rounding(rounding);
auto mod = design->addModule(ID(symfpu));
symfpu_mod = mod;
fpt i_format(i_exp, i_size-i_exp);
fpt o_format(o_exp, o_size-o_exp);
auto i_bv = input_ubv(ID(i), i_size);
uf i_f = symfpu::unpack<rtlil_traits>(i_format, i_bv);
prop i_sNaN(i_f.getNaN() && is_sNaN(i_bv, i_size-i_exp));
auto output_flags = [](IdString name, const prop &nv, const prop &nx, const prop &of = prop(false), const prop &uf = prop(false), const prop &dz = prop(false)) {
output_ubv(name, ubv{SigSpec({nv.bit, dz.bit, of.bit, uf.bit, nx.bit})});
};
uf_flagged o_ff = symfpu::convertFloatToFloat_flagged(i_format, o_format, rounding_mode, i_f);
output_ubv(ID(o_ff), symfpu::pack<rtlil_traits>(o_format, o_ff.val));
output_flags(ID(flags_ff), o_ff.nv || i_sNaN, o_ff.nx, o_ff.of, o_ff.uf);
auto is_signed = input_prop(ID(is_signed));
// use riscv behavior for invalid inputs
ubv o_signed_default = symfpu::ITE(i_f.getSign(), ubv::one(1).append(ubv::zero(o_size-1)), ubv::zero(1).append(ubv::allOnes(o_size-1)));
ubv o_unsigned_default = symfpu::ITE(i_f.getSign(), ubv::zero(o_size), ubv::allOnes(o_size));
auto o_fi_signed = symfpu::convertFloatToSBV_flagged(i_format, rounding_mode, i_f, o_size, o_signed_default);
auto o_fi_unsigned = symfpu::convertFloatToUBV_flagged(i_format, rounding_mode, i_f, o_size, o_unsigned_default);
output_ubv(ID(o_fi), symfpu::ITE(is_signed, o_fi_signed.val.toUnsigned(), o_fi_unsigned.val));
output_flags(ID(flags_fi),
symfpu::ITE(is_signed, o_fi_signed.nv, o_fi_unsigned.nv),
symfpu::ITE(is_signed, o_fi_signed.nx, o_fi_unsigned.nx));
uf_flagged o_if(uf_flagged_ite::iteOp(is_signed,
symfpu::convertSBVToFloat_flagged<rtlil_traits>(o_format, rounding_mode, i_bv),
symfpu::convertUBVToFloat_flagged<rtlil_traits>(o_format, rounding_mode, i_bv)));
output_ubv(ID(o_if), symfpu::pack<rtlil_traits>(o_format, o_if.val));
output_flags(ID(flags_if), o_if.nv, o_if.nx, o_if.of);
symfpu_mod->fixup_ports();
}
} SymFpuConvertPass;
PRIVATE_NAMESPACE_END

View File

@ -198,9 +198,6 @@ yosys_pass(dfflegalize
yosys_pass(dffunmap
dffunmap.cc
)
yosys_pass(flowmap
flowmap.cc
)
yosys_pass(extractinv
extractinv.cc
)

View File

@ -35,12 +35,6 @@
#define ABC_COMMAND_SOP "strash; &get -n; &fraig -x; &put; scorr; dc2; dretime; strash; dch -f; cover {I} {P}"
#define ABC_COMMAND_DFL "strash; &get -n; &fraig -x; &put; scorr; dc2; dretime; strash; &get -n; &dch -f; &nf {D}; &put"
#define ABC_FAST_COMMAND_LIB "strash; dretime; map {D}"
#define ABC_FAST_COMMAND_CTR "strash; dretime; map {D}; buffer; upsize {D}; dnsize {D}; stime -p"
#define ABC_FAST_COMMAND_LUT "strash; dretime; if"
#define ABC_FAST_COMMAND_SOP "strash; dretime; cover {I} {P}"
#define ABC_FAST_COMMAND_DFL "strash; dretime; map"
#include "kernel/register.h"
#include "kernel/sigtools.h"
#include "kernel/newcelltypes.h"
@ -139,7 +133,6 @@ struct AbcConfig
std::vector<std::string> dont_use_cells;
bool cleanup = true;
bool keepff = false;
bool fast_mode = false;
bool show_tempdir = false;
bool sop_mode = false;
bool abc_dress = false;
@ -1077,16 +1070,15 @@ void AbcModuleState::prepare_module(RTLIL::Design *design, RTLIL::Module *module
for (int this_cost : config.lut_costs)
if (this_cost != config.lut_costs.front())
all_luts_cost_same = false;
run_abc.abc_script += config.fast_mode ? ABC_FAST_COMMAND_LUT : ABC_COMMAND_LUT;
if (all_luts_cost_same && !config.fast_mode)
run_abc.abc_script += ABC_COMMAND_LUT;
if (all_luts_cost_same)
run_abc.abc_script += "; lutpack -S 1";
} else if (!config.liberty_files.empty() || !config.genlib_files.empty())
run_abc.abc_script += config.constr_file.empty() ?
(config.fast_mode ? ABC_FAST_COMMAND_LIB : ABC_COMMAND_LIB) : (config.fast_mode ? ABC_FAST_COMMAND_CTR : ABC_COMMAND_CTR);
run_abc.abc_script += config.constr_file.empty() ? ABC_COMMAND_LIB : ABC_COMMAND_CTR;
else if (config.sop_mode)
run_abc.abc_script += config.fast_mode ? ABC_FAST_COMMAND_SOP : ABC_COMMAND_SOP;
run_abc.abc_script += ABC_COMMAND_SOP;
else
run_abc.abc_script += config.fast_mode ? ABC_FAST_COMMAND_DFL : ABC_COMMAND_DFL;
run_abc.abc_script += ABC_COMMAND_DFL;
if (config.script_file.empty() && !config.delay_target.empty())
for (size_t pos = run_abc.abc_script.find("dretime;"); pos != std::string::npos; pos = run_abc.abc_script.find("dretime;", pos+1))
@ -1911,25 +1903,6 @@ struct AbcPass : public Pass {
log(" otherwise:\n");
log("%s\n", fold_abc_cmd(ABC_COMMAND_DFL));
log("\n");
log(" -fast\n");
log(" use different default scripts that are slightly faster (at the cost\n");
log(" of output quality):\n");
log("\n");
log(" for -liberty/-genlib without -constr:\n");
log("%s\n", fold_abc_cmd(ABC_FAST_COMMAND_LIB));
log("\n");
log(" for -liberty/-genlib with -constr:\n");
log("%s\n", fold_abc_cmd(ABC_FAST_COMMAND_CTR));
log("\n");
log(" for -lut/-luts:\n");
log("%s\n", fold_abc_cmd(ABC_FAST_COMMAND_LUT));
log("\n");
log(" for -sop:\n");
log("%s\n", fold_abc_cmd(ABC_FAST_COMMAND_SOP));
log("\n");
log(" otherwise:\n");
log("%s\n", fold_abc_cmd(ABC_FAST_COMMAND_DFL));
log("\n");
log(" -liberty <file>\n");
log(" generate netlists for the specified cell library (using the liberty\n");
log(" file format).\n");
@ -2093,7 +2066,6 @@ struct AbcPass : public Pass {
config.abc_dress = design->scratchpad_get_bool("abc.dress", false);
g_arg = design->scratchpad_get_string("abc.g", g_arg);
config.fast_mode = design->scratchpad_get_bool("abc.fast", false);
bool dff_mode = design->scratchpad_get_bool("abc.dff", false);
std::string clk_str;
if (design->scratchpad.count("abc.clk")) {
@ -2202,10 +2174,6 @@ struct AbcPass : public Pass {
g_arg_from_cmd = true;
continue;
}
if (arg == "-fast") {
config.fast_mode = true;
continue;
}
if (arg == "-dff") {
dff_mode = true;
continue;

File diff suppressed because it is too large Load Diff

View File

@ -13,7 +13,6 @@ yosys_pass(synth
check
clean
flatten
flowmap
fsm
hierarchy
memory

View File

@ -92,9 +92,6 @@ struct SynthPass : public ScriptPass {
log(" -abc9\n");
log(" use new ABC9 flow (EXPERIMENTAL)\n");
log("\n");
log(" -flowmap\n");
log(" use FlowMap LUT techmapping instead of ABC\n");
log("\n");
log(" -no-rw-check\n");
log(" marks all recognized read ports as \"return don't-care value on\n");
log(" read/write collision\" (same result as setting the no_rw_check\n");
@ -115,7 +112,7 @@ struct SynthPass : public ScriptPass {
}
string top_module, fsm_opts, memory_opts, abc, latches_opt;
bool autotop, flatten, noalumacc, nofsm, noabc, noshare, flowmap, booth, arith_tree, hieropt, relative_share;
bool autotop, flatten, noalumacc, nofsm, noabc, noshare, booth, arith_tree, hieropt, relative_share;
int lut;
std::vector<std::string> techmap_maps;
@ -133,7 +130,6 @@ struct SynthPass : public ScriptPass {
nofsm = false;
noabc = false;
noshare = false;
flowmap = false;
booth = false;
arith_tree = false;
hieropt = false;
@ -216,10 +212,6 @@ struct SynthPass : public ScriptPass {
abc = "abc9";
continue;
}
if (args[argidx] == "-flowmap") {
flowmap = true;
continue;
}
if (args[argidx] == "-no-rw-check") {
memory_opts += " -no-rw-check";
continue;
@ -246,8 +238,6 @@ struct SynthPass : public ScriptPass {
if (abc == "abc9" && !lut)
log_cmd_error("ABC9 flow only supported for FPGA synthesis (using '-lut' option)\n");
if (flowmap && !lut)
log_cmd_error("FlowMap is only supported for FPGA synthesis (using '-lut' option)\n");
log_header(design, "Executing SYNTH pass.\n");
log_push();
@ -334,16 +324,13 @@ struct SynthPass : public ScriptPass {
if (help_mode) {
run(techmap_cmd + " -map +/gate2lut.v", "(if -noabc and -lut)");
run("clean; opt_lut", " (if -noabc and -lut)");
run("flowmap -maxlut K", " (if -flowmap and -lut)");
} else if (noabc && lut) {
run(stringf("%s -map +/gate2lut.v -D LUT_WIDTH=%d", techmap_cmd, lut));
run("clean; opt_lut");
} else if (flowmap) {
run(stringf("flowmap -maxlut %d", lut));
}
run("opt -fast" + hieropt_flag);
if ((!noabc && !flowmap) || help_mode) {
if (!noabc || help_mode) {
#ifdef YOSYS_ENABLE_ABC
if (help_mode) {
run(abc, " (unless -noabc, unless -lut)");

View File

@ -38,7 +38,6 @@ yosys_pass(synth_ice40
deminout
dfflegalize
flatten
flowmap
fsm
hierarchy
ice40_braminit

View File

@ -109,9 +109,6 @@ struct SynthIce40Pass : public ScriptPass
log(" -noabc9\n");
log(" disable use of new ABC9 flow\n");
log("\n");
log(" -flowmap\n");
log(" use FlowMap LUT techmapping instead of abc (EXPERIMENTAL)\n");
log("\n");
log(" -no-rw-check\n");
log(" marks all recognized read ports as \"return don't-care value on\n");
log(" read/write collision\" (same result as setting the no_rw_check\n");
@ -130,7 +127,7 @@ struct SynthIce40Pass : public ScriptPass
}
string top_opt, blif_file, edif_file, json_file, device_opt, latches;
bool nocarry, nodffe, nobram, spram, dsp, flatten, retime, noabc, abc2, vpr, abc9, dff, flowmap, no_rw_check;
bool nocarry, nodffe, nobram, spram, dsp, flatten, retime, noabc, abc2, vpr, abc9, dff, no_rw_check;
int min_ce_use;
void clear_flags() override
@ -151,7 +148,6 @@ struct SynthIce40Pass : public ScriptPass
abc2 = false;
vpr = false;
abc9 = true;
flowmap = false;
device_opt = "hx";
no_rw_check = false;
latches = "error";
@ -257,10 +253,6 @@ struct SynthIce40Pass : public ScriptPass
device_opt = args[++argidx];
continue;
}
if (args[argidx] == "-flowmap") {
flowmap = true;
continue;
}
if (args[argidx] == "-no-rw-check") {
no_rw_check = true;
continue;
@ -284,10 +276,6 @@ struct SynthIce40Pass : public ScriptPass
log_cmd_error("-retime option not currently compatible with -abc9!\n");
if (abc9 && noabc)
log_cmd_error("-abc9 is incompatible with -noabc!\n");
if (abc9 && flowmap)
log_cmd_error("-abc9 is incompatible with -flowmap!\n");
if (flowmap && noabc)
log_cmd_error("-flowmap is incompatible with -noabc!\n");
log_header(design, "Executing SYNTH_ICE40 pass.\n");
log_push();
@ -422,12 +410,10 @@ struct SynthIce40Pass : public ScriptPass
if (latches == "error" || help_mode)
run("check -latchonly -assert", "(only if -latches error, the default)");
run("techmap -map +/ice40/latches_map.v");
if (noabc || flowmap || help_mode) {
run("simplemap", " (if -noabc or -flowmap)");
if (noabc || help_mode) {
run("simplemap", " (if -noabc)");
if (noabc || help_mode)
run("techmap -map +/gate2lut.v -D LUT_WIDTH=4", "(only if -noabc)");
if (flowmap || help_mode)
run("flowmap -maxlut 4", "(only if -flowmap)");
}
if (!noabc) {
if (abc9) {

View File

@ -77,7 +77,7 @@ void run_fixed(xilinx_srl_pm &pm)
}
else
log_abort();
if (first_cell->type.in(ID($_DFFE_NP_), ID($_DFFE_PP_)))
if (first_cell->type.in(ID($_DFFE_NP_), ID($_DFFE_PP_), ID(FDRE), ID(FDRE_1)))
c->setParam(ID(ENPOL), 1);
else if (first_cell->type.in(ID($_DFFE_NN_), ID($_DFFE_PN_)))
c->setParam(ID(ENPOL), 0);

View File

@ -76,6 +76,7 @@ MK_TEST_DIRS += ./aiger
MK_TEST_DIRS += ./alumacc
MK_TEST_DIRS += ./check_mem
MK_TEST_DIRS += ./write_verilog
MK_TEST_DIRS += ./symfpu
all: vanilla-test

View File

@ -0,0 +1,46 @@
# Regression test for a xilinx_srl bug where a fixed shift register inferred
# from FDRE cells dropped the clock enable. FDRE has an active high clock
# enable but run_fixed assigned it ENPOL 2 (no enable) instead of ENPOL 1,
# so the resulting shift register shifted every cycle and ignored stalls.
read_verilog <<EOT
module xilinx_srl_enable_test(input i, clk, ce, output q);
reg [3:0] shift = 4'b0000;
always @(posedge clk)
if (ce)
shift <= {shift[2:0], i};
assign q = shift[3];
endmodule
module $__XILINX_SHREG_(input C, D, E, input [1:0] L, output Q);
parameter CLKPOL = 1;
parameter ENPOL = 1;
parameter DEPTH = 2;
parameter [DEPTH-1:0] INIT = {DEPTH{1'b0}};
reg [DEPTH-1:0] r = INIT;
wire ce = (ENPOL == 2) ? 1'b1 : (ENPOL == 1) ? E : ~E;
always @(posedge C)
if (ce)
r <= { r[DEPTH-2:0], D };
assign Q = r[L];
endmodule
EOT
design -copy-to model $__XILINX_SHREG_
hierarchy -top xilinx_srl_enable_test
prep
design -save gold
synth_xilinx -noiopad -noclkbuf -run begin:map_luts
opt_expr -mux_undef -noclkinv
techmap -map +/xilinx/ff_map.v
xilinx_srl -fixed
opt
select -assert-count 1 t:$__XILINX_SHREG_
design -stash gate
design -import gold -as gold
design -import gate -as gate
design -copy-from model -as $__XILINX_SHREG_ \$__XILINX_SHREG_
prep
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -show-ports -seq 6 miter

1
tests/symfpu/.gitignore vendored Normal file
View File

@ -0,0 +1 @@
*_edges.ys

784
tests/symfpu/edges.sv Normal file
View File

@ -0,0 +1,784 @@
module edges(input clk);
`ifdef MASK
(* anyseq *) reg [31:0] a_in, b_in, c_in;
wire [31:0] a, b, c;
assign a = a_in & 32'hffc42108;
assign b = b_in & 32'hfff80001;
assign c = c_in & 32'hfff80001;
`elsif MAP
(* anyseq *) reg [31:0] a_pre, b_pre, c_pre;
wire [31:0] a_in, b_in, c_in;
// assuming 8/24
assign a_in[31:22] = a_pre[31:22];
assign b_in[31:22] = b_pre[31:22];
assign a_in[21:0] = (a_pre[21:0] & 22'h042100) | (|(a_pre[21:0] & ~22'h042100) << 3);
assign b_in[21:0] = (b_pre[21:0] & 22'h380000) | (|(b_pre[21:0] & ~22'h380000) << 0);
assign c_in = c_pre;
wire [31:0] a, b, c;
assign a = a_in & 32'hffc42108;
assign b = b_in & 32'hfff80001;
assign c = c_in & 32'hfff80001;
`else
(* anyseq *) reg [31:0] a, b, c;
`endif
(* anyseq *) reg [4:0] rm;
reg [31:0] o;
reg NV, DZ, OF, UF, NX;
symfpu mod (.*);
wire [31:0] pos_max = 32'h7f7fffff;
wire [31:0] pos_inf = 32'h7f800000;
wire [31:0] neg_max = 32'hff7fffff;
wire [31:0] neg_inf = 32'hff800000;
wire a_sign = a[31];
wire [30:0] a_unsigned = a[30:0];
wire [7:0] a_exp = a[30:23];
wire [22:0] a_sig = a[22:0];
wire a_zero = a_unsigned == '0;
wire a_special = a_exp == 8'hff;
wire a_inf = a_special && a_sig == '0;
wire a_nan = a_special && a_sig != '0;
wire a_qnan = a_nan && a_sig[22] && a_sig[21:0] == '0;
wire a_snan = a_nan && !a_sig[22];
wire a_norm = a_exp > 8'h00 && !a_special;
wire a_subnorm = a_exp == 8'h00 && a_sig != '0;
wire a_finite = a_norm || a_subnorm;
wire signed [8:0] a_sexp = $signed({1'b0, a_exp}) - 8'h7f;
wire signed [8:0] half_a_sexp = a_sexp >>> 1;
wire b_sign = b[31];
wire [30:0] b_unsigned = b[30:0];
wire [7:0] b_exp = b[30:23];
wire [22:0] b_sig = b[22:0];
wire b_zero = b_unsigned == '0;
wire b_special = b_exp == 8'hff;
wire b_inf = b_special && b_sig == '0;
wire b_nan = b_special && b_sig != '0;
wire b_qnan = b_nan && b_sig[22];
wire b_snan = b_nan && !b_sig[22];
wire b_norm = b_exp > 8'h00 && !b_special;
wire b_subnorm = b_exp == 8'h00 && b_sig != '0;
wire b_finite = b_norm || b_subnorm;
wire c_sign = c[31];
wire [30:0] c_unsigned = c[30:0];
wire [7:0] c_exp = c[30:23];
wire [22:0] c_sig = c[22:0];
wire c_zero = c_unsigned == '0;
wire c_special = c_exp == 8'hff;
wire c_inf = c_special && c_sig == '0;
wire c_nan = c_special && c_sig != '0;
wire c_qnan = c_nan && c_sig[22];
wire c_snan = c_nan && !c_sig[22];
wire c_norm = c_exp > 8'h00 && !c_special;
wire c_subnorm = c_exp == 8'h00 && c_sig != '0;
wire c_finite = c_norm || c_subnorm;
wire o_sign = o[31];
wire [30:0] o_unsigned = o[30:0];
wire [7:0] o_exp = o[30:23];
wire [22:0] o_sig = o[22:0];
wire o_zero = o_unsigned == '0;
wire o_special = o_exp == 8'hff;
wire o_inf = o_special && o_sig == '0;
wire o_nan = o_special && o_sig != '0;
wire o_qnan = o_nan && o_sig[22];
wire o_snan = o_nan && !o_sig[22];
wire o_norm = o_exp > 8'h00 && !o_special;
wire o_subnorm = o_exp == 8'h00 && o_sig != '0;
wire o_finite = o_norm || o_subnorm;
wire o_clamped = o_unsigned == 31'h7f7fffff;
wire o_unclamped = o_finite && !o_clamped;
wire o_ebmin = o_exp == 8'h01 && o_sig == '0;
wire signed [8:0] o_sexp = $signed({1'b0, o_exp}) - 8'h7f;
(* keep *) wire [25:0] a_faux = {2'b10, !a_subnorm, a_sig};
(* keep *) wire [25:0] b_faux = {2'b00, !b_subnorm, b_sig};
(* keep *) wire [25:0] o_faux = (a_faux - b_faux);
`ifdef MULADD
wire muladd_zero = c_zero;
wire a_is_1 = a == 32'h3f800000;
wire b_is_1 = b == 32'h3f800000;
wire use_lhs = a_is_1 || b_is_1;
wire lhs_sign = b_is_1 ? a_sign : b_sign;
wire [30:0] lhs_unsigned = b_is_1 ? a_unsigned : b_unsigned;
wire [7:0] lhs_exp = b_is_1 ? a_exp : b_exp;
wire [22:0] lhs_sig = b_is_1 ? a_sig : b_sig;
wire lhs_zero = b_is_1 ? a_zero : b_zero;
wire lhs_inf = b_is_1 ? a_inf : b_inf;
wire lhs_nan = b_is_1 ? a_nan : b_nan;
wire lhs_qnan = b_is_1 ? a_qnan : b_qnan;
wire lhs_snan = b_is_1 ? a_snan : b_snan;
wire lhs_norm = b_is_1 ? a_norm : b_norm;
wire lhs_subnorm = b_is_1 ? a_subnorm : b_subnorm;
wire lhs_finite = b_is_1 ? a_finite : b_finite;
wire rhs_sign = c_sign;
wire [30:0] rhs_unsigned = c_unsigned;
wire [7:0] rhs_exp = c_exp;
wire [22:0] rhs_sig = c_sig;
wire rhs_zero = c_zero;
wire rhs_inf = c_inf;
wire rhs_nan = c_nan;
wire rhs_qnan = c_qnan;
wire rhs_snan = c_snan;
wire rhs_norm = c_norm;
wire rhs_subnorm = c_subnorm;
wire rhs_finite = c_finite;
`else
wire muladd_zero = 1;
wire use_lhs = 1;
wire lhs_sign = a_sign;
wire [30:0] lhs_unsigned = a_unsigned;
wire [7:0] lhs_exp = a_exp;
wire [22:0] lhs_sig = a_sig;
wire lhs_zero = a_zero;
wire lhs_inf = a_inf;
wire lhs_nan = a_nan;
wire lhs_qnan = a_qnan;
wire lhs_snan = a_snan;
wire lhs_norm = a_norm;
wire lhs_subnorm = a_subnorm;
wire lhs_finite = a_finite;
wire rhs_sign = b_sign;
wire [30:0] rhs_unsigned = b_unsigned;
wire [7:0] rhs_exp = b_exp;
wire [22:0] rhs_sig = b_sig;
wire rhs_zero = b_zero;
wire rhs_inf = b_inf;
wire rhs_nan = b_nan;
wire rhs_qnan = b_qnan;
wire rhs_snan = b_snan;
wire rhs_norm = b_norm;
wire rhs_subnorm = b_subnorm;
wire rhs_finite = b_finite;
`endif
`ifdef SUB
wire is_sub = lhs_sign == rhs_sign;
`else
wire is_sub = lhs_sign != rhs_sign;
`endif
wire lhs_dominates = lhs_exp > rhs_exp;
wire [7:0] exp_diff = lhs_dominates ? lhs_exp - rhs_exp : rhs_exp - lhs_exp;
wire round_p_001, round_p_011, round_n_001, round_n_011;
wire [30:0] rounded_100, rounded_010, rounded_000;
`ifdef MUL
assign round_p_001 = 0;
assign round_p_011 = a == 32'h40400000 && b == 32'h40000001;
assign round_n_001 = 0;
assign round_n_011 = a == 32'hc0400000 && b == 32'h40000001;
assign rounded_100 = 31'h40C00002;
assign rounded_010 = 31'h40C00001;
assign rounded_000 = 31'h40C00000;
`elsif ADD
assign round_p_001 = a == 32'h4c000000 && b == 32'h40000000;
assign round_p_011 = a == 32'h4c000001 && b == 32'h40000000;
assign round_n_001 = a == 32'hcc000000 && b == 32'hc0000000;
assign round_n_011 = a == 32'hcc000001 && b == 32'hc0000000;
assign rounded_100 = 31'h4C000002;
assign rounded_010 = 31'h4C000001;
assign rounded_000 = 31'h4C000000;
`else
assign round_p_001 = 0;
assign round_p_011 = 0;
assign round_n_001 = 0;
assign round_n_011 = 0;
assign rounded_100 = '0;
assign rounded_010 = '0;
assign rounded_000 = '0;
`endif
`ifdef MAX
wire choose_max = 1;
`else
wire choose_max = 0;
`endif
wire rm_RNE = rm[0] == 1'b1;
wire rm_RNA = rm[1:0] == 2'b10;
wire rm_RTP = rm[2:0] == 3'b100;
wire rm_RTN = rm[3:0] == 4'b1000;
wire rm_RTZ = rm[4:0] == 5'b10000;
wire c_muladd_turning = rm_RNE || rm_RNA ? c_sig <= 23'h200000 :
rm_RTP ? c_sig == '0 :
rm_RTN ? c_sig < 23'h400000 :
c_sig == '0;
always @* begin
// all classes of input are possible (for all inputs)
cover (a_sign);
cover (!a_sign);
cover (a_zero);
cover (a_norm);
cover (a_subnorm);
cover (a_inf);
cover (a_qnan);
cover (a_snan);
`ifndef SQRTS
// sqrt has no b input
cover (b_sign);
cover (!b_sign);
cover (b_zero);
cover (b_norm);
cover (b_subnorm);
cover (b_inf);
cover (b_qnan);
cover (b_snan);
`endif
`ifdef MULADD
// only muladd has c input
cover (c_sign);
cover (!c_sign);
cover (c_zero);
cover (c_norm);
cover (c_subnorm);
cover (c_inf);
cover (c_qnan);
cover (c_snan);
`endif
// all flags are possible
cover (NV);
`ifndef COMPARES
`ifdef DIVS
// only div can div/zero
cover (DZ);
`endif
`ifndef SQRTS
// sqrt can't overflow or underflow
cover (OF);
`ifndef ADDSUB
// add/sub can't underflow
cover (UF);
`endif
`endif
cover (NX);
`endif
cover (!NV);
cover (!DZ);
cover (!OF);
cover (!UF);
cover (!NX);
// all classes of output are possible
cover (o_sign);
cover (!o_sign);
cover (o_zero);
cover (o_norm);
cover (o_inf);
cover (o_nan);
`ifndef SQRTS
// subnormal outputs not possible for 8/24 sqrt
cover (o_subnorm);
cover (o_ebmin);
`endif
`ifndef COMPARES
`ifndef SQRTS
if (OF) begin
cover (o_inf);
cover (o_clamped);
end else begin
cover (o_inf);
cover (o_clamped);
end
if (UF) begin
`ifndef ADDSUB
cover (o_zero);
cover (o_ebmin);
cover (o_subnorm);
`endif
end else begin
cover (o_zero);
cover (o_ebmin);
cover (o_subnorm);
end
if (NX) begin
cover (o_norm);
cover (o_inf);
`ifndef ADDSUB
cover (o_subnorm);
cover (o_zero);
`endif
end
`endif
if (a_nan || b_nan || c_nan) begin
// input NaN = output NaN
assert (o_nan);
// NaN inputs give NaN outputs, do not raise exceptions (unless signaling NV)
assert (!DZ);
assert (!OF);
assert (!UF);
assert (!NX);
end
if (NV)
// output = qNaN
assert (o_qnan);
`endif // !COMPARES
if (a_snan || b_snan)
// signalling NaN raises invalid exception
assert (NV);
if (a_qnan && b_qnan && c_qnan)
// quiet NaN inputs do not raise invalid exception
assert (!NV);
if (DZ)
// output = +-inf
assert (o_inf);
if (OF)
// overflow is always inexact
assert (NX);
if (UF)
// underflow is always inexact
assert (NX);
if (UF)
// output = subnormal or zero or +-e^bmin
assert (o_subnorm || o_zero || o_ebmin);
if (o_inf && !OF)
// a non-overflowing infinity is exact
assert (!NX);
if (o_subnorm && !UF)
// a non-underflowing subnormal is exact
assert (!NX);
`ifdef COMPARES
assume (c_zero);
assert (!OF);
assert (!UF);
assert (!NX);
assert (!DZ);
if (!a_nan && b_nan)
assert (o == a);
else if (a_nan && !b_nan)
assert (o == b);
else if (a_nan && b_nan)
assert (o_nan);
else begin
assert (o == a || o == b);
if (a_inf) begin
if (a_sign == choose_max)
assert (o == b);
else
assert (o == a);
end
if (b_inf) begin
if (b_sign == choose_max)
assert (o == a);
else
assert (o == b);
end
end
if (!a_special && !b_special) begin
if (a_sign != b_sign)
if (a_sign == choose_max)
assert (o == b);
else
assert (o == a);
// a_sign == b_sign
else if (a_exp != b_exp)
if ((a_exp > b_exp) ^ a_sign ^ choose_max)
assert (o == b);
else
assert (o == a);
// a_exp == b_exp
else if ((a_sig > b_sig) ^ a_sign ^ choose_max)
assert (o == b);
else
assert (o == a);
end
`endif
`ifdef DIVS
assume (c_zero);
// div/zero only when a is finite
assert (DZ ^~ (a_finite && b_zero));
// 0/0 or inf/inf
if ((a_zero && b_zero) || (a_inf && b_inf))
assert (NV);
// dividing by a very small number will overflow
if (a_norm && a_exp > 8'h80 && b == 32'h00000001)
assert (OF);
// dividing by a much smaller number will overflow
if (a_norm && b_finite && lhs_dominates && exp_diff > 8'h80)
assert (OF);
// dividing by a much larger number will hit 0 bias
if (a_finite && b_norm && !lhs_dominates && exp_diff > 8'h7f) begin
assert (o_exp == '0);
// if the divisor is large enough, underflow (or zero) is guaranteed
if (exp_diff > 8'h95) begin
assert (NX);
assert (UF || o_zero);
end
end
// an unrounded result between +-e^bmin is still an underflow when rounded to ebmin
if (a_unsigned == 31'h0031b7be && b_unsigned == 31'h3ec6def9)
assert (UF);
`ifdef ALTDIV
if (!NV && !NX && !a_special && b_finite && o_norm)
// if o is subnorm then it can be shifted arbitrarily depending on exponent difference
assert (o_sig == (o_faux[25] ? o_faux[24:2] : o_faux[23:1]));
`endif
`endif
`ifdef MUL
assume (c_zero);
// an unrounded result between +-e^bmin is still an underflow when rounded to ebmin
if (a_unsigned == 31'h0ffffffd && b_unsigned == 31'h30000001) begin
assert (UF);
// but it's only ebmin when rounded towards the nearest infinity
assert (o_ebmin ^~ (o_sign ? rm_RTN : rm_RTP));
end
`endif
`ifdef MULS
if (a_unsigned == 31'h0ffffffd && b_unsigned == 31'h30000001 && c_subnorm)
if (!c_sign ^ b_sign ^ a_sign)
assert (!UF);
else
assert (UF);
// 0/inf or inf/0
if ((a_inf && b_zero) || (a_zero && b_inf))
assert (NV);
// very large multiplications overflow
if (a_unsigned == 31'h7f400000 && b_unsigned == a_unsigned && !c_special)
assert (OF);
// multiplying a small number by an even smaller number will underflow
if (a_norm && a_exp < 8'h68 && b_subnorm && !c_special) begin
assert (NX);
`ifdef MULADD
// within rounding
assert (UF || (c_zero ? o_zero : (o == c || o == c+1 || o == c-1)));
`else
assert (UF || o_zero);
if (o_zero)
assert (o_sign == a_sign ^ b_sign);
`endif
end
`endif
`ifdef ADDSUB
assume (c_zero);
// adder can't underflow, subnormals are always exact
assert (!UF);
`endif
`ifdef RNE
assume (rm_RNE);
`elsif RNA
assume (rm_RNA);
`elsif RTP
assume (rm_RTP);
`elsif RTN
assume (rm_RTN);
`elsif RTZ
assume (rm_RTZ);
`else
assume ($onehot(rm));
`endif
if (OF)
// rounding mode determines if overflow value is inf or max
casez (rm)
5'bzzzz1 /* RNE */: assert (o_inf);
5'bzzz10 /* RNA */: assert (o_inf);
5'bzz100 /* RTP */: assert (o == pos_inf || o == neg_max);
5'bz1000 /* RTN */: assert (o == pos_max || o == neg_inf);
5'b10000 /* RTZ */: assert (o == pos_max || o == neg_max);
endcase
// RTx modes cannot underflow to the opposite ebmin (or either for RTZ)
if (UF && o_ebmin)
if (o_sign)
assert (rm_RNE || rm_RNA || rm_RTN);
else
assert (rm_RNE || rm_RNA || rm_RTP);
// and the same for overflowing to infinities
if (OF && o_inf)
if (o_sign)
assert (rm_RNE || rm_RNA || rm_RTN);
else
assert (rm_RNE || rm_RNA || rm_RTP);
// test rounding
if (round_p_001)
casez (rm)
5'bzzzz1 /* RNE */: assert (o_unsigned == rounded_000);
5'bzzz10 /* RNA */: assert (o_unsigned == rounded_010);
5'bzz100 /* RTP */: assert (o_unsigned == rounded_010);
5'bz1000 /* RTN */: assert (o_unsigned == rounded_000);
5'b10000 /* RTZ */: assert (o_unsigned == rounded_000);
endcase
if (round_p_011)
casez (rm)
5'bzzzz1 /* RNE */: assert (o_unsigned == rounded_100);
5'bzzz10 /* RNA */: assert (o_unsigned == rounded_100);
5'bzz100 /* RTP */: assert (o_unsigned == rounded_100);
5'bz1000 /* RTN */: assert (o_unsigned == rounded_010);
5'b10000 /* RTZ */: assert (o_unsigned == rounded_010);
endcase
if (round_n_001)
casez (rm)
5'bzzzz1 /* RNE */: assert (o_unsigned == rounded_000);
5'bzzz10 /* RNA */: assert (o_unsigned == rounded_010);
5'bzz100 /* RTP */: assert (o_unsigned == rounded_000);
5'bz1000 /* RTN */: assert (o_unsigned == rounded_010);
5'b10000 /* RTZ */: assert (o_unsigned == rounded_000);
endcase
if (round_n_011)
casez (rm)
5'bzzzz1 /* RNE */: assert (o_unsigned == rounded_100);
5'bzzz10 /* RNA */: assert (o_unsigned == rounded_100);
5'bzz100 /* RTP */: assert (o_unsigned == rounded_010);
5'bz1000 /* RTN */: assert (o_unsigned == rounded_100);
5'b10000 /* RTZ */: assert (o_unsigned == rounded_010);
endcase
`ifdef ADDS
if (use_lhs) begin
// inf - inf
if (lhs_inf && rhs_inf && is_sub)
assert (NV);
// very large additions overflow
if (lhs_unsigned == 31'h7f400000 && rhs_unsigned == lhs_unsigned && !is_sub)
assert (OF);
// if the difference in exponent is more than the width of the mantissa,
// the result cannot be exact
if (lhs_finite && rhs_finite && exp_diff > 8'd24)
assert (NX || OF);
if (!UF) begin
// for a small difference in exponent with zero LSB, the result must be
// exact
if (o_unclamped && lhs_dominates && exp_diff < 8'd08 && rhs_sig[7:0] == 0 && lhs_sig[7:0] == 0)
assert (!NX);
if (exp_diff == 0 && !OF && lhs_sig[7:0] == 0 && rhs_sig[7:0] == 0)
assert (!NX);
end
// there's probably a better general case for this, but a moderate
// difference in exponent with non zero LSB must be inexact
if (o_finite && lhs_dominates && exp_diff > 8'd09 && rhs_sig[7:0] != 0 && lhs_sig[7:0] == 0)
assert (NX);
end
`endif
`ifdef MULADD
// not sure how to check this in the generic case since we don't have the partial mul
if ((a_inf || b_inf) && !(a_nan || b_nan) && c_inf && (a_sign ^ b_sign ^ c_sign))
assert (NV);
// normal multiplication, overflow addition
if (a == 31'h5f400000 && b == a && c == 32'h7f400000) begin
assert (OF);
end
// if multiplication overflows, addition can bring it back in range
if (a == 32'hc3800001 && b == 32'h7b800000 && !c_special) begin
if (c_sign)
// result is negative, so a negative addend can't
assert (OF);
else if (c_exp <= 8'he7)
// addend can't be too small
assert (OF);
else if (c_exp == 8'he8 && c_muladd_turning)
// this is just the turning point for this particular value
assert (OF);
else
// a large enough positive addend will never overflow (but is
// still likely to be inexact)
assert (!OF);
end
`endif
`ifdef SQRTS
assume (b_zero);
assume (c_zero);
assert (!UF);
assert (!OF);
// complex roots are invalid
if (a_sign) begin
if (a_norm || a_subnorm)
assert (NV);
end else begin
// root exponents for normal numbers are trivial
if (a_norm) begin
// root of a normal is always normal
assert (o_norm);
if (rm_RTZ)
assert (o_sexp == half_a_sexp);
else
assert (o_sexp == half_a_sexp || o_sexp == (half_a_sexp + 1));
`ifdef ALTSQRT
if (o_sexp == half_a_sexp) begin
if (NX) begin
assert (a_sig[0] == 1'b1);
if (rm_RTZ || rm_RTN) begin
assert (o_sig[22] == 1'b1);
assert (o_sig[21:0] == a_sig >> 1);
end else begin
assert (o_sig[22] != &a_sig);
if (rm_RNE && a_sig[1] == 1'b0) begin
assert (o_sig[21:0] == a_sig >> 1);
end else begin
assert (o_sig[21:0] == (a_sig[22:1]+1'b1));
end
end
end else begin
assert (a_sig[0] == 1'b0);
assert (o_sig[22] == a_sig[0]);
assert (o_sig[21:0] == a_sig >> 1);
end
end
`endif
end else if (a_subnorm) begin
// root of a subnormal is either normal or an exact subnormal
assert (o_norm || !NX);
end
end
`endif
end
`ifdef EDGE_EVENTS
reg skip = 1;
always @(posedge clk) begin
if (skip) begin
skip <= 0;
end else begin
// same input, different rounding mode
if ($stable(a) && $stable(b) && $stable(c)) begin
// general rounding
cover (NX && rm_RNE && o_sig[1:0] == 2'b00);
cover (NX && rm_RNE && o_sig[1:0] == 2'b10);
if (NX && $fell(rm_RNE)) begin
if ($past(o_sig[1:0]) == 2'b00) begin // should be rounding from 001
if (o_sign) begin
`ifndef SQRTS
cover ($rose(rm_RNA) && o_sig[1:0] == 2'b01);
cover ($rose(rm_RTP) && o_sig[1:0] == 2'b00);
cover ($rose(rm_RTN) && o_sig[1:0] == 2'b01);
cover ($rose(rm_RTZ) && o_sig[1:0] == 2'b00);
`endif
end else begin
cover ($rose(rm_RNA) && o_sig[1:0] == 2'b01);
cover ($rose(rm_RTP) && o_sig[1:0] == 2'b01);
cover ($rose(rm_RTN) && o_sig[1:0] == 2'b00);
cover ($rose(rm_RTZ) && o_sig[1:0] == 2'b00);
end
end else if ($past(o_sig[1:0]) == 2'b10) begin // should be rounding from 011
if (o_sign) begin
`ifndef SQRTS
cover ($rose(rm_RNA) && o_sig[1:0] == 2'b10);
cover ($rose(rm_RTP) && o_sig[1:0] == 2'b01);
cover ($rose(rm_RTN) && o_sig[1:0] == 2'b10);
cover ($rose(rm_RTZ) && o_sig[1:0] == 2'b01);
`endif
end else begin
cover ($rose(rm_RNA) && o_sig[1:0] == 2'b10);
cover ($rose(rm_RTP) && o_sig[1:0] == 2'b10);
cover ($rose(rm_RTN) && o_sig[1:0] == 2'b01);
cover ($rose(rm_RTZ) && o_sig[1:0] == 2'b01);
end
end
end
`ifndef SQRTS
// none of these are applicable for sqrt since we can't underflow or overflow
// inf edge cases
cover ($rose(o_inf));
if ($rose(o_inf)) begin
cover ($rose(rm_RNE));
cover ($rose(rm_RNA));
cover ($rose(rm_RTN));
cover ($rose(rm_RTP));
// rm_RTZ can never round to inf
end
`ifndef ADDSUB
// these aren't applicable to addsub since we they rely on underflow
// ebmin edge cases
cover ($rose(o_ebmin));
if ($rose(o_ebmin)) begin
cover ($rose(rm_RNE));
cover ($rose(rm_RNA));
cover ($rose(rm_RTN));
cover ($rose(rm_RTP));
cover ($rose(rm_RTZ));
end
// zero edge cases
cover ($rose(o_zero));
if ($rose(o_zero)) begin
cover ($rose(rm_RNE));
cover ($rose(rm_RNA));
cover ($rose(rm_RTN));
cover ($rose(rm_RTP));
cover ($rose(rm_RTZ));
end
`endif
`ifndef DIV
cover ($rose(OF));
`endif
`ifdef TININESS_AFTER
cover ($rose(UF));
`endif
`endif
`ifdef MULADD
// same multiplier output, different addend
end else if ($stable(a) && $stable(b) && $stable(rm)) begin
// we can get boundary cases
cover ($rose(o_inf));
cover ($rose(o_ebmin));
cover ($rose(o_zero));
// multiplication with an exception can be recovered by addend
if ($fell(c_zero)) begin
cover ($fell(OF));
cover ($fell(UF));
cover ($fell(NX));
// unless it was an invalid multiplication
if ($past(NV))
assert (NV);
end
// flags are always determined after addition
cover ($rose(OF));
cover ($rose(UF));
cover ($rose(NV));
cover ($rose(NX));
`endif
end
end
end
`endif
endmodule

View File

@ -0,0 +1,50 @@
#!/usr/bin/env python3
import sys
sys.path.append("..")
import gen_tests_makefile
from pathlib import Path
from textwrap import dedent
cwd = Path.cwd()
for path in cwd.glob("*_edges.*"):
path.unlink()
for op, defs in {
# standard ops
"sqrt": "-DSQRT -DSQRTS",
"add": "-DADD -DADDSUB -DADDS",
"sub": "-DSUB -DADDSUB -DADDS",
"mul": "-DMUL -DMULS",
"div": "-DDIV -DDIVS",
"muladd": "-DMULADD -DMULS -DADDS",
# altops
"altdiv": "-DALTDIV -DDIVS",
"altsqrt": "-DALTSQRT -DSQRTS",
# unrounded
"min": "-DMIN -DCOMPARES",
"max": "-DMAX -DCOMPARES",
}.items():
rms = ["DYN"]
dyn_only = op in ["min", "max"]
if not dyn_only:
rms.extend(["RNE", "RNA", "RTP", "RTN", "RTZ"])
for rm in rms:
with open(f"{op}_{rm}_edges.ys", "w") as ys:
print(f"symfpu -op {op} -rm {rm}", file=ys)
if rm != "DYN" or dyn_only:
print("sat -prove-asserts -verify", file=ys)
print(
dedent(f"""\
chformal -remove
opt
read_verilog -sv -formal {defs} -D{rm} edges.sv
chformal -remove -cover
chformal -lower
prep -top edges -flatten
sat -set-assumes -prove-asserts -verify"""
), file=ys)
gen_tests_makefile.generate(["--yosys-scripts"])

View File

@ -14,6 +14,7 @@ function(yosys_gtest arg_TARGET)
)
yosys_expand_components(test_components essentials ${arg_COMPONENTS})
yosys_link_components(${target} PRIVATE ${test_components})
add_dependencies(yosys-gtest-all ${target})
if(NOT CMAKE_CROSSCOMPILING)
gtest_discover_tests(${target})
@ -21,6 +22,8 @@ function(yosys_gtest arg_TARGET)
endfunction()
if (GTest_FOUND)
add_custom_target(yosys-gtest-all)
add_subdirectory(kernel)
add_subdirectory(opt)
add_subdirectory(techmap)

View File

@ -78,12 +78,21 @@ module \top
end
end
EOT
design -save fanout_test
logger -expect log "Rename cell .name in top to bcd_.and_B" 1
logger -expect log "Rename cell .name2 in top to c_has_a_long_name_.or_B" 1
logger -expect log "Renamed 2 objects" 1
debug autoname
logger -check-expected
# a selection only limits what gets renamed, never the name that gets picked:
# \a's fanout still counts $name2, even though it isn't selected
design -load fanout_test
logger -expect log "Rename cell .name in top to bcd_.and_B" 1
logger -expect log "Renamed 1 objects" 1
debug autoname c:$name
logger -check-expected
# names are unique
design -reset
read_rtlil <<EOT
@ -177,29 +186,41 @@ end
EOT
design -save order_test
# don't rename prematurely (some objects should be named after $name2)
# wires are named for being cell outputs
logger -expect log "Rename wire .d in top to or_Y" 1
logger -expect log "Rename cell .name2 in top to or_Y_.or_B" 1
logger -expect log "Renamed 2 objects" 1
debug autoname t:$or
logger -check-expected
logger -expect log "Rename wire .e in top to or_Y_.or_B_Y" 1
# $name gets shortest name (otherwise bcd_$__unknown_B)
logger -expect log "Rename cell .name in top to a_.__unknown_A" 1
# another output wire
logger -expect log "Rename wire .e in top to or_Y_.or_B_Y" 1
logger -expect log "Renamed 4 objects" 1
debug autoname
logger -check-expected
# don't rename prematurely (some objects should be named after $name2)
design -load order_test
# $name3 named for lowest fanout wire (otherwise a_$__unknown_A_Y_$and_A)
logger -expect log "Rename cell .name3 in top to or_Y_.or_B_Y_.and_B" 1
# $c gets shortest name, since the cell driving it doesn't have known port
# directions (otherwise a_$__unknown_A_Y)
logger -expect log "Rename wire .c in top to or_Y_.or_B_A" 1
# $name3 named for lowest fanout wire (otherwise a_$__unknown_A_Y_$and_A)
logger -expect log "Rename cell .name3 in top to or_Y_.or_B_Y_.and_B" 1
logger -expect log "Renamed 6 objects" 1
debug autoname
logger -check-expected
# Only selected objects are renamed, but each one gets exactly the name the
# unrestricted run above gave it, whatever the selection.
design -load order_test
logger -expect log "Rename cell .name2 in top to or_Y_.or_B" 1
logger -expect log "Renamed 1 objects" 1
debug autoname t:$or
logger -check-expected
design -load order_test
logger -expect log "Rename wire .d in top to or_Y" 1
logger -expect log "Rename wire .e in top to or_Y_.or_B_Y" 1
logger -expect log "Rename wire .c in top to or_Y_.or_B_A" 1
logger -expect log "Renamed 3 objects" 1
debug autoname w:*
logger -check-expected
# $name3 is named after a chain of objects that all keep their $-names
design -load order_test
logger -expect log "Rename cell .name3 in top to or_Y_.or_B_Y_.and_B" 1
logger -expect log "Renamed 1 objects" 1
debug autoname c:$name3
logger -check-expected