aboutsummaryrefslogtreecommitdiffstats
path: root/backends/btor/test_cells.sh
Commit message (Collapse)AuthorAgeFilesLines
* Respect \A_SIGNED for $shiftXiretza2020-08-181-2/+2
| | | | | | This reflects the behaviour of $shr/$shl, which sign-extend their A operands to the size of their output, then do a logical shift (shift in 0-bits).
* Add flooring division operatorXiretza2020-05-281-1/+1
| | | | | | | | | | 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 $divfloor cell provides this flooring division. This commit also fixes the handling of $div in opt_expr, which was previously optimized as if it was $divfloor.
* Add flooring modulo operatorXiretza2020-05-281-1/+1
| | | | | | | | | | | 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.
* Minor style fixesClifford Wolf2018-12-181-0/+0
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add btor ops for $mul, $div, $mod and $concatmakaimann2018-12-171-0/+0
|
* Add btor $shift/$shiftx supportClifford Wolf2017-12-111-2/+2
|
* Fix btor back-end shift handlingClifford Wolf2017-12-101-1/+1
|
* Add support for more cell types to btor back-endClifford Wolf2017-12-101-0/+30