{-# OPTIONS --safe --cubical #-}

module Spartan6.Primitive.Carry4 where

open import Spartan6.Prelude

-- Primary source pin:
--
--   AMD/Xilinx, UG615, Spartan-6 Libraries Guide for HDL Designs,
--   v14.7, 2013-10-02, Chapter 4, CARRY4, printed pages 74-75.
--   https://docs.amd.com/v/u/en-US/spartan6_hdl
--
-- The schematic and port table are on page 74.  The schematic gives four
-- bit-ordered MUXCY/XORCY stages: MUXCY selects DI[i] when S[i] is 0 and the
-- incoming carry when S[i] is 1; XORCY emits S[i] XOR the incoming carry.
-- Page 75 contains the HDL templates.  UG615 supplies no separate textual
-- logic table for CARRY4.

ug615Document : String
ug615Document = "UG615"

ug615Revision : String
ug615Revision = "v14.7"

ug615PublicationDate : String
ug615PublicationDate = "2013-10-02"

ug615Carry4Location : String
ug615Carry4Location = "Chapter 4, CARRY4, printed pages 74-75"

-- UG615 identifies CI as the cascade input and CYINIT as the initialization
-- input, but does not specify behavior for treating both as simultaneously
-- selected raw drivers.  Admission therefore records which documented source
-- feeds the first stage.  The non-selected raw port must be unused/tied low.

data CarryEntry : Type₀ where
  fromCI     : Bit → CarryEntry
  fromCYINIT : Bit → CarryEntry

entryBit : CarryEntry → Bit
entryBit (fromCI ci)         = ci
entryBit (fromCYINIT cyinit) = cyinit

record Carry4Output : Type₀ where
  constructor carry4Output
  field
    oPort  : Vec Bit 
    coPort : Vec Bit 

open Carry4Output public

-- Arguments are ordered select, DI, incoming carry.  These equations are the
-- two-valued truth tables of the page-74 MUXCY and XORCY symbols.

muxCY : Bit → Bit → Bit → Bit
muxCY select di incoming = mux select di incoming

xorCY : Bit → Bit → Bit
xorCY select incoming = select ⊕ incoming

-- Vector order is ascending bit order: the head of each vector is port bit 0,
-- followed by bits 1, 2, and 3.  The output vectors use the same order.

evalCarryChain : Bit → Vec Bit  → Vec Bit  → Carry4Output
evalCarryChain c0
  (di0 ∷ di1 ∷ di2 ∷ di3 ∷ [])
  (s0  ∷ s1  ∷ s2  ∷ s3  ∷ []) =
  carry4Output
    (xorCY s0 c0 ∷ xorCY s1 c1 ∷ xorCY s2 c2 ∷ xorCY s3 c3 ∷ [])
    (c1 ∷ c2 ∷ c3 ∷ c4 ∷ [])
  where
  c1 : Bit
  c1 = muxCY s0 di0 c0

  c2 : Bit
  c2 = muxCY s1 di1 c1

  c3 : Bit
  c3 = muxCY s2 di2 c2

  c4 : Bit
  c4 = muxCY s3 di3 c3

evalCarry4 : CarryEntry → Vec Bit  → Vec Bit  → Carry4Output
evalCarry4 entry di s = evalCarryChain (entryBit entry) di s

-- Source-specific entry points make the treatment of the two raw scalar ports
-- explicit at call sites.

evalCarry4FromCI : Bit → Vec Bit  → Vec Bit  → Carry4Output
evalCarry4FromCI ci = evalCarry4 (fromCI ci)

evalCarry4FromCYINIT : Bit → Vec Bit  → Vec Bit  → Carry4Output
evalCarry4FromCYINIT cyinit = evalCarry4 (fromCYINIT cyinit)

-- Checked one-stage truth-table rows.

muxCY-selects-DI : ∀ di incoming → muxCY low di incoming ≡ di
muxCY-selects-DI di incoming = refl

muxCY-propagates-carry : ∀ di incoming → muxCY high di incoming ≡ incoming
muxCY-propagates-carry di incoming = refl

xorCY-select-low : ∀ incoming → xorCY low incoming ≡ incoming
xorCY-select-low incoming = refl

xorCY-select-high : ∀ incoming → xorCY high incoming ≡ not incoming
xorCY-select-high incoming = refl

allLow4 : Vec Bit 
allLow4 = low ∷ low ∷ low ∷ low ∷ []

allHigh4 : Vec Bit 
allHigh4 = high ∷ high ∷ high ∷ high ∷ []

alternatingDI : Vec Bit 
alternatingDI = high ∷ low ∷ high ∷ low ∷ []

-- With every S bit high, the initial carry propagates through all four stages.

CI-low-propagates :
  evalCarry4FromCI low allLow4 allHigh4
  ≡ carry4Output allHigh4 allLow4
CI-low-propagates = refl

CYINIT-high-propagates :
  evalCarry4FromCYINIT high allLow4 allHigh4
  ≡ carry4Output allLow4 allHigh4
CYINIT-high-propagates = refl

-- With every S bit low, each DI bit becomes that stage's carry output and the
-- following O bit observes the previous stage's carry.

DI-generates-carries :
  evalCarry4FromCYINIT low alternatingDI allLow4
  ≡ carry4Output
      (low ∷ high ∷ low ∷ high ∷ [])
      alternatingDI
DI-generates-carries = refl

-- Once admission has selected a source, equal source values have identical
-- combinational behavior.

CI-CYINIT-same-value : ∀ bit di s
  → evalCarry4FromCI bit di s ≡ evalCarry4FromCYINIT bit di s
CI-CYINIT-same-value bit di s = refl