Verilog verification

Aristotle verifies properties of circuit designs written in SystemVerilog. Properties can be written informally in English or as supported SystemVerilog Assertions (SVA). After analysis, Aristotle returns a summary of the properties you specified and the properties it inferred. A refutation is supported by a concrete counterexample, a formal proof of the negation, or both. For a concrete counterexample, Aristotle returns a testbench or harness that reproduces it and a VCD waveform.

Submitting a design

You can upload Verilog or SystemVerilog files directly in the Aristotle web UI. Include any supporting design files and describe the properties you want verified in your prompt. No CLI installation is required to use the web UI.

Optional CLI installation

If you prefer to submit designs from the command line, install the CLI with uv:

$ uv tool install "aristotlelib>=3"

The installation guide covers logging in and the other ways to install.

Example workflow

This example uses a 5-tap systolic filter in a file named semisystolic_fir.sv:

module tap #(parameter logic [15:0] WEIGHT = 16'd1) (
    input  logic        clk,
    input  logic        enable,
    input  logic        reset,
    input  logic [15:0] xin,
    input  logic [15:0] yin,
    output logic [15:0] xout,
    output logic [15:0] yout);

    logic [15:0] xin_delayed;

    // Unit delay register for xin.
    always_ff @(posedge clk) begin
        if (reset) begin
            xin_delayed <= 16'd0;
        end else if (enable) begin
            xin_delayed <= xin;
        end
    end

    // xout passes the delayed sample to the next tap.
    assign xout = xin_delayed;

    // Multiply-accumulate: weight * delayed sample + incoming partial sum.
    assign yout = (xin_delayed * WEIGHT) + yin;

endmodule: tap

module semisystolic_fir #(parameter int N = 5,
    parameter logic [0:N-1][15:0] WEIGHTS = {16'd2, 16'd5, 16'd7, 16'd4, 16'd3}) (
    input  logic        clk,
    input  logic        enable,
    input  logic        reset,
    input  logic [15:0] x,
    output logic [15:0] y);

    // Internal wires connecting adjacent taps.
    logic [15:0] xwire [0:N];
    logic [15:0] ywire [0:N];

    // Feed the input sample into the first tap.
    assign xwire[0] = x;

    // The partial sum starts at zero.
    assign ywire[0] = 16'd0;

    // Generate the chain of tap instances.
    genvar i;
    generate
        for (i = 0; i < N; i++) begin: inst_tap
            tap #(.WEIGHT(WEIGHTS[i])) u_tap (
                .clk  (clk),
                .enable(enable),
                .reset(reset),
                .xin  (xwire[i]),
                .yin  (ywire[i]),
                .xout (xwire[i+1]),
                .yout (ywire[i+1]));
        end: inst_tap
    endgenerate

    // The filter output is the final tap's accumulated sum.
    assign y = ywire[N];

endmodule: semisystolic_fir

To specify the correct behavior of the semi-systolic filter, create a file filter_spec.md that describes its operation in English:

# Formally Verify Correctness of the Semi-Systolic FIR Filter

For an $N$-tap filter with weights $w_0, w_1, \ldots, w_{N-1}$, the output at clock cycle $n$ is:

$$y[n] = \sum_{i=0}^{N-1} w_i \cdot x[n - i - 1]$$

Each tap $i$ contributes $w_i \cdot x[n-(i+1)]$ because the sample passes through
$i+1$ registers on the $x$-path before being multiplied (one register per tap it
has traversed, including tap $i$'s own register). The $y$-path is purely
combinational, so all the products are summed in the same cycle.

This is a standard FIR convolution with a single extra cycle of latency (the
$-1$ in the index) compared to a direct-form implementation, which is the cost
of registering the $x$-path to make it semi-systolic.

Formally verify the top level circuit `semisystolic_fir` implements a semi-systolic filter for all inputs using the specified weight values for a 5-tap filter with the constant weights (2, 5, 7, 4, 3). All signals (apart from clock, reset and enable) are 16-bit unsigned numbers. Assume the enable input is always asserted (high). Assume the synchronous reset signal has been asserted during the first cycle, initializing each register delay element to 0, and is de-asserted in all subsequent cycles.

To submit this example in the web UI, upload semisystolic_fir.sv and filter_spec.md, along with any supporting design files, and enter the prompt: "Perform the formal verification of the semisystolic_fir circuit specified in the file filter_spec.md".

To submit it from the command line, put semisystolic_fir.sv and filter_spec.md together in one directory and submit that directory:

$ aristotle submit "Perform the formal verification of the semisystolic_fir circuit specified in the file filter_spec.md" --project-dir .

Either submission method creates a hardware verification job for Aristotle which you can monitor at https://aristotle.harmonic.fun/projects. Aristotle may ask you questions while it works, and waits up to 15 minutes for each answer. Answer them on the project page, or with the aristotle questions <project-id> command that aristotle submit prints.

The CLI uploads the directory, except what an ignore rule matches and a few kinds of file it never sends, such as files named like credentials. In a git repository, git's ignore rules apply; elsewhere, or in a folder git ignores, only the directory's top-level .gitignore does. Add --include-ignored to upload what the ignore rules match too, such as sources a build generates. Without an aristotle.f, -f, or -F (see Specifying SystemVerilog build options), nothing from outside the directory goes up. A link to a file goes up only when the file it points to does too, and a link to a folder never does. So the directory has to hold everything the design needs, such as included headers, library modules, and the specification. Add --dry-run to list what would go up without sending anything.

For a verification run where all the properties are proved correct you will see a summary file with text like this:

## V2L Formal Verification Complete

All properties of the semi-systolic FIR filter have been formalized and proven sorry-free.

### Files modified/created:
- **`VeriLeanOut/tapsemisystolicfirtaps{0-4}utap_proofs.lean`** — Each tap module has 3 proven theorems:
  - `yout` computes `xin_delayed * weight + yin`
  - `xout` passes through `xin_delayed`
  - Next state stores `xin` into `xin_delayed`

- **`VeriLeanOut/semisystolicfir_proofs.lean`** — The top-level module has 7 proven theorems:
  - Single-cycle weighted sum of all tap registers
  - 5 state propagation lemmas (shift register behavior)
  - **`semisystolic_fir_correct`**: Multi-cycle FIR convolution correctness — for n ≥ 5:
    `y[n] = 2*x[n-1] + 5*x[n-2] + 7*x[n-3] + 4*x[n-4] + 3*x[n-5]` (mod 2^16)

- **`ARISTOTLE_SUMMARY.md`** — Human-readable summary for hardware engineers.

All proofs compile cleanly with no `sorry` statements. The full project builds successfully.

A human-readable summary of the verification is also returned with the run.

For a verification task where a bug was found you will get a message like this:

V2L: Formally verified the semi-systolic FIR filter design and found a critical bug.

## What was done

### Leaf modules (tap, 5 instances with weights 2,5,7,4,3)
For each tap instance, 4 properties were formalized and proven sorry-free:
- **Reset clears delay**: `reset=1` → `xin_delayed` becomes 0
- **xout passthrough**: `xout` always equals current `xin_delayed`
- **Enable update**: `reset=0, enable=1` → `xin_delayed` captures `xin`
- **yout computation**: `yout = (xin_delayed * WEIGHT + yin) % 64`

Proof files: `VeriLeanOut/alttapaltsemisystolicfirtaps{0..4}utap_proofs.lean`

### Top-level module (semisystolic_fir)
7 properties formalized and proven sorry-free in `VeriLeanOut/altsemisystolicfir_proofs.lean`:
1. **fir_reset_clears_state**: Reset zeros all 5 delay registers
2. **fir_state_update_with_enable**: Delays form a shift register chain
3. **fir_output_actual_computation**: Output = chained `% 64` accumulation
4. **fir_shift_register_n_cycles**: Multi-cycle shift register property
5. **fir_module_total**: Module relation is total (non-vacuous)
6. **fir_standard_convolution_is_false**: Single-cycle FIR convolution is FALSE
7. **semisystolic_fir_correct_is_false**: Multi-cycle FIR correctness is FALSE

### Bug found
The `tap` module contains `assign yout = ((xin_delayed * WEIGHT) + yin) % 64;` — the `% 64` is a bug that prevents the filter from computing the correct FIR convolution. The counterexample: after reset, feed x=32, then x=0. Expected FIR output at cycle 2: 64. Actual: 32.

### Testbench
`semisystolic_fir_convolution_tb.sv` reproduces the bug with Verilator. VCD waveform at `semisystolic_fir_convolution_tb.vcd`.

You can download the VCD waveform file and view it with a VCD viewer like gtkwave or surfer. You can also download the SystemVerilog testbench file and run it locally to re-generate the VCD waveform file.

Implementing, fixing, and optimizing RTL

Aristotle can also write a new design. Describe it in your prompt and attach any specifications. State the properties the design must satisfy or ask Aristotle to derive them from the specification. Aristotle implements the design in SystemVerilog, verifies the properties against it and returns the new source files with the results.

Aristotle changes your design files only when you ask it to, in your prompt or in answer to one of its questions. When a property is refuted with a counterexample, reply in the same project and ask Aristotle to fix the design. It edits the RTL, verifies your properties against the revised design, and lists what it changed in the summary. To review a fix before it is applied, ask for a proposed fix instead: your files stay unchanged until you approve it.

To optimize a design, synthesize it yourself, reply in the project with the reports attached, and say which metrics to improve. Aristotle revises the RTL, verifies the same properties again, and estimates the effect of each change, which your next synthesis run then measures. Name every metric that matters: Aristotle optimizes what you ask for.

Specifying SystemVerilog build options

Aristotle infers the build from the sources, so most designs need no build options. When a design has more than one candidate top module, or needs defines or include directories, list them with its sources in a filelist named aristotle.f at the root of the directory you submit:

--top soc_top
-I rtl/include
-D DATA_WIDTH=32
--blackbox sram_1p
-F rtl/soc.f

aristotle submit reads aristotle.f as a simulator reads a filelist, so the one your flow writes usually works as it is. Nested -f and -F filelists, +incdir+ and +define+, comments, quotes, and environment variables all work, and options that don't change which files make up the design, such as -sv, are left out. Every file the filelists name, and every header the sources include, goes up, even when an ignore rule matches it. A file from outside the directory goes up under _ext/. An option the CLI doesn't know, a file that isn't there, or a variable that isn't set stops the command before anything is sent. Add --dry-run to see each file of the design with where it comes from, and the aristotle.f that would go up.

The design on the command line

--top, -f, and -F on aristotle submit add to the design the directory's aristotle.f describes, or describe it on their own, with paths relative to the current directory. A --top replaces any top module the filelists name. Without --project-dir, only the design's files go up:

$ aristotle submit "Prove that sum is a+b, a cycle later" --top alu_top -F design/alu/alu.f

--top and --blackbox need a filelist that names the design's sources. For a directory with no filelist, name the top module in the prompt instead.

Black boxes

--blackbox <module> has Aristotle treat a module, such as a foundry cell, as a black box with unconstrained outputs. Give it on the command line, once per module, or on a line of aristotle.f. A file that declares nothing but black boxes stays out of the upload, whether the filelists name it or it is a .v, .sv, .vh, or .svh file in the directory. Anything else it holds, such as a `define, stays out with it. A file that declares a black box beside another design unit stops the command: move the module to a file of its own. So does a header the design includes that declares one: drop the `include and name the header in the filelists instead. The CLI can't see a module that a macro declares, or a model encrypted whole, so take such a file out of the filelists and the directory yourself. Add --dry-run to list the files each black box leaves out.

Through an assistant

If your assistant uses Aristotle's MCP server, tell it the design's top module, defines, include directories, and black boxes. It writes the top module, defines, and include directories into an aristotle.f at the root of the project it uploads, in the format Aristotle reads, and names each black box when it starts the run. The server doesn't take a black box's source out of an upload, so a model that mustn't be sent has to stay outside the project's folder. For nested filelists, files outside the project's folder, or generated sources an ignore rule matches, use the CLI.

The format Aristotle reads

Aristotle itself reads a simpler form of aristotle.f: the one the CLI generates, and the one to follow when you write it by hand, for example to upload with a design in the web UI. In the web UI, end the prompt with Use aristotle.f as the commands file., the line the CLI adds. The CLI sends your aristotle.f as it is when it already follows this form, and otherwise generates one that does. A generated one can't use -y yet: name the library's files instead.

• One option, or one source file, per line, with a space between an option and its value: -I include, --top top. List the source files as well as any options.
• Paths are relative to the folder holding aristotle.f, and stay inside it. There are no globs, environment variables, nested filelists, or +...+ forms.
• A line that starts with # or // is a comment.

Only these options are supported:

The example workflow needs no aristotle.f. To name its top module explicitly:

--top semisystolic_fir
semisystolic_fir.sv

A design split across directories, with shared headers and a macro, might use:

--top soc_top
-I include
-D SYNTHESIS
rtl/tap.sv
rtl/soc_top.sv

Checking properties in CI

aristotle ci checks the properties listed in an aristotle.toml at the root of your repository, and reports each one as a test in your CI system: a proved property passes, and a refuted one fails. It takes the design's build options and black boxes from the aristotle.f committed at the root of the repository. Unlike aristotle submit, it expands no environment variables, and by default it sends only files git tracks there. Every aristotle ci run proves every property again, so run it only when the design, its filelists, or aristotle.toml changes. aristotle ci setup has Aristotle propose properties for you to review and commit. It doesn't read aristotle.f, so it sends a black box's file with the rest of the checkout: match a model you mustn't send with a .gitignore rule. In GitHub Actions, add the action after the checkout:

steps:
  - uses: actions/checkout@v4
  - uses: harmonic-ai/aristotle@v3
    with:
      api-key: ${{ secrets.ARISTOTLE_API_KEY }}

Current limitations

Aristotle's hardware verification has the following limitations.

X and Z values are unconstrained

Aristotle uses a two-state formal model: every bit is either 0 or 1. When SystemVerilog says that a bit is unknown (x) or high-impedance (z), Aristotle models that bit as unconstrained: it may be either 0 or 1, and a proof must hold for both possibilities.

For example, 4'b10xz keeps the upper two bits fixed at 10, while each lower bit is allowed to take either value. The same treatment applies to undriven nets, uninitialized flip-flops and memories, division or modulo by zero, out-of-range memory reads, and out-of-bounds dynamic bit or part selects. For a partially out-of-bounds part select, the in-range bits are still constrained to the selected source bits and only the out-of-range bits are unconstrained.

module dynamic_slice (
    input  wire [7:0] data,
    input  wire [2:0] addr,
    output wire [3:0] slice);
  assign slice = data[addr +: 4];
  // When addr == 6, slice[1:0] equals data[7:6] and slice[3:2] is unconstrained.
endmodule

This is intentionally different from four-state simulation. An x is not a third value that propagates through every downstream expression. It represents an unspecified hardware value, and ordinary logic operates on whichever 0 or 1 that value takes. Separately unknown bits are not assumed to have the same value. Consequently, a successful proof cannot depend on an x resolving in a particular way, but waveforms may not show the same X propagation as a simulator.

Case equality also has two-state semantics. If neither operand contains an x or z literal, === and !== are treated like == and !=. In a comparison such as a === 4'b10xx, the unknown literal bits are treated as wildcards and only the known bits are compared. This differs from IEEE case equality, which tests whether those bits are literally X. Aristotle reports a warning when it encounters a case comparison; do not use ===, !==, or $isunknown to check for X/Z values in a property.

SystemVerilog Assertion support is partial

Aristotle can import module-level concurrent assert property, assume property, and cover property directives. The supported subset includes:

• explicit posedge and negedge clock events on a module signal;
• the clock must be equivalent to the circuit's single global clock;
• ordinary arithmetic, logical, comparison, concatenation, and select expressions;
• $past with a constant positive delay, $stable, $onehot, and $onehot0;
• fixed, bounded, and unbounded sequence delays (##N, ##[m:n], and ##[m:$]), plus sequence and and or;
• property not, and, and or, overlapped and non-overlapped implication (|-> and |=>), s_eventually, and disable iff.

This is not the complete SVA language. Unsupported examples include assertions within procedural blocks, default clocking, sequence repetition ([*], [->], and [=]), and sampled-value functions such as $rose, $fell, and $changed. X/Z literals inside an assertion are also unsupported because assertions use the same two-state model as the circuit model.

An unsupported directive is omitted rather than approximated, while supported directives and the circuit itself are still processed. The generated VeriLeanOut/Public/SVA_WARNINGS.md file lists every omitted directive with its source location and reason. If SVA processing fails as a whole, Aristotle still verifies the circuit and the report states that all SVA directives were omitted. Review this report before relying on the SVA results.

Initial state

Aristotle does not ignore initial values. If your design has something like

reg [3:0] a = 4'b0100;

then Aristotle will assume that the flip-flop a has value 4'b0100 at time zero. If you're working on an ASIC design, then you're responsible for removing these initial values.

Independent clock domains are not supported

Aristotle currently supports single-clock verification. It does not verify communication between independent clock domains, such as an asynchronous FIFO with separate read and write clocks.

You can ask Aristotle to verify a single-clock domain block on its own. Those results do not verify clock-domain crossings.

Sensitivity lists are ignored

All always blocks execute on every clock tick, regardless of their sensitivity list, so gated-clock behavior is not preserved:

wire gated_clk = clk & enable;

always @(posedge gated_clk)
  out <= in;
// Aristotle updates `out` on every posedge of `clk`, not just when `enable` is high

Memory write-port ordering

Aristotle supports two kinds of memory write-port ordering, covering the majority of real designs:

• Totally ordered. A single writer, or multiple writers with a clear priority chain (for example, several non-blocking assignments to the same memory within one always block, where the last write wins on an address collision). These lower to a direct sequential application of the writes.
• Completely unordered. Multiple writers with no priority relationship between them (for example, separate always blocks writing the same memory). These lower to an order-independent relational constraint: per address, the unique active writer determines the new value. If two or more writers are active at the same address in the same cycle, that location is left unconstrained—modeling 'x—even if the writers supply identical data (the relation does not compare the values).

Partially ordered write ports—where a priority relation exists between some, but not all, pairs of writers (neither a full chain nor fully edge-free)—are not yet supported.

Latches are not supported

Level-sensitive latches (inferred from incomplete always @* blocks or from explicit always_latch constructs) are not supported. Designs that infer latches will be rejected.

always @*
  if (en) q = d;
// incomplete assignment infers a latch -- rejected by Aristotle

Inout ports are not supported

Bidirectional (inout) ports are rejected. Designs must use separate input and output ports.

module bus_driver(inout wire [7:0] data); // rejected