SJV SystemVerilog Subset Reference

Documentation version: 1.0
Implementation snapshot: 6dd5716a8f3bcf29d27ae9ca64800bb517601236 (SekuraJS repository).

This page records behavior present in that source snapshot. It does not define planned or desired SystemVerilog support.

Prepared by A. T. Kuangaliyev, Jupiter Soft LLP, with assistance from ChatGPT.

1. Scope

sekura-sjv can parse and elaborate a defined subset of SystemVerilog and verify supported combinational or sequential RTL behavior against an SJV contract. This is not a complete SystemVerilog implementation, simulator, or synthesis tool.

SystemVerilog verification is a direct RTL path. It does not compile SystemVerilog into Sekura JS .sobj:

Sekura JS:      .sjs + .sjv + .sobj -> SJV verification
SystemVerilog:  .sv + .sjv          -> RTL elaboration and verification

The implementation has separate stages. A construct may be tokenized or parsed but still be unsupported by elaboration or proof lowering. This page distinguishes syntax accepted by the frontend from behavior currently supported in a proof.

2. Selecting a SystemVerilog design

An SJV file selects its source by using an .sv path in the module declaration:

module "rtl/top.sv";

{
    ready == 0;
}

function step {
    enable;
    ready' == 1;
}

A quoted path may be absolute or relative to the SJV file. The CLI can add further SystemVerilog source files, include directories, macro definitions, and parameter overrides. These settings affect which design is elaborated and must be kept with the verification inputs.

3. Supported source organization

The parser recognizes modules and packages. A verification run selects one root module by the SJV source reference and elaborates modules found in the configured source set. Only behavior that the RTL proof backend lowers is included in a proof.

Implemented hierarchy features include ordinary module instances, named or positional port connections, constant parameter overrides, and statically selected generate conditions/loops for elaboration. Child module behavior can participate in a parent proof when the elaborated hierarchy and port connections are supported.

The current proof backend rejects generate-scoped assignments/processes that it cannot lower into the symbolic hierarchy. Successful parsing or elaboration of a generate block alone does not mean the generated behavior was included in the proof.

The parser/elaborator handles package/import, typedef, and constant-expression forms used by the implementation. This statement describes frontend handling only; it does not promise that arbitrary package declarations or all typedef forms can be used in a proof.

4. Preprocessing

The preprocessor implements object-like macros and conditional compilation using directives including:

`define WIDTH 8
`undef WIDTH
`ifdef FEATURE
`ifndef FEATURE
`elsif OTHER_FEATURE
`else
`endif
`include "config.svh"

Include files must be present in the configured source/include search set. The CLI supplies initial macro definitions and include directories. Object-like macro expansion is supported; function-like macros, token pasting, and stringification are rejected. Unsupported or unresolved directives do not count as verified input. The SV lexer also permits the system-function tokens $clog2, $bits, $signed, $unsigned, $readmemh, and $readmemb; this lexical allowlist is not a claim that each function is implemented in every elaboration or proof context. The RTL proof lowering implements $signed/$unsigned casts. $clog2 is handled in supported constant-expression contexts during elaboration, not as a general runtime RTL function. The other allowlisted names may still be unsupported by a selected proof path.

The lexer accepts both // line comments and /* ... */ block comments. Strings are not supported as ordinary RTL expressions; string tokens can occur in preprocessor include directives and selected attributes.

5. Two-state proof model

The RTL proof model uses two-valued bit vectors. It does not model four-state X/Z behavior or net-resolution semantics. Four-state literals containing x, z, or ? are rejected by the base profile, and an unknown value must not be treated as zero.

Common supported literal forms include decimal and sized based integral literals, for example:

8'd7
8'h2a
4'b1010
'0
'1

Unsized or sized values are interpreted according to the frontend’s width and signedness rules. Keep widths explicit in RTL where truncation, extension, or signed comparisons matter.

6. Types and declarations

The parser recognizes integral built-in types including logic, reg, bit, byte, shortint, int, integer, longint, time, and genvar, along with signed/unsigned qualifiers and packed or unpacked dimensions. It also parses supported alias, packed-structure, and enumeration typedef forms.

Whether a parsed declaration can participate in a proof depends on the elaborated width and use. The RTL lowering currently rejects zero-width or greater-than-1024-bit proof values. Fixed unpacked arrays used as state are limited to 65,536 elements total. Dynamic arrays, queues, associative arrays, and other runtime-sized storage are outside the proof model.

The frontend accepts ANSI-style module port declarations. Ports used by a proof must resolve to a supported type and width; a declaration without a packed range is a scalar. inout ports are outside the two-state hierarchical proof model.

Packed structs, enum typedefs, and typedef aliases may be parsed and elaborated. The proof backend only supports operations it can lower while preserving packed bit layout; do not infer general support for every SystemVerilog type operation from successful parsing.

7. Expressions

The parser accepts expression syntax for identifiers, literals, parentheses, calls, member/qualified names, bit-selects, part-selects, concatenations, replications, casts, unary/binary operations, and conditional expressions. Parsing a form does not guarantee proof support.

The RTL lowering implements these operators in supported expression contexts:

Unary:     +  -  !  ~  &  ~&  |  ~|  ^  ~^  ^~
Binary:    +  -  *  /  %  &  |  ^  ~^  ^~
Compare:   ==  !=  <  <=  >  >=
Logical:   &&  ||
Shift:     <<  >>  <<<  >>>
Conditional: condition ? true_value : false_value

Support depends on expression widths, signedness, lvalue context, array selections, and the operation location. Division or remainder with a literal zero divisor is unsupported. For symbolic divisors, the verifier adds a nonzero-divisor obligation; if it cannot establish that condition, verification does not report a successful proof.

Case equality/inequality (===, !==), wildcard equality, assertion implication operators, and other unsupported operators are outside the profile. The frontend rejects known unsupported operators, and proof lowering reports UNSUPPORTED for operations it cannot model.

8. Combinational RTL

Combinational logic can be described with continuous assignments and supported always_comb procedural blocks. Supported procedural statements include a subset of blocks, blocking assignments, conditionals, case statements, and statically bounded for loops.

Every combinational output must be assigned on every relevant branch. Incomplete always_comb assignment (latch inference), combinational cycles, unresolved dependencies, and multiple combinational drivers are unsupported.

Example:

module adder;
  function automatic logic [7:0] add(input logic [7:0] a, input logic [7:0] b);
    begin
      add = a + b;
    end
  endfunction
endmodule

An SJV contract can specify the function result:

module "adder.sv";
{ 1 == 1; }
function add {
    return' == a + b;
}

This function example is covered by the current RTL proof tests.

9. Sequential RTL

The sequential proof path supports always_ff with a single clock edge and optionally one asynchronous reset edge, subject to structural constraints. All sequential processes in one proof slice must use the same clock signal and edge polarity. Derived or combinationally driven clocks and multiple clock domains are unsupported.

Sequential state updates use nonblocking assignments. A sequential process must have supported state targets and a modelable control-flow structure. For asynchronous reset, the event list and first reset guard must match the supported reset form. Multiple sequential processes driving the same state, mixed sequential/combinational drivers, or assignments to input ports are rejected.

Example:

module sequential(input logic clk, input logic d, output logic [7:0] q);
  always_ff @(posedge clk) begin
    if (!d) q <= 8'b0;
    else    q <= q + 1'b1;
  end
endmodule

Corresponding SJV contracts describe the transition at the selected event boundary:

module "sequential.sv";
{ 1 == 1; }
function step {
    d;
    q' == q + 1'b1;
}
function reset {
    !d;
    q' == 0;
}

The RTL backend checks preconditions, postconditions, and the state condition for the modeled transition. It does not model analog metastability, timing delays, waveforms, or reset-release behavior as a continuous-time simulation.

10. Fixed memories and arrays

Fixed unpacked arrays can be modeled as state when their dimensions resolve statically and the selected RTL operations are supported. The current model caps total array depth at 65,536 elements. A dynamic index may be used in supported read/write forms; proof preserves declared index ranges and can report reachable out-of-range accesses as counterexamples.

Example:

module ram(input logic clk, input logic we, input logic [2:0] waddr,
           input logic [7:0] wdata, output logic [7:0] q);
  logic [7:0] mem [0:3];
  always_ff @(posedge clk) begin
    if (we) mem[waddr] <= wdata;
    q <= mem[waddr];
  end
endmodule

Writes to unpacked arrays require supported sequential nonblocking-assignment forms. Partial RAM writes are restricted; current lowering supports selected packed-word/part-select cases with static bounds after loop unrolling. Unpacked-array elements as child output lvalues and unsupported partial-write layouts are rejected.

Array initial contents are not assumed to be zero unless the RTL reset or verification environment establishes that fact. Memory initialization file behavior is not a general default guarantee; use only initialization/configuration paths explicitly handled by the selected CLI and proof backend.

11. Functions, tasks, and procedural control

Pure function forms supported by the RTL lowering can be used in supported expressions. Recursive expansion is limited; recursive or unsupported function behavior produces an unsupported result. Tasks are tokenized and parsed in some forms but are not a general substitute for supported proof functions.

Procedural if, case, and statically bounded loops are supported only where the backend can lower them. A case used for combinational selection must be complete; a missing default can be rejected when completeness cannot be established. Dynamic loops, unbounded loops, while, repeat, forever, fork, and event scheduling are outside the proof subset.

12. Unsupported language and simulation constructs

The profile rejects or cannot prove general uses of the following constructs:

  • four-state values and resolution: X, Z, tri-state behavior, multiple unresolved drivers, casex, case equality;
  • simulation/event constructs: initial, final, delays, event controls outside the supported always_ff form, wait, fork, join, force, release;
  • dynamic or object-oriented SystemVerilog: classes, dynamic arrays, associative arrays, queues, strings, DPI/VPI/PLI, dynamic compilation;
  • verification-language constructs: SVA property/sequence, assert, assume, cover, restrict, bind, checker/interface/modport/clocking blocks;
  • unsupported procedural flow: while, do, repeat, forever, foreach, disable, and unsupported forms of break/continue;
  • unsupported net/port forms: inout, tri, wand, wor, uwire, unresolved multiple drivers;
  • unsupported operators: ===, !==, ==?, !=?, |->, |=>, ##, and &&&.

This list is not exhaustive. The parser and proof backend report additional constructs as UNSUPPORTED when encountered. Do not treat a parsed construct as proof coverage.

13. SJV contract names for RTL

SJV refers to selected module ports, internal signals, supported hierarchical signals, and function inputs using names resolved by the elaborated design. Post-state uses the apostrophe marker:

function transfer {
    enable;
    count' == count + 1;
    child.q' == input_value;
}

SystemVerilog name binding supports selected hierarchical paths, static array selections, and function-local names in supported cases. The backend rejects unresolved names or expressions outside the SJV/SV binding model. See the SJV Language Reference for SJV expression syntax and state-block semantics.

14. Proof result boundaries

A successful result applies to the SJV properties checked against the selected elaborated design and the semantics implemented by this backend. It does not establish correctness for another parameterization, unmodeled environment, analog behavior, unsupported construct, or property absent from the contract.

When the current implementation encounters an unsupported construct on the proof path, it reports an unsupported or inconclusive outcome. A counterexample is a modeled input/state assignment that violates a checked contract. A passing simulation or test is not equivalent to an SJV proof.

15. Checked examples

The repository’s current SystemVerilog proof tests exercise examples including:

  • an 8-bit combinational function with a correct contract and a counterexample for an incorrect contract;
  • a single-clock always_ff transition with conditional state update;
  • division with an explicit nonzero-divisor precondition;
  • preprocessor includes, object-like defines, include directories, and parameter overrides;
  • a two-instance hierarchy with continuous and combinational logic and sequential state;
  • a small synchronous RAM with bounded addressing and an out-of-range counterexample.

These tests demonstrate covered cases, not a guarantee that every syntactic variation of those constructs is supported.

16. Relationship to SOBJ and SJP

SOBJ is the compiled MR8 implementation artifact used by the Sekura JS verification path. It is not generated from SystemVerilog. The SystemVerilog frontend constructs an RTL transition model directly from the selected .sv source set.

A successful SystemVerilog verification can be packaged as SJP. SJP records the proof inputs/results according to its own format specification; it does not expand the SystemVerilog subset supported by the verifier.