New IC3: compare SAT backends on HWMCC17 - #2066
Draft
kroening wants to merge 27 commits into
Draft
Conversation
This extracts the code that turns the data in verilog_set_genvarst into a map into a method.
An implicitly declared net used in a port connection is a one-bit scalar net (IEEE 1800-2017 6.10). When a wider output port drives such a net, the value must be truncated to the least-significant bit, as a narrowing continuous assignment would be. EBMC instead casts the port value to bool, i.e. computes (port != 0), so the resulting bit is wrong for any port value whose LSB differs from its zero/non-zero status.
When a port connection ties a wider signal to a one-bit net (e.g. an implicitly declared net, which per IEEE 1800-2017 6.10 is a one-bit scalar), the value must be narrowed by taking the least-significant bit, exactly as a narrowing continuous assignment does (see assignment_conversion). instantiate_port instead used typecast_exprt::conditional_cast to bool, which lowers to a (!= 0) reduction, so the net received the wrong bit whenever the source's LSB differed from its zero/non-zero status. Promote the accompanying regression test from KNOWNBUG to CORE.
This adds a call to log_version_and_architecture(...) to both ebmc and vlindex, to match the behavior of cbmc and hw-cbmc.
Struct literals (assignment patterns) used as parameter values were rejected because the constant expression check only accepted expressions with id() == ID_constant. Struct, array and union expressions have their own IDs (ID_struct, ID_array, ID_union) but are constant when all their operands are. This adds a recursive is_constant_rec() check in both elaborate_constant_expression_check() and verilog_simplifier_rec(), enabling struct-typed parameters and member access on them (e.g., P.x where P is a struct-valued parameter).
defines[identifier] returns a reference to any existing macro entry. When a macro was redefined, the new parameters and body tokens were appended to the previous definition instead of replacing it. For a macro such as FORCE_CONTENTION_ASSERTION_RESET_ACTIVE, defined as 1'b1 several times in one file, the expansion became "1'b11'b1", which the parser then rejected. The entry is now reset before it is populated, so the most recent definition wins (IEEE 1800-2017 22.5.1). Resolves the parse error in LogikBench large/nvdlafull and large/nvdlasmall (both still need library modules that are not part of the benchmark). Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
…ments
When splitting the actual arguments of a function-like macro on commas,
the preprocessor treated every comma and the first ')' as significant,
regardless of nesting. A single argument containing commas inside
parentheses, brackets or braces -- e.g.
`debug($display("%d %d", a, b);) -- was therefore miscounted, and the
first inner ')' terminated the list prematurely.
Commas and the closing ')' are now only significant at nesting depth
zero (IEEE 1800-2017 22.5.1).
Fixes LogikBench blocks/picorv32.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
This bumps to the top of the develop branch.
…in synthesis
When synthesising a blocking assignment, synth_assign tries to simplify the
right-hand side to a constant so the value can be propagated (needed, among
other things, to unroll for/while loops by evaluating their guard each
iteration). It used the plain simplifier, which does not know how to reduce
Verilog-specific constructs such as replication ({n{x}}) to a constant.
As a result a loop whose bit-vector loop variable is initialised with a
replication, e.g.
for(data_mask = {1'b1, {DW-1{1'b0}}}; data_mask != 0;
data_mask = data_mask >> 1)
left data_mask non-constant, so synthesis reported "synthesis failed to
evaluate loop guard". Use the Verilog-aware simplifier instead, which lowers
replication to a concatenation before folding. The result is only used when
it is constant, so non-constant right-hand sides are unaffected.
This is the root cause of the loop-guard failures for the LogikBench
blocks/ethmac (rtl/eth_lfsr.v:235) and blocks/lfsr (rtl/lfsr.v:235)
benchmarks.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
SystemVerilog allows an optional block name after endfunction and endtask, e.g. "endfunction : is_width_valid" (IEEE 1800-2017 A.9.3). The grammar previously rejected the colon. Fixes the first parse error in LogikBench blocks/hmac, blocks/i2c, blocks/uart and large/aes. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
SystemVerilog allows unpacked array dimensions on a parameter or
localparam declarator, e.g. "parameter logic [3:0] p [73] = '{...}"
(IEEE 1800-2017 A.2.4). The grammar previously rejected the '[' after
the parameter name. The declarator's dimensions are now merged with the
declaration type via verilog_declaratort::merged_type().
This addresses the first parse error in LogikBench blocks/spi and
large/cva6. Elaborating an array assignment pattern as a constant
parameter value is a separate gap tracked by the accompanying KNOWNBUG
regression test.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Adding the optional end label after endfunction/endtask makes the grammar read one lookahead token before reducing, which shifted the source location of the whole declaration onto that lookahead token. The declaration's location is now taken from its declarator, so it points at the function/task name (an improvement over the previous behaviour, which pointed at the endfunction/endtask keyword). Updates the task_name_collision expectation accordingly. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
test.pl inverts the pass/fail verdict for KNOWNBUG-tagged tests: the
required-pattern section is meant to describe the aspirational, fixed
behaviour, so that a *mismatch* (the bug still reproducing) is reported
OK, and a match (the bug turns out to be fixed) is flagged so the test
can be promoted to CORE.
unpacked_array_param1.desc had this backwards: its patterns matched the
*current* buggy error message ("expected constant expression, but got
...", EXIT=2) verbatim, which -- given the inversion -- meant the test
would report a hard FAILURE on every single run for as long as the bug
remains unfixed, rather than the intended "known, not yet fixed" OK.
This is what CI's "KNOWNBUG checks" job was catching.
Rewritten to expect the aspirational post-fix output (successful
elaboration, "no properties", matching the convention already used by
e.g. macro_arg_commas1.desc for the same --bound 0/no-properties case).
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
The small interpreter used to evaluate Verilog functions in constant contexts (e.g. computing a parameter value) handled blocking assignments, blocks and for loops, but threw "Don't know how to interpret statement `if'" on if statements. Add support: evaluate the condition as a constant expression and interpret the taken branch (handling both if and if/else). This is the root cause of the elaboration failure for the LogikBench large/axicrossbar benchmark, whose calcBaseAddrs() constant function (rtl/axi_crossbar_addr.v) uses if statements. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Module-level 'integer' variables are idiomatically used as loop counters and combinational scratch. They are elaboration-only: the synthesis pass never turns them into state (synth_assignments skips them), yet assignment() still tracked their assignments for driver and assignment-type conflicts. When such a variable was (blocking-) assigned in more than one always/initial block -- e.g. a shared 'for' loop index -- this produced a spurious "conflict with previous assignment" or "conflicting assignment types (new: clocked, old: combinational)" error, even though only one block's value is ever observable. Exempt variables carrying the Verilog 'integer' type from assignment-type and member/driver-conflict tracking. Fixes elaboration of LogikBench basic/crossbar, blocks/viterbi (signal j) and large/qr (signal k). Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
A part-select expression is unsigned even when it selects a signed vector in its entirety (IEEE 1800-2017 11.5.1). When such a full-width part-select appears on the left-hand side of an assignment (e.g. areg[DW-1:0] <= a), synth_assignments took a shortcut that assigned the unsigned right-hand side straight into the signed target symbol. The right- and left-hand sides then differed in signedness, tripping the "synth_assignments type consistency" DATA_INVARIANT and aborting (SIGABRT). We now reinterpret the right-hand side to the type of the source when the full-width part-select is elided; the bits are identical, so this is a sign-preserving reinterpret cast that makes the invariant hold. This is the crash observed on the LogikBench arithmetic/mulreg benchmark. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
This adds support for typed assignment patterns.
Add -f option to ebmc and vlindex to read source file names and options from a command file, as is common in EDA tools. Each line is treated as a command line option. Blank lines and // comments are ignored. Resolves diffblue#1337
When an interface instance is passed to a module port with explicit modport selection (e.g., sb.receiver), resolve the hierarchical identifier to the interface instance itself. The modport name is verified against the interface's modport declarations per IEEE 1800-2017 section 25.5.3.
Add support for virtual interface variable declarations and assignments per IEEE 1800-2017 section 25.9. The parser now stores the interface name with a proper IREP ID, the type elaboration accepts the type, and assignment conversion handles assignments to virtual interface variables. Member access through virtual interfaces (vif.data) is left for future work and tracked as a KNOWNBUG test.
When a module has a port of a parameterized interface type, the port's interface members are instantiated with default parameters during type checking. When a differently-parameterized interface instance is connected, the types may not match. This fixes the issue in two places: 1. In verilog_synthesis.cpp, synth_module_instance() now updates port member types in the symbol table to match the actual bound interface before synthesizing the submodule. This ensures the transition system invariant constraints have matching types. 2. In ebmc_properties.cpp, a fix_symbol_types() pass updates symbol expression types in property expressions to match the symbol table, handling cases where the property was type-checked before the type update. The test case verifies that a param_if #(32) interface can be connected through a port declared as param_if (defaulting to W=8), per IEEE 1800-2017 section 25.8.
Add SAT backend selection for the new IC3 engine, generalize the benchmark runner, and include a full HWMCC 2017 single-track comparison report for ictminisat, minisat2, and cadical.
kroening
marked this pull request as draft
August 9, 2026 18:47
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
This change adds SAT-backend selection for
--new-ic3and benchmarks theavailable backends on the HWMCC 2017 single-track benchmark suite.
Supported backends:
ictminisatminisat2cadicalThe PR also generalizes the benchmarking script so it can run full benchmark
directories and emit comparable CSV results across multiple solver backends.
User-facing changes
Example:
Experimental setup
clang++ccachebenchmarking/hwmcc17_single_new_ic3_sat_backends.csvbenchmarking/hwmcc17_single_expected.csvbenchmarking/hwmcc17_single_new_ic3_sat_solver_report.mdResults
On the 166 benchmarks with known expected outcomes:
minisat2: 107 correct solvesictminisat: 105 correct solvescadical: 96 correct solvesictminisat: 1minisat2: 3cadical: 1The report recommends keeping backend selection user-visible and treating
cadicalas opt-in. If choosing a default solely from HWMCC 2017 results,minisat2is the strongest candidate.Validation
clang++andccachemake -C src -j4 CXX='ccache clang++' MINISAT2=/local/home/dkr/3hw-cbmc/lib/cbmc/minisat-2.2.1 CADICAL=/local/home/dkr/3hw-cbmc/lib/cbmc/cadicalmake -C unit -j4 CXX='ccache clang++'