From 17163cf43a6b6eec9aac44f6a4463dda54b8ed68 Mon Sep 17 00:00:00 2001 From: Xiretza Date: Wed, 8 Apr 2020 19:30:47 +0200 Subject: Add flooring modulo operator The $div and $mod cells use truncating division semantics (rounding towards 0), as defined by e.g. Verilog. Another rounding mode, flooring (rounding towards negative infinity), can be used in e.g. VHDL. The new $modfloor cell provides this flooring modulo (also known as "remainder" in several languages, but this name is ambiguous). This commit also fixes the handling of $mod in opt_expr, which was previously optimized as if it was $modfloor. --- backends/btor/btor.cc | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) (limited to 'backends/btor/btor.cc') diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index 14c8484e8..2816d3246 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -266,20 +266,26 @@ struct BtorWorker goto okay; } - if (cell->type.in(ID($div), ID($mod))) + if (cell->type.in(ID($div), ID($mod), ID($modfloor))) { + bool a_signed = cell->hasParam(ID::A_SIGNED) ? cell->getParam(ID::A_SIGNED).as_bool() : false; + bool b_signed = cell->hasParam(ID::B_SIGNED) ? cell->getParam(ID::B_SIGNED).as_bool() : false; + string btor_op; if (cell->type == ID($div)) btor_op = "div"; + // "rem" = truncating modulo if (cell->type == ID($mod)) btor_op = "rem"; + // "mod" = flooring modulo + if (cell->type == ID($modfloor)) { + // "umod" doesn't exist because it's the same as "urem" + btor_op = a_signed || b_signed ? "mod" : "rem"; + } log_assert(!btor_op.empty()); int width = GetSize(cell->getPort(ID::Y)); width = std::max(width, GetSize(cell->getPort(ID::A))); width = std::max(width, GetSize(cell->getPort(ID::B))); - bool a_signed = cell->hasParam(ID::A_SIGNED) ? cell->getParam(ID::A_SIGNED).as_bool() : false; - bool b_signed = cell->hasParam(ID::B_SIGNED) ? cell->getParam(ID::B_SIGNED).as_bool() : false; - int nid_a = get_sig_nid(cell->getPort(ID::A), width, a_signed); int nid_b = get_sig_nid(cell->getPort(ID::B), width, b_signed); -- cgit v1.2.3