Combinational and sequential circuits

In Agda

Utrecht University, June 2017

Plan for the talk

  • We'll start with an example
  • EDSL definitions to understand the example
  • Combinational vs. sequential (example)
  • Semantics, equivalence
  • Circuit patterns, etc.

What does this compute?

Haskell's mapAccumL

A.K.A "stateful map"


mapAccumL :: (s -> a -> (s,b)) -> s -> [a] -> (s, [b])
mapAccumL _ s []     = (s, [])
mapAccumL f s (x:xs) = (s″,y:ys)
  where (s′, y ) = f s x
        (s″,ys)  = mapAccumL f s′ xs

mapAccumL in Agda (λ₁)

  • λ₁ (Lambda1) is the name of our EDSL
  • This mapAccL-par works with vectors

mapAccL-par : ∀ n (λ₁ σ → λ₁ ρ → λ₁ (σ ⊗ τ)) → λ₁ σ → λ₁ (vec ρ n) → λ₁ (σ ⊗ vec τ n)
mapAccL-par zero     _ s _  = s ， []
mapAccL-par (suc n′) f s xs = case[] xs of λ x xs′ →
                                case⊗ (f s x) of λ s′ y →
                                  case⊗ (mapAccL-par n′ f s′ xs′) of λ s″ ys′ →
                                    s″ ， (y ∷ ys′)
  • This is a "parallel" version, later a sequential one

Definitions and notation

  • Universe of types for circuit I/O
    • Unit, base type (B), sums, products
    • Notation for object type vars: σₙ, τₙ, ρₙ

data Uₚ (B : Set) : Set where
  𝟙         : Uₚ B
  ι         : Uₚ B
  _⊗_ _⊕_  : (τ₁ τ₂ : Uₚ B) → Uₚ B

vec τ n = τ ⊗ τ ⊗ … ⊗ τ

Tₚ : ∀ {B} (τ : Uₚ B) → Set
Tₚ      𝟙          = ⊤
Tₚ {B}  ι          = B
Tₚ      (τ₁ ⊗ τ₂)  = Tₚ τ₁  × Tₚ τ₂
Tₚ      (τ₁ ⊕ τ₂)  = Tₚ τ₁  ⊎ Tₚ τ₂

Context, Environments and Gates

  • A Ctxt (inputs) is a list of Uₚ
  • An Env is a heterogenous list indexed by a Ctxt
    • Contexts: Γₙ, Δₙ,…
    • Environments: γₙ, δₙ,…
  • A Gate has an interface (Δ,τ) and a spec (⟦–⟧g)
    • Other information for synthesis…

record Gate {B} (Δ : Ctxt B) (τ : Uₚ B) : Set where
  constructor MkG
  field  ⟦–⟧g : Env Tₚ Δ → Tₚ τ

CONST : ∀ {B} {τ : Uₚ B} (x : Tₚ τ) → Gate {B} ε τ
CONST x = MkG (const x)

The "Lambda1" EDSL

  • Core datatype (λ₁′) indexed by inputs, output
  • De Bruijn indices, let's for sharing, explicit looping construct
    • Products, sums, fundamental gates
    • No arrow types: no lambda, no application

data λ₁′ {B} : (Γ : Ctxt B) (τ : Uₚ B) → Set where
  [_]    : ∀ {Γ τ}                (i : Γ ∋ τ)
                                   → λ₁′ Γ τ

  letₓ′  : ∀ {Γ σ τ}    (x : λ₁′ Γ σ)  (b : λ₁′ (σ ◅ Γ) τ)
                                   → λ₁′ Γ τ

  loop′  : ∀ {Γ σ τ}       (c : λ₁′ (σ ◅ Γ) (σ ⊗ τ))
                                  → λ₁′ Γ τ

Lambda1 surface language (λ₁)

  • De Bruijn isn't so friendly
    • So we transform Agda binders into binders of the EDSL
    • Using a version of "unembedding"

λ₁ : ∀ {B} (τ : Uₚ B) → Set
λ₁ {B} τ = ∀ {Γ : Ctxt B} → λ₁′ Γ τ

letₓ : ∀ (x : λ₁ σ) (f : λ₁ σ → λ₁ τ) → λ₁ τ
loop : ∀ (f : λ₁ σ → λ₁ (σ ⊗ τ)) → λ₁ τ

syntax letₓ eₓ (λ x → b) = let͘ x ≔ eₓ in͘ b
syntax loop {σ} (λ s → b) = loop s ∶ σ in͘ b
					

(c₁ ＄ c₂)  ⇒  (letₓ c₂ c₁)
(λ₁ σ₀ → λ₁ σ₁ → … → λ₁ σₙ → λ₁ τ)  ⇒  (λ₁′ (σ₀ ◅ σ₁ ◅ … ◅ σₙ ◅ ε) τ)

Back to an example for a while

  • Remember mapAccL-par

mapAccL-par : ∀ n (λ₁ σ → λ₁ ρ → λ₁ (σ ⊗ τ)) → λ₁ σ → λ₁ (vec ρ n) → λ₁ (σ ⊗ vec τ n)
mapAccL-par zero     _ s _  = s ， []
mapAccL-par (suc n′) f s xs = case[] xs of λ x xs′ →
                                case⊗ (f s x) of λ s′ y →
                                  case⊗ (mapAccL-par n′ f s′ xs′) of λ s″ ys′ →
                                    s″ ， (y ∷ ys′)

Sequential mapAccL

  • We can easily define a sequential version of mapAccL
  • mapAccL-seq, has a loop instead of recursion

mapAccL-seq : (f : λ₁ σ → λ₁ ρ → λ₁ (σ ⊗ τ)) (x : λ₁ ρ) → λ₁ τ
mapAccL-seq {σ} f x = loop s ∶ σ in͘ (f s x)

Semantics, one step at a time

  • Loops in circuits: semantics must consider state

⟦_⟧s : (c : λ₁′ Γ τ) (s : λₛ c) (γ : Env Tₚ Γ) → (λₛ c × Tₚ τ)
  • There's an inductive family giving the state type of a circuit

data λs {B} : {Γ : Ctxt B} {τ : Uₚ B} (c : λ₁′ Γ τ) → Set where
  s[_]   : ∀ {Γ σ}     (i : Γ ∋ σ)                            → λₛ [ i ]
  sLet   : ∀ {Γ σ τ}   {x : λ₁′ Γ σ} {e : λ₁′ (σ ◅ Γ) τ}  (xₛ : λₛ x) (eₛ : λₛ e)
                                                            → λₛ (letₓ′ x e)

  sLoop  : ∀ {Γ σ τ}   {c : λ₁′ (σ ◅ Γ) (σ ⊗ τ)}         (iₛ : Tₚ σ) (cₛ : λₛ c)
                                                            → λₛ (loop′ c)

  _s，_   : ∀ {Γ τ₁ τ₂}  {x : λ₁′ Γ τ₁} {y : λ₁′ Γ τ₂}        (xₛ : λₛ x) (yₛ : λₛ y)
                                                              → λₛ (x ，′ y)

Circuits in (discrete) time: n steps

  • One state transition per clock cycle
  • We can simulate a number of cycles with ⟦_⟧n
    • Final state also returned
    • Usefulness clear soon

⟦_⟧n : (c : λ₁′ Γ τ) (s : λₛ c) (γn : Vec (Env Tₚ Γ) n) → λₛ c × Vec (Tₚ τ) n
⟦_⟧n n c s = mapAccumL n s ⟦ c ⟧s

Parallel vs. sequential

  • It's quite intuitive how mapAccL-par and mapAccL-seq are related
    • In one step from mapAccL-par, in n steps from mapAccL-seq
  • But the exact relation is not so short…

mapAccL-seq : (f : λ₁ σ → λ₁ ρ → λ₁ (σ ⊗ τ)) (x : λ₁ ρ) → λ₁ τ
mapAccL-seq {σ} f x = loop s ∶ σ in͘ (f s x)

mapAccL-par vs. mapAccL-seq


_⊒_ : ∀ {α β φ : Set} → φ × (α × β) → α × β → Set
(_ , sa,ra) ⊒ sb,rb = sa,ra ≡ sb,rb
					

n : ℕ
X : λₛ (mapAccL-par n f)

σ ρ τ : Uₚ
f     : λ₁ σ → λ₁ ρ → λ₁ (σ ⊗ τ)
s     : Tₚ σ
xs    : Tₚ (vec ρ n)

MALSt  : Tₚ σ → λₛ (mapAccL-seq {σ} f)
MALIns : Tₚ (vec ρ n) → Vec (Env Tₚ (ρ ◅ ε)) n

⟦ mapAccL-par n f ⟧s X (s ↦ xs ◅ ε) ⊒ ⟦ mapAccL-seq f ⟧n n (MALSt s) (MALIns xs)

From mapAccL, other patterns…


iterate-par : ∀ n (f : λ₁ τ → λ₁ τ) (x : λ₁ τ) → λ₁ (vec τ (suc n))
iterate-par n {τ} f x = mapAccL-par n f′ x (replicate͘ unit)
  where  f′ : λ₁ τ → λ₁ 𝟙 → λ₁ (τ ⊗ τ)
         f′ x _ = fork (f x)

Sequential version: iterate-seq


iterate-seq : (f : λ₁ τ → λ₁ τ) → λ₁ τ
iterate-seq {τ} f = mapAccL-seq f′ unit
  where  f′ : λ₁ τ → λ₁ 𝟙 → λ₁ (τ ⊗ τ)
         f′ x _ = fork (f x)

Folds and scans, all-in-one


foldl-scanl-par : ∀ n (λ₁ τ → λ₁ τ → λ₁ τ) → λ₁ τ → λ₁ (vec τ n) → λ₁ (τ ⊗ vec τ n)
foldl-scanl-par n _⊞_ = mapAccL-par n (λ acc x → acc ， (acc ⊞ x))
						

foldl-par n _⊞_ e xs = fst (foldl-scanl-par n _⊞_ e xs)
scanl-par n _⊞_ e xs = snd (foldl-scanl-par n _⊞_ e xs)

Sequential version: foldl-scanl-seq


foldl-scanl-seq : ∀ (_⊞_ : λ₁ τ → λ₁ τ → λ₁ τ) (x : λ₁ τ) → λ₁ τ
foldl-scanl-seq _⊞_ = mapAccL-seq (λ acc x → acc ， (acc ⊞ x))

Composition and pipelining

  • Pardon the flipped composition, it makes things easier…

_comp_ : (f : λ₁ σ → λ₁ ρ) (g : λ₁ ρ → λ₁ τ) → (λ₁ σ → λ₁ τ)
_comp_ = flip _∘_
						

_compD_ : (f : λ₁ σ → λ₁ ρ) (g : λ₁ ρ → λ₁ τ) → (λ₁ σ → λ₁ τ)
f compD g = (f comp delay) comp g

Correctness of pipelining

  • Here the whole output Stream really matters
  • The pipelined version should be shifted by one time unit
  • Bisimilarity

⟦ f comp g ⟧* (stComp sf sg) γ ≈ tail (⟦ f compD g ⟧* (stCompD sf sg sd) γ)

N-ary composition

  • Type-aligned sequence: VecA F as bs
    • fs : VecA F as bs = [f₀ : F a₀ b₀, f₁ : F a₁ b₁, …
    • With b₀ = a₁, b₁ = a₂, …

compN : let F = λ σ τ → (λ₁ σ → λ₁ τ)
        in (fs : VecA F σs τs) → λ₁ (head σs) → λ₁ (last τs))

⟦ compN fs ⟧* (stCompN n sfs) γ ≈ drop n (⟦ compDN fs ⟧* (stCompDN n sfs sds) γ)

That's all for today!