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

module Spartan6.Primitive.DSP48A1 where

open import Spartan6.Prelude
open import Spartan6.Evidence

-- This module models one deliberately narrow DSP48A1 mode, not the complete
-- primitive.
--
-- UG389 v1.2, "Two's Complement Multiplier and M Output Port", printed page
-- 19, specifies two 18-bit two's-complement operands and a full-precision
-- 36-bit result.  The same section explicitly permits unsigned arithmetic by
-- forcing each 18-bit operand's MSB to zero.  It also identifies M as the
-- direct, optionally registered multiplier output.  Tables 1-4 through 1-7,
-- printed pages 20-21, specify that OPMODE[4]=0 bypasses the pre-adder,
-- OPMODE[3:2]=00 selects zero for Z, and OPMODE[1:0]=01 selects the multiplier
-- for X.  The pipeline attributes are described on printed pages 12-13.
--
-- UG615 v14.7, "DSP48A1", printed pages 92-95, independently records the
-- 18x18 signed multiplier, the 36-bit direct M port, the OPMODE controls, and
-- the register-bypass attributes.
--
-- Supported here:
--   * A and B are unsigned 17-bit magnitudes, presented to the hardware as
--     18-bit inputs with A[17]=B[17]=0;
--   * A0REG=A1REG=B0REG=B1REG=MREG=OPMODEREG=0;
--   * OPMODE[7:0]=00000001 (a concrete choice from the Multiply row);
--   * OPMODE[4]=0 therefore supplies B directly to the multiplier;
--   * only the combinational M[35:0] output is modelled.
--
-- Signed inputs, pre-add/subtract, P/post-add/subtract, carry, cascade,
-- clocking, resets, enables, and every registered configuration are outside
-- this module's claim.

ug389-v1-2 : PinnedSource
ug389-v1-2 =
  pinSource UG389 (revision "v1.2" (just "2014-05-29"))

ug615-v14-7 : PinnedSource
ug615-v14-7 =
  pinSource UG615 (revision "v14.7" (just "2013-10-02"))

dsp48a1MultiplyLocator : SourceLocator
dsp48a1MultiplyLocator =
  locate ug389-v1-2 "Two's Complement Multiplier and M Output Port"
    "printed pages 19-21; Figure 1-10 and Tables 1-4 through 1-7; pipeline attributes on pages 12-13"

dsp48a1PrimitiveLocator : SourceLocator
dsp48a1PrimitiveLocator =
  locate ug615-v14-7 "DSP48A1"
    "printed pages 92-95: introduction, ports, OPMODE, and attributes"

dsp48a1MultiplyTrace : RuleTraceability
dsp48a1MultiplyTrace =
  traceRule "primitive.DSP48A1.unsigned17-combinational-M"
            officialDocumentation
            (just dsp48a1MultiplyLocator)
            partiallySupported
            guaranteed
            "Only zero-MSB unsigned operands and the unregistered direct 36-bit M output are executable; the full DSP48A1 is not modelled. UG615 v14.7 pages 92-95 provide the primitive-level cross-check."

-- A concrete OPMODE record avoids silently choosing a vector ordering.

record OPMODE : Type₀ where
  constructor opmodeBits
  field
    opmode7 : Bit
    opmode6 : Bit
    opmode5 : Bit
    opmode4 : Bit
    opmode3 : Bit
    opmode2 : Bit
    opmode1 : Bit
    opmode0 : Bit

open OPMODE public

multiplyOnlyOPMODE : OPMODE
multiplyOnlyOPMODE =
  opmodeBits low low low low low low low high

-- Only pipeline selectors on the modelled A/B-to-M path are represented.

data PipelineSelection : Type₀ where
  bypassed  : PipelineSelection
  registered : PipelineSelection

record MultiplyOnlyAttributes : Type₀ where
  constructor multiplyAttributes
  field
    a0reg     : PipelineSelection
    a1reg     : PipelineSelection
    b0reg     : PipelineSelection
    b1reg     : PipelineSelection
    mreg      : PipelineSelection
    opmodereg : PipelineSelection

open MultiplyOnlyAttributes public

combinationalMultiplyAttributes : MultiplyOnlyAttributes
combinationalMultiplyAttributes =
  multiplyAttributes bypassed bypassed bypassed bypassed bypassed bypassed

-- Words in this file are least-significant-bit first: the head is port bit 0.

UnsignedOperand : Type₀
UnsignedOperand = Word 17

DSPInput : Type₀
DSPInput = Word 18

MOutput : Type₀
MOutput = Word 36

appendWord : ∀ {m n} → Word m → Word n → Word (m + n)
appendWord []       suffix = suffix
appendWord (bit ∷ bits) suffix = bit ∷ appendWord bits suffix

-- Appending low as the most-significant bit implements the unsigned mode
-- prescribed by UG389: input bits [16:0] carry the magnitude and bit 17 is 0.

toDSPInput : UnsignedOperand → DSPInput
toDSPInput magnitude = appendWord magnitude (low ∷ [])

widenDSPInput : DSPInput → MOutput
widenDSPInput input = appendWord input (replicate low)

-- Fixed-width binary arithmetic.  addModulo discards the carry beyond the
-- declared width; shiftLeftModulo discards the bit shifted beyond that width.
-- The multiply accumulator, and hence multiplyModulo and multiplyM, is
-- explicitly modular at its result width.  For the exported 17x17 subset,
-- each operand is below 2^17 and the mathematical product is below 2^34, so
-- the 36-bit hardware result has no product truncation.

sumBit : Bit → Bit → Bit → Bit
sumBit left right carry = (left ⊕ right) ⊕ carry

carryBit : Bit → Bit → Bit → Bit
carryBit left right carry =
  (left and right) or (carry and (left ⊕ right))

addWithCarry : ∀ {width}
             → Bit → Word width → Word width → Word width × Bit
addWithCarry carry [] [] = [] , carry
addWithCarry carry (left ∷ lefts) (right ∷ rights)
  with addWithCarry (carryBit left right carry) lefts rights
... | result , carry-out =
  (sumBit left right carry ∷ result) , carry-out

addModulo : ∀ {width} → Word width → Word width → Word width
addModulo left right = fst (addWithCarry low left right)

dropLast : ∀ {width} → Word (suc width) → Word width
dropLast {zero}  (bit ∷ [])   = []
dropLast {suc width} (bit ∷ bits) = bit ∷ dropLast bits

shiftLeftModulo : ∀ {width} → Word width → Word width
shiftLeftModulo {zero}  []   = []
shiftLeftModulo {suc width} word = low ∷ dropLast word

gateWord : ∀ {width} → Bit → Word width → Word width
gateWord select = map (λ bit → select and bit)

multiplyAccumulate : ∀ {steps width}
                   → Word steps → Word width → Word width → Word width
multiplyAccumulate [] multiplier accumulator = accumulator
multiplyAccumulate (bit ∷ bits) multiplicand accumulator =
  multiplyAccumulate bits
    (shiftLeftModulo multiplicand)
    (addModulo accumulator (gateWord bit multiplicand))

multiplyModulo : ∀ {width} → Word width → Word width → Word width
multiplyModulo left right =
  multiplyAccumulate right left (replicate low)

-- The sole executable DSP48A1 semantics exported here: zero-extend both
-- unsigned operands to the documented 18-bit ports, widen them to the fixed
-- 36-bit arithmetic boundary, and expose the unregistered multiplier M port.

multiplyM : UnsignedOperand → UnsignedOperand → MOutput
multiplyM left right =
  multiplyAccumulate
    (toDSPInput right)
    (widenDSPInput (toDSPInput left))
    (replicate low)

-- Checked arithmetic and mode examples.

zero17 one17 two17 three17 : UnsignedOperand
zero17  = replicate low
one17   = high ∷ replicate low
two17   = low ∷ high ∷ replicate low
three17 = high ∷ high ∷ replicate low

zero4 one4 two4 three4 six4 : Word 4
zero4  = low ∷ low ∷ low ∷ low ∷ []
one4   = high ∷ low ∷ low ∷ low ∷ []
two4   = low ∷ high ∷ low ∷ low ∷ []
three4 = high ∷ high ∷ low ∷ low ∷ []
six4   = low ∷ high ∷ high ∷ low ∷ []

unsigned-port-is-zero-extended :
  toDSPInput three17
  ≡ high ∷ high ∷ low ∷ low ∷ low ∷ low ∷ low ∷ low ∷ low
    ∷ low ∷ low ∷ low ∷ low ∷ low ∷ low ∷ low ∷ low ∷ low ∷ []
unsigned-port-is-zero-extended = refl

one-plus-one-mod-4 : addModulo one4 one4 ≡ two4
one-plus-one-mod-4 = refl

one-shifted-left-mod-4 : shiftLeftModulo one4 ≡ two4
one-shifted-left-mod-4 = refl

two-times-three-mod-4 : multiplyModulo two4 three4 ≡ six4
two-times-three-mod-4 = refl

fifteen-times-two-wraps-mod-4 :
  multiplyModulo
    (high ∷ high ∷ high ∷ high ∷ [])
    two4
  ≡ low ∷ high ∷ high ∷ high ∷ []
fifteen-times-two-wraps-mod-4 = refl

multiply-mode-bypasses-pre-adder : opmode4 multiplyOnlyOPMODE ≡ low
multiply-mode-bypasses-pre-adder = refl

multiply-mode-selects-zero-Z :
  (opmode3 multiplyOnlyOPMODE ≡ low)
  × (opmode2 multiplyOnlyOPMODE ≡ low)
multiply-mode-selects-zero-Z = refl , refl

multiply-mode-selects-multiplier-X :
  (opmode1 multiplyOnlyOPMODE ≡ low)
  × (opmode0 multiplyOnlyOPMODE ≡ high)
multiply-mode-selects-multiplier-X = refl , refl