Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

The Nail DSL

This book describes the Nail DSL, a language for specifying RTL in the Guru formal verification system. Nail is built on top Guru’s PHOAS system.

Objectives

The goals of Nail are:

  • Developer Ergonomics: Nail is easy to learn. Developers that come from a Chisel or SystemVerilog background should be able to be productive with Nail from day 1.
  • Idiomatic SystemVerilog generation: We strive to define a clear mapping from Nail to SystemVerilog primitves. This enables designs built with Nail to play nicely with other tools/components in SystemVerilog.
  • Formal Methods Friendly: Being built on top of the Lean4/Rocq proof assistant, Nail enables usage of higher-order logic to verify your hardware design. This serves as a compliment to generative AI assistants, which can use formal defined specifications to constrain their designs to provably correct systems.

Trivia

The name nail comes from two sources:

  1. Parts of the tool are inspired by the Chisel language. Both chisels and nails are used in woodworking projects.
  2. Nail’s purpose is to serve Guru.