{-# OPTIONS --safe --cubical #-}
module Spartan6.Architecture.Primitive where
open import Spartan6.Prelude
open import Spartan6.Evidence
data PrimitiveKind : Type₀ where
LUT1 : PrimitiveKind
LUT2 : PrimitiveKind
LUT3 : PrimitiveKind
LUT4 : PrimitiveKind
LUT5 : PrimitiveKind
LUT6 : PrimitiveKind
MUXF7 : PrimitiveKind
MUXF8 : PrimitiveKind
CARRY4 : PrimitiveKind
FDRE : PrimitiveKind
FDSE : PrimitiveKind
SRL16E : PrimitiveKind
RAM64X1S : PrimitiveKind
IBUF : PrimitiveKind
OBUF : PrimitiveKind
OBUFDS : PrimitiveKind
OBUFT : PrimitiveKind
BUFG : PrimitiveKind
BUFGCE : PrimitiveKind
ones : ℕ → List ℕ
ones zero = []ᴸ
ones (suc n) = 1 ∷ᴸ ones n
record PortSpecification : Type₀ where
constructor portSpecification
field
canonicalPortName : String
canonicalPortWidth : ℕ
open PortSpecification public
scalarPort : String → PortSpecification
scalarPort name = portSpecification name 1
inputPortSpecifications : PrimitiveKind → List PortSpecification
inputPortSpecifications LUT1 = scalarPort "I0" ∷ᴸ []ᴸ
inputPortSpecifications LUT2 =
scalarPort "I0" ∷ᴸ scalarPort "I1" ∷ᴸ []ᴸ
inputPortSpecifications LUT3 =
scalarPort "I0" ∷ᴸ scalarPort "I1" ∷ᴸ scalarPort "I2" ∷ᴸ []ᴸ
inputPortSpecifications LUT4 =
scalarPort "I0" ∷ᴸ scalarPort "I1" ∷ᴸ scalarPort "I2"
∷ᴸ scalarPort "I3" ∷ᴸ []ᴸ
inputPortSpecifications LUT5 =
scalarPort "I0" ∷ᴸ scalarPort "I1" ∷ᴸ scalarPort "I2"
∷ᴸ scalarPort "I3" ∷ᴸ scalarPort "I4" ∷ᴸ []ᴸ
inputPortSpecifications LUT6 =
scalarPort "I0" ∷ᴸ scalarPort "I1" ∷ᴸ scalarPort "I2"
∷ᴸ scalarPort "I3" ∷ᴸ scalarPort "I4" ∷ᴸ scalarPort "I5" ∷ᴸ []ᴸ
inputPortSpecifications MUXF7 =
scalarPort "I0" ∷ᴸ scalarPort "I1" ∷ᴸ scalarPort "S" ∷ᴸ []ᴸ
inputPortSpecifications MUXF8 =
scalarPort "I0" ∷ᴸ scalarPort "I1" ∷ᴸ scalarPort "S" ∷ᴸ []ᴸ
inputPortSpecifications CARRY4 =
scalarPort "CI" ∷ᴸ scalarPort "CYINIT"
∷ᴸ portSpecification "DI" 4 ∷ᴸ portSpecification "S" 4 ∷ᴸ []ᴸ
inputPortSpecifications FDRE =
scalarPort "D" ∷ᴸ scalarPort "C" ∷ᴸ scalarPort "CE"
∷ᴸ scalarPort "R" ∷ᴸ []ᴸ
inputPortSpecifications FDSE =
scalarPort "D" ∷ᴸ scalarPort "C" ∷ᴸ scalarPort "CE"
∷ᴸ scalarPort "S" ∷ᴸ []ᴸ
inputPortSpecifications SRL16E =
portSpecification "A" 4 ∷ᴸ scalarPort "D" ∷ᴸ scalarPort "CLK"
∷ᴸ scalarPort "CE" ∷ᴸ []ᴸ
inputPortSpecifications RAM64X1S =
portSpecification "A" 6 ∷ᴸ scalarPort "D" ∷ᴸ scalarPort "WCLK"
∷ᴸ scalarPort "WE" ∷ᴸ []ᴸ
inputPortSpecifications IBUF = scalarPort "I" ∷ᴸ []ᴸ
inputPortSpecifications OBUF = scalarPort "I" ∷ᴸ []ᴸ
inputPortSpecifications OBUFDS = scalarPort "I" ∷ᴸ []ᴸ
inputPortSpecifications OBUFT =
scalarPort "I" ∷ᴸ scalarPort "T" ∷ᴸ []ᴸ
inputPortSpecifications BUFG = scalarPort "I" ∷ᴸ []ᴸ
inputPortSpecifications BUFGCE =
scalarPort "I" ∷ᴸ scalarPort "CE" ∷ᴸ []ᴸ
outputPortSpecifications : PrimitiveKind → List PortSpecification
outputPortSpecifications LUT1 = scalarPort "O" ∷ᴸ []ᴸ
outputPortSpecifications LUT2 = scalarPort "O" ∷ᴸ []ᴸ
outputPortSpecifications LUT3 = scalarPort "O" ∷ᴸ []ᴸ
outputPortSpecifications LUT4 = scalarPort "O" ∷ᴸ []ᴸ
outputPortSpecifications LUT5 = scalarPort "O" ∷ᴸ []ᴸ
outputPortSpecifications LUT6 = scalarPort "O" ∷ᴸ []ᴸ
outputPortSpecifications MUXF7 = scalarPort "O" ∷ᴸ []ᴸ
outputPortSpecifications MUXF8 = scalarPort "O" ∷ᴸ []ᴸ
outputPortSpecifications CARRY4 =
portSpecification "O" 4 ∷ᴸ portSpecification "CO" 4 ∷ᴸ []ᴸ
outputPortSpecifications FDRE = scalarPort "Q" ∷ᴸ []ᴸ
outputPortSpecifications FDSE = scalarPort "Q" ∷ᴸ []ᴸ
outputPortSpecifications SRL16E = scalarPort "Q" ∷ᴸ []ᴸ
outputPortSpecifications RAM64X1S = scalarPort "O" ∷ᴸ []ᴸ
outputPortSpecifications IBUF = scalarPort "O" ∷ᴸ []ᴸ
outputPortSpecifications OBUF = scalarPort "O" ∷ᴸ []ᴸ
outputPortSpecifications OBUFDS =
scalarPort "O" ∷ᴸ scalarPort "OB" ∷ᴸ []ᴸ
outputPortSpecifications OBUFT = scalarPort "O" ∷ᴸ []ᴸ
outputPortSpecifications BUFG = scalarPort "O" ∷ᴸ []ᴸ
outputPortSpecifications BUFGCE = scalarPort "O" ∷ᴸ []ᴸ
inputPortWidths : PrimitiveKind → List ℕ
inputPortWidths kind =
mapList canonicalPortWidth (inputPortSpecifications kind)
outputPortWidths : PrimitiveKind → List ℕ
outputPortWidths kind =
mapList canonicalPortWidth (outputPortSpecifications kind)
inputPortNames : PrimitiveKind → List String
inputPortNames kind =
mapList canonicalPortName (inputPortSpecifications kind)
outputPortNames : PrimitiveKind → List String
outputPortNames kind =
mapList canonicalPortName (outputPortSpecifications kind)
inputPortCount : PrimitiveKind → ℕ
inputPortCount kind = lengthList (inputPortWidths kind)
outputPortCount : PrimitiveKind → ℕ
outputPortCount kind = lengthList (outputPortWidths kind)
stateBitCount : PrimitiveKind → ℕ
stateBitCount LUT1 = 0
stateBitCount LUT2 = 0
stateBitCount LUT3 = 0
stateBitCount LUT4 = 0
stateBitCount LUT5 = 0
stateBitCount LUT6 = 0
stateBitCount MUXF7 = 0
stateBitCount MUXF8 = 0
stateBitCount CARRY4 = 0
stateBitCount FDRE = 1
stateBitCount FDSE = 1
stateBitCount SRL16E = 16
stateBitCount RAM64X1S = 64
stateBitCount IBUF = 0
stateBitCount OBUF = 0
stateBitCount OBUFDS = 0
stateBitCount OBUFT = 0
stateBitCount BUFG = 0
stateBitCount BUFGCE = 0
kindSupport : PrimitiveKind → SupportStatus
kindSupport LUT1 = partiallySupported
kindSupport LUT2 = partiallySupported
kindSupport LUT3 = partiallySupported
kindSupport LUT4 = partiallySupported
kindSupport LUT5 = partiallySupported
kindSupport LUT6 = partiallySupported
kindSupport MUXF7 = partiallySupported
kindSupport MUXF8 = partiallySupported
kindSupport CARRY4 = partiallySupported
kindSupport FDRE = partiallySupported
kindSupport FDSE = partiallySupported
kindSupport SRL16E = partiallySupported
kindSupport RAM64X1S = partiallySupported
kindSupport IBUF = partiallySupported
kindSupport OBUF = partiallySupported
kindSupport OBUFDS = partiallySupported
kindSupport OBUFT = partiallySupported
kindSupport BUFG = partiallySupported
kindSupport BUFGCE = partiallySupported
kindSemantics : PrimitiveKind → SemanticStatus
kindSemantics LUT1 = guaranteed
kindSemantics LUT2 = guaranteed
kindSemantics LUT3 = guaranteed
kindSemantics LUT4 = guaranteed
kindSemantics LUT5 = guaranteed
kindSemantics LUT6 = guaranteed
kindSemantics MUXF7 = guaranteed
kindSemantics MUXF8 = guaranteed
kindSemantics CARRY4 = guaranteedConditionally
kindSemantics FDRE = guaranteed
kindSemantics FDSE = guaranteed
kindSemantics SRL16E = guaranteed
kindSemantics RAM64X1S = guaranteed
kindSemantics IBUF = guaranteed
kindSemantics OBUF = guaranteed
kindSemantics OBUFDS = guaranteed
kindSemantics OBUFT = guaranteedConditionally
kindSemantics BUFG = guaranteed
kindSemantics BUFGCE = guaranteed
ug615-v14-7 : PinnedSource
ug615-v14-7 =
pinSource UG615 (revision "v14.7" (just "2013-10-02"))
ug384-v1-1 : PinnedSource
ug384-v1-1 =
pinSource UG384 (revision "v1.1" (just "2010-02-22"))
lut1Locator lut2Locator lut3Locator lut4Locator lut5Locator : SourceLocator
lut1Locator =
locate ug615-v14-7 "LUT1"
"printed pages 148-149: logic table, INIT attribute, and templates"
lut2Locator =
locate ug615-v14-7 "LUT2"
"printed pages 154-155: logic table, INIT attribute, and templates"
lut3Locator =
locate ug615-v14-7 "LUT3"
"printed pages 160-161: logic table, INIT attribute, and templates"
lut4Locator =
locate ug615-v14-7 "LUT4"
"printed pages 166-168: logic table, ports, INIT attribute, and templates"
lut5Locator =
locate ug615-v14-7 "LUT5"
"printed pages 175-177: logic table, ports, INIT attribute, and templates"
lut6Locator : SourceLocator
lut6Locator =
locate ug615-v14-7 "LUT6" "pages 186-189"
muxf7Locator : SourceLocator
muxf7Locator =
locate ug615-v14-7 "MUXF7" "PDF and printed page 204 logic table"
muxf8Locator : SourceLocator
muxf8Locator =
locate ug615-v14-7 "MUXF8" "PDF and printed page 210 logic table"
carry4Locator : SourceLocator
carry4Locator =
locate ug615-v14-7 "CARRY4"
"printed pages 74-75: schematic, port table, and HDL templates"
fdreLocator : SourceLocator
fdreLocator =
locate ug615-v14-7 "FDRE"
"PDF page 102 (printed page 103) logic table; printed page 104 template"
fdseLocator : SourceLocator
fdseLocator =
locate ug615-v14-7 "FDSE"
"printed page 105: introduction, logic table, and INIT attribute; printed page 106 templates"
srl16eLocator : SourceLocator
srl16eLocator =
locate ug615-v14-7 "SRL16E"
"printed pages 308-309: logic table, ports, and INIT attribute"
ram64x1sLocator : SourceLocator
ram64x1sLocator =
locate ug615-v14-7 "RAM64X1S"
"printed pages 270-271: logic table, asynchronous read, and INIT default"
ibufLocator : SourceLocator
ibufLocator = locate ug615-v14-7 "IBUF" "printed pages 109-110"
obufLocator : SourceLocator
obufLocator = locate ug615-v14-7 "OBUF" "printed pages 216-217"
obufdsLocator : SourceLocator
obufdsLocator = locate ug615-v14-7 "OBUFDS" "printed page 218 logic table"
obuftLocator : SourceLocator
obuftLocator = locate ug615-v14-7 "OBUFT" "printed pages 220-221 logic table"
bufgLocator : SourceLocator
bufgLocator = locate ug615-v14-7 "BUFG" "printed pages 53-54"
bufgceLocator : SourceLocator
bufgceLocator = locate ug615-v14-7 "BUFGCE" "printed page 55 logic table"
lutTraceNote : String
lutTraceNote =
"Executable INIT truth-table semantics and exact canonical LUT1-LUT6 hexadecimal decoding are implemented, with scheduler-certified pure/mixed raw translation and exact-design admission. Kind-wide architecture-profile admission remains incomplete."
fdreTraceNote : String
fdreTraceNote =
"Executable two-valued transition semantics covers reset priority, enable, hold, and documented INIT values. Canonical scalar INIT and witnessed single-clock single/pure-multiple/mixed translators feed exact-design admission; kind-wide profile admission remains incomplete and timing is not modeled."
fdseTraceNote : String
fdseTraceNote =
"Executable two-valued transition semantics covers synchronous-set priority, enable, hold, and documented INIT values. Witnessed single-clock single/pure-multiple/mixed translators feed exact-design admission; kind-wide profile admission remains incomplete, and timing and configuration/GSR are not modeled."
lut1Trace : RuleTraceability
lut1Trace =
traceRule "primitive.LUT1.two-valued-init"
officialDocumentation
(just lut1Locator)
partiallySupported
guaranteed
"General-output INIT selection, range-checked canonical two-bit decoding, and restricted raw translation are executable; macro expansion, packing, routing, and full admission remain incomplete."
lut2Trace : RuleTraceability
lut2Trace =
traceRule "primitive.LUT2.two-valued-init"
officialDocumentation
(just lut2Locator)
partiallySupported
guaranteed
"General-output INIT selection, exact canonical decoding, and restricted raw translation are executable; macro expansion, packing, routing, and full admission remain incomplete."
lut3Trace : RuleTraceability
lut3Trace =
traceRule "primitive.LUT3.two-valued-init"
officialDocumentation
(just lut3Locator)
partiallySupported
guaranteed
"General-output INIT selection, exact canonical decoding, and restricted raw translation are executable; macro expansion, packing, routing, and full admission remain incomplete."
lut4Trace : RuleTraceability
lut4Trace =
traceRule "primitive.LUT4.two-valued-init"
officialDocumentation
(just lut4Locator)
partiallySupported
guaranteed
"General-output INIT selection, exact canonical decoding, and restricted raw translation are executable; macro expansion, packing, routing, and full admission remain incomplete."
lut5Trace : RuleTraceability
lut5Trace =
traceRule "primitive.LUT5.two-valued-init"
officialDocumentation
(just lut5Locator)
partiallySupported
guaranteed
"General-output INIT selection, exact canonical decoding, and restricted raw translation are executable; LUT6 packing/dual outputs, routing, and full admission remain incomplete."
lut6Trace : RuleTraceability
lut6Trace =
traceRule "primitive.LUT6.two-valued-init"
officialDocumentation
(just lut6Locator)
partiallySupported
guaranteed
lutTraceNote
fdreTrace : RuleTraceability
fdreTrace =
traceRule "primitive.FDRE.two-valued"
officialDocumentation
(just fdreLocator)
partiallySupported
guaranteed
fdreTraceNote
fdseTrace : RuleTraceability
fdseTrace =
traceRule "primitive.FDSE.two-valued"
officialDocumentation
(just fdseLocator)
partiallySupported
guaranteed
fdseTraceNote
muxf7Trace : RuleTraceability
muxf7Trace =
traceRule "primitive.MUXF7.two-valued"
officialDocumentation
(just muxf7Locator)
partiallySupported
guaranteed
"Two-valued Low/High selection, proved parameterless decoding, scheduler-certified raw translation, and exact-design admission are executable; kind-wide admission and routing restrictions remain incomplete."
muxf8Trace : RuleTraceability
muxf8Trace =
traceRule "primitive.MUXF8.two-valued"
officialDocumentation
(just muxf8Locator)
partiallySupported
guaranteed
"Two-valued Low/High selection, proved parameterless decoding, scheduler-certified raw translation, and exact-design admission are executable; kind-wide admission and routing restrictions remain incomplete."
carry4Trace : RuleTraceability
carry4Trace =
traceRule "primitive.CARRY4.two-valued"
officialDocumentation
(just carry4Locator)
partiallySupported
guaranteedConditionally
"The four two-valued carry stages and an isolated witnessed raw builder are executable when the nonselected CI/CYINIT source is literally low; unified admission remains incomplete and simultaneous raw-source interpretation is rejected."
srl16eTrace : RuleTraceability
srl16eTrace =
traceRule "primitive.SRL16E.two-valued"
officialDocumentation
(just srl16eLocator)
partiallySupported
guaranteed
"The 16-bit state, addressed read, hold, and enabled rising-edge shift are executable; raw INIT decoding and netlist admission remain incomplete."
ram64x1sTrace : RuleTraceability
ram64x1sTrace =
traceRule "primitive.RAM64X1S.two-valued" officialDocumentation
(just ram64x1sLocator) partiallySupported guaranteed
"The asynchronous addressed read and enabled rising-edge write are executable; non-default raw INIT decoding and netlist admission remain incomplete."
ibufTrace : RuleTraceability
ibufTrace =
traceRule "primitive.IBUF.two-valued" officialDocumentation
(just ibufLocator) partiallySupported guaranteed
"The one-bit digital buffer rule and a restricted parameterless raw alias translation are executable; electrical I/O attributes and full admission remain outside this subset."
obufTrace : RuleTraceability
obufTrace =
traceRule "primitive.OBUF.two-valued" officialDocumentation
(just obufLocator) partiallySupported guaranteed
"The one-bit constantly-driven rule and a restricted parameterless raw alias translation are executable; electrical drive attributes and full admission remain outside this subset."
obufdsTrace : RuleTraceability
obufdsTrace =
traceRule "primitive.OBUFDS.two-valued" officialDocumentation
(just obufdsLocator) partiallySupported guaranteed
"The complementary two-valued output pair and an isolated witnessed raw builder are executable; unified admission and differential electrical behavior are not modeled."
obuftTrace : RuleTraceability
obuftTrace =
traceRule "primitive.OBUFT.drive-contract" officialDocumentation
(just obuftLocator) partiallySupported guaranteedConditionally
"The output is either a driven Bit or explicit high impedance; multi-driver resolution and electrical behavior are not modeled."
bufgTrace : RuleTraceability
bufgTrace =
traceRule "primitive.BUFG.untimed" officialDocumentation
(just bufgLocator) partiallySupported guaranteed
"Identity transport and a restricted parameterless raw alias translation are modeled; routing, skew, timing, and full admission are excluded."
bufgceTrace : RuleTraceability
bufgceTrace =
traceRule "primitive.BUFGCE.untimed" officialDocumentation
(just bufgceLocator) partiallySupported guaranteed
"CE-low suppression, CE-high transport, and a restricted raw translation are executable; physical clock gating behavior and full admission are excluded."
kindTraceability : PrimitiveKind → RuleTraceability
kindTraceability LUT1 = lut1Trace
kindTraceability LUT2 = lut2Trace
kindTraceability LUT3 = lut3Trace
kindTraceability LUT4 = lut4Trace
kindTraceability LUT5 = lut5Trace
kindTraceability LUT6 = lut6Trace
kindTraceability MUXF7 = muxf7Trace
kindTraceability MUXF8 = muxf8Trace
kindTraceability CARRY4 = carry4Trace
kindTraceability FDRE = fdreTrace
kindTraceability FDSE = fdseTrace
kindTraceability SRL16E = srl16eTrace
kindTraceability RAM64X1S = ram64x1sTrace
kindTraceability IBUF = ibufTrace
kindTraceability OBUF = obufTrace
kindTraceability OBUFDS = obufdsTrace
kindTraceability OBUFT = obuftTrace
kindTraceability BUFG = bufgTrace
kindTraceability BUFGCE = bufgceTrace
LUT6-input-count : inputPortCount LUT6 ≡ 6
LUT6-input-count = refl
LUT6-input-names :
inputPortNames LUT6
≡ "I0" ∷ᴸ "I1" ∷ᴸ "I2" ∷ᴸ "I3" ∷ᴸ "I4" ∷ᴸ "I5" ∷ᴸ []ᴸ
LUT6-input-names = refl
FDRE-input-count : inputPortCount FDRE ≡ 4
FDRE-input-count = refl
FDSE-input-count : inputPortCount FDSE ≡ 4
FDSE-input-count = refl
FDRE-port-names :
inputPortNames FDRE ≡ "D" ∷ᴸ "C" ∷ᴸ "CE" ∷ᴸ "R" ∷ᴸ []ᴸ
FDRE-port-names = refl
FDSE-port-names :
inputPortNames FDSE ≡ "D" ∷ᴸ "C" ∷ᴸ "CE" ∷ᴸ "S" ∷ᴸ []ᴸ
FDSE-port-names = refl
FDRE-state-count : stateBitCount FDRE ≡ 1
FDRE-state-count = refl
FDSE-state-count : stateBitCount FDSE ≡ 1
FDSE-state-count = refl
FDRE-is-not-yet-fully-supported : fullySupported? (kindSupport FDRE) ≡ false
FDRE-is-not-yet-fully-supported = refl
LUT6-has-guaranteed-semantics : executable? (kindSemantics LUT6) ≡ true
LUT6-has-guaranteed-semantics = refl
FDRE-trace-is-official : traceOfficial? (kindTraceability FDRE) ≡ true
FDRE-trace-is-official = refl