---
title: "Architecture note"
description: "Architecture note 1. Design objective The objective is a vertically integrated, inspectable prototype: SQL text is parsed, persisted rows are scanned, eligible predicates are compiled into a packed ha…"
doc_version: 1
last_updated: 2026-10-17
canonical_url: "http://parc.yolo.scapegoat.dev/note/projects/2026/07/10/_assets/verisql-hw-report/sources/project/docs/architecture"
---

# Architecture note

Architecture note 1. Design objective The objective is a vertically integrated, inspectable prototype: SQL text is parsed, persisted rows are scanned, eligible predicates are compiled into a packed ha…

## Content

# Architecture note

## 1. Design objective

The objective is a vertically integrated, inspectable prototype: SQL text is
parsed, persisted rows are scanned, eligible predicates are compiled into a
packed hardware configuration, and results are consumed through a valid/ready
stream. The accelerator is intentionally a predicate filter, not a complete SQL
processor. This isolates a common scan bottleneck while keeping the proof state
space finite and the semantic boundary explicit.

## 2. Database layer

### Parser and AST

`verisql/parser.py` is a hand-written tokenizer and recursive-descent parser.
It accepts only the grammar listed in the main README. Unquoted identifiers are
normalized to lower case. It does not attempt error recovery.

### Storage format

Each database is a directory containing `catalog.json` and one `.vsql` file per
table. A table file begins with:

```text
8 bytes   magic: VSQLTB01
1 byte    column count
3 bytes   reserved
32 bytes  SHA-256 of canonical table schema
```

Each record is:

```text
1 byte             NULL bitmap
4 * column_count   little-endian signed INT32 words
```

NULL words are physically zero and semantically identified only by the bitmap.
Catalog updates use write–fsync–rename and table appends are fsynced. POSIX
advisory locks are used when available. The design is append-only and has no
rollback or crash-recovery journal.

## 3. Planner boundary

The planner offloads a `WHERE` clause only when all of the following hold:

- It is a conjunction.
- It contains at most four predicates.
- Every predicate references one of the table's at most four columns.
- Every scalar constant is signed INT32.
- Every operation is one of the eight hardware opcodes.

A disabled predicate slot contributes logical TRUE, so fewer than four
predicates require no special reduction path. Zero predicates produce a plain
table scan. More than four predicates produce a software filter scan.

## 4. Scalar predicate cell

`rtl/sql_cmp32.vhd` implements signed ordering without converting either input
to VHDL `signed` for the datapath comparison:

```text
if sign(lhs) != sign(rhs):
    lhs < rhs := sign(lhs)
else:
    lhs < rhs := unsigned(lhs) < unsigned(rhs)
```

Greater-than is the same relation with operands reversed. Equality is bitwise.
Comparisons against a NULL column produce false because SQL WHERE retains only
TRUE; `IS NULL` and `IS NOT NULL` inspect the NULL bit directly.

## 5. Streaming accelerator

`rtl/sql_predicate_datapath.vhd` contains four column-selection muxes and
four comparator cells. Enabled results are reduced with AND.
`rtl/sql_predicate_accel.vhd` captures that reduction result in a one-entry
output register.

State transition:

```text
in_ready = !valid_q || out_ready

on rising edge:
    if reset:
        valid_q = 0
        match_q = 0
    else if in_ready:
        valid_q = in_valid
        if in_valid:
            match_q = combinational_match
```

Consequences:

- Latency is one registered stage from accepted input to visible output.
- The core accepts one row per clock when the downstream consumer is ready.
- A full output slot can be consumed and replaced on the same edge.
- When `out_valid && !out_ready`, both `out_valid` and `out_match` remain stable.
- Configuration and input data are sampled semantically at the accepted edge;
  they need not remain stable afterward.
- Match results are in order and one-for-one with accepted rows. A transport
  shell must retain or delay each accepted row until the corresponding result
  is consumed; the Python stream model demonstrates that correlation FIFO.

## 6. Software/RTL correspondence

`verisql/accelerator.py` contains:

- Exact opcode constants.
- The same sign-bit/unsigned less-than lowering.
- Packed row and configuration helpers.
- A combinational four-slot model.
- A cycle-accurate stream-register model.
- An independent Python reference evaluator using ordinary signed integers.

Python differential tests compare the model and reference evaluator. A
file-driven GHDL testbench consumes 1,000 deterministic vectors generated by
`pack_row` and `pack_config`, checking the cross-language bit layout at the
actual VHDL datapath ports. The Z3 proofs use symbolic bit-vectors and signed
specification operators. The SBY harnesses prove the comparator, packed
datapath, and stream next-state blocks after VHDL elaboration and synthesis.

## 7. Integration path to an FPGA system

The core is transport-neutral. A board design can place an AXI-stream, Avalon-
ST, DMA, or custom FIFO shell around the valid/ready interface. Configuration
can be delivered through registers or a descriptor stream. The database's
`pack_row` and `pack_config` functions define the byte/bit mapping expected by
such a driver. A production implementation would also need pinned buffers,
coherent ownership rules, completion signaling, error reporting, and explicit
clock/reset-domain handling.

## Backlinks

- [logs/2026/07/daily-report-2026-07-10](http://parc.yolo.scapegoat.dev/note/logs/2026/07/daily-report-2026-07-10)

## Sitemap

- [Home](http://parc.yolo.scapegoat.dev/)
- [Home markdown mirror](http://parc.yolo.scapegoat.dev/index.md)
- [Markdown sitemap](http://parc.yolo.scapegoat.dev/sitemap.md)