Skip to content

New IC3: compare SAT backends on HWMCC17 #2066

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
kroening wants to merge 27 commits into
base: main
Choose a base branch
from
Draft

New IC3: compare SAT backends on HWMCC17 #2066

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
27 commits
Select commit Hold shift + click to select a range
17cf794
extract verilog_set_genvarst::build_map()
kroening Aug 5, 2026
0d525f4
KNOWNBUG test for genvar as parameter argument
kroening Aug 4, 2026
f434689
KNOWNBUG test for narrowing of a wide output port to a one-bit net
kroening Aug 4, 2026
0403654
Verilog: truncate wide port values to a one-bit net's LSB
kroening Aug 4, 2026
88fcbce
Print version and architecture banner
kroening Aug 4, 2026
3b8b65a
KNOWNBUG test for struct-typed parameters
kroening Jul 24, 2026
7263275
Verilog: tests for array-typed parameters
kroening Aug 1, 2026
2b83513
Verilog: accept struct/array/union as constant expressions
kroening Aug 1, 2026
a7b6ce6
Verilog preprocessor: replace, not append, on macro redefinition
kroening Jul 23, 2026
6c4c83f
Verilog preprocessor: track bracket nesting when splitting macro argu…
kroening Jul 23, 2026
fe6b52e
bump CBMC dependency
kroening Jul 23, 2026
3d9dac1
Verilog: fold Verilog-specific constructs when propagating constants …
kroening Jul 23, 2026
5ed5c74
Verilog: parse end labels after endfunction/endtask
kroening Jul 23, 2026
1a1c061
Verilog: parse unpacked array dimensions on parameter declarators
kroening Jul 23, 2026
7fe28aa
Verilog: anchor function/task declaration location to the declarator
kroening Jul 24, 2026
578f7d4
Verilog: fix KNOWNBUG polarity of unpacked_array_param1
kroening Jul 24, 2026
ad862c4
Verilog: interpret if statements in the constant-expression interpreter
kroening Jul 23, 2026
db09f0c
Verilog: don't treat 'integer' loop counters as driver conflicts
kroening Jul 23, 2026
a03a4ba
Verilog: fix synthesis crash on full-width part-select of signed vector
kroening Jul 23, 2026
6b799ac
Verilog: typed assignment patterns
kroening Jul 21, 2026
cf75098
Support reading source files from .f command files
kroening Jul 2, 2026
a52d473
Verilog: modport selection in interface port connections
kroening Jul 8, 2026
f96962d
Verilog: virtual interface declarations
kroening Jul 8, 2026
9b6ab0c
Verilog: parameterized interface port connections
kroening Jul 8, 2026
a3e54f8
fixup KNOWNBUG tests
kroening Aug 9, 2026
27b8db9
New IC3: compare SAT backends on HWMCC17
kroening Aug 9, 2026
a6bb3a7
New IC3: apply git-clang-format
kroening Aug 9, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions CHANGELOG
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
# EBMC 6.1

* version and architecture banner
* Netlist: module outputs are now classified as outputs rather than
wires (visible in --show-varmap); they remain shown in
counterexample traces
Expand Down
Loading
Loading