Commit Graph

65 Commits

Author SHA1 Message Date
Alberto Gonzalez 0fda8308bc Add support for optimizing exists-forall problems.
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.
2020-03-13 17:10:29 +00:00
Pepijn de Vos ae93c034ad set undriven pads to zero 2019-09-04 16:29:40 +02:00
Pepijn de Vos d65a47c86d fix tcl script 2019-09-04 15:35:33 +02:00
Pepijn de Vos 06062090da add broken TCL run script 2019-09-04 14:47:59 +02:00
Pepijn de Vos 0723672451 Add demonstration of breakage
Unused outputs lead to undriven buffers, which lead to syntax errors.
2019-09-04 11:01:28 +02:00
Pepijn de Vos 6cf5157fe7 Update example for GW1NR-9
This uses the Trenz TEC0117 on Gowin IDE 1.8.4
2019-09-04 10:52:28 +02:00
Marcin Kościelnicki f4c62f33ac Add clock buffer insertion pass, improve iopadmap.
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.
2019-08-13 00:16:38 +02:00
Marcin Kościelnicki 173c975894 Add a simple example for Spartan 6 2019-07-24 18:59:03 +02:00
Benedikt Tutzer 539a7f3fbc Added cell_stats example 2019-04-03 11:24:50 +02:00
Benedikt Tutzer 03d1606b42 Merge remote-tracking branch 'origin/master' into feature/python_bindings 2019-03-28 12:16:39 +01:00
Clifford Wolf df0598f455
Merge pull request #856 from kprasadvnsi/master
examples/anlogic/ now also output the SVF file.
2019-03-07 11:34:12 -08:00
Clifford Wolf 78762316aa Refactor SF2 iobuf insertion, Add clkint insertion
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-03-06 00:41:02 -08:00
Clifford Wolf b1b9edf5cc Improve igloo2 example
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-03-05 20:47:07 -08:00
Clifford Wolf e22afeae90 Improve igloo2 example
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-03-05 20:36:00 -08:00
Clifford Wolf da5181a3df Improvements in SF2 flow and demo
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-03-05 20:36:00 -08:00
Kali Prasad 7c03b0b082 examples/anlogic/ now also output the SVF file. 2019-03-06 09:51:11 +05:30
Clifford Wolf 24d1b92eda Improve igloo2 exmaple
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-03-05 17:27:58 -08:00
Clifford Wolf 3ef427f4a9 Add missing newline
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-03-05 15:21:04 -08:00
Kali Prasad 32a901ddf2 Added examples/anlogic/ 2019-03-04 23:26:56 +05:30
Clifford Wolf 107d884804 Improve igloo2 example
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-03-03 23:54:35 -08:00
Clifford Wolf a176ac95de Update igloo2 example to Libero v12.0
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-03-03 21:36:03 -08:00
Clifford Wolf f3556e9f7a Cleanups in igloo2 example design
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-01-17 14:54:04 +01:00
Clifford Wolf db5765b443 Add SF2 IO buffer insertion
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-01-17 14:38:37 +01:00
Clifford Wolf 9b277fc21e Improve Igloo2 example
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-01-17 13:35:52 +01:00
Clifford Wolf 2a2e0a4722 Improve igloo2 example
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-01-08 20:16:36 +01:00
Clifford Wolf f589ce86ba Add skeleton Yosys-Libero igloo2 example project
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-01-05 17:02:01 +01:00
Benedikt Tutzer c151bb31eb Added sample code for python-api 2018-12-11 08:13:42 +01:00
Clifford Wolf 67b1026297
Merge pull request #591 from hzeller/virtual-override
Consistent use of 'override' for virtual methods in derived classes.
2018-08-15 14:05:38 +02:00
japm48 beedaa5856 fix basys3 example
Added `CONFIG_VOLTAGE` and `CFGBVS` to constraints file
to avoid warning `DRC 23-20`.

Added `open_hw` needed for programming.
2018-07-22 22:29:31 +02:00
Henner Zeller 3aa4484a3c 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)
2018-07-20 23:51:06 -07:00
Clifford Wolf 7f0548c16f Update examples/cmos/counter.ys to use "synth" command
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-05-30 14:17:36 +02:00
Clifford Wolf b13e6bd375 Add smtbmc support for exist-forall problems
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-02-23 19:33:30 +01:00
Clifford Wolf eb67a7532b Add $allconst and $allseq cell types
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-02-23 13:14:47 +01:00
dh73 acee813a5c Fixed the -vout flag to -vqm in examples/intel directory 2017-11-14 22:55:48 -06:00
Clifford Wolf 142f4ca03a Add timing constraints to osu035 example 2017-10-10 13:32:04 +02:00
Clifford Wolf dca3b3cd5f Add examples/osu035 2017-05-23 18:38:20 +02:00
Clifford Wolf b72a7e1104 Replace CRLF line endings with LF in de2i.qsf (quartus example) 2017-04-12 16:51:46 +02:00
Larry Doolittle 2021ddecb3 Squelch trailing whitespace 2017-04-12 15:11:09 +02:00
dh73 c27dcc1e47 Add initial support for both MAX10 and Cyclone IV (E|GX) FPGAs 2017-04-05 23:01:29 -05:00
Clifford Wolf a44cc7a3d1 Added $assert/$assume support to AIGER back-end 2016-12-03 13:20:29 +01:00
Clifford Wolf 105b6374ae Added examples/aiger/ 2016-12-01 13:42:17 +01:00
Clifford Wolf 617693e691 Progress in examples/gowin/ 2016-11-08 19:07:22 +01:00
Clifford Wolf 84badc97b3 Added examples/gowin/ 2016-11-07 12:55:56 +01:00
Clifford Wolf bdc316db50 Added $anyseq cell type 2016-10-14 15:24:03 +02:00
Clifford Wolf 14bfd3c5c1 yosys-smtbmc meminit support 2016-09-08 11:16:12 +02:00
Clifford Wolf cb7dbf4070 Improvements in assertpmux 2016-09-07 12:42:16 +02:00
Clifford Wolf 068d5bc02f Made examples/smtbmc/demo1.v more interesting 2016-09-02 13:54:24 +02:00
Clifford Wolf aa25a4cec6 Added $anyconst support to yosys-smtbmc 2016-08-30 19:27:42 +02:00
Clifford Wolf b04a40d9fe Made "write_smt2 -bv -mem" default, added "write_smt2 -nobv -nomem" 2016-08-30 12:40:09 +02:00
Clifford Wolf eae390ae17 Removed $predict again 2016-08-28 21:35:33 +02:00