SJV Verification Language Reference

Documentation version: 1.0
Status: Describes the current SJV parser and verification paths; it is not a promise that every parseable expression is supported by every backend.

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

1. Purpose and scope

SJV is a text format for describing valid implementation states and function transition contracts. The Sekura verification toolchain parses an .sjv file, binds its names to an implementation, and can check supported properties against a compiled Sekura JS object (.sobj) or supported SystemVerilog source.

SJV is not an implementation language and is not itself a proof artifact. A successful verification run can produce an SJP artifact. The SJP container and command-line workflows are described on their own reference pages.

The grammar accepted by the parser is broader than the expression subset currently supported by each verification backend. A successful parse alone does not establish that a model can be bound or proved.

2. File structure

An SJV file starts with one module declaration, followed by one or more state blocks, function contracts, and—on the supported SystemVerilog dependency path—optional dependency declarations.

module_decl
state_block*
function_contract*
dependency_declaration*

The module declaration identifies the implementation source. Names, types, and function signatures are taken from that implementation rather than redeclared in SJV.

3. Module declaration and source selection

The parser accepts an identifier path, a dotted identifier path, or a quoted path:

module motor.sjs;
module "control/motor.sjs";
module top_level_cpu.sv;

The referenced path is resolved relative to the SJV file by the CLI. If no source extension is supplied, the current resolver treats it as an SJS source. An .sv suffix selects the SystemVerilog frontend; other references use the SJS frontend.

A quoted path is useful for paths containing slashes or other characters outside the identifier-path form. The implementation path and source kind affect which names and expressions can be bound and which proof backend is selected.

4. State blocks

A state block contains one or more semicolon-terminated constraints. Constraints in the same block are conjoined. Multiple state blocks describe alternative valid state classes and are disjoined:

module motor.sjs;

{
    enabled == 1;
    speed < 100;
}

{
    fault != 0;
    speed == 0;
}

This represents (enabled == 1 && speed < 100) || (fault != 0 && speed == 0).

At least one non-empty state block is required for verification. In the SJS binding path, top-level state constraints must refer to pre-state; post-state references are rejected there.

The current consistency checker catches empty state blocks and a limited form of direct contradictory equalities, such as the same simple name being required to equal two different numeric literals. This is not a general satisfiability analysis and should not be treated as one.

5. Function contracts

A function contract names an implementation function and contains constraints:

function setSpeed {
    value < 100;
    speed' == value;
}

The function name must resolve in the selected implementation. For SJS, ordinary parameter and module-level value names are resolved against the corresponding .sjs source. For SystemVerilog, names are bound against the selected/elaborated module and supported function scope.

SJV does not repeat a function’s parameter list or type signature. Use the implementation’s exact function and parameter names.

A contract intended for an implementation proof needs post-state constraints supported by the selected backend. A model that parses but has no applicable postcondition can still be rejected as unsupported during verification.

6. Pre-state and post-state

An apostrophe after a supported name denotes its value after the function transition. Without the apostrophe, the name denotes its pre-state value:

function add {
    value < 100;
    count' == count + value;
}

Here value < 100 constrains the pre-state/input domain, while the equality containing count' describes a required post-state relation.

In the current SJS proof path, a function constraint with no post-state reference is treated as a precondition. A constraint containing post-state is treated as a postcondition. The prover also checks that the resulting state satisfies one of the declared state blocks. Do not assume that omitted fields are preserved: state preservation must be written explicitly when required.

The return result can be referenced as return' in supported SJS contracts:

module verification_identity.sjs;

{
    r2 == r2;
}

function identity {
    value < 100;
    return' == value;
}

Support for return expressions and post-state names depends on the source kind and proof backend.

7. Expressions and operators

SJV constraints use integer-like expressions and Boolean conditions. The current parser recognizes the following operator groups:

Prefer == for equality in examples. The SJS verifier treats = as equality too; it is not an imperative assignment statement.

A block is the clearest way to state conjunction. Implication can be used for conditional constraints:

function stop {
    reason == 1 => {
        running' == 0;
        mode' == 0;
    }
}

In the parser, precedence from low to high is =>, =, ||, &&, equality, ordered comparison, + -, then * / %. Operators of equal binary precedence are grouped left-to-right by the parser. Parentheses should be used to make intended grouping explicit.

The SJS/SOBJ SMT translation currently supports a narrower arithmetic subset than the parser: integer literals, bound simple names, unary minus, addition, subtraction, equality/inequality, ordered comparisons, conjunction, disjunction, and implication. Other parsed operations may produce an unsupported-verification result. Consult the SystemVerilog reference for that backend’s support boundaries.

8. Binding to Sekura JS

For SJS, the module reference selects an .sjs source file. The verifier uses source declarations to resolve function names, parameters, and supported module-level values, then checks the SJV model against the supplied .sobj implementation artifact.

Typical inputs are:

motor.sjs   implementation source and symbol/type context
motor.sjv   state and function contract
motor.sobj  compiled MR8 implementation checked by the verifier

Example:

module counter.sjs;

{
    count <= 1000;
}

function add {
    value <= 10;
    count' == count + value;
}

The exact proof also depends on the compiler-produced SOBJ, source-to-machine mapping, target semantics, any explicit execution environment, and the verifier’s supported instruction and control-flow model. SJV alone cannot guarantee correctness outside that proof scope.

The current SJS SJV binder accepts only supported simple value atoms in expressions; do not assume that arbitrary compound names, pointer expressions, array accesses, or structure member paths are supported merely because the SJS language has those features.

9. Binding to SystemVerilog

An SJV module declaration ending in .sv selects the SystemVerilog verification frontend:

module top_level_cpu.sv;

{
    ready == 0;
}

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

The frontend binds names to the selected, elaborated module and supports a defined subset of SystemVerilog constructs. Its exact source grammar, elaboration rules, and verification limits are documented in the separate SystemVerilog reference. Do not assume that an SJV construct supported for SJS/SOBJ is implemented identically by the SystemVerilog backend, or vice versa.

10. SystemVerilog proof dependencies

The current parser also accepts dependency declarations of this form:

depends instance_path: "child.sjv" {
    child_function;
}

The path must name an .sjv file, the block must select at least one unique child function contract, and the named instance and child contract must resolve in the SystemVerilog design. The current CLI restricts SJV proof dependencies to a SystemVerilog parent module; SJS/SOBJ proof dependencies are not supported through this declaration.

Dependency proof composition is toolchain behavior. The SJP reference describes how dependency identities are recorded in proof artifacts.

11. What a verification result means

For SJS/SOBJ, the verifier checks supported contracts against symbolic execution of the compiled MR8 implementation and checks the declared valid-state condition at the transition boundary. The implementation may be reported as failed, unsupported, or inconclusive when a counterexample is found, required semantics are outside the supported model, or the solver cannot complete.

For SystemVerilog, the separate RTL verification backend applies its own supported-subset and result rules. A result is limited to the exact source, parameters/configuration, contract, backend semantics, and assumptions used in that run.

A successful result does not prove properties absent from the SJV model, unsupported language behavior, liveness, or correctness under environments outside the recorded verification scope. Passing tests and a formal verification result are different claims.

12. SJV and SJP

An .sjv file is specification input. It is not a self-contained proof and does not itself establish that the implementation satisfies the contract. A verification run can create an .sjp proof artifact containing proof results and recorded inputs/obligations. SJP structure, signatures, replay, and compatibility are specified separately.

implementation source + SJV contract + implementation artifact
                           |
                           v
                    verification run
                           |
                           v
                          SJP

13. Informative structure outline

This outline summarizes the parser’s top-level structure; it is not a complete normative grammar:

specification
    := module_decl (state_block | function_contract | dependency_decl)*

module_decl
    := "module" (identifier_path | quoted_path) ";"

state_block
    := "{" constraint* "}"

function_contract
    := "function" identifier "{" constraint* "}"

dependency_decl
    := "depends" instance_path ":" quoted_sjv_path "{" identifier+ "}"

constraint
    := expression [";"]
     | expression "=>" expression
     | expression "=>" state_block

The parser consumes semicolons as separators inside blocks; the optional notation above reflects that the parser does not require a trailing semicolon after the final expression in a block. For portable examples, include a semicolon after every constraint.

14. Areas not specified by this reference

The following are not fully specified as stable, backend-independent SJV rules:

1. a complete normative grammar and lexical specification;
2. backend-independent type width, signedness, and conversion rules;
3. support for every parser-accepted operator in every backend;
4. support for compound SJS names, structures, arrays, and pointer expressions;
5. the complete treatment of function return values across backends;
6. assumptions and execution-environment defaults for every verification command;
7. full satisfiability and contradiction analysis of state blocks and preconditions;
8. behavior for overlapping implications and multiple contracts for one function;
9. SJS/SOBJ dependency-contract composition;
10. compatibility guarantees between SJV syntax versions and verifier releases.

When relying on an operation or expression, confirm that the selected backend supports it. Parser acceptance alone is not evidence that the operation has been verified.