Formal methods do not verify the continuous analog RF circuitry of a transceiver. They do apply at its digital control interface. This narrow use case suits five-person RF design teams: the digital layer has bounded state, and useful checks need little infrastructure. Full-chip formal verification still demands resources small teams may lack, but the interface around an analog RF block can be checked effectively.
This post explains why that layer fits formal methods, which assertion patterns Skycore creates for SPI and I2C register maps, and where the method stops being practical.
Why the Control Interface Differs
An RF block's analog core, the transistor-level circuit handling RF signals, uses mixed-signal simulation: Spectre or ADE with a SPICE-level netlist and process, voltage, and temperature corners. Formal methods do not fit this continuous, non-enumerable state space.
The digital control interface has a bounded structure. An SPI-programmable RF block commonly contains a state machine decoding serial frames into register writes, a fixed register file, and combinational logic feeding analog configuration inputs. Its SPI decoder has roughly tens to hundreds of reachable states, while addresses are fixed and read-back is combinational. Formal tools can exhaustively check this layer in minutes.
Formal targets bugs simulation commonly misses. Simulation samples selected transaction sequences; formal explores every reachable sequence. An SPI decoder state reached only through an unusual frame length or unexpected CS deassertion timing may escape simulation, but formal exposes it.
SPI Decoder Properties
For an SPI register map, Skycore creates three formal-property groups: decoder protocol checks, register-file address decoding, and constraints on individual fields.
Protocol checks define SPI decoder behavior: a transaction ends exactly when CS deasserts, MISO remains stable during the sampling window, the state machine returns to idle after completion, and an interrupted transaction cannot affect the next transaction. These properties derive from the SPI specification and are checked formally against decoder RTL:
// Property: decoder must return to IDLE after CS deassertion
property spi_return_to_idle;
@(posedge sclk)
$rose(cs_n) |-> ##1 (spi_state == SPI_IDLE);
endproperty
assert property (spi_return_to_idle)
else $error("SPI decoder did not return to IDLE after CS deassertion");
// Property: no register write occurs if frame is incomplete (< 16 bits)
property no_write_on_short_frame;
@(posedge sclk)
(cs_n == 1'b0 && bit_count < 16 && $rose(cs_n))
|-> !reg_write_en;
endproperty
assert property (no_write_on_short_frame)
else $error("Register write enabled on incomplete SPI frame");Address checks ensure every register-map address selects exactly one register, no address selects multiple registers, and reserved-address writes are ignored rather than aliased. RTL aliasing is uncommon yet hard to catch in simulation because it appears only at particular addresses a directed test may omit.
I2C Register-Map Properties
I2C-programmable blocks add different concerns. Repeated starts, clock stretching, and NACK responses create states absent from SPI. Skycore generates properties for the I2C behavior required by the digital control interface:
// Property: register write only commits on ACK, not NACK
property i2c_write_on_ack_only;
@(posedge clk)
(i2c_byte_done && !i2c_ack) |-> !reg_write_en;
endproperty
assert property (i2c_write_on_ack_only)
else $error("Register write committed on NACK byte");
// Property: repeated start resets address phase without corrupting prior data
property repeated_start_resets_address;
@(posedge clk)
i2c_repeated_start |-> ##1 (i2c_state == I2C_ADDR_PHASE);
endproperty
assert property (repeated_start_resets_address)
else $error("Repeated start did not reset address phase");When supported, clock stretching requires checks that the master waits for SCL release before sampling the next bit and that stretch time stays within the block's maximum hold specification. Without RTL support, a useful negative constraint asserts that the slave never holds SCL low.
Field-Level Constraints
Formal also checks field rules: read-only fields reject writes, range-limited fields do not accept out-of-range values when hardware checks range, and write-once fields remain unchanged after their first write.
Skycore derives these checks from your register-map description. A read-only field produces a property that no write changes its stored value. A maximum valid value produces a property requiring values above it to be rejected or clamped to the maximum, as specified for the block.
Directed simulation often checks read-only protection and write-once behavior with a test case: write a value, read it back, and check the result. Formal verification checks every possible input sequence, including a write at an unusual point in initialization or after a reset that the test infrastructure did not exercise.
Practical Limits of Formal Here
Formal verification helps with the interface properties above, not the complete block. It cannot show that written register values create the intended analog behavior. That digital-to-analog relationship requires mixed-signal simulation, not formal methods.
Large FIFOs or memories also limit scalability. A 256-deep FIFO in the control path gives many formal states, and most tools struggle with liveness proofs without manual abstraction. In such cases Skycore generates simulation-based testbench code instead, and flags the FIFO in its report for separate treatment.
Formal tool access is another concern. JasperGold or VC Formal requires a license. For teams lacking formal licenses, Skycore's generated SVA properties still work as simulation assertions. They catch the same bug classes when relevant transaction sequences run, though without exhaustive coverage. The assertions work in both contexts without modification.
Setting Up an SPI Formal Run
For a first formal run on an RF control interface, provide the SPI decoder and register-file RTL, Skycore's generated SVA property file, and a constraints file identifying primary inputs, SCLK, MOSI, and CS, versus internal state. Skycore creates a starter constraints file from the block port list.
A minimal JasperGold TCL setup is:
# Load design and properties
analyze -sv rtl/spi_reg_ctrl.sv
analyze -sv rtl/skycore_gen/spi_reg_ctrl_props.sv
elaborate -top spi_reg_ctrl
# Apply constraints from generated file
source rtl/skycore_gen/spi_reg_ctrl_constraints.tcl
# Run proof on all assertions
prove -allA first run on a small SPI register file typically finishes in under ten minutes. Results mark properties proved, falsified, or bounded. Falsified checks include counterexample traces for a waveform viewer, where they can be stepped through like simulation. SPI protocol traces are nearly always short, usually fewer than twenty clock cycles, making RTL debugging straightforward.
When to Add Formal Checks
Formal setup is worthwhile for an RF block with a non-trivial SPI or I2C decoder: more than three registers, read-modify-write operations, or state-dependent access. It helps most when the interface changed across multiple tape-outs and conditional logic accumulated in the decoder RTL.
A simple two-register, write-only interface gains less from formal setup. Skycore's simulation-based assertions are usually enough for that behavior.
A practical split is to exhaustively check SPI/I2C decoder properties with formal once, then use simulation for regression as the register map changes. Regenerate Skycore properties after each revision and rerun formal on changed sections. The constraints file and TCL setup remain unchanged, so later formal runs cost less than initial setup.