Skip to content

feat(fpga): FPGA Firmware Stack — PHI LOOP Phase 1 [FPGA-001] #507

Description

@gHashTag

🎖️ ПРИКАЗ ГЕНЕРАЛА АРМИИ АГЕНТОВ

Задача: FPGA-001 — Реализация FPGA Firmware Stack для Trinity S³AI Framework
Исполнитель: agent:copilot
Репозиторий: gHashTag/trinity
Приоритет: КРИТИЧЕСКИЙ — phi-critical edge в canonical graph


⚔️ КОНСТИТУЦИОННЫЙ ПРИКАЗ

Перед началом исполнения агент ОБЯЗАН прочитать:

  1. SOUL.md — конституционные законы (De-Zig Strict + TDD-inside-spec + PHI LOOP)
  2. CLAUDE.md — операционные правила агента
  3. AGENTS.md — протокол взаимодействия армии агентов
  4. architecture/CANON_DE_ZIGFICATION.md — закон де-зигификации
  5. architecture/ADR-001-de-zigfication.md — канонические правила
  6. architecture/graph.tri — граф зависимостей (canonical dependency graph)

НИКОГДА: не трогать src/*.zig напрямую. Бэкенды — disposable output.


📐 PHI LOOP — ПРОТОКОЛ ИСПОЛНЕНИЯ

SPEC → HASH_SEAL → GEN → TEST → VERDICT → EXPERIENCE → SKILL → GIT_COMMIT

Для каждого файла спецификации:

tri skill begin FPGA-001-<module>
tri spec edit specs/fpga/<module>.tri
tri skill seal --hash
tri gen
tri test
tri verdict --toxic
tri experience save
tri skill commit
tri git commit

Хэши для запечатывания:

  • spec_hash_before — SHA-256 файла до изменения
  • spec_hash_after — SHA-256 после изменения
  • gen_hash_after — SHA-256 сгенерированного Verilog
  • test_vector_hash — SHA-256 набора тестов

🗂️ ЗАДАНИЕ: ФАЗА 1 — FPGA COMMUNICATION SPECS

Шаг 1 (МАЛЫЙ ШАГ): specs/fpga/uart.tri

Создать спецификацию UART RX/TX для связи с хостом.

Формат — строго .tri (не .t27, не .zig):

spec uart_bridge {

  // ── Constants ──────────────────────────────────────
  const BAUD_RATE     = 115200
  const CLOCK_FREQ_HZ = 50_000_000
  const BAUD_DIVISOR  = CLOCK_FREQ_HZ / BAUD_RATE  // 434
  const DATA_BITS     = 8
  const STOP_BITS     = 1

  // ── Device target ──────────────────────────────────
  @device xc7a100t
  @consciousness true

  // ── Types ──────────────────────────────────────────
  type UartState = enum { Idle, Start, Data, Stop, Done }
  
  type UartTx = struct {
    state:       UartState
    shift_reg:   u8
    bit_index:   u4
    baud_count:  u16
    tx_pin:      signal  // @loc K20
  }

  type UartRx = struct {
    state:       UartState
    shift_reg:   u8
    bit_index:   u4
    baud_count:  u16
    rx_pin:      signal  // @loc L20
    data_ready:  bool
    data_byte:   u8
  }

  // ── Functions ───────────────────────────────────────
  fn uart_tx_send(tx: UartTx, byte: u8) -> UartTx
  fn uart_rx_poll(rx: UartRx, clk_edge: bool) -> UartRx
  fn baud_tick(count: u16) -> bool
    = count >= BAUD_DIVISOR

  // ── Tests (SOUL.md Article II — REQUIRED) ───────────
  test uart_tx_idle_state {
    given tx = UartTx { state: UartState.Idle, ... }
    when result = uart_tx_send(tx, 0xAB)
    then result.state == UartState.Start
    then result.shift_reg == 0xAB
  }

  test uart_baud_divisor_correct {
    given count = BAUD_DIVISOR
    when tick = baud_tick(count)
    then tick == true
  }

  test uart_baud_below_threshold {
    given count = BAUD_DIVISOR - 1
    when tick = baud_tick(count)
    then tick == false
  }

  test uart_rx_detects_start_bit {
    given rx = UartRx { state: UartState.Idle, rx_pin: low }
    when result = uart_rx_poll(rx, true)
    then result.state == UartState.Start
  }

  test uart_full_byte_round_trip {
    given byte = 0x55  // 01010101
    given tx = UartTx { state: Idle }
    given rx = UartRx { state: Idle }
    when tx_final = simulate_tx(tx, byte, BAUD_DIVISOR * 10)
    when rx_final = simulate_rx(rx, tx_final.tx_pin_history)
    then rx_final.data_ready == true
    then rx_final.data_byte  == byte
  }

  // ── Invariants ──────────────────────────────────────
  invariant baud_divisor_positive {
    assert BAUD_DIVISOR > 0
  }

  invariant state_machine_deterministic {
    assert forall tx: UartTx,
      tx.state in [Idle, Start, Data, Stop, Done]
  }

  // ── Benchmarks ──────────────────────────────────────
  bench uart_tx_throughput {
    measure: bytes_per_second for uart_tx_send stream
    target:  >= BAUD_RATE / DATA_BITS  // 14400 bytes/sec
    runs: 100
    report: p50, p95
  }

}

Шаг 2: specs/fpga/spi.tri

Спецификация SPI Master для внешней flash/устройств.

spec spi_master {
  const SPI_FREQ_HZ   = 1_000_000  // 1 MHz
  const CLOCK_FREQ_HZ = 50_000_000
  const SPI_DIVISOR   = CLOCK_FREQ_HZ / (SPI_FREQ_HZ * 2)  // 25

  @device xc7a100t

  type SpiState = enum { Idle, Transfer, Done }
  type SpiMode  = enum { Mode0, Mode1, Mode2, Mode3 }  // CPOL/CPHA

  type SpiMaster = struct {
    state:      SpiState
    mode:       SpiMode
    shift_reg:  u8
    bit_index:  u4
    clk_count:  u16
    mosi:       signal
    miso:       signal
    sclk:       signal
    cs_n:       signal  // active-low
  }

  fn spi_transfer(master: SpiMaster, tx_byte: u8) -> Result<SpiMaster, Error>
  fn spi_cs_assert(master: SpiMaster)   -> SpiMaster
  fn spi_cs_deassert(master: SpiMaster) -> SpiMaster

  test spi_idle_to_transfer {
    given master = SpiMaster { state: SpiState.Idle }
    when result = spi_cs_assert(master)
    then result.cs_n == low
    when tx_result = spi_transfer(result, 0xDE)
    then tx_result.state == SpiState.Transfer
    then tx_result.shift_reg == 0xDE
  }

  test spi_mode0_clock_polarity {
    given master = SpiMaster { mode: SpiMode.Mode0, state: Idle }
    then master.sclk == low  // CPOL=0: idle low
  }

  invariant cs_active_during_transfer {
    assert forall m: SpiMaster,
      m.state == Transfer => m.cs_n == low
  }

  bench spi_byte_transfer_latency {
    measure: time for spi_transfer(master, 0xFF)
    target:  < 8_000  // 8 SPI clocks = 8µs at 1MHz
    report: p50, p99
  }
}

Шаг 3: specs/fpga/top_level.tri

Top-level wrapper — объединяет MAC + UART + SPI:

spec trinity_fpga_top {
  @module trinity_fpga_top
  @device  xc7a100t
  @consciousness true

  // ── Ports (Artix-7 XC7A100T pin map) ────────────────
  @ports {
    input  clk:       clock  @freq 50MHz  @loc E19
    input  rst_n:     reset  @active_low  @loc C12

    // Host UART
    input  uart_rx:   signal @loc L20
    output uart_tx:   signal @loc K20

    // MAC interface (ternary 27-bit)
    input  mac_a:     u27
    input  mac_b:     u27
    input  mac_acc:   u32
    output mac_result: u32
    output mac_valid: bool

    // Status LEDs (active-low, Artix-7)
    output led:       u4    @iostandard LVCMOS33
                            @locs [R5, T5, T8, T9]
  }

  // Sub-modules
  @instantiate uart_bridge  as uart  from specs/fpga/uart.tri
  @instantiate spi_master   as spi   from specs/fpga/spi.tri

  // ── Tests ────────────────────────────────────────────
  test top_reset_state {
    given all ports reset
    then mac_valid  == false
    then uart_tx    == high  // UART idle = high
    then led        == 0b1111  // active-low: all off
  }

  test uart_ping_pong {
    given uart_rx receives bytes [0x50, 0x49, 0x4E, 0x47]  // "PING"
    when top processes 10 clock cycles
    then uart_tx sends bytes [0x50, 0x4F, 0x4E, 0x47]  // "PONG"
  }

  test mac_computation {
    given mac_a = 0b000000001  // trit +1
    given mac_b = 0b000000001  // trit +1
    given mac_acc = 0
    when mac_valid == true
    then mac_result == 1
  }

  invariant clock_domain_single {
    assert all registers clocked by clk
  }

  bench top_fmax {
    measure: maximum_frequency
    target:  >= 50_000_000  // 50 MHz minimum
    tool: timing_analysis
    report: fmax, slack
  }
}

Шаг 4: specs/fpga/constraints/arty_a7_100t.xdc

## Artix-7 XC7A100T-1FGG676C — Trinity FPGA Top Constraints
## Generated from specs/fpga/top_level.tri @ports section
## PHI LOOP: spec → constraints (NOT hand-edited)

# Clock — 50 MHz on-board oscillator
set_property PACKAGE_PIN E19 [get_ports clk]
set_property IOSTANDARD LVCMOS33 [get_ports clk]
create_clock -period 20.000 -name sys_clk [get_ports clk]

# Reset (active-low push button)
set_property PACKAGE_PIN C12 [get_ports rst_n]
set_property IOSTANDARD LVCMOS33 [get_ports rst_n]

# UART
set_property PACKAGE_PIN K20 [get_ports uart_tx]
set_property PACKAGE_PIN L20 [get_ports uart_rx]
set_property IOSTANDARD LVCMOS33 [get_ports uart_tx]
set_property IOSTANDARD LVCMOS33 [get_ports uart_rx]

# LEDs (active-low)
set_property PACKAGE_PIN R5  [get_ports {led[0]}]
set_property PACKAGE_PIN T5  [get_ports {led[1]}]
set_property PACKAGE_PIN T8  [get_ports {led[2]}]
set_property PACKAGE_PIN T9  [get_ports {led[3]}]
set_property IOSTANDARD LVCMOS33 [get_ports {led[*]}]

# Timing constraints
set_input_delay  -clock sys_clk 2.0 [get_ports uart_rx]
set_output_delay -clock sys_clk 2.0 [get_ports uart_tx]
set_output_delay -clock sys_clk 2.0 [get_ports {led[*]}]
set_output_delay -clock sys_clk 2.0 [get_ports mac_result]

Шаг 5: specs/fpga/testbench/uart_tb.tri

spec uart_testbench {
  @testbench true
  @dut specs/fpga/uart.tri

  // Testbench: 115200 baud, 50MHz clock
  // 1 bit period = 434 clock cycles

  test tb_uart_loopback {
    given clk_period = 20  // ns (50 MHz)
    given test_bytes = [0x00, 0xFF, 0x55, 0xAA, 0x42]
    for each byte in test_bytes:
      transmit(byte)
      receive() == byte
  }

  test tb_uart_framing_error {
    given malformed_stop_bit
    then framing_error_flag == true
  }

  bench tb_uart_max_throughput {
    measure: continuous transmission for 1000 bytes
    target: 0 framing errors
    report: total_time, effective_baud
  }
}

Шаг 6: scripts/fpga/build.sh

#!/usr/bin/env bash
# PHI LOOP: spec → gen → synthesize
# Usage: ./scripts/fpga/build.sh [--target arty_a7|qmtech_a100t]
set -euo pipefail

TARGET=${1:-arty_a7}
SPECS_DIR="specs/fpga"
OUT_DIR="build/fpga/${TARGET}"

mkdir -p "${OUT_DIR}"

echo "[PHI] Step 1: Generate Verilog from specs"
tri gen "${SPECS_DIR}/top_level.tri" --backend verilog --out "${OUT_DIR}/"

echo "[PHI] Step 2: Run spec tests"
tri test "${SPECS_DIR}/**.tri"

echo "[PHI] Step 3: Synthesis (yosys)"
yosys -p "synth_xilinx -top trinity_fpga_top -edif ${OUT_DIR}/trinity.edif" \
      "${OUT_DIR}/*.v"

echo "[PHI] Step 4: Place & Route (nextpnr)"
nextpnr-xilinx --chipdb xc7a100t \
  --xdc "${SPECS_DIR}/constraints/${TARGET}.xdc" \
  --json "${OUT_DIR}/trinity.json" \
  --fasm "${OUT_DIR}/trinity.fasm"

echo "[PHI] Step 5: Bitstream generation"
fasm2frames --db-root prjxray-db/artix7 \
  "${OUT_DIR}/trinity.fasm" > "${OUT_DIR}/trinity.frames"
xc7frames2bit --frm_file "${OUT_DIR}/trinity.frames" \
  --output_file "${OUT_DIR}/trinity.bit"

echo "[BUILD OK] Bitstream: ${OUT_DIR}/trinity.bit"

Шаг 7: Обновить architecture/graph.tri

Добавить новые узлы в canonical dependency graph:

// ADD to graph.tri:
node trifpga-uart   { spec: "specs/fpga/uart.tri",      kind: fpga-comm,  phi_critical: true }
node trifpga-spi    { spec: "specs/fpga/spi.tri",       kind: fpga-comm,  phi_critical: true }
node trifpga-top    { spec: "specs/fpga/top_level.tri", kind: fpga-top,   phi_critical: true }
node trifpga-uart-tb { spec: "specs/fpga/testbench/uart_tb.tri", kind: testbench }

edge trifpga-uart  → trifpga-top   // uart depends on top
edge trifpga-spi   → trifpga-top   // spi depends on top
edge trifpga-mac   → trifpga-top   // mac (existing) depends on top
edge trifpga-uart  → trifpga-uart-tb

📋 ТАБЛИЦА ФАЙЛОВ К СОЗДАНИЮ

Файл Тип PHI Critical
specs/fpga/uart.tri spec ✅
specs/fpga/spi.tri spec ✅
specs/fpga/top_level.tri spec ✅
specs/fpga/constraints/arty_a7_100t.xdc constraints ✅
specs/fpga/testbench/uart_tb.tri testbench ✅
specs/fpga/testbench/mac_tb.tri testbench —
scripts/fpga/build.sh script —
scripts/fpga/flash.sh script —
Файл Изменение
architecture/graph.tri Добавить: trifpga-uart, trifpga-spi, trifpga-top
compiler/codegen/verilog/codegen.tri Добавить: emit_uart, emit_spi, emit_fpga_top

✅ КРИТЕРИИ ЗАВЕРШЕНИЯ

  • tri test specs/fpga/*.tri — все тесты зелёные
  • tri verdict --toxic specs/fpga/ — verdict CLEAN (не TOXIC)
  • tri gen specs/fpga/top_level.tri — генерирует валидный Verilog
  • yosys -p synth_xilinx — синтез без ошибок
  • architecture/graph.tri обновлён (новые phi-critical узлы)
  • .trinity/experience/episodes/fpga-uart-001.json создан
  • tri skill commit зарегистрирован для каждого шага

⚠️ ЗАПРЕЩЕНО

  1. ❌ Редактировать src/*.zig напрямую
  2. ❌ Создавать .t27 файлы для новых модулей (используй .tri)
  3. ❌ Мёрджить без прохождения tri verdict --toxic
  4. ❌ Коммитить без tri experience save
  5. ❌ Пропускать hash seal (tri skill seal --hash)

Приказ выдан: 2026-04-05 | Генерал Армии Агентов | PHI LOOP фаза 1

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions