# JasperGold Formal Verification

> Executed via `jg_run` (or `python3 jg_run`) in the project root folder.

UVE provides a dedicated entry point for JasperGold formal verification, separate from the simulation flow.

## Environment Setup

### -env_setup

Print the environment variable setup commands for JasperGold. Source the output to configure your shell.

### -env_unset

Print the commands to unset JasperGold environment variables.

## Project Configuration

### -json

Specify the project JSON config file. Default: `jg.json`.

### -name

Specify the verification task name (e.g., `my_module_fpv`).

### -top

Specify the DUT top module name.

### -lib

Specify the design library name. Default: `work`.

### -gen_jg_proj

Generate a template JSON config file with the given name.

## Design Files

### -fl

Specify the design filelist (`.f` file).

### -sva_fl

Specify the SVA / property filelist.

### -inc

Specify include directories (space-separated, repeatable).

## Formal Apps

Multiple apps can be combined in a single run.

| Option | Description |
|--------|-------------|
| `-fpv` | Formal Property Verification (default) |
| `-conn` | Connectivity Check |
| `-csr` | CSR Check |
| `-xprop` | X-propagation Check |
| `-lpv` | Low Power Verification |
| `-cdc` | Clock Domain Crossing Verification |
| `-sec` | Sequential Equivalence Checking |
| `-superlint` | Superlint (formal lint + overflow checks) |
| `-cov_app` | Coverage App (formal coverage measurement) |
| `-spv` | Security Path Verification |

## Environment Constraints

### -clock

Specify the primary clock signal.

### -reset

Specify the reset signal. Use `~` prefix for active-low (e.g., `-reset=~rst_n`).

### -assume

Specify assumption expressions. Can be repeated for multiple assumptions.

## Proof Options

### -gui

Open JasperGold in interactive GUI mode.

### -dry_run

Print the generated commands without executing.

### -regen_tcl

Force regeneration of the TCL script even if one already exists under `verif/`.

### -check

Run the result checker automatically after each formal app completes.

### -check_only

Skip the JasperGold run and only check results from a previous run. Requires `-name` and the relevant app flag(s).

### -max_jobs

Maximum number of parallel proof jobs. Default: `50`.

### -bbox_mul

Blackbox multipliers wider than N bits. Default: `0` (disabled).

### -cov

Enable coverage collection during the formal run.

## Run Directory

### -run_dir

Specify where run directories are created. Default: `work/formal` if a `work/` folder exists, otherwise `jasper_run`.

## Formal Regression

### -fl_formal

Run all formal tests listed in a formal testlist file.

Example: `-fl_formal=verif/formal/adder/formal_adder`

### -suite

Restrict the regression to only the named SUITE within the testlist.

### -gen_formal_testlist

Generate a formal testlist template for the given module name.