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

module Spartan6.Primitive.RAM32X1S 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

-- Source: UG615 v14.7, "RAM32X1S", printed pages 257-258.
--
-- Printed page 257 specifies a 32-word by one-bit memory.  WE low ignores
-- WCLK transitions; WE high writes D to the A4-A0-selected word on a
-- low-to-high WCLK transition.  O is the data stored at the selected address,
-- and the enabled rising-edge write row of the logic table gives O=D.  The
-- same page gives a 32-bit INIT attribute whose default is all zeros.  Printed
-- page 258 gives the positive-edge-write, asynchronous-read HDL templates and
-- labels A0 through A4 as address bits 0 through 4.
--
-- This module is an untimed, two-valued model of only that positive-edge,
-- single-port subset.  It does not model RAM32X1S_1, an externally inverted
-- clock, setup/hold behavior, delay, unstable edge inputs, placement, or
-- electrical behavior.  UG615's entry does not provide a hexadecimal
-- INIT-bit-to-address decoding table, so arbitrary raw INIT decoding is not
-- claimed; callers may supply already address-indexed contents, and only the
-- unambiguous all-zero default is constructed here.

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

ram32x1sLocator : SourceLocator
ram32x1sLocator =
  locate ram32x1sPinnedSource "RAM32X1S"
    "printed page 257: introduction, logic table, and INIT attribute; printed page 258: positive-edge-write asynchronous-read templates"

ram32x1sTrace : RuleTraceability
ram32x1sTrace =
  traceRule "primitive.RAM32X1S.two-valued"
            officialDocumentation
            (just ram32x1sLocator)
            partiallySupported
            guaranteed
            "Executable addressed asynchronous read, hold, enabled rising-edge write, post-write O=D, and all-zero default INIT; raw hexadecimal INIT decoding and physical timing are not modelled."

RAM32X1SState : Type₀
RAM32X1SState = Memory.Memory  

-- Runtime address order follows the port labels on printed page 258:
--
--   A0 ∷ A1 ∷ A2 ∷ A3 ∷ A4 ∷ []
--
-- A0 is address bit 0 (least significant), and A4 is address bit 4.

RAM32X1SAddress : Type₀
RAM32X1SAddress = Vec Bit 

addressIndex : RAM32X1SAddress → Fin 
addressIndex = LUT.address

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

-- O depends only on current addressed contents.  No clock, event, WE, or D
-- argument is needed, expressing the documented asynchronous read.

readRAM32X1S : RAM32X1SState → RAM32X1SAddress → Bit
readRAM32X1S state address =
  wordBit (Memory.read (addressIndex address) state)

-- WCLK is represented by the project's abstract event.  idle covers static
-- levels, falling edges, and every other observation with no positive edge.

updateRAM32X1S :
  Event → Bit → RAM32X1SAddress → Bit → RAM32X1SState → RAM32X1SState
updateRAM32X1S idle       write-enable address data-in state = state
updateRAM32X1S risingEdge write-enable address data-in state =
  Memory.writeIf write-enable (addressIndex address) (data-in ∷ []) state

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

-- Boundary classifications make the supported write row and unsupported
-- physical/raw-data cases explicit.

data RAM32X1SBoundary : Type₀ where
  sameAddressPostWriteOutput : RAM32X1SBoundary
  defaultINIT                : RAM32X1SBoundary
  rawHexINITDecoding         : RAM32X1SBoundary
  unstableWriteEdgeInputs    : RAM32X1SBoundary

boundarySupport : RAM32X1SBoundary → SupportStatus
boundarySupport sameAddressPostWriteOutput = fullySupported
boundarySupport defaultINIT                = fullySupported
boundarySupport rawHexINITDecoding         = planned
boundarySupport unstableWriteEdgeInputs    = unsupportedFeature

boundarySemantics : RAM32X1SBoundary → SemanticStatus
boundarySemantics sameAddressPostWriteOutput = guaranteed
boundarySemantics defaultINIT                = guaranteed
boundarySemantics rawHexINITDecoding         = unsupportedSemantics
boundarySemantics unstableWriteEdgeInputs    = insufficientEvidence

boundaryNote : RAM32X1SBoundary → String
boundaryNote sameAddressPostWriteOutput =
  "UG615 printed page 257 gives O=D on an enabled rising-edge write; the model exposes that post-update value."
boundaryNote defaultINIT =
  "UG615 printed page 257 gives all zeros as the default 32-bit INIT value."
boundaryNote rawHexINITDecoding =
  "The cited entry gives no raw hexadecimal bit-to-address table; import must supply address-indexed contents."
boundaryNote unstableWriteEdgeInputs =
  "The source requires stable address and data for predictable physical performance; setup/hold and unstable-edge outcomes are outside this untimed model."

-- Checked runtime address order.

allLowAddress : RAM32X1SAddress
allLowAddress = low ∷ low ∷ low ∷ low ∷ low ∷ []

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

onlyA4HighAddress : RAM32X1SAddress
onlyA4HighAddress = low ∷ low ∷ low ∷ low ∷ high ∷ []

address16 : Fin 
address16 =
  fsuc (fsuc (fsuc (fsuc (fsuc (fsuc (fsuc (fsuc
    (fsuc (fsuc (fsuc (fsuc (fsuc (fsuc (fsuc (fsuc fzero)))))))))))))))

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

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

A4-has-weight-sixteen : addressIndex onlyA4HighAddress ≡ address16
A4-has-weight-sixteen = refl

-- Checked hold and enabled-write laws.

no-rising-edge-holds : ∀ write-enable address data-in state
  → updateRAM32X1S 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
  → updateRAM32X1S 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
  → readRAM32X1S
      (updateRAM32X1S risingEdge low write-address data-in state)
      read-address
  ≡ readRAM32X1S state read-address
disabled-rising-edge-preserves-read read-address write-address data-in state =
  refl

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

-- This is the source-backed O=D row interpreted after the simultaneous write
-- update.  It is not a claim about analogue values during the physical edge.

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

-- All-zero default INIT, for every address, without assuming a raw hexadecimal
-- decoding convention for non-default values.

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
  → readRAM32X1S defaultInitialState address ≡ low
default-output-is-low address =
  cong wordBit
    (lookup-replicate (addressIndex address) (low ∷ []))

-- Address changes affect the asynchronous output without an event.  This
-- example state differs from the default only at address 1.

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

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

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

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

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

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