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

module Spartan6.Primitive.FDRE where

open import Spartan6.Prelude
open import Spartan6.Netlist.Expression

-- UG615 v14.7 describes FDRE as a positive-edge D flip-flop with clock
-- enable and synchronous reset.  Reset has priority over enable.

fdreStep : Bit → Bit → Bit → Bit → Bit
fdreStep data-in enable reset current =
  mux reset (mux enable current data-in) low

fdreNext : ∀ {inputs registers}
         → Expr inputs registers  -- D
         → Expr inputs registers  -- CE
         → Expr inputs registers  -- R
         → Expr inputs registers  -- current Q
         → Expr inputs registers
fdreNext data-in enable reset current =
  select reset (select enable current data-in) (constant low)

eval-fdreNext : ∀ {inputs registers} external state data-in enable reset current
              → eval {inputs} {registers} external state
                  (fdreNext data-in enable reset current)
              ≡ fdreStep (eval external state data-in)
                         (eval external state enable)
                         (eval external state reset)
                         (eval external state current)
eval-fdreNext external state data-in enable reset current = refl

fdre-reset : ∀ data-in enable current
           → fdreStep data-in enable high current ≡ low
fdre-reset data-in enable current = refl

fdre-hold : ∀ data-in current
          → fdreStep data-in low low current ≡ current
fdre-hold data-in current = refl

fdre-load : ∀ data-in current
          → fdreStep data-in high low current ≡ data-in
fdre-load data-in current = refl