Spartan6.Examples.DuplicatedToggle

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

module Spartan6.Examples.DuplicatedToggle where

open import Spartan6.Prelude
open import Spartan6.Netlist.Expression
open import Spartan6.Semantics.Design
open import Spartan6.Semantics.Invariant

firstQ : Expr 0 2
firstQ = register fzero

secondQ : Expr 0 2
secondQ = register (fsuc fzero)

duplicatedToggle : Design 0 2 2
duplicatedToggle =
  mkDesign
    (low ∷ low ∷ [])
    (firstQ ∷ secondQ ∷ [])
    (invert firstQ ∷ invert secondQ ∷ [])

EqualState : State duplicatedToggle → Type₀
EqualState (first ∷ second ∷ []) = first ≡ second

duplicated-toggle-invariant : Invariant duplicatedToggle EqualState
initially duplicated-toggle-invariant = refl
preserved duplicated-toggle-invariant idle [] (first ∷ second ∷ []) equal =
  equal
preserved duplicated-toggle-invariant risingEdge [] (first ∷ second ∷ []) equal =
  cong not equal

all-finite-runs-keep-copies-equal :
  ∀ samples
  → EqualState
      (run duplicatedToggle (initial duplicatedToggle) samples)
all-finite-runs-keep-copies-equal =
  initial-run-preserves duplicated-toggle-invariant