Lambda32

Project is a work in progress

Progress report 08/21/2023: I have an idea of how the carry-ripple adder would be specified; a series of 2-bit carry-look-ahead adders as opposed to a typical full-adder configuration. This will efectively halve the states needed to sum two n-bit numbers. Currently, I am verifying the carry-look-ahead adder against the standard full-adder configuration to reinforce its integrity. Then, I will be confident enough to actually implement it in Verilog.

Summary

Lambda32 is a 32-bit pipelined processor with a robust mathematical foundation. Not only is it mathematically specified and verified for correctness, it also features a set of pure instructions, as its functional programming-inspired name implies. Additionally, Lambda32 integrates a neural network within its micro-architecture, enabling fast deep-learning processing directly at the hardware level.

Design Process

The design process can be broken down into a couple of steps:

• Specifying Lambda32 using predicate calculus (first-order logic).
• Designing finite-state automata to derive the necessary combinational logic to implement Lambda32 in hardware.
• Verifying that the combinational logic conforms to the specification by using mathematical proofs.
• Implementing the verified combinational logic in Verilog HDL for subsequent FPGA programming.

Table of Contents

1. ISA
   • R-Register
   • Variable
   • Constant
   • Operative Instruction
   • Term
   • Formula
   • IF THEN ELSE Instruction
   • ISA Structure
   • Variable Assignment
   • Term Assignment
   • Assignment Instruction
   • References

ISA

Definition of an R-Register

The ISA contains thirty-two 32-bit general purpose R-Registers defined as follows:

R0, ..., R31

Definition of a Variable

If r is an R-Register in the ISA, then a variable is either:

• An R-Register r, or
• A memory location defined as:
  • r_i[r_j], where r_i and r_j are each R-Registers and r_i holds the base memory address and r_j the index.
  • [r], where r holds the memory address.

Definition of a Constant

A constant is a 32-bit sized integer in the range [-2³¹, 2³¹ - 1].

Definition of an Operative Instruction

For a Variable v in the ISA; a Constant c; an R-Register r; and g representing either the add operation + or the multiplication *, an Operative Instruction p is such that either:

• p :≡ g(r_i, ..., r_k, ..., r_n), where g is n-ary and each r_i is an R-Register such that r_i ≠ r_k.
• p :≡ g(v₁, v₂), where g is a binary operation and each v_i is a Variable in the ISA.
• p :≡ g(v, c), where g is a binary operation.
• p :≡ g(v, f), where g is a binary operation and f is a function (defined later in Term).
• p :≡ g(v, p_i), where g is a binary operation and p_i is an Operative Instruction in the ISA.
• p :≡ -(v), where - is a unary operation.
• p :≡ -(c), where - is a unary operation.
• p :≡ -(f), where - is a unary operation and f is a function (defined later in Term).
• p :≡ -(p_i), where - is a unary operation and p_i is an Operative Instruction in the ISA.

Definition of a Term [1]

A Term t is such that either:

• t is a Variable, or
• t is a Constant, or
• t is an Operative Instruction, or
• t is an IF THEN ELSE Instruction (defined later), or
• t :≡ f(t_i, ..., t_k, ..., t_n), where f is an n-ary function and each t_i is a Term

Definition of a Formula [1]

A Formula φ is such that either:

• φ :≡ = (t₁, t₂), where t₁ and t₂ are Terms of the ISA.
• φ :≡ P(t_i, ..., t_k, ..., t_n), where P is an n-ary predicate and each t_i is a Term.
• φ :≡ ¬(α), where α is a Formula of the ISA.
• φ :≡ \/(α, β) where α and β are formulas of the ISA.
• φ :≡ /\(α, β) where α and β are formulas of the ISA.

Definition of an IF THEN ELSE Instruction

If φ is a Formula in the ISA and t₁ and t₂ are Terms, then an IF THEN ELSE Instruction is defined as follows:

IF φ THEN t₁ ELSE t₂

Definition of the ISA Structure [1]

The ISA Structure M is the set A { i | -2³¹ ≤ i ≤ 2³¹ - 1}, called the universe of M, together with:

• For each Constant c, an element c^M of A.
• For each n-ary function f, a function f^M : Aⁿ -> A.
• For each n-ary Operative Instruction g, an Operative Instruction g^M : Aⁿ -> A.

Definition of the Variable Assignment Function [1]

If M is the ISA Structure, then a Variable Assignment Function s maps each Variable in the ISA to an element of the universe A. In other words, s is a function with domain Variable and codomain A as follows:

Variable -> A

Definition of the Term Assignment Function [1]

For the ISA Structure M and the Variable Assignment Function s into M, the Term Assignment Function s' has a domain Term of the ISA and codomain A and is defined recursively as follows:

• If t is a Variable, s'(t) = s(t)
• If t is a Constant c, s'(t) = c^M
• If t :≡ g(t_i, ..., t_k, ..., t_n), such that g is an n-ary Operative Instruction in the ISA, then s'(t) = g^M(s'(t_i), ..., s'(t_k), ..., s'(t_n))
• If t :≡ f(t_i, ..., t_k, ..., t_n), such that f is an n-ary function in the ISA, then s'(t) = f^M(s'(t_i), ..., s'(t_k), ..., s'(t_n))

Definition of the Assignment Instruction

The Assignment Instruction, defined as:

v -> t, where v is a Variable and t is a Term in the ISA,

assigns a Variable v to a mapped element of A from a Term t after implicity doing the following:

v -> s'(t), where v is a Variable of the ISA and s' is a Term Assignment Function.

References

[1] Leary, Christopher C. and Kristiansen, Lars, "A Friendly Introduction to Mathematical Logic" (2015). Geneseo Authors. 6.