| Commit message (Collapse) | Author | Age | Files | Lines |
| |
|
|
|
|
|
|
| |
Modifies smt2 backend to recognize `$anyconst` etc. assigned to a wire with the `maximize` or `minimize` attribute and emit `; yosys-smt2-maximize` or `; yosys-smt2-minimize` directives as appropriate.
Modifies `backends/smt2/smtbmc.py` and `smtio.py` to recognize those directives and emit a `(maximize ...)` or `(minimize ...)` command at the end of `smt_forall_assert()`, as described in the paper "νZ - An Optimizing SMT Solver" by Nikolaj Bjørner et al.
Adds an example `examples/smtbmc/demo9.v` to show how it can be used.
|
| |
|
| |
|
| |
|
|
|
|
| |
Unused outputs lead to undriven buffers, which lead to syntax errors.
|
|
|
|
| |
This uses the Trenz TEC0117 on Gowin IDE 1.8.4
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
A few new attributes are defined for use in cell libraries:
- iopad_external_pin: marks PAD cell's external-facing pin. Pad
insertion will be skipped for ports that are already connected
to such a pin.
- clkbuf_sink: marks an input pin as a clock pin, requesting clock
buffer insertion.
- clkbuf_driver: marks an output pin as a clock buffer output pin.
Clock buffer insertion will be skipped for nets that are already
driven by such a pin.
All three are module attributes that should be set to a comma-separeted
list of pin names.
Clock buffer insertion itself works as follows:
1. All cell ports, starting from bottom up, can be marked as clock sinks
(requesting clock buffer insertion) or as clock buffer outputs.
2. If a wire in a given module is driven by a cell port that is a clock
buffer output, it is in turn also considered a clock buffer output.
3. If an input port in a non-top module is connected to a clock sink in a
contained cell, it is also in turn considered a clock sink.
4. If a wire in a module is driven by a non-clock-buffer cell, and is
also connected to a clock sink port in a contained cell, a clock
buffer is inserted in this module.
5. For the top module, a clock buffer is also inserted on input ports
connected to clock sinks, optionally with a special kind of input
PAD (such as IBUFG for Xilinx).
6. Clock buffer insertion on a given wire is skipped if the clkbuf_inhibit
attribute is set on it.
|
| |
|
| |
|
|\ |
|
| |\
| | |
| | | |
examples/anlogic/ now also output the SVF file.
|
| | | |
|
| | |
| | |
| | |
| | | |
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>
|
| | |
|
| |
| |
| |
| | |
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>
|
| |
| |
| |
| | |
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
| |\
| | |
| | | |
Consistent use of 'override' for virtual methods in derived classes.
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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)
|
| |/
| |
| |
| |
| |
| |
| | |
Added `CONFIG_VOLTAGE` and `CFGBVS` to constraints file
to avoid warning `DRC 23-20`.
Added `open_hw` needed for programming.
|
|/ |
|
|
|
|
| |
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
|
|
|
| |
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
|
|
|
| |
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|