Chapter 7: skalp Integration

What This Chapter Teaches

Up to this point, you have used skalp as a VHDL compiler and simulator – a drop-in replacement for ModelSim or GHDL. But skalp is more than a build tool. It adds capabilities on top of standard VHDL: safety pragmas for redundancy, CDC annotations that catch metastability at compile time, tracing directives for debug visibility, and a formal verification engine that proves properties for all possible input sequences.

None of these features require non-standard VHDL. They are comment-based pragmas – ignored by any other tool – and skalp-specific commands that operate on your unchanged source.

By the end of this chapter you will understand:

• How the -- skalp: comment pragma system works
• How to annotate signals for triple modular redundancy, ECC, CDC synchronization, and debug tracing
• How to add formal verification assertions that skalp can prove exhaustively
• How to mix skalp-native .sk files with .vhd files in the same project
• How to instantiate VHDL entities from skalp code and vice versa
• How the UART design demonstrates these features in a realistic, non-trivial context

The reference design for this chapter is a full UART transmitter and receiver with baud rate generation, oversampled reception, and handshake signaling.

The UART Design

Before diving into skalp-specific features, let us look at the design we will annotate. Create src/uart.vhd:

library ieee;
use ieee.std_logic_1164.all;
use ieee.numeric_std.all;
use ieee.math_real.all;

entity uart is
    generic (
        baud                : positive := 9600;
        clock_frequency     : positive := 153600
    );
    port (
        clock               :   in  std_logic;
        reset               :   in  std_logic;
        data_stream_in      :   in  std_logic_vector(7 downto 0);
        data_stream_in_stb  :   in  std_logic;
        data_stream_in_ack  :   out std_logic;
        data_stream_out     :   out std_logic_vector(7 downto 0);
        data_stream_out_stb :   out std_logic;
        tx                  :   out std_logic;
        rx                  :   in  std_logic
    );
end uart;

This entity declares two generic parameters and a port list that implements a streaming data interface in both directions. Let us walk through the key architectural features.

Generic Parameters

The baud and clock_frequency generics default to values that give clean integer division (153600 / 9600 = 16), but the instantiating design can override them. The type positive restricts both to values greater than zero – a VHDL type constraint that skalp enforces at elaboration time.

Compile-Time Math with math_real

Inside the architecture, the UART computes counter widths from the generic parameters:

constant c_tx_div       : integer := clock_frequency / baud;
constant c_tx_div_width : integer := integer(log2(real(c_tx_div))) + 1;
constant c_rx_div       : integer := clock_frequency / (baud * 16);
constant c_rx_div_width : integer := integer(log2(real(c_rx_div))) + 1;

The chain integer(log2(real(c_tx_div))) + 1 converts the integer divisor to a real, takes the base-2 log from ieee.math_real, truncates back to integer, and adds one – giving the minimum number of bits needed to represent the divisor. This is a standard VHDL idiom for computing signal widths from parameters. skalp evaluates these expressions at compile time; they produce constants, not hardware.

Enumerated State Types

The UART uses two FSMs with named state types:

type uart_tx_states is (
    tx_send_start_bit, tx_send_data, tx_send_stop_bit
);
type uart_rx_states is (
    rx_get_start_bit, rx_get_data, rx_get_stop_bit
);

Each value is a named constant, not a magic number. skalp automatically chooses an efficient binary encoding during synthesis. In simulation, the state names appear in waveforms and debug output, making FSM behavior easy to trace.

Oversampled Receiver

The receiver samples the rx line at 16 times the baud rate. A two-stage synchronizer captures the asynchronous input:

signal uart_rx_data_sr : std_logic_vector(1 downto 0) := (others => '1');

This shift register crosses the clock domain boundary – the rx pin is asynchronous with respect to clock. The first flip-flop may go metastable; the second settles it. A digital filter then counts consecutive identical samples to reject glitches before the FSM acts on the data.

Handshake Protocol

The TX path uses a strobe/acknowledge handshake: the upstream logic asserts data_stream_in_stb with valid data, the UART asserts data_stream_in_ack when it accepts the byte, and the upstream deasserts the strobe in response. The FSM only transitions from idle to sending when it sees the strobe.

Named Processes

The architecture contains multiple named processes: oversample_clock_divider (16x baud tick), rxd_synchronise (two-stage synchronizer), rxd_filter (digital low-pass), uart_receive_data (RX FSM), and uart_send_data (TX FSM and baud generator). Named processes appear in skalp’s diagnostic output, making it easy to locate issues.

Complete Architecture

Add the following architecture after the entity in src/uart.vhd:

architecture rtl of uart is
    constant c_tx_div       : integer := clock_frequency / baud;
    constant c_tx_div_width : integer := integer(log2(real(c_tx_div))) + 1;
    constant c_rx_div       : integer := clock_frequency / (baud * 16);
    constant c_rx_div_width : integer := integer(log2(real(c_rx_div))) + 1;

    type uart_tx_states is (
        tx_send_start_bit, tx_send_data, tx_send_stop_bit
    );
    type uart_rx_states is (
        rx_get_start_bit, rx_get_data, rx_get_stop_bit
    );

    signal uart_tx_state   : uart_tx_states := tx_send_start_bit;
    signal uart_tx_data    : std_logic_vector(7 downto 0);
    signal uart_tx_count   : unsigned(c_tx_div_width-1 downto 0);
    signal uart_tx_bit     : unsigned(2 downto 0);

    signal uart_rx_data_sr : std_logic_vector(1 downto 0) := (others => '1');
    signal uart_rx_filter  : unsigned(1 downto 0);
    signal uart_rx_bit     : std_logic := '1';

    signal uart_rx_state   : uart_rx_states := rx_get_start_bit;
    signal uart_rx_data    : std_logic_vector(7 downto 0);
    signal uart_rx_count   : unsigned(3 downto 0);
    signal uart_rx_bit_cnt : unsigned(2 downto 0);

    signal uart_rx_clk_count : unsigned(c_rx_div_width-1 downto 0);
    signal uart_rx_clk_tick  : std_logic;
begin

    -- Oversample clock divider (16x baud rate tick)
    oversample_clock_divider : process(clock)
    begin
        if rising_edge(clock) then
            if reset = '1' then
                uart_rx_clk_count <= (others => '0');
                uart_rx_clk_tick  <= '0';
            else
                if to_integer(uart_rx_clk_count) = c_rx_div - 1 then
                    uart_rx_clk_count <= (others => '0');
                    uart_rx_clk_tick  <= '1';
                else
                    uart_rx_clk_count <= uart_rx_clk_count + 1;
                    uart_rx_clk_tick  <= '0';
                end if;
            end if;
        end if;
    end process oversample_clock_divider;

    -- Two-stage synchronizer for async RX input
    rxd_synchronise : process(clock)
    begin
        if rising_edge(clock) then
            if reset = '1' then
                uart_rx_data_sr <= (others => '1');
            else
                uart_rx_data_sr(0) <= rx;
                uart_rx_data_sr(1) <= uart_rx_data_sr(0);
            end if;
        end if;
    end process rxd_synchronise;

    -- Digital filter on synchronized RX
    rxd_filter : process(clock)
    begin
        if rising_edge(clock) then
            if reset = '1' then
                uart_rx_filter <= (others => '0');
                uart_rx_bit    <= '1';
            elsif uart_rx_clk_tick = '1' then
                if uart_rx_data_sr(1) = '1' and uart_rx_filter < 3 then
                    uart_rx_filter <= uart_rx_filter + 1;
                elsif uart_rx_data_sr(1) = '0' and uart_rx_filter > 0 then
                    uart_rx_filter <= uart_rx_filter - 1;
                end if;
                if uart_rx_filter = 3 then
                    uart_rx_bit <= '1';
                elsif uart_rx_filter = 0 then
                    uart_rx_bit <= '0';
                end if;
            end if;
        end if;
    end process rxd_filter;

    -- RX FSM
    uart_receive_data : process(clock)
    begin
        if rising_edge(clock) then
            if reset = '1' then
                uart_rx_state       <= rx_get_start_bit;
                uart_rx_data        <= (others => '0');
                uart_rx_count       <= (others => '0');
                uart_rx_bit_cnt     <= (others => '0');
                data_stream_out     <= (others => '0');
                data_stream_out_stb <= '0';
            elsif uart_rx_clk_tick = '1' then
                case uart_rx_state is
                    when rx_get_start_bit =>
                        if uart_rx_bit = '0' then
                            if uart_rx_count = 7 then
                                uart_rx_count   <= (others => '0');
                                uart_rx_bit_cnt <= (others => '0');
                                uart_rx_state   <= rx_get_data;
                            else
                                uart_rx_count <= uart_rx_count + 1;
                            end if;
                        else
                            uart_rx_count <= (others => '0');
                        end if;
                    when rx_get_data =>
                        if uart_rx_count = 15 then
                            uart_rx_count <= (others => '0');
                            uart_rx_data(to_integer(uart_rx_bit_cnt)) <= uart_rx_bit;
                            if uart_rx_bit_cnt = 7 then
                                uart_rx_state <= rx_get_stop_bit;
                            else
                                uart_rx_bit_cnt <= uart_rx_bit_cnt + 1;
                            end if;
                        else
                            uart_rx_count <= uart_rx_count + 1;
                        end if;
                    when rx_get_stop_bit =>
                        if uart_rx_count = 15 then
                            uart_rx_state       <= rx_get_start_bit;
                            uart_rx_count       <= (others => '0');
                            data_stream_out     <= uart_rx_data;
                            data_stream_out_stb <= '1';
                        else
                            uart_rx_count <= uart_rx_count + 1;
                        end if;
                end case;
            end if;
        end if;
    end process uart_receive_data;

    -- TX FSM with baud rate generator
    uart_send_data : process(clock)
    begin
        if rising_edge(clock) then
            if reset = '1' then
                uart_tx_state      <= tx_send_start_bit;
                data_stream_in_ack <= '0';
                tx                 <= '1';
                uart_tx_count      <= (others => '0');
                uart_tx_bit        <= (others => '0');
            else
                data_stream_in_ack <= '0';
                case uart_tx_state is
                    when tx_send_start_bit =>
                        if data_stream_in_stb = '1' and uart_tx_count = 0 then
                            uart_tx_data       <= data_stream_in;
                            data_stream_in_ack <= '1';
                            tx                 <= '0';
                            uart_tx_count      <= uart_tx_count + 1;
                        elsif uart_tx_count /= 0 then
                            tx <= '0';
                            if uart_tx_count = c_tx_div - 1 then
                                uart_tx_count <= (others => '0');
                                uart_tx_bit   <= (others => '0');
                                uart_tx_state <= tx_send_data;
                            else
                                uart_tx_count <= uart_tx_count + 1;
                            end if;
                        else
                            tx <= '1';
                        end if;
                    when tx_send_data =>
                        tx <= uart_tx_data(to_integer(uart_tx_bit));
                        if uart_tx_count = c_tx_div - 1 then
                            uart_tx_count <= (others => '0');
                            if uart_tx_bit = 7 then
                                uart_tx_state <= tx_send_stop_bit;
                            else
                                uart_tx_bit <= uart_tx_bit + 1;
                            end if;
                        else
                            uart_tx_count <= uart_tx_count + 1;
                        end if;
                    when tx_send_stop_bit =>
                        tx <= '1';
                        if uart_tx_count = c_tx_div - 1 then
                            uart_tx_count <= (others => '0');
                            uart_tx_state <= tx_send_start_bit;
                        else
                            uart_tx_count <= uart_tx_count + 1;
                        end if;
                end case;
            end if;
        end if;
    end process uart_send_data;

end architecture rtl;

The architecture uses no concurrent signal assignments for output ports – all outputs (tx, data_stream_in_ack, data_stream_out, data_stream_out_stb) are driven directly from their respective processes. This avoids pipeline delays that concurrent assignments can introduce in simulation.

The tx_send_start_bit state doubles as the idle state: when uart_tx_count = 0 and no strobe is present, the TX line idles high. When the strobe arrives, the FSM accepts the byte, starts the start bit, and begins counting. When uart_tx_count is non-zero, the start bit is in progress.

With the default generics (clock_frequency = 153600, baud = 9600), c_tx_div = 16 and c_rx_div = 1. One TX bit takes 16 system clocks (start + 8 data + stop = 160 total). The RX oversample tick fires every system clock, so 16 ticks = 1 bit period.

skalp Pragmas

skalp pragmas are VHDL comments that begin with -- skalp:. Any standard VHDL tool ignores them – they are just comments. skalp recognizes them and acts on them during compilation, simulation, or formal analysis.

The general syntax is:

signal my_signal : std_logic; -- skalp:pragma_name
signal my_signal : std_logic; -- skalp:pragma_name(argument)

Pragmas can appear on signal declarations, process labels, or standalone comment lines. They are always on the same line as the construct they annotate, or on the line immediately preceding it.

-- skalp:trace – Debug Visibility

The trace pragma marks a signal for inclusion in debug output. When you export waveforms with tb.export_waveform() in a Rust test, traced signals are always included even if the simulator would otherwise optimize them away. When you synthesize for an FPGA with skalp build --target, traced signals are connected to the on-chip logic analyzer.

Apply it to the UART state machines:

signal uart_tx_state : uart_tx_states := tx_send_start_bit; -- skalp:trace
signal uart_rx_state : uart_rx_states := rx_get_start_bit;  -- skalp:trace

Now tb.export_waveform() will always include uart_tx_state and uart_rx_state in the waveform file, and skalp build --target ice40 will route these signals to the debug fabric.

You can trace any signal — not just state machines. For high-fanout buses or deeply nested signals that are hard to find in a full waveform dump, -- skalp:trace is the simplest way to guarantee visibility.

-- skalp:cdc(sync) – Clock Domain Crossing

The cdc pragma tells skalp that a signal crosses a clock domain boundary. The argument specifies the synchronization strategy:

signal uart_rx_data_sr : std_logic_vector(1 downto 0) := (others => '1'); -- skalp:cdc(sync)

The sync argument means “this signal is synchronized by a multi-stage register chain.” skalp verifies that the annotated signal feeds through at least two flip-flops before reaching combinational logic. If you accidentally read the first-stage output directly, skalp reports an error.

Other CDC annotations:

CDC bugs manifest as intermittent failures that depend on exact timing. By annotating crossing points, you give skalp enough information to check synchronization at compile time.

-- skalp:safety(tmr) – Triple Modular Redundancy

The safety pragma with the tmr argument tells skalp to triplicate a signal and add majority voting logic:

signal uart_tx_state : uart_tx_states := tx_send_start_bit; -- skalp:safety(tmr)

skalp creates three independent copies of uart_tx_state and a voter that selects the majority value. If a single-event upset (radiation hit) corrupts one copy, the other two outvote it. TMR is essential for space, aviation, and automotive applications. skalp handles the replication and voting automatically – you do not need to manually triplicate your logic.

You can combine pragmas:

signal uart_tx_state : uart_tx_states := tx_send_start_bit; -- skalp:safety(tmr) skalp:trace

-- skalp:safety(ecc) – Error Correction Coding

For data registers where full triplication is too expensive, ECC provides single-error correction and double-error detection with lower overhead:

signal tx_data : std_logic_vector(7 downto 0); -- skalp:safety(ecc)

skalp adds parity bits to the stored value and inserts correction logic on every read. A single bit flip is corrected silently; a double bit flip is detected and flagged. The overhead is proportional to log2(width) additional bits, not 3x the full signal width.

-- skalp:breakpoint – Simulation Breakpoints

The breakpoint pragma halts the simulator when a condition is reached:

-- skalp:breakpoint
assert uart_tx_state /= tx_send_start_bit or data_stream_in_stb = '0'
    report "TX started unexpectedly" severity note;

During simulation (via cargo test), when the assertion condition fails, the simulator pauses and drops into the skalp debugger (or halts if non-interactive). You can inspect signal values, step forward, or resume.

Summary of Pragmas

Formal Verification

Simulation tests your design against specific input sequences. Formal verification proves properties for all possible input sequences. If a formal property holds, it holds for every reachable state of the design – no corner case can slip through.

skalp converts VHDL assertions annotated with -- skalp:formal into formal properties and feeds them to its built-in model checker. You do not need to learn PSL or SVA – standard VHDL assert statements are sufficient.

Adding Formal Properties to the UART

The TX path should never accept a strobe while it is busy transmitting. Express this as an assertion:

-- skalp:formal
assert not (data_stream_in_stb = '1' and data_stream_in_ack = '0'
            and uart_tx_state /= tx_send_start_bit)
    report "Data strobe asserted while TX is busy" severity failure;

If the upstream logic violates the handshake protocol by asserting the strobe while the UART is busy, this property will fail.

Another useful property – the TX line should always be high when idle:

-- skalp:formal
assert uart_tx_state /= tx_send_start_bit or tx = '1'
    report "TX line not idle-high when FSM is idle" severity failure;

And a liveness property – the TX FSM should always eventually return to idle:

-- skalp:formal
-- skalp:formal_type(liveness)
assert uart_tx_state = tx_send_start_bit
    report "TX FSM stuck in non-idle state" severity failure;

The liveness annotation tells skalp this is not a safety property (which must hold at every cycle) but a liveness property (which must hold eventually). skalp uses different proof strategies for each.

Running Formal Verification

skalp verify --entity uart

Output:

   Verifying uart
   [1/3] TX handshake safety .............. PROVED (depth 24)
   [2/3] TX idle-high .................... PROVED (depth 16)
   [3/3] TX FSM liveness ................. PROVED (depth 48)
   All 3 properties verified.

The depth indicates how many clock cycles the model checker explored. The result is exhaustive – not a bounded check.

When Formal Finds a Bug

If a property fails, skalp generates a counterexample:

   [1/3] TX handshake safety .............. FAILED
   Counterexample (12 cycles):
     cycle  0: reset=1
     cycle  1: reset=0
     cycle  2: data_stream_in_stb=1, data_stream_in=0x41
     cycle  3: data_stream_in_ack=1
     cycle  4: data_stream_in_stb=1, data_stream_in=0x42  <-- VIOLATION
   Property violated: Data strobe asserted while TX is busy

You can replay the counterexample with skalp sim --replay to see the full waveform.

Formal vs Simulation

Use both. Simulation tests that the design does what you want. Formal verification proves that it never does what you forbid.

Annotating the Full UART

Here is the UART’s signal declaration section with skalp pragmas applied:

    -- TX signals
    signal uart_tx_state   : uart_tx_states := tx_send_start_bit; -- skalp:trace skalp:safety(tmr)
    signal uart_tx_data    : std_logic_vector(7 downto 0);        -- skalp:safety(ecc)
    signal uart_tx_count   : unsigned(c_tx_div_width-1 downto 0);
    signal uart_tx_bit     : unsigned(2 downto 0);

    -- RX synchronizer and filter
    signal uart_rx_data_sr : std_logic_vector(1 downto 0) := (others => '1'); -- skalp:cdc(sync)
    signal uart_rx_filter  : unsigned(1 downto 0);
    signal uart_rx_bit     : std_logic := '1';

    -- RX state
    signal uart_rx_state   : uart_rx_states := rx_get_start_bit;  -- skalp:trace skalp:safety(tmr)
    signal uart_rx_data    : std_logic_vector(7 downto 0);
    signal uart_rx_count   : unsigned(c_rx_div_width-1 downto 0);
    signal uart_rx_bit_cnt : unsigned(2 downto 0);

The choices are deliberate: state registers get TMR and trace (a bit flip in the FSM state is catastrophic, and you always want state visibility in debug). TX data gets ECC (triplicating 8 bits costs 16 extra flip-flops; ECC costs only 4 parity bits). The RX synchronizer gets CDC (skalp verifies the two-stage chain is intact). Counters are left unannotated (a bit flip self-corrects on the next counter reload).

Mixed skalp+VHDL Projects

skalp supports projects that contain both .sk (skalp-native) and .vhd (VHDL) files. This lets you write new logic in skalp while reusing existing VHDL IP, or wrap a VHDL design with a skalp-native top level.

Project Configuration

[package]
name = "mixed-project"
version = "0.1.0"

[build]
top = "SystemTop"
sources = ["src/*.sk", "src/*.vhd"]

The sources array lists glob patterns for both file types. skalp compiles each with the appropriate frontend and links them into a unified design hierarchy.

Instantiating VHDL from skalp

Suppose src/uart.vhd defines the uart entity shown above, and you want to instantiate it from src/top.sk:

entity SystemTop {
    clock      : in  bit,
    reset      : in  bit,
    uart_tx    : out bit,
    uart_rx    : in  bit,
    led        : out bit[8],
}

impl SystemTop {
    let tx_data  : bit[8];
    let tx_stb   : bit;
    let tx_ack   : bit;
    let rx_data  : bit[8];
    let rx_stb   : bit;

    inst my_uart = uart {
        clock           = clock,
        reset           = reset,
        data_stream_in  = tx_data,
        data_stream_in_stb = tx_stb,
        data_stream_in_ack = tx_ack,
        data_stream_out = rx_data,
        data_stream_out_stb = rx_stb,
        tx              = uart_tx,
        rx              = uart_rx,
    } with {
        baud            = 115200,
        clock_frequency = 50_000_000,
    };

    // Echo received data back, display on LEDs
    tx_data = rx_data;
    tx_stb  = rx_stb;
    led     = rx_data;
}

The inst keyword instantiates the VHDL entity by name. skalp resolves entities across language boundaries. Port connections use = (skalp syntax), and generics are passed in the with block.

Instantiating skalp from VHDL

Going the other direction, suppose src/blinker.sk defines a skalp entity:

entity Blinker {
    clk    : in  bit,
    rst    : in  bit,
    led    : out bit,
} with {
    period : nat[32] = 50_000_000,
}

You can instantiate it from VHDL using direct entity instantiation:

architecture rtl of top_board is
begin
    blink_inst : entity work.Blinker
        generic map (
            period => 25_000_000
        )
        port map (
            clk => clock,
            rst => reset,
            led => heartbeat_led
        );
end architecture rtl;

skalp compiles the entity into a VHDL-compatible interface, so the instantiation syntax is standard. The entity name is case-sensitive. Generics map to generic map, ports to port map.

Type Mapping Between Languages

When crossing the language boundary, skalp maps types automatically:

Port directions (in, out, inout) map directly between the two languages.

Coming from skalp?

If you write skalp-native code, the features described in this chapter are already part of the language:

VHDL + pragma	skalp native	Notes
-- skalp:safety(tmr)	@safety(tmr) signal state	First-class annotation, not a comment
-- skalp:cdc(sync)	@cdc(sync) signal rx_sync	Type system tracks clock domains
-- skalp:trace	@trace signal debug_sig	Same effect, different syntax
-- skalp:formal + assert	formal { assert ... }	Dedicated formal block
-- skalp:breakpoint	@breakpoint	Attribute syntax

The key difference: in skalp, CDC safety is enforced by the type system. A signal in clock domain A cannot be read from domain B without a synchronizer – the compiler rejects it. In VHDL, skalp can only check what you annotate. The VHDL pragma approach is opt-in and backward compatible; the skalp-native approach is mandatory and catches more bugs.

Testing the UART

Create tests/uart_test.rs:

use skalp_testing::Testbench;

#[tokio::test]
async fn test_uart_tx() {
    let mut tb = Testbench::new("src/uart.vhd").await.unwrap();

    // Reset — this UART uses "clock" and "reset", not "clk"/"rst",
    // so we drive reset manually and use clock_signal("clock", n)
    tb.set("reset", 1u8)
        .set("data_stream_in", 0u8)
        .set("data_stream_in_stb", 0u8)
        .set("rx", 1u8);
    tb.clock_signal("clock", 4).await;
    tb.set("reset", 0u8);
    tb.clock_signal("clock", 5).await;

    // Send a byte (0x55 = alternating bits, good for baud rate testing)
    tb.set("data_stream_in", 0x55u32)
        .set("data_stream_in_stb", 1u8);

    // Wait for acknowledgment
    for _ in 0..100 {
        tb.clock_signal("clock", 1).await;
        if tb.get_u64("data_stream_in_ack").await == 1 {
            break;
        }
    }
    tb.expect("data_stream_in_ack", 1u32).await;
    tb.set("data_stream_in_stb", 0u8);

    // Wait for transmission to complete
    tb.clock_signal("clock", 200).await;
}

Notice tb.clock_signal("clock", n) instead of the usual tb.clock(n). The convenience method tb.clock(n) assumes the clock port is named clk, but this UART entity names it clock. The clock_signal method lets you specify any clock port name. Similarly, we drive reset manually with tb.set rather than using tb.reset() (which assumes rst).

The test resets, presents a byte with the strobe, polls for acknowledgment (the loop avoids hardcoding cycle counts), deasserts the strobe, and waits for the transmission to complete. With default generics (153600 Hz clock, 9600 baud), one byte takes 16 cycles/bit times 10 bits = 160 cycles.

Testing the RX Path

#[tokio::test]
async fn test_uart_rx() {
    let mut tb = Testbench::new("src/uart.vhd").await.unwrap();

    // Reset with explicit clock/reset port names
    tb.set("reset", 1u8)
        .set("data_stream_in", 0u8)
        .set("data_stream_in_stb", 0u8)
        .set("rx", 1u8);
    tb.clock_signal("clock", 4).await;
    tb.set("reset", 0u8);
    tb.clock_signal("clock", 4).await;

    // Send start bit (low)
    tb.set("rx", 0u8);
    tb.clock_signal("clock", 16).await; // One bit period at 16x oversample

    // Send 0x55 = 01010101, LSB first
    let byte: u8 = 0x55;
    for i in 0..8 {
        let bit = (byte >> i) & 1;
        tb.set("rx", bit);
        tb.clock_signal("clock", 16).await;
    }

    // Send stop bit (high)
    tb.set("rx", 1u8);
    tb.clock_signal("clock", 16).await;

    // Check that the received byte is available
    tb.clock_signal("clock", 10).await; // Allow pipeline to settle
    tb.expect("data_stream_out_stb", 1u32).await;
    tb.expect("data_stream_out", 0x55u32).await;
}

This test manually constructs a UART frame on the rx pin: idle high, start bit (16 oversample clocks), 8 data bits LSB-first (0x55), and a stop bit. It then verifies that data_stream_out_stb is asserted and data_stream_out contains the correct byte.

Combine simulation tests with formal verification: cargo test verifies the UART transmits and receives specific bytes, while skalp verify --entity uart proves the handshake invariants hold for all possible input sequences.

Quick Reference

Exercise: Add -- skalp:trace to the baud rate counters. Export waveforms with tb.export_waveform("build/uart_baud.skw.gz") in a Rust test and verify in the skalp VS Code extension that the TX counter period matches clock_frequency / baud. Then write a formal property asserting the TX line is never low for more than 10 bit periods (hint: you need an auxiliary counter).

Next: VHDL-2019 Features

The pragmas and formal verification in this chapter work with any VHDL standard from VHDL-93 onward. But VHDL has continued to evolve, and the 2019 revision introduces features that most free tools do not support: interfaces, views, and generic type parameters.

In Chapter 8, you will learn:

• How VHDL-2019 interfaces bundle related signals into a single named connection
• How views define which signals are inputs and outputs from each side of an interface
• How generic type parameters let you write truly reusable components
• Why skalp is one of the few free tools that compiles VHDL-2019

Continue to Chapter 8: VHDL-2019 Features.