| Commit message (Collapse) | Author | Age | Files | Lines |
| |
|
|
|
|
|
|
| |
This attribute can be used by formal backends to indicate which clocks
were mapped to the global clock. Update the btor and smt2 backend which
already handle clock inputs to understand this attribute.
|
|
|
|
|
|
|
|
| |
This approach had major issues with ROMs whose initialization was not
fully defined. If required, memory_map -rom-only -keepdc should be
called early in a formal flow instead. (This does require a careful
choice of optimization passes though. Sby's scripts will be updated
accordingly.)
|
|
|
|
| |
Use it when invoking memory_map -rom-only from write_{smt2,btor}.
|
| |
|
|
|
|
|
|
| |
This avoids provability regressions now that we infer more ROMs.
This fixes #3378
|
| |
|
|
|
|
| |
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
|
| |
|
| |
|
| |
|
|
|
|
|
|
|
|
| |
s/((Claire|Xen|Xenia|Clifford)\s+)+(Wolf|Xen)\s+<(claire|clifford)@(symbioticeda.com|clifford.at|yosyshq.com)>/Claire Xenia Wolf <claire@yosyshq.com>/gi;
s/((Nina|Nak|N\.)\s+)+Engelhardt\s+<nak@(symbioticeda.com|yosyshq.com)>/N. Engelhardt <nak@yosyshq.com>/gi;
s/((David)\s+)+Shah\s+<(dave|david)@(symbioticeda.com|yosyshq.com|ds0.me)>/David Shah <dave@ds0.me>/gi;
s/((Miodrag)\s+)+Milanovic\s+<(miodrag|micko)@(symbioticeda.com|yosyshq.com)>/Miodrag Milanovic <micko@yosyshq.com>/gi;
s,https?://www.clifford.at/yosys/,http://yosyshq.net/yosys/,g;
|
|
|
|
|
|
| |
This essentially adds wide port support for free in passes that don't
have a usefully better way of handling wide ports than just breaking
them up to narrow ports, avoiding "please run memory_narrow" annoyance.
|
| |
|
| |
|
|
|
|
|
|
| |
There will soon be more (versioned) memory cells, so handle passes that
only care if a cell is memory-related by a simple helper call instead of
a hardcoded list.
|
| |
|
| |
|
| |
|
|
|
|
|
|
| |
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).
|
| |
|
| |
|
|
|
|
| |
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
|
| |
|
|
|
|
|
|
|
|
|
|
| |
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.
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
| |
Co-Authored-By: Alberto Gonzalez <61295559+boqwxp@users.noreply.github.com>
|
| |
|
|
|
|
| |
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
|
|
|
|
| |
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
|
|
|
|
| |
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
| |
|
|
|
|
| |
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
| |
|
|
|
|
| |
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
| |
|
|
|
|
| |
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
|
|
|
| |
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
|
|
|
| |
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
|
|
|
|
|
|
| |
we need to do this because they changed the parser:
https://github.com/Boolector/btor2tools/commit/e97fc9cedabadeec4f621de22096e514f862c690
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
|
|
|
| |
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
|
|
|
| |
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
|
|
|
| |
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
| |
|
|
|
|
| |
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
|
|
|
|
|
|
|
|
| |
o Not all derived methods were marked 'override', but it is a great
feature of C++11 that we should make use of.
o While at it: touched header files got a -*- c++ -*- for emacs to
provide support for that language.
o use YS_OVERRIDE for all override keywords (though we should probably
use the plain keyword going forward now that C++11 is established)
|
| |
|
| |
|
| |
|