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

module Spartan6.Examples.Toggle where

open import Spartan6.Prelude
open import Spartan6.Netlist.Expression
open import Spartan6.Primitive.FDRE
open import Spartan6.Semantics.Design

resetInput : Expr  
resetInput = input fzero

qRegister : Expr  
qRegister = register fzero

-- A one-bit toggle register implemented as an FDRE.  Its synchronous reset is
-- the sole external input; Q is the sole output.

toggle : Design   
toggle =
  mkDesign
    (low ∷ [])
    (qRegister ∷ [])
    (fdreNext (invert qRegister)
              (constant high)
              resetInput
              qRegister
     ∷ [])

noResetTick : Stimulus 
noResetTick = stimulus (low ∷ []) risingEdge

resetTick : Stimulus 
resetTick = stimulus (high ∷ []) risingEdge

initial-is-low : initial toggle ≡ low ∷ []
initial-is-low = refl

observation-is-q : ∀ reset q
                 → observe toggle (reset ∷ []) (q ∷ []) ≡ q ∷ []
observation-is-q reset q = refl

idle-preserves-q : ∀ reset q
                 → step toggle idle (reset ∷ []) (q ∷ []) ≡ q ∷ []
idle-preserves-q reset q = refl

reset-clears : ∀ q
             → step toggle risingEdge (high ∷ []) (q ∷ []) ≡ low ∷ []
reset-clears q = refl

tick-from-low :
  step toggle risingEdge (low ∷ []) (low ∷ []) ≡ high ∷ []
tick-from-low = refl

tick-from-high :
  step toggle risingEdge (low ∷ []) (high ∷ []) ≡ low ∷ []
tick-from-high = refl

toggle-twice : ∀ q
             → step toggle risingEdge (low ∷ [])
                 (step toggle risingEdge (low ∷ []) (q ∷ []))
             ≡ q ∷ []
toggle-twice false = refl
toggle-twice true = refl

twoTicks : List (Stimulus )
twoTicks = noResetTick ∷ᴸ noResetTick ∷ᴸ []ᴸ

two-tick-run-returns-to-initial :
  run toggle (initial toggle) twoTicks ≡ initial toggle
two-tick-run-returns-to-initial = refl

two-tick-observation-trace :
  execute toggle (initial toggle) twoTicks
  ≡ frame (low ∷ []) (low ∷ []) (high ∷ [])
    ∷ᴸ frame (high ∷ []) (high ∷ []) (low ∷ [])
    ∷ᴸ []ᴸ
two-tick-observation-trace = refl