Miodrag Milanovic
131b557727
Initial implementation of synthesizable assertions
2023-02-13 17:23:26 +01:00
Jannis Harder
c0063288d6
Add the $anyinit cell and the formalff pass
...
These can be used to protect undefined flip-flop initialization values
from optimizations that are not sound for formal verification and can
help mapping all solver-provided values in witness traces for flows that
use different backends simultaneously.
2022-08-16 13:37:30 +02:00
Iris Johnson
ccc6060f52
Makefile: properly conditionalize features requiring compression.
2022-04-07 20:07:44 -05:00
whitequark
b43c282e4e
Add WASI platform support.
...
This includes the following significant changes:
* Patching ezsat and minisat to disable resource limiting code
on WASM/WASI, since the POSIX functions they use are unavailable.
* Adding a new definition, YOSYS_DISABLE_SPAWN, present if platform
does not support spawning subprocesses (i.e. Emscripten or WASI).
This definition hides the definition of `run_command()`.
* Adding a new Makefile flag, DISABLE_SPAWN, present in the same
condition. This flag disables all passes that require spawning
subprocesses for their function.
2020-04-30 18:56:25 +00:00
Alberto Gonzalez
fb878b2a70
Initial skeleton for `qbfsat` command.
2020-04-04 22:13:25 +00:00
Clifford Wolf
3fa374a698
Add fminit pass
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2020-01-09 21:22:54 +01:00
Clifford Wolf
ddc1a4488e
Add "cutpoint" pass
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-03-25 19:49:00 +01:00
Clifford Wolf
370db33a4c
Add fmcombine pass
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-03-15 20:46:17 +01:00
Clifford Wolf
ea8ee24140
Add basic "mutate -list N" framework
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-03-14 22:04:42 +01:00
Clifford Wolf
a58dbcf2ba
Add "supercover" skeleton
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-02-27 11:37:08 -08:00
Clifford Wolf
87aef8f0cc
Add async2sync pass
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-07-19 15:31:12 +02:00
Clifford Wolf
75046aa531
Add "sim" command skeleton
2017-08-16 13:05:21 +02:00
Clifford Wolf
2733994aeb
Added clk2fflogic
2016-10-14 14:55:07 +02:00
Clifford Wolf
ab18e9df7c
Added assertpmux
2016-09-07 00:28:01 +02:00
Clifford Wolf
0a225f8b27
Moved equiv stuff to passes/equiv/
2015-01-22 12:03:15 +01:00
Clifford Wolf
5febbe3620
Added equiv_simple
2015-01-19 15:08:44 +01:00
Clifford Wolf
615c2e136e
Added equiv_status
2015-01-19 14:20:04 +01:00
Clifford Wolf
76c5d863c5
Added equiv_make command
2015-01-19 13:59:08 +01:00
Clifford Wolf
d5148f2e01
Moved "share" and "wreduce" to passes/opt/
2014-09-01 11:45:26 +02:00
Clifford Wolf
2278995bd8
Started to implement real resource sharing
2014-07-19 20:54:32 +02:00
Clifford Wolf
cd06055e77
Added expose command
2014-02-05 23:59:55 +01:00
Clifford Wolf
fa92722358
Added miter command
2014-02-01 10:35:56 +01:00
Clifford Wolf
6efca9ea5a
Added freduce command
2013-08-06 15:04:52 +02:00
Clifford Wolf
21e38bed98
Added "eval" pass
2013-06-19 09:30:37 +02:00
Clifford Wolf
08e2fa978c
Renamed "sat_solve" pass to "sat"
2013-06-09 21:55:53 +02:00
Clifford Wolf
46fbe9d262
Added SAT generator and simple sat_solve command
2013-06-07 13:59:13 +02:00