mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-04-22 12:55:30 +00:00
Code Activity

Add smtbmc --stdt option

Browse source 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
This commit is contained in:
Clifford Wolf 2018-03-04 14:08:55 +01:00
parent 4eed5ec8bb
commit e966f3dca4
3 changed files with 10 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

2
docs/source/reference.rst
View file

@ -110,6 +110,8 @@ the following options:
| ``--stbv`` | Use large bit vectors (instead of uninterpreted |
| | functions) to represent the circuit state. |
+-----------------+---------------------------------------------------------+
| ``--stdt`` | Use SMT-LIB 2.6 datatypes to represent states. |
+-----------------+---------------------------------------------------------+
| ``--nopresat`` | Do not run "presat" SMT queries that make sure that |
| | assumptions are non-conflicting (and potentially |
| | warmup the SMT solver). |