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.

Data type system

Logic

Logic types represent the basic element of computation. This is either a boolean value, or a 4 state logic value (depending on the simulator).

logic foo;

val foo = Bool();

logic foo;

Arrays

Array types represent a repeating data elements.

logic[10] foo;

val foo = Vec(10, Bool());

logic[9:0] foo;

Structs

Structures are also present in Nail. We use the keyword “structdef” in Nail to avoid confusion with the struct keyword in lean4/rocq.

structdef my_struct {
  logic a;
  logic[32] b;
}

class MyStruct extends Bundle {
  val a = Bool()
  val b = Vec(32, Bool())
}

typedef struct packed {
  logic a;
  logic[31:0] b;
} my_struct;

Parametric structs are also supported in Nail. Note that SystemVerilog does not have native parametric structs: the work around for this is to define a struct within a parametric interface.

template<int N>
structdef my_param_struct {
  logic a;
  logic[N] b;
}

class MyParamStruct(n: Int) extends Bundle {
  val a = Bool()
  val b = Vec(n, Bool())
}

interface my_interface #(
    parameter int N = 32
);
  typedef struct packed {
    logic a;
    logic[N-1:0] b;
  } my_struct_t;
endinterface

Functions

Functions

Like SV and Chisel, Nail has functions.

function logic[32] ax_plus_b(
    logic[32] a,
    logic[32] x,
    logic[32] b);
  return a * x + b;
endfunction

def axPlusB(a: UInt, x: UInt, b: UInt): UInt = {
    a * x + b
}

function logic [31:0] ax_plus_b(logic [31:0] a, x, b);
  return a * x + b;
endfunction

Parametric Functions

Nail also provides parametric functions.

template<int N>
function logic[N] ax_plus_b(
    logic[N] a,
    logic[N] x,
    logic[N] b);
  return a * x + b;
endfunction

def axPlusB(a: UInt, x: UInt, b: UInt): UInt = {
    a * x + b
}

function logic [N-1:0] ax_plus_b(logic [N-1:0] a, x, b);
  return a * x + b;
endfunction

Struct Functions

Nail allows functions to be defined within a struct. These functions are translated to functions with the struct name as a prefix in SystemVerilog.

structdef Foo {
  logic[32] x;
  function logic[32] Bar(logic[32] y);
    return x + y;
  endfunction
}

class Foo extends Bundle {
  val x = UInt(32.W)
  def Bar(y: UInt): UInt = {
    x + y
  }
}

function logic [31:0] Foo_Bar(
    Foo self,
    logic [31:0] y);
  return self.x + y;
endfunction

Actions

Nail introduces a concept called “actions” to a struct. Functionally, we can think of an action as monadic function of type S -> X -> S where S is a struct type and X is an input type. In more laymans terms, an action in naive Nail will look like the following:

structdef Foo {
  function Foo ExampleAction(logic x)
      // Compute and return a new Foo
      ...
  endfunction
}

As we will see in later tutorials, actions are useful abstractions for formal verification. Because of this, Nail defines the action keyword which can be used in structs.

structdef Foo {
  action Example(logic x)
    // Compute new Foo
  endaction
}

The action keywork implicitly infers the return type of the function. Additionally, member variables of the struct are assumed to be preserved across an action unless assigned to.

structdef ValidCommand {
  logic valid;
  DataStruct data;

  action Gate(logic x)
    // The `valid` field of the result is updated.
    valid = valid & x;
    // The `data` field is preserved in the result.
  endaction
}

Importantly to note: actions do not imply the result will be stored in a register. Actions define combinatorial functions where the output is the same type as the first inpute.

Interfaces

Interfaces operate on a level above data types. They augment data with information about the directionality of signals.

Directionality

The input and output keywords in Nail behave the same as in SystemVerilog.

input logic a;
output logic[4] b;

  val a = Input(Bool())
  val b = Output(UInt(4.W))

input logic a;
output logic[3:0] b;

Interface definition

The interface keyword in Nail will generate a SystemVerilog interface. The generated interface will contain three modports: forward, flipped and monitor.

interface my_interface {
  input logic a;
  output logic[32] b;
}

class MyInterface extends Bundle {
  val a = Input(Bool())
  val b = Output(UInt(32.W))
}

interface my_interface;
  logic a;
  logic [31:0] b;
  modport forward (input a, output b);
  modport flipped (output a, input b);
  modport monitor (input a, input b);
endinterface

Nesting interfaces

Nail supports nesting interfaces within other interfaces.

Clock/Reset Domain annotation

TODO(derekjchow): Check if this is necessary?

interface inner_if {
  input logic valid;
  input logic write;
  input logic[32] addr;
  input logic[32] data;
  output logic ready;
};
interface outer_if {
inner_if req;
output logic[32] result;
};

  val a = Input(Bool())
  val b = Output(UInt(4.W))

interface inner_if;
  input logic valid;
  input logic write;
  input logic[32] addr;
  input logic[32] data;
  output logic ready;
endinterface
interface outer_if;
  inner_if req;
  output logic[32] result;
endinterface;

Modules

Modules are fundamental building blocks of a logical circuit design. They encapsulate the structural and behavioural description of a digital circuit. The external interface, internal state, assignments and hierarchy are defined by a module instance.

Module Definition

module axpb(
  input logic[32] a,
  input logic[32] x,
  input logic[32] b,
  output logic[32] result
)
endmodule;

class MyParamStruct(n: Int) extends Bundle {
  val a = Bool()
  val b = Vec(n, Bool())
}

module(
  input logic[31:0] a,
  input logic[31:0] x,
  input logic[31:0] b,
  output logic[31:0] result
)
endmodule;

Defining Module Logic

Combinatorial vs Registered Logic

By default, operations in Nail are combinatorial.

module axpb(
  input logic[32] a,
  input logic[32] x,
  input logic[32] b,
  output logic[32] result  
)
  // This operation is combinatorial (as if inside of always_comb in
  // SystemVerilog).
  let ax = a * x;
  // This operation is also combinatorial
  assign result = ax + b;
endmodule

Registered Logic

Nail makes the following assumptions about registered logic:

1. There is only one clock/reset domain in the design.
2. There is a single defined update to the register.

Here is Nail’s simple syntax for registered logic:

// Define a register of signal_t, initialized to initializer on reset.
reg<signal_t> example_register(initializer);
// Update the value of this register. Subsequent updates will raise
// an error.
example_register <= updated_value;