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

module Tutorials.Project02.Main where

open import Spartan6.API.Circuit
open Expression
open FDRE
open Design

-- The two external inputs are clock-enable and synchronous reset.  The clock
-- itself is represented by `Event`: a rising edge is an event, not a Boolean
-- data input.

enableInput resetInput : Expr 2 1
enableInput = input fzero
resetInput = input (fsuc fzero)

storedQ : Expr 2 1
storedQ = register fzero

enabledToggle : Design 2 1 1
enabledToggle =
  mkDesign
    (low ∷ [])
    (storedQ ∷ [])
    (fdreNext (invert storedQ) enableInput resetInput storedQ ∷ [])

enabledNoReset : Vec Bit 2
enabledNoReset = high ∷ low ∷ []

disabledNoReset : Vec Bit 2
disabledNoReset = low ∷ low ∷ []

resetAsserted : Vec Bit 2
resetAsserted = high ∷ high ∷ []

toggle-starts-low : initial enabledToggle ≡ low ∷ []
toggle-starts-low = refl

idle-does-not-clock : ∀ enable reset q
  -> step enabledToggle idle (enable ∷ reset ∷ []) (q ∷ []) ≡ q ∷ []
idle-does-not-clock enable reset q = refl

disabled-edge-holds : ∀ q
  -> step enabledToggle risingEdge disabledNoReset (q ∷ []) ≡ q ∷ []
disabled-edge-holds q = refl

enabled-edge-toggles : ∀ q
  -> step enabledToggle risingEdge enabledNoReset (q ∷ []) ≡ not q ∷ []
enabled-edge-toggles q = refl

reset-has-priority : ∀ q
  -> step enabledToggle risingEdge resetAsserted (q ∷ []) ≡ low ∷ []
reset-has-priority q = refl

enabledEdge : Stimulus 2
enabledEdge = stimulus enabledNoReset risingEdge

twoEnabledEdges : List (Stimulus 2)
twoEnabledEdges = enabledEdge ∷ᴸ enabledEdge ∷ᴸ []ᴸ

two-edges-return-to-initial :
  run enabledToggle (initial enabledToggle) twoEnabledEdges
  ≡ initial enabledToggle
two-edges-return-to-initial = refl

two-edge-trace-shows-pre-state-observation :
  execute enabledToggle (initial enabledToggle) twoEnabledEdges
  ≡ frame (low ∷ []) (low ∷ []) (high ∷ [])
    ∷ᴸ frame (high ∷ []) (high ∷ []) (low ∷ [])
    ∷ᴸ []ᴸ
two-edge-trace-shows-pre-state-observation = refl