index
:
iCE40/yosys
master
[no description]
about
summary
refs
log
tree
commit
diff
stats
log msg
author
committer
range
path:
root
/
backends
/
smt2
Commit message (
Expand
)
Author
Age
Files
Lines
*
smtbmc: Add --check-witness mode
Jannis Harder
2022-08-16
1
-1
/
+22
*
aiger: Add yosys-witness support
Jannis Harder
2022-08-16
1
-2
/
+148
*
smtbmc: Add native json based witness format + smt2 backend support
Jannis Harder
2022-08-16
6
-113
/
+968
*
smt2: Support $anyinit cells
Jannis Harder
2022-08-16
1
-10
/
+11
*
formalff: Set new replaced_by_gclk attribute on removed dff's clks
Jannis Harder
2022-08-16
1
-0
/
+11
*
Switched to utf-8 in smtio.py
Miodrag Milanovic
2022-08-09
1
-2
/
+2
*
smt2: Fix $shift/$shiftx with negative shift ammounts
Jannis Harder
2022-08-02
1
-4
/
+4
*
smt2, btor: Revert calling memory_map -rom-only
Jannis Harder
2022-06-29
1
-1
/
+0
*
memory_map: -keepdc option for formal
Jannis Harder
2022-06-27
1
-1
/
+1
*
smt2, btor: Use memory_map -rom-only to make ROMs usable for k-induction
Jannis Harder
2022-06-17
1
-0
/
+1
*
smtbmc: noincr: keep solver running for post check-sat unrolling
Jannis Harder
2022-06-08
1
-2
/
+7
*
Merge pull request #3357 from jix/smtbmc-cvc5
Jannis Harder
2022-06-08
1
-3
/
+13
|
\
|
*
smtbmc: recognize cvc5 and fix unrolling for cvc4/cvc5
Jannis Harder
2022-06-03
1
-3
/
+13
*
|
smt2: emit smtlib2_comb_expr outputs after all inputs
Jannis Harder
2022-06-07
1
-5
/
+9
*
|
Merge pull request #3319 from programmerjake/smtlib2-expr-support
Jannis Harder
2022-06-07
1
-6
/
+57
|
\
\
|
*
|
smt2: Add smtlib2_comb_expr attribute to allow user-selected smtlib2 expressions
Jacob Lifshay
2022-06-02
1
-6
/
+57
|
|
/
*
/
smtbmc: Force nonincremental mode when yices is used with forall
Jannis Harder
2022-06-03
1
-1
/
+4
|
/
*
add $divfloor support to write_smt2
Jacob Lifshay
2022-05-24
1
-0
/
+21
*
smt2: Make write port array stores conditional on nonzero write mask
Jannis Harder
2022-04-20
1
-2
/
+4
*
smtbmc: fix bmc with no assertions
Jannis Harder
2022-03-29
1
-0
/
+2
*
Merge pull request #3253 from jix/smtbmc-nodeepcopy
Jannis Harder
2022-03-28
1
-6
/
+6
|
\
|
*
smtbmc: Avoid unnecessary deep copies during unrolling
Jannis Harder
2022-03-28
1
-6
/
+6
*
|
Merge pull request #3247 from jix/smtbmc-keepgoing
Jannis Harder
2022-03-28
1
-50
/
+143
|
\
\
|
|
/
|
/
|
|
*
yosys-smtbmc: Option to keep going after failed assertions in BMC mode
Jannis Harder
2022-03-24
1
-48
/
+141
|
*
yosys-smtbmc: Fix typo in help text, remove trailing whitespace
Jannis Harder
2022-03-24
1
-2
/
+2
*
|
ignore # comment lines
N. Engelhardt
2022-03-24
1
-1
/
+1
|
/
*
Merge pull request #3186 from nakengelhardt/smtbmc_sby_print_id
Miodrag Milanović
2022-03-04
2
-4
/
+12
|
\
|
*
print cell name for properties in yosys-smtbmc
N. Engelhardt
2022-02-22
2
-4
/
+12
*
|
Add a bit of flexibilty re trace length when processing aiger witnesses in sm...
Claire Xenia Wolf
2022-02-11
1
-1
/
+4
|
/
*
Add $bmux and $demux cells.
Marcelina Kościelnicka
2022-01-28
1
-0
/
+5
*
Hook up $aldff support in various passes.
Marcelina Kościelnicka
2021-10-02
1
-1
/
+1
*
yosys-smtbmc: Fix reused loop variable.
Marcelina Kościelnicka
2021-09-10
1
-4
/
+4
*
Add support for the Bitwuzla solver
GCHQDeveloper560
2021-07-12
1
-5
/
+5
*
Fixing old e-mail addresses and deadnames
Claire Xenia Wolf
2021-06-08
3
-3
/
+3
*
Make a few passes auto-call Mem::narrow instead of rejecting wide ports.
Marcelina Kościelnicka
2021-05-28
1
-6
/
+1
*
Reject wide ports in some passes that will never support them.
Marcelina Kościelnicka
2021-05-25
1
-0
/
+6
*
kernel/rtlil: Extract some helpers for checking memory cell types.
Marcelina Kościelnicka
2021-05-22
1
-2
/
+2
*
btor, smt2, smv: Add a hint on how to deal with funny FF types.
Marcelina Kościelnicka
2021-02-25
1
-0
/
+12
*
smt2: Use Mem helper.
Marcelina Kościelnicka
2020-10-21
1
-186
/
+244
*
smtbmc: escape identifiers in verilog testbench
Jakob Wenzel
2020-10-06
1
-11
/
+29
*
use the new isPublic() in a few places
N. Engelhardt
2020-09-14
1
-2
/
+2
*
write_smt2: fix SMT-LIB tutorial URL
whitequark
2020-08-29
1
-1
/
+1
*
Ensure smt2 comments are associated with accessors
Noah Moroze
2020-08-20
1
-9
/
+20
*
smtio: Emit `mode: start` options before `set-logic` command and any other op...
Alberto Gonzalez
2020-07-20
1
-1
/
+8
*
smtio: Add support for parsing `yosys-smt2-solver-option` info statements.
Alberto Gonzalez
2020-07-20
1
-3
/
+10
*
smt2: Add `-solver-option` option.
Alberto Gonzalez
2020-07-20
1
-0
/
+13
*
Only allow "sat" and "unsat" smt solver responses in yosys-smtbmc
Claire Wolf
2020-07-20
2
-4
/
+4
*
Use C++11 final/override keywords.
whitequark
2020-06-18
1
-2
/
+2
*
more reasonable numbers for memory
Yehowshua Immanuel
2020-06-04
1
-1
/
+1
*
MacOS has even stricter stack limits in catalina.
Yehowshua Immanuel
2020-06-04
1
-1
/
+1
[next]