Commit Graph

10078 Commits

Author SHA1 Message Date
Alberto Gonzalez ea30465107
smtbmc: Remove superfluous `yosys-smt2-timeout` file macro.
Co-Authored-By: clairexen <claire@symbioticeda.com>
2020-05-29 21:33:00 +00:00
clairexen 0a14e1e837
Merge pull request #2029 from whitequark/fix-simplify-memory-sv_logic
ast/simplify: don't bitblast async ROMs declared as `logic`
2020-05-29 16:52:11 +02:00
clairexen 94c1035389
Merge pull request #1885 from Xiretza/mod-rem-cells
Fix modulo/remainder semantics
2020-05-29 16:37:23 +02:00
clairexen af36afe722
Merge pull request #2092 from whitequark/rtlil-no-space-control
Restrict RTLIL::IdString to not contain whitespace or control chars
2020-05-29 16:31:44 +02:00
clairexen 5874a14d65
Merge pull request #2017 from boqwxp/qbfsat-cvc4
qbfsat: Add support for CVC4.
2020-05-29 16:23:10 +02:00
clairexen 1c8d5a08a0
Merge pull request #2016 from boqwxp/qbfsat-yices
qbfsat: Add `-solver` option and allow choice of Z3 or Yices, making Yices the default.
2020-05-29 16:21:45 +02:00
whitequark 626c74adbd
Merge pull request #2097 from whitequark/ilang_lexer-fix-erange
ilang_lexer: fix check for out of range literal
2020-05-29 09:04:27 +00:00
whitequark 13b2963ded ilang_lexer: fix check for out of range literal.
Commit ca70a104 did not use a correct check.
2020-05-29 06:58:44 +00:00
whitequark 2116d9500c
Merge pull request #2033 from boqwxp/cleanup-verilog-lexer
verilog: Move lexer location variables from global namespace to `VERILOG_FRONTEND` namespace.
2020-05-29 06:46:33 +00:00
whitequark efa7424fb9 Restrict RTLIL::IdString to not contain whitespace or control chars.
This is an existing invariant (most backends can't cope with these)
but one that was not checked or documented.
2020-05-29 06:43:18 +00:00
Xiretza f88bef7672
Document division and modulo cells 2020-05-28 22:59:04 +02:00
Xiretza c34cb90a20
Update CHANGELOG 2020-05-28 22:59:04 +02:00
Xiretza 7c89738382
Add comments for mod/div semantics to rtlil.h 2020-05-28 22:59:04 +02:00
Xiretza 6a2bac21d3
Expand tests/simple/constmuldivmod.v 2020-05-28 22:59:04 +02:00
Xiretza edd8ff2c07
Add flooring division 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 $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.
2020-05-28 22:59:04 +02:00
Xiretza 17163cf43a
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.
2020-05-28 22:59:03 +02:00
whitequark 0d99522b3c
Merge pull request #2095 from rswarbrick/hier-typo
Fix small typos in documentation for hierarchy command
2020-05-28 10:49:14 +00:00
Rupert Swarbrick 1158bbf7db Fix small typos in documentation for hierarchy command 2020-05-28 11:39:44 +01:00
whitequark abac0ab28e
Merge pull request #2091 from boqwxp/printattrs
Add `printattrs` command to print attributes of currently selected objects.
2020-05-28 10:25:34 +00:00
whitequark 2384a59e2a
Merge pull request #2051 from Xiretza/makefile-cd-warning
Suppress warning during initial clone of ABC repo
2020-05-28 10:00:49 +00:00
whitequark 736ccb2ad5
Merge pull request #2031 from epfl-vlsc/master
Add extmodule support to firrtl backend
2020-05-28 09:59:17 +00:00
whitequark 2974183855
Merge pull request #2063 from boqwxp/techmapped-firrtl
firrtl: Accept techmapped cell types in FIRRTL backend.
2020-05-28 09:42:58 +00:00
whitequark 02bb52eef1
Merge pull request #2088 from rswarbrick/count-at
Minor optimisation in Module::wire() and Module::cell()
2020-05-28 09:41:17 +00:00
whitequark fdca785eda
Merge pull request #2087 from rswarbrick/lex-warn
Silence spurious warning in Verilog lexer when compiling with GCC
2020-05-28 09:41:04 +00:00
whitequark 8a44a46806
Merge pull request #2086 from rswarbrick/sigbit
Use default copy constructor for RTLIL::SigBit
2020-05-28 09:40:49 +00:00
whitequark 5b62dbb0af
Merge pull request #2084 from rswarbrick/c_str
Use c_str(), not str() for IdString/std::string == and != operators
2020-05-28 09:40:35 +00:00
Alberto Gonzalez 5896ffd56f
printattrs: Simplify `get_indent_str()`.
Co-Authored-By: Xiretza <xiretza@xiretza.xyz>
2020-05-28 05:34:28 +00:00
Alberto Gonzalez f671c99cb8
printattrs: Refactor indentation string building for clarity.
Co-Authored-By: whitequark <whitequark@whitequark.org>
2020-05-27 23:15:07 +00:00
Rupert Swarbrick d681c9df85 Pass some more args by reference in select.cc
Before this patch, the code passed around std::string objects by
value. It's probably not a hot-spot, but it can't hurt to avoid the
copying.

Removing the copy and clean-up code means the resulting code is ~6.1kb
smaller when compiled with GCC 9.3 and standard settings.
2020-05-27 09:42:23 +01:00
Rupert Swarbrick 061d1f0c07 Minor optimisations in select.cc's match_ids function
- Pass a string argument by reference

  - Avoid multiple calls to IdString::str and IdString::c_str

  - Avoid combining checks for size > 0 and first char (C strings are
    null terminated, so foo[0] != '\0' implies that foo has positive
    length)
2020-05-27 09:36:33 +01:00
Rupert Swarbrick 0d9beb5b2e Silence warning in select.cc
With GCC 9.3, at least, compiling select.cc spits out a warning about
an implausible bound being passed to strncmp. This comes from inlining
IdString::compare(): it turns out that passing std::string::npos as a
bound to strncmp triggers it.

This patch replaces the compare call with a memcmp with the same
effect. The repeated calls to IdString::c_str are slightly
inefficient, but I'll address that in a follow-up commit.
2020-05-27 09:34:15 +01:00
Alberto Gonzalez 6228b10c9f
printattrs: Add test. 2020-05-27 08:00:00 +00:00
Alberto Gonzalez e50e4ee285
printattrs: Use `flags` to pretty-print the `RTLIL::Const` appropriately.
Co-Authored-By: whitequark <whitequark@whitequark.org>
2020-05-27 08:00:00 +00:00
Alberto Gonzalez b8365547e9
misc: Add `printattrs` command. 2020-05-27 08:00:00 +00:00
whitequark b651352193
Merge pull request #2090 from whitequark/cxxrtl-fixes
Minor fixes for CXXRTL
2020-05-26 22:18:14 +00:00
whitequark 0bf6b164be cxxrtl: make logging a little bit nicer. 2020-05-26 21:37:32 +00:00
whitequark e9c07e2bda cxxrtl: add missing parts of commit 281c9685. 2020-05-26 21:34:20 +00:00
Rupert Swarbrick 6aa0f72ae9 Silence spurious warning in Verilog lexer when compiling with GCC
The chosen value shouldn't have any effect. I considered something
clearly wrong like -1, but there's no checking inside the generated
lexer, and I suspect this will cause even weirder bugs if triggered
than just setting it to INITIAL.
2020-05-26 17:54:57 +01:00
Rupert Swarbrick 7746bba69a Simplify a modport check in hierarchy.cc
This code originally comes from commit 458a940. When an interface is
used via a modport, code in genrtlil.cc sets '\\interface_type' and
'\\interface_modport' properties on the wire.

In hierarchy.cc, we pick up the modport name and add it to a dict
called modports_used_in_submodule (that maps connection source to
modport name).

Before this patch, the modport name is retrieved as a strpool and then
iterated over in an arbitrary order, discarding all entries but the
last. In practice, the pool will always have 0 or 1 entries because
the string used to construct it is a valid identifier, so doesn't
contain any pipe symbols.

This patch changes the code to retrieve the modport name as just a
string. This will have the same effect in practice, but may be a bit
less confusing!

The code also gets moved down closer to where the result is used,
which might be a bit more efficient since we won't always get as far
as the check.

The patch also removes some commented-out code, which I think was
intended to add some typechecking at some point, but was never
implemented. Since this dates back to October 2018, I think it makes
more sense to just take it out.
2020-05-26 16:50:42 +01:00
Rupert Swarbrick 7ff306ccdb Minor optimisation in Module::wire() and Module::cell()
The existing code does a search to figure out whether id is in the
dict (with the call to count()), and then looks it up again to get the
result (with the call to at()). This version calls find() instead,
avoiding the double lookup.

Code size increases slightly (6kb). I think this is because the
contents of find() are getting inlined, and then inlined into lots of
the callsites for cell() and wire().

Looking at the compiled code before this patch, you just get
a (non-inlined) call to count() followed by a call to at(). After the
patch, the contents of find() have been inlined (so you see do_hash,
then do_lookup). The result for each function is about 30 bytes / 40%
bigger, which presumably also enlarges call-sites that inline it.
2020-05-26 16:07:36 +01:00
Rupert Swarbrick 17b5f23f20 Use default copy constructor for RTLIL::SigBit
There was a handwritten copy constructor, which I'm not sure was
actually legal C++ (it unconditionally read from the 'data' member of
a union, which wouldn't have been written if wire was true). It was
also a bit less efficient than the constructor you get from the
compiler by default (which is allowed to just copy the memory).

This gives a marginal (~0.25%) decrease in code size when compiled
with GCC 9.3.
2020-05-26 13:18:01 +01:00
Rupert Swarbrick 8f87ccec9b Use c_str(), not str() for IdString/std::string == and != operators
These operators work by fetching the string from the global string
table and then comparing with the std::string that was passed in as
rhs.

Using str() means that we create a std::string (strlen; malloc;
memcpy), compare for equality (another memcmp if they have the same
length) and then finally free the string.

Using c_str() means that we pass the const char* straight to
std::string's equality operator. This ends up as a call to
std::string::compare (the const char* flavour), which is essentially
strcmp.
2020-05-26 12:27:15 +01:00
Eddie Hung 00c5ceb1f2 abc9_ops: -prep_xaiger exclude (* abc9_keep *) wires from toposort 2020-05-25 16:40:53 -07:00
Eddie Hung 1826370b3a xaiger: promote abc9_keep wires 2020-05-25 16:40:30 -07:00
Eddie Hung 1dce798dc5 tests: add ecp5 latch testcase with -abc9 2020-05-25 16:39:16 -07:00
Eddie Hung a7f2ef6d34
Merge pull request #2078 from YosysHQ/eddie/xilinx_sim_tidy
xilinx: tidy up cells_sim.v a little
2020-05-25 14:21:10 -07:00
Alberto Gonzalez 9847a4eea8
smtbmc and qbfsat: Add timeout option to set solver timeouts for Z3, Yices, and CVC4. 2020-05-25 20:39:30 +00:00
Alberto Gonzalez f9eef5e3f7
qbfsat: Add support for CVC4. 2020-05-25 20:39:03 +00:00
Alberto Gonzalez 54570a3978
qbfsat: Move SMT2 info statements back to the top of the file. 2020-05-25 20:38:29 +00:00
Alberto Gonzalez 903456c267
qbfsat: Add `-solver` option and allow choice of Z3 or Yices, making Yices the default.
Ensures that "BV" is the logic whenever solving an exists-forall problem with Yices, moves the "(set-logic ...)" directive above any non-info line, sets the `ef-max-iters` parameter to a very high number when using Yices in exists-forall mode so as not to prematurely abandon difficult problems, and does not provide the incompatible "--incremental" Yices argument when in exists-forall mode.
2020-05-25 20:38:29 +00:00