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

module Spartan6.Primitive.LUTSmall where

open import Spartan6.Prelude
open import Spartan6.Evidence
open import Spartan6.Primitive.LUT

-- Source: UG615 v14.7, Chapter 4, the general-output LUT entries:
--
--   LUT1  printed pages 148-149  (2-bit INIT)
--   LUT2  printed pages 154-155  (4-bit INIT)
--   LUT3  printed pages 160-161  (8-bit INIT)
--   LUT4  printed pages 166-168  (16-bit INIT)
--   LUT5  printed pages 175-177  (32-bit INIT)
--
-- Each logic table orders its inputs as I(n-1) ... I1 I0 and maps the binary
-- input value to the same-numbered INIT bit.  Thus I0 is the least-significant
-- address bit.  Each attribute table gives an all-zero default INIT.
--
-- The code below reuses the generic tableSize/address/evalLUT semantics.  It
-- models only the documented two-valued general output and INIT-bit selection.
-- It does not parse raw hexadecimal syntax or model macro expansion, LUT5
-- packing, local/dual-output variants, routing, delay, or electrical behavior.

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

lut1Locator lut2Locator lut3Locator lut4Locator lut5Locator : SourceLocator
lut1Locator =
  locate lutSmallPinnedSource "LUT1"
    "printed pages 148-149: logic table, 2-bit INIT attribute, and templates"
lut2Locator =
  locate lutSmallPinnedSource "LUT2"
    "printed pages 154-155: logic table, 4-bit INIT attribute, and templates"
lut3Locator =
  locate lutSmallPinnedSource "LUT3"
    "printed pages 160-161: logic table, 8-bit INIT attribute, and templates"
lut4Locator =
  locate lutSmallPinnedSource "LUT4"
    "printed pages 166-168: logic table, 16-bit INIT attribute, and templates"
lut5Locator =
  locate lutSmallPinnedSource "LUT5"
    "printed pages 175-177: logic table, ports, 32-bit INIT attribute, and templates"

lut1Trace lut2Trace lut3Trace lut4Trace lut5Trace : RuleTraceability
lut1Trace =
  traceRule "primitive.LUT1.two-valued-init"
            officialDocumentation
            (just lut1Locator)
            partiallySupported
            guaranteed
            "General-output truth-table semantics only; LUT1 is documented as a macro, and raw INIT decoding and macro expansion are not modelled."
lut2Trace =
  traceRule "primitive.LUT2.two-valued-init"
            officialDocumentation
            (just lut2Locator)
            partiallySupported
            guaranteed
            "General-output truth-table semantics only; LUT2 is documented as a macro, and raw INIT decoding and macro expansion are not modelled."
lut3Trace =
  traceRule "primitive.LUT3.two-valued-init"
            officialDocumentation
            (just lut3Locator)
            partiallySupported
            guaranteed
            "General-output truth-table semantics only; LUT3 is documented as a macro, and raw INIT decoding and macro expansion are not modelled."
lut4Trace =
  traceRule "primitive.LUT4.two-valued-init"
            officialDocumentation
            (just lut4Locator)
            partiallySupported
            guaranteed
            "General-output truth-table semantics only; LUT4 is documented as a macro, and raw INIT decoding and macro expansion are not modelled."
lut5Trace =
  traceRule "primitive.LUT5.two-valued-init"
            officialDocumentation
            (just lut5Locator)
            partiallySupported
            guaranteed
            "General-output truth-table semantics only; raw INIT decoding, LUT6 packing, local/dual outputs, and routing are not modelled."

-- Arity-specific table and input aliases.  TruthTable computes the documented
-- INIT widths as 2^arity.

LUT1Table LUT2Table LUT3Table LUT4Table LUT5Table : Type₀
LUT1Table = TruthTable 
LUT2Table = TruthTable 
LUT3Table = TruthTable 
LUT4Table = TruthTable 
LUT5Table = TruthTable 

LUT1Inputs LUT2Inputs LUT3Inputs LUT4Inputs LUT5Inputs : Type₀
LUT1Inputs = Word 
LUT2Inputs = Word 
LUT3Inputs = Word 
LUT4Inputs = Word 
LUT5Inputs = Word 

evalLUT1Inputs : LUT1Table → LUT1Inputs → Bit
evalLUT1Inputs = evalLUT

evalLUT2Inputs : LUT2Table → LUT2Inputs → Bit
evalLUT2Inputs = evalLUT

evalLUT3Inputs : LUT3Table → LUT3Inputs → Bit
evalLUT3Inputs = evalLUT

evalLUT4Inputs : LUT4Table → LUT4Inputs → Bit
evalLUT4Inputs = evalLUT

evalLUT5Inputs : LUT5Table → LUT5Inputs → Bit
evalLUT5Inputs = evalLUT

-- Port-oriented evaluators list arguments I0, I1, ..., matching the generic
-- evaluator's least-significant-first input vector.

evalLUT1 : LUT1Table → Bit → Bit
evalLUT1 init input0 = evalLUT1Inputs init (input0 ∷ [])

evalLUT2 : LUT2Table → Bit → Bit → Bit
evalLUT2 init input0 input1 =
  evalLUT2Inputs init (input0 ∷ input1 ∷ [])

evalLUT3 : LUT3Table → Bit → Bit → Bit → Bit
evalLUT3 init input0 input1 input2 =
  evalLUT3Inputs init (input0 ∷ input1 ∷ input2 ∷ [])

evalLUT4 : LUT4Table → Bit → Bit → Bit → Bit → Bit
evalLUT4 init input0 input1 input2 input3 =
  evalLUT4Inputs init (input0 ∷ input1 ∷ input2 ∷ input3 ∷ [])

evalLUT5 : LUT5Table → Bit → Bit → Bit → Bit → Bit → Bit
evalLUT5 init input0 input1 input2 input3 input4 =
  evalLUT5Inputs init
    (input0 ∷ input1 ∷ input2 ∷ input3 ∷ input4 ∷ [])

-- Named INIT indices used to check the documented weight of the highest input
-- of each arity.

INIT1-of-2 : Fin 
INIT1-of-2 = fsuc fzero

INIT1-of-4 INIT2-of-4 : Fin 
INIT1-of-4 = fsuc fzero
INIT2-of-4 = fsuc (fsuc fzero)

INIT1-of-8 INIT4-of-8 : Fin 
INIT1-of-8 = fsuc fzero
INIT4-of-8 = fsuc (fsuc (fsuc (fsuc fzero)))

INIT1-of-16 INIT8-of-16 : Fin 
INIT1-of-16 = fsuc fzero
INIT8-of-16 =
  fsuc (fsuc (fsuc (fsuc (fsuc (fsuc (fsuc (fsuc fzero)))))))

INIT1-of-32 INIT16-of-32 : Fin 
INIT1-of-32 = fsuc fzero
INIT16-of-32 =
  fsuc (fsuc (fsuc (fsuc (fsuc (fsuc (fsuc (fsuc
    (fsuc (fsuc (fsuc (fsuc (fsuc (fsuc (fsuc (fsuc fzero)))))))))))))))

-- Checked INIT/address-order laws.  The table is arbitrary, so these prove
-- selection rather than merely testing a specially chosen table.

LUT1-low-selects-INIT0 : ∀ init
  → evalLUT1 init low ≡ lookup fzero init
LUT1-low-selects-INIT0 init = refl

LUT1-high-selects-INIT1 : ∀ init
  → evalLUT1 init high ≡ lookup INIT1-of-2 init
LUT1-high-selects-INIT1 init = refl

LUT2-all-low-selects-INIT0 : ∀ init
  → evalLUT2 init low low ≡ lookup fzero init
LUT2-all-low-selects-INIT0 init = refl

LUT2-I0-selects-INIT1 : ∀ init
  → evalLUT2 init high low ≡ lookup INIT1-of-4 init
LUT2-I0-selects-INIT1 init = refl

LUT2-I1-selects-INIT2 : ∀ init
  → evalLUT2 init low high ≡ lookup INIT2-of-4 init
LUT2-I1-selects-INIT2 init = refl

LUT3-all-low-selects-INIT0 : ∀ init
  → evalLUT3 init low low low ≡ lookup fzero init
LUT3-all-low-selects-INIT0 init = refl

LUT3-I0-selects-INIT1 : ∀ init
  → evalLUT3 init high low low ≡ lookup INIT1-of-8 init
LUT3-I0-selects-INIT1 init = refl

LUT3-I2-selects-INIT4 : ∀ init
  → evalLUT3 init low low high ≡ lookup INIT4-of-8 init
LUT3-I2-selects-INIT4 init = refl

LUT4-all-low-selects-INIT0 : ∀ init
  → evalLUT4 init low low low low ≡ lookup fzero init
LUT4-all-low-selects-INIT0 init = refl

LUT4-I0-selects-INIT1 : ∀ init
  → evalLUT4 init high low low low ≡ lookup INIT1-of-16 init
LUT4-I0-selects-INIT1 init = refl

LUT4-I3-selects-INIT8 : ∀ init
  → evalLUT4 init low low low high ≡ lookup INIT8-of-16 init
LUT4-I3-selects-INIT8 init = refl

LUT5-all-low-selects-INIT0 : ∀ init
  → evalLUT5 init low low low low low ≡ lookup fzero init
LUT5-all-low-selects-INIT0 init = refl

LUT5-I0-selects-INIT1 : ∀ init
  → evalLUT5 init high low low low low ≡ lookup INIT1-of-32 init
LUT5-I0-selects-INIT1 init = refl

LUT5-I4-selects-INIT16 : ∀ init
  → evalLUT5 init low low low low high ≡ lookup INIT16-of-32 init
LUT5-I4-selects-INIT16 init = refl

-- The documented default INIT for every entry is all zeros.

defaultLUT1 : LUT1Table
defaultLUT1 = replicate low

defaultLUT2 : LUT2Table
defaultLUT2 = replicate low

defaultLUT3 : LUT3Table
defaultLUT3 = replicate low

defaultLUT4 : LUT4Table
defaultLUT4 = replicate low

defaultLUT5 : LUT5Table
defaultLUT5 = replicate low

LUT1-default-example : evalLUT1 defaultLUT1 high ≡ low
LUT1-default-example = refl

LUT2-default-example : evalLUT2 defaultLUT2 high high ≡ low
LUT2-default-example = refl

LUT3-default-example : evalLUT3 defaultLUT3 high high high ≡ low
LUT3-default-example = refl

LUT4-default-example : evalLUT4 defaultLUT4 high high high high ≡ low
LUT4-default-example = refl

LUT5-default-example :
  evalLUT5 defaultLUT5 high high high high high ≡ low
LUT5-default-example = refl