Skip to content

H264.md

Latest commit

 

History

History
117 lines (94 loc) · 5.34 KB

H264.md

File metadata and controls

117 lines (94 loc) · 5.34 KB

H.264 Baseline Profile Video Codec

H.264 Baseline Profile Video Codec

A complete H.264 Baseline Profile encoder and decoder pipeline — pure Lean reference functions with formal proofs, and fully synthesizable hardware codec producing playable MP4 files directly from hardware. 16×16 frame → H.264 encode → MP4 mux, all in Signal DSL.

Pipeline Architecture

ENCODER:  Pixels → Intra Pred → DCT → Quant → CAVLC → NAL → H.264 Bitstream → MP4 Container
          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
          Fully synthesizable Signal DSL — h264MP4Encoder module (Phase 40)

DECODER:  Bitstream → NAL Parse → CAVLC Decode → Dequant → IDCT → Intra Recon → Pixels
          Synthesizable decoder pipeline (Phase 32)

Hardware MP4 Encoder (Phase 40)

A single hardware module that takes a 16×16 frame and produces a complete playable MP4 file — no software post-processing needed.

h264MP4Encoder (Signal.loop, 12 registers, ~6100 cycles)
├── h264FrameEncoder (nested sub-module — SPS + PPS + IDR slice)
├── IDR buffer memory (1024×8-bit)
├── MP4 ROM memory (1024×8-bit, host-loaded ftyp+moov template)
└── FSM: buffer encoder output → emit ROM (with runtime patching) → emit mdat
Component File Description
MP4 Encoder MP4Encoder.lean 12-register FSM, 7 phases, ROM patching at 16 offsets
Frame Encoder FrameEncoder.lean 21-register FSM, 20 phases, 3 nested sub-modules
MP4 Muxer MP4Mux.lean Software MP4 box builder + ROM template generator
Synth MP4EncoderSynth.lean #writeDesign → SV + CppSim + JIT 
lake build h264-mp4-encoder-test && lake exe h264-mp4-encoder-test
# Output: 709 bytes, byte-identical to software muxer
# ffprobe: valid 16×16 H.264 Baseline MP4, 1 frame

Synthesizable Decoder Pipeline (Phase 32)

Quantized Levels (16×16-bit) → [Dequant FSM] → [IDCT FSM] → [Reconstruct FSM] → Pixels [0,255]
                                 16 cycles       64 cycles      16 cycles
Module File Cycles Description
Dequant DequantSynth.lean 16 level × V[posClass] × 2^(qp/6), fixed QP=20
Inverse DCT IDCTSynth.lean 64 Butterfly row+col transforms, +32>>6 rounding
Reconstruct ReconstructSynth.lean 16 predicted + residual, clamp [0,255]
Pipeline DecoderSynth.lean ~96 Monolithic FSM: IDLE→DEQUANT→IDCT→RECON→DONE

Each module generates SystemVerilog + CppSim header + JIT wrapper via #writeDesign.

Modules (14 phases)

Module Pure Lean Proofs Tests Synth
DRAM Interface DRAMInterface.lean 3 theorems DRAMTest.lean Sim model
4×4 Integer DCT/IDCT DCT.lean bounded error, linearity DCTTest.lean IDCTSynth
Quantization Quant.lean zero/sign preservation QuantTest.lean DequantSynth
CAVLC Decode CAVLCDecode.lean 4 roundtrip proofs CAVLCDecodeTest.lean —
NAL Pack/Parse NAL.lean roundtrip proof NALTest.lean —
Intra Prediction (9 modes) IntraPred.lean residual roundtrip IntraPredTest.lean —
Encoder Top Encoder.lean — H264PipelineTest.lean —
Decoder Top Decoder.lean — H264PipelineTest.lean —
Frame-Level E2E — — H264FrameTest.lean —
Quant/Dequant Roundtrip QuantRoundtripSynth.lean — H264JITTest.lean Full
Reconstruction ReconstructSynth.lean — H264DecoderSynthTest.lean Full
Decoder Pipeline DecoderSynth.lean — H264DecoderSynthTest.lean Full
CAVLC Encoder CAVLCSynth.lean — H264BitstreamTest.lean Full
Frame Encoder FrameEncoder.lean — H264FrameEncoderTest.lean Full
MP4 Encoder MP4Encoder.lean — H264MP4EncoderTest.lean Full
MP4 Muxer MP4Mux.lean — H264PlayableTest.lean Software

JIT End-to-End Test

The quant→dequant roundtrip module synthesizes to SystemVerilog, compiles via JIT, and passes all 4 tests:

lake exe h264-jit-test
# === H.264 JIT End-to-End Test ===
# JIT: Compiling IP/Video/H264/gen/quant_roundtrip_jit.cpp...
# JIT: Loaded shared library
#   Test 1: Zero block...        PASS
#   Test 2: DCT coefficients...  PASS (all 16 match)
#   Test 3: Single large coeff... PASS
#   Test 4: Negative coeffs...   PASS
# *** ALL H.264 JIT TESTS PASSED ***

Hardware MP4 Encoder Test

lake exe h264-mp4-encoder-test
# === H.264 MP4 Encoder JIT Test ===
#   ROM loaded (629 bytes)
#   Frame encoder completed in 5437 cycles
#   Output: 709 bytes — byte-identical to software muxer
#   ftyp: OK, moov: OK, mdat: OK, IDR NAL (0x65): OK
#   ROM vs reference: MATCH, IDR NAL (68 bytes): MATCH
# TEST PASSED

Formal Proofs (all without sorry)

  • DRAM: read-after-write, write-write, read-default
  • DCT: |IDCT(DCT(x))[i] - x[i]| ≤ 1, linearity
  • Quant: quant(0) = 0, sign preservation
  • CAVLC: decode(encode(coeffs)) = coeffs (zero block, mixed coefficients, DC-only, trailing ones)
  • NAL: parse(pack(payload)) = payload
  • Intra: predicted + (original - predicted) = original