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

module Spartan6.Primitive.FDSE where

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

-- Source: UG615 v14.7, "FDSE", printed pages 105-106.
--
-- The introduction and logic table on printed page 105 specify a positive-
-- edge D flip-flop with active-high clock enable and active-high synchronous
-- set.  On a rising edge, S=1 sets Q high regardless of CE and D; with S=0,
-- CE=0 holds Q and CE=1 loads D.  Thus synchronous set has priority over CE.
--
-- The attribute table on printed page 105 permits binary INIT values 0 and 1,
-- gives 1 as the default, and recommends 1 to match this element's set
-- polarity.  It says that selecting INIT=0 creates additional asynchronous
-- circuitry.  The template on printed page 106 explicitly demonstrates an
-- INIT=0 override; that does not change the attribute table's stated default.
--
-- This untimed module models the documented logical initial Q value and the
-- idle/rising-edge behavior only.  It does not model configuration, power-on,
-- GSR, timing, or the physical asynchronous circuitry used for INIT=0.

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

fdseLocator : SourceLocator
fdseLocator =
  locate fdsePinnedSource "FDSE"
    "printed page 105: introduction, logic table, and INIT attribute; printed page 106: instantiation templates"

fdseTrace : RuleTraceability
fdseTrace =
  traceRule "primitive.FDSE.two-valued"
            officialDocumentation
            (just fdseLocator)
            partiallySupported
            guaranteed
            "Executable untimed INIT, hold, load, and synchronous-set semantics; raw admission, configuration/GSR, timing, and INIT=0 implementation circuitry are not modelled."

-- Both binary INIT values are documented.  The default and recommended value
-- for FDSE is high.

FDSEInit : Type₀
FDSEInit = Bit

fdseDefaultInit fdseRecommendedInit : FDSEInit
fdseDefaultInit     = high
fdseRecommendedInit = high

fdseInitialQ : FDSEInit → Bit
fdseInitialQ init = init

fdse-default-initial-Q-is-high : fdseInitialQ fdseDefaultInit ≡ high
fdse-default-initial-Q-is-high = refl

fdse-explicit-low-INIT-is-logically-low : fdseInitialQ low ≡ low
fdse-explicit-low-INIT-is-logically-low = refl

-- Next Q at a low-to-high clock transition.  mux selects its final argument
-- when its selector is high, so the outer mux makes set dominate enable.

fdseStep : Bit → Bit → Bit → Bit → Bit
fdseStep data-in enable set current =
  mux set (mux enable current data-in) high

-- The clock port is abstracted to the project's untimed event vocabulary.
-- Set is synchronous: it has no effect during idle.

fdseUpdate : Event → Bit → Bit → Bit → Bit → Bit
fdseUpdate idle       data-in enable set current = current
fdseUpdate risingEdge data-in enable set current =
  fdseStep data-in enable set current

-- Typed next-state expression used by the admitted expression core on a
-- rising edge.  Design-level idle events preserve state without evaluating a
-- next-state expression.

fdseNext : ∀ {inputs registers}
         → Expr inputs registers  -- D
         → Expr inputs registers  -- CE
         → Expr inputs registers  -- S
         → Expr inputs registers  -- current Q
         → Expr inputs registers
fdseNext data-in enable set current =
  select set (select enable current data-in) (constant high)

eval-fdseNext :
  ∀ {inputs registers} external state data-in enable set current
  → eval {inputs} {registers} external state
      (fdseNext data-in enable set current)
  ≡ fdseStep (eval external state data-in)
             (eval external state enable)
             (eval external state set)
             (eval external state current)
eval-fdseNext external state data-in enable set current = refl

-- Checked logic-table laws and event examples.

fdse-set-priority : ∀ data-in enable current
                  → fdseStep data-in enable high current ≡ high
fdse-set-priority data-in enable current = refl

fdse-hold : ∀ data-in current
          → fdseStep data-in low low current ≡ current
fdse-hold data-in current = refl

fdse-load : ∀ data-in current
          → fdseStep data-in high low current ≡ data-in
fdse-load data-in current = refl

fdse-idle-holds : ∀ data-in enable set current
                → fdseUpdate idle data-in enable set current ≡ current
fdse-idle-holds data-in enable set current = refl

fdse-set-is-synchronous : ∀ data-in enable current
                        → fdseUpdate idle data-in enable high current ≡ current
fdse-set-is-synchronous data-in enable current = refl

fdse-rising-set-overrides-disabled-enable : ∀ data-in current
  → fdseUpdate risingEdge data-in low high current ≡ high
fdse-rising-set-overrides-disabled-enable data-in current = refl

fdse-rising-set-overrides-enabled-data : ∀ data-in current
  → fdseUpdate risingEdge data-in high high current ≡ high
fdse-rising-set-overrides-enabled-data data-in current = refl

fdse-rising-disabled-holds : ∀ data-in current
  → fdseUpdate risingEdge data-in low low current ≡ current
fdse-rising-disabled-holds data-in current = refl

fdse-rising-enabled-loads : ∀ data-in current
  → fdseUpdate risingEdge data-in high low current ≡ data-in
fdse-rising-enabled-loads data-in current = refl