mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2026-07-25 00:22:34 +00:00
Code Activity

Merge pull request #6042 from YosysHQ/krys/symfpu

Browse source 
Add `symfpu` pass
This commit is contained in:
Miodrag Milanović 2026-07-20 10:20:23 +00:00 • committed by GitHub
commit e2c27aaafa
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
10 changed files with 1683 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

32
kernel/constids.inc
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)

6
libs/CMakeLists.txt
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

5
passes/cmds/CMakeLists.txt
View file

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

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

1
tests/Makefile
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

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

50
tests/symfpu/generate_mk.py Normal file
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"])