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

module Tutorials.Project03.Main where

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

import Tutorials.Project02.Main as Single

-- This implementation duplicates the state bit.  Redundancy is a common
-- hardware technique, but it is useful only if the copies cannot silently
-- diverge.  Both copies see the same enable and reset inputs.

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

firstQ secondQ : Expr  
firstQ = register fzero
secondQ = register (fsuc fzero)

redundantToggle : Design   
redundantToggle =
  mkDesign
    (low ∷ low ∷ [])
    (firstQ ∷ [])
    ( fdreNext (invert firstQ) enableInput resetInput firstQ
    ∷ fdreNext (invert secondQ) enableInput resetInput secondQ
    ∷ [] )

CopiesAgree : State redundantToggle -> Type₀
CopiesAgree (first ∷ second ∷ []) = first ≡ second

copies-remain-equal : Invariant.Invariant redundantToggle CopiesAgree
Invariant.initially copies-remain-equal = refl
Invariant.preserved copies-remain-equal idle
  (enable ∷ reset ∷ []) (first ∷ second ∷ []) equal = equal
Invariant.preserved copies-remain-equal risingEdge
  (enable ∷ reset ∷ []) (first ∷ second ∷ []) equal =
  cong
    (λ stored -> fdreStep (not stored) enable reset stored)
    equal

every-finite-run-preserves-redundancy : ∀ samples
  -> CopiesAgree
      (run redundantToggle (initial redundantToggle) samples)
every-finite-run-preserves-redundancy =
  Invariant.initial-run-preserves copies-remain-equal

-- An invariant talks about one implementation.  A simulation relates two
-- implementations that may have different state shapes.  Here one state bit
-- is related to both copies in the redundant implementation.

SingleMatchesCopies :
  State Single.enabledToggle -> State redundantToggle -> Type₀
SingleMatchesCopies (single ∷ []) (first ∷ second ∷ []) =
  (single ≡ first) × (single ≡ second)

single-simulates-redundant :
  Simulation.Simulation
    Single.enabledToggle redundantToggle SingleMatchesCopies
Simulation.initialRelated single-simulates-redundant = refl , refl
Simulation.observationsAgree single-simulates-redundant
  (enable ∷ reset ∷ []) (single ∷ []) (first ∷ second ∷ []) related =
  cong (_∷ []) (fst related)
Simulation.stepsRelated single-simulates-redundant idle
  (enable ∷ reset ∷ []) (single ∷ []) (first ∷ second ∷ []) related =
  related
Simulation.stepsRelated single-simulates-redundant risingEdge
  (enable ∷ reset ∷ []) (single ∷ []) (first ∷ second ∷ []) related =
  cong nextValue (fst related) , cong nextValue (snd related)
  where
  nextValue : Bit -> Bit
  nextValue stored = fdreStep (not stored) enable reset stored

all-finite-runs-have-the-same-observation : ∀ samples observationInputs
  -> observe Single.enabledToggle observationInputs
      (run Single.enabledToggle (initial Single.enabledToggle) samples)
    ≡ observe redundantToggle observationInputs
      (run redundantToggle (initial redundantToggle) samples)
all-finite-runs-have-the-same-observation =
  Simulation.initial-run-observations-agree single-simulates-redundant