Conversation
kroening
force-pushed
the
dk
branch
4 times, most recently
from
August 13, 2026 15:42
3f88fde to
f3e196a
Compare
This extracts the code that turns the data in verilog_set_genvarst into a map into a method.
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).
…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>
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>
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 #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.
An ANSI port list could only use an interface port, with or without a
modport, if the interface declaration had already been parsed. The two
grammar rules for interface ports were keyed on TOK_INTERFACE_IDENTIFIER,
which the scanner returns only for identifiers that are already in the
scope table as an interface (make_identifier in scanner.l and
verilog_scopet::identifier_token). For an interface that has not been seen
yet the scanner returns TOK_NON_TYPE_IDENTIFIER instead, and the port list
failed with a syntax error:
module m(my_if.slave a); // syntax error if my_if comes later
endmodule
interface my_if;
logic v;
modport slave (input v);
endinterface
The order of the input files on the command line therefore decided whether
valid RTL was accepted.
Interface ports are now recognised by their shape rather than by the token
class: within a port list, an identifier followed by another identifier,
optionally with an intervening ".modport", can only be an interface port
(IEEE 1800-2017 A.1.3, interface_port_header). The two rules are moved into
a new interface_port_declaration nonterminal, which is an alternative of
ansi_port_declaration_brace rather than of ansi_port_declaration. That
placement is what keeps the grammar LALR(1): the leading identifier is
shifted before the nullable attribute_instance_brace has to be reduced.
Bison reports no shift/reduce or reduce/reduce conflicts.
Both the "my_if.modport name" and the plain "my_if name" forms are fixed.
Adds regression tests regression/verilog/interface/port4 (modport form,
interface file listed after the module file), port5 (no-modport form, same),
and port6 (modport form, interface declared after the module in one file).
SystemVerilog allows an interface port to have unpacked dimensions, i.e.,
an array of interface ports (IEEE 1800-2017 section 25.4, and
ansi_port_declaration in A.1.3). The parser rejected the dimension:
interface ifc;
logic x;
modport mp (input x);
endinterface
module m(ifc.mp a[0:3]); // syntax error, unexpected '['
endmodule
The two interface-port alternatives of ansi_port_declaration did not
accept a dimension after the port identifier. They now use the existing
unpacked_dimension_brace nonterminal, in the same way as the net and
variable port declarations do: the interface type goes onto the
declaration and the unpacked array type onto the declarator. No new
grammar conflicts are introduced.
Elaboration of arrays of interface ports is not implemented yet, as it
requires support for arrays of interface instances, which we do not have
(compare "no support for instance arrays"). To make sure the dimension is
not silently dropped, which would yield a model with a single interface
instance instead of an array, collect_port_symbols now rejects an
interface port that has a declarator type with "no support for arrays of
interface ports".
Adds regression/verilog/interface/port_array1 (parsing, with and without
a modport, and with multiple dimensions), port_array2 (the diagnostic for
the unimplemented elaboration), and port_array3 as a KNOWNBUG for the
elaboration.
IEEE 1800-2017 26.3 requires that the compilation of a package precedes the compilation of the scopes in which the package is imported, but the standard does not prescribe an order for the input files. We hence determine the order in which the input files are parsed and elaborated from the packages that they declare and reference, using a scanner-only pre-pass over the preprocessed input. The parse trees are still returned in the order in which the files were given, so that the choice of top-level modules is unaffected. Furthermore, the operand of an import can only ever be a package name, and hence the grammar now also accepts an identifier that is not classified as a package name. That yields a diagnostic that names the offending package instead of a syntax error about a token class. The elaboration order is extended when a module is resolved from a library directory given with -y or +libdir+, as those files are parsed after the files given on the command line.
Library files are parsed after the given files, and hence are appended to the list of parse trees once the given files have been parsed. Extend the elaboration order accordingly, as it would otherwise not cover them, and add an invariant that the elaboration order covers all parse trees.
Arrays of interface ports, IEEE 1800-2017 25.4, are now elaborated. Each element of the array yields an interface instance of its own, named bus[0], bus[1], and so on, and each of those is bound to the interface instance that the port connection gives for that element. Selecting an element of such an array, e.g. bus[0].some_signal, resolves to the member of the interface instance for that element. Any number of dimensions is supported. The array elements may be given as an assignment pattern, one interface instance per element, or by the name of another array of interfaces, which is how a module passes on an array of interface ports that it has itself been given. This replaces the "no support for arrays of interface ports" error.
Per 1800-2017 20.3, add support for $time, $stime and $realtime, which previously gave "unknown system function". The types of the results follow 1800-2017 20.3: $time yields a 64-bit integer, $stime yields the low-order 32 bits thereof, and $realtime yields a real. EBMC has no notion of continuous simulation time: delay controls are ignored, and so are `timescale and timeunit. The simulation time is therefore modelled by a global state variable that counts the timeframes, i.e., the time advances by exactly one time unit per timeframe. Consequently, the absolute times reported will not match those of an event-driven simulator when delays or a timescale are given.
Per 1800-2017 27.4, a genvar that is declared in the header of a loop generate construct is local to that loop. Two loops in the same scope may hence both declare a genvar with the same name. Such genvars are no longer added to the enclosing scope; their value is tracked in the genvar environment, which is also what references to them are now resolved against, and they are removed from that environment once the loop has been elaborated. Genvars that are declared separately from the loop are unaffected, and remain shared between loops. This fixes the KNOWNBUG added in #2085.
A genvar that is declared in the header of a loop generate construct is local to that loop, 1800-2017 27.4. It does not have a symbol of its own, and hence a reference to it must be resolved using the genvar environment rather than the symbol table. Any symbol with the same base name that is visible from the scope that contains the loop is shadowed for the extent of the loop, i.e., in the loop condition, the iteration expression, and the loop body. The genvar environment now records, for each genvar that is local to a loop, the scope that contains that loop. A reference resolves to the genvar when the symbol that resolve() finds is not declared inside the loop. Genvars that are declared separately from the loop generate construct are unaffected, as these do have a symbol.
The elaboration of module instances, of their parameter values, and of parameter overrides recurses through the set_genvars module items that the elaboration of the generate constructs has produced, but did not restore the genvar environment when doing so. This went unnoticed for genvars that are declared separately from the loop generate construct, as these have a symbol that resolve() finds, albeit with the value the genvar has once the loop has terminated. A genvar that is declared in the header of the loop generate construct is local to that loop, 1800-2017 27.4, and does not have a symbol, and hence failed to resolve altogether. The genvar environment is now restored from the set_genvars module item in elaborate_module_instances, parameterize_instantiated_modules, and process_parameter_override, which also yields the value the genvar has in the given iteration of the loop.
The loop-local genvar fix makes the genvar in the part selects of the port connections evaluate per iteration, and hence this test now passes. Leaving it as KNOWNBUG fails the KNOWNBUG checks CI job, which runs test.pl -K and expects KNOWNBUG tests to fail.
The elaboration of module instances now restores the genvar environment, and hence a genvar that is local to a loop generate construct also resolves when it indexes the actual of an output port, which is checked as an lvalue rather than converted as an expression. Adds a test for that case. verilog_set_genvarst::build_map() is removed, as the genvar environment is now built by verilog_typecheckt::build_genvars, which also carries over the scopes of the loop-local genvars.
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.
No description provided.