Generate equivalent Verilog test case modules for the Vera equivalence checker
You are writing a SystemVerilog module that will be used as a test case for Vera, a formally verified Verilog equivalence checker. The module must implement the requested operation in the requested style, and must be semantically equivalent to the other implementations of the same operation that already exist in the same directory.
examples/ for the same operation to
determine the interface (input/output names, widths, module naming).
.sv file implementing the same operation in the requested style.examples/<operation>/ directory.dune exec vera -- compare --solver=z3 examples/<operation>/existing.sv examples/<operation>/new.sv
Equivalent (UNSAT)Only purely combinational logic using assign statements is supported.
assign statements (continuous assignment only)+, -, *&, |, ^, ~<<, >>, <<<? :signal[idx]{a, b}wire declarations for intermediate valuesalways blocks of any kind (always, always_comb, always_ff)<=)for, generate, while loopscase, if/else statements (use the ternary ? : operator instead)function, task definitionsinteger, real, or other non-logic types{N{expr}} syntax (e.g., {8{1'b0}})8'd0, 4'b0000, 1'b0, etc.8'd0 not 0).module <descriptive_name> (
input logic [W_IN-1:0] <input_names>,
output logic [W_OUT-1:0] <output_names>
);
wire [N:0] intermediate;
assign intermediate = ...;
assign <output> = ...;
endmodule
If equivalence checking fails unexpectedly:
Check for unimplemented features - Even if an operator is listed as supported, it may not be fully implemented yet. Look for error messages like "Unary operators not supported" or "Unknown operator".
Test operators in isolation - If a complex expression fails, create a minimal test case using just the suspect operator to verify it works:
// Simple test for operator ~
assign out = ~a;
Build incrementally - Start with simple test cases before creating complex ones. For example, test ~(a & b) before testing nested expressions like ~((a & b) | c).
It's okay to create tests for future features - You can write test cases that use unimplemented operators. They'll error out now but will work once the feature is implemented.
For testing across multiple bit widths, use Jinja2 templates instead of hardcoded modules.
examples/templates/<category>/<name>.sv.j2examples/gen_<category>_<N>/<name>.svshake examples/summary.csv generates and tests all configured widthsjinja2 -D N=8 examples/templates/<category>/<name>.sv.j2{% set N = N | int -%}
{% set HALF = N // 2 -%}
{% set OUT_W = 2 * N -%}
module example (
input logic [{{ N-1 }}:0] in,
output logic [{{ OUT_W-1 }}:0] out
);
Common patterns:
| Pattern | Jinja2 Syntax |
|---|---|
| Width parameter | {% set N = N | int -%} |
| Derived width | {% set HALF = N // 2 -%} |
Verilog { brace | {% raw %}{{% endraw %} |
| Whitespace control | {%- and -%} to trim newlines |
| Loop (descending) | {% for i in range(N-1, -1, -1) %}...{% endfor %} |
| Conditional | {% if COND %}...{% else %}...{% endif %} |
Manual log2 (Jinja2 has no log function):
{%- if N < 2 -%}{% set IDX_W = 0 %}
{%- elif N < 4 -%}{% set IDX_W = 1 %}
{%- elif N < 8 -%}{% set IDX_W = 2 %}
{%- elif N < 16 -%}{% set IDX_W = 3 %}
...
{%- endif -%}
For algorithms like Karatsuba that split inputs in half, handle odd widths with asymmetric splits:
{% set H_LOW = N // 2 -%}
{% set H_HIGH = N - H_LOW -%}
wire [{{ H_HIGH-1 }}:0] a_high; // Larger half
wire [{{ H_LOW-1 }}:0] a_low; // Smaller half
assign a_high = in[{{ N-1 }}:{{ H_LOW }}];
assign a_low = in[{{ H_LOW-1 }}:0];
Key width calculations:
z_low = 2*H_LOW bits, z_high = 2*H_HIGH bitsH_HIGH + 1 bits (zero-extend smaller operand)H_LOW, not NReference implementations in examples/templates/:
adder/ - plus_operator, ripple_carry, carry_lookaheadmultiplier/ - star_operator, shift_and_add, karatsubarangeselect/ - rangeselect, concatbitselect/ - bitselect, shiftconditional/ - ternary, gates