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

module Spartan6.Primitive.RAM64X1S where

open import Spartan6.Prelude
open import Spartan6.Evidence
open import Spartan6.Semantics.Design using (Event; idle; risingEdge)

import Spartan6.Foundation.Memory as Memory
import Spartan6.Primitive.LUT as LUT

-- Official sources:
--
-- * UG615 v14.7 (2013-10-02), "RAM64X1S", printed pages 270-271.
--   Page 270 gives the introduction and logic table.  It specifies a
--   positive-edge write when WE is high, hold when WE is low, addressed O,
--   and O=D for the write row.  Page 271 gives the 64-bit hexadecimal INIT
--   attribute, whose documented default is all zeros, and calls the read
--   asynchronous in both HDL templates.
-- * UG384 v1.1, Figure 10 on printed page 19 and "Distributed RAM Data Flow"
--   on printed page 25.  Page 25 specifies a one-edge active-high-WE write
--   and a clock-independent asynchronous addressed read.

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

ug615RAM64X1SLocator : SourceLocator
ug615RAM64X1SLocator =
  locate ug615RAM64X1SSource "RAM64X1S"
    "printed pages 270-271: introduction, logic table, INIT attribute, and HDL templates"

ug384DistributedRAMSource : PinnedSource
ug384DistributedRAMSource =
  pinSource UG384 (revision "v1.1" (just "2010-02-22"))

ug384DistributedRAMLocator : SourceLocator
ug384DistributedRAMLocator =
  locate ug384DistributedRAMSource "Distributed RAM"
    "Figure 10 on printed page 19; synchronous write and asynchronous read on printed page 25"

ram64x1sTrace : RuleTraceability
ram64x1sTrace =
  traceRule "primitive.RAM64X1S.two-valued"
            officialDocumentation
            (just ug615RAM64X1SLocator)
            partiallySupported
            guaranteed
            "Executable two-valued addressed read, hold, enabled rising-edge write, post-write O=D, and all-zero default INIT; physical timing and raw hexadecimal INIT decoding are outside this module."

ram64x1sDataFlowTrace : RuleTraceability
ram64x1sDataFlowTrace =
  traceRule "primitive.RAM64X1S.distributed-data-flow"
            officialDocumentation
            (just ug384DistributedRAMLocator)
            fullySupported
            guaranteed
            "The admitted subset models a single-edge active-high-WE write and a clock-independent asynchronous addressed read."

RAM64X1SState : Type₀
RAM64X1SState = Memory.Memory  

-- Address vector order follows the primitive port order shown in UG615:
--
--   A0 ∷ A1 ∷ A2 ∷ A3 ∷ A4 ∷ A5 ∷ []
--
-- Thus the head A0 is least significant and A5 is most significant.

RAM64X1SAddress : Type₀
RAM64X1SAddress = Vec Bit 

addressIndex : RAM64X1SAddress → Fin 
addressIndex = LUT.address

wordBit : Word  → Bit
wordBit (bit ∷ []) = bit

-- O is purely a function of the current state and address.  It deliberately
-- has no Event, WE, D, or clock argument, expressing the documented
-- asynchronous and clock-independent read.

readRAM64X1S : RAM64X1SState → RAM64X1SAddress → Bit
readRAM64X1S state address =
  wordBit (Memory.read (addressIndex address) state)

-- WCLK is abstracted to Event.  idle covers every observation with no
-- positive transition, including static clock levels and falling edges.

updateRAM64X1S :
  Event → Bit → RAM64X1SAddress → Bit → RAM64X1SState → RAM64X1SState
updateRAM64X1S idle       write-enable address data-in state = state
updateRAM64X1S risingEdge write-enable address data-in state =
  Memory.writeIf write-enable (addressIndex address) (data-in ∷ []) state

-- UG615 documents arbitrary 64-bit INIT values, but the cited RAM64X1S entry
-- does not give a raw hexadecimal bit-to-address decoding table.  Callers may
-- provide an already address-indexed state.  Only the all-zero raw default is
-- constructed here without an external decoding assumption.

defaultInitialState : RAM64X1SState
defaultInitialState = replicate (low ∷ [])

-- Explicit support classification for boundary cases.

data RAM64X1SBoundary : Type₀ where
  sameAddressReadDuringWrite : RAM64X1SBoundary
  defaultINIT                : RAM64X1SBoundary
  rawHexINITDecoding         : RAM64X1SBoundary
  unstableWriteEdgeInputs    : RAM64X1SBoundary

boundarySupport : RAM64X1SBoundary → SupportStatus
boundarySupport sameAddressReadDuringWrite = fullySupported
boundarySupport defaultINIT                = fullySupported
boundarySupport rawHexINITDecoding         = planned
boundarySupport unstableWriteEdgeInputs    = unsupportedFeature

boundarySemantics : RAM64X1SBoundary → SemanticStatus
boundarySemantics sameAddressReadDuringWrite = guaranteed
boundarySemantics defaultINIT                = guaranteed
boundarySemantics rawHexINITDecoding         = unsupportedSemantics
boundarySemantics unstableWriteEdgeInputs    = insufficientEvidence

boundaryNote : RAM64X1SBoundary → String
boundaryNote sameAddressReadDuringWrite =
  "UG615 page 270 gives O=D on the enabled rising-edge write row; the model exposes that post-edge value."
boundaryNote defaultINIT =
  "UG615 page 271 gives all zeros as the default value of the 64-bit INIT attribute."
boundaryNote rawHexINITDecoding =
  "The cited sections do not provide a raw hexadecimal bit-to-address decoding table; admission must supply address-indexed contents."
boundaryNote unstableWriteEdgeInputs =
  "Setup/hold violations and physical edge collisions are outside the untimed model and have no invented two-valued result."

allLowAddress : RAM64X1SAddress
allLowAddress = low ∷ low ∷ low ∷ low ∷ low ∷ low ∷ []

onlyA0HighAddress : RAM64X1SAddress
onlyA0HighAddress = high ∷ low ∷ low ∷ low ∷ low ∷ low ∷ []

A0-is-least-significant : addressIndex onlyA0HighAddress ≡ fsuc fzero
A0-is-least-significant = refl

all-low-is-address-zero : addressIndex allLowAddress ≡ fzero
all-low-is-address-zero = refl

-- Logic-table hold rows.

no-rising-edge-holds : ∀ write-enable address data-in state
  → updateRAM64X1S idle write-enable address data-in state ≡ state
no-rising-edge-holds write-enable address data-in state = refl

disabled-rising-edge-holds : ∀ address data-in state
  → updateRAM64X1S risingEdge low address data-in state ≡ state
disabled-rising-edge-holds address data-in state = refl

disabled-rising-edge-preserves-read : ∀ read-address write-address data-in state
  → readRAM64X1S
      (updateRAM64X1S risingEdge low write-address data-in state)
      read-address
  ≡ readRAM64X1S state read-address
disabled-rising-edge-preserves-read read-address write-address data-in state =
  refl

-- The enabled write rule and UG615's O=D write row.

enabled-rising-edge-writes : ∀ address data-in state
  → updateRAM64X1S risingEdge high address data-in state
  ≡ Memory.write (addressIndex address) (data-in ∷ []) state
enabled-rising-edge-writes address data-in state = refl

write-edge-output-is-D : ∀ address data-in state
  → readRAM64X1S
      (updateRAM64X1S risingEdge high address data-in state)
      address
  ≡ data-in
write-edge-output-is-D address data-in state =
  cong wordBit
    (Memory.read-after-write-same
      (addressIndex address) (data-in ∷ []) state)

-- A small generic fact is enough to check every address of the documented
-- all-zero default without enumerating 64 cases.

lookup-replicate : ∀ {ℓ n} {A : Type ℓ} (index : Fin n) (value : A)
  → lookup index (replicate value) ≡ value
lookup-replicate fzero value = refl
lookup-replicate (fsuc index) value = lookup-replicate index value

default-output-is-low : ∀ address
  → readRAM64X1S defaultInitialState address ≡ low
default-output-is-low address =
  cong wordBit
    (lookup-replicate (addressIndex address) (low ∷ []))

-- Address changes are immediately reflected by readRAM64X1S; no event is
-- needed.  This state differs only at address 1.

exampleState : RAM64X1SState
exampleState =
  Memory.write (addressIndex onlyA0HighAddress) (high ∷ [])
               defaultInitialState

asynchronous-read-address-zero :
  readRAM64X1S exampleState allLowAddress ≡ low
asynchronous-read-address-zero = refl

asynchronous-read-address-one :
  readRAM64X1S exampleState onlyA0HighAddress ≡ high
asynchronous-read-address-one = refl

write-address-one-read-after-write :
  readRAM64X1S
    (updateRAM64X1S risingEdge high onlyA0HighAddress high
      defaultInitialState)
    onlyA0HighAddress
  ≡ high
write-address-one-read-after-write = refl

same-address-write-read-is-supported :
  fullySupported? (boundarySupport sameAddressReadDuringWrite) ≡ true
same-address-write-read-is-supported = refl

raw-INIT-decoding-is-not-executable :
  executable? (boundarySemantics rawHexINITDecoding) ≡ false
raw-INIT-decoding-is-not-executable = refl