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

module Spartan6.Examples.ToggleEquivalence where

open import Spartan6.Prelude
open import Spartan6.Netlist.Expression
open import Spartan6.Semantics.Design
open import Spartan6.Semantics.Equivalence
open import Spartan6.Examples.Toggle

-- A technology-independent functional specification of the same machine.

toggleSpecification : Design 1 1 1
toggleSpecification =
  mkDesign
    (low ∷ [])
    (qRegister ∷ [])
    (select resetInput (invert qRegister) (constant low) ∷ [])

toggle-refines-specification :
  BehaviorallyEquivalent toggle toggleSpecification
initialAgreement toggle-refines-specification = refl
outputAgreement toggle-refines-specification external state = refl
stepAgreement toggle-refines-specification idle external state = refl
stepAgreement toggle-refines-specification risingEdge external state = refl

all-finite-runs-agree :
  ∀ stimuli
  → run toggle (initial toggle) stimuli
  ≡ run toggleSpecification (initial toggleSpecification) stimuli
all-finite-runs-agree =
  initial-run-agreement toggle-refines-specification