Spartan6.Examples.CheckedToggle

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

module Spartan6.Examples.CheckedToggle where

open import Spartan6.Prelude
open import Spartan6.Netlist.Checked
open import Spartan6.Semantics.Design
open import Spartan6.Semantics.Equivalence
open import Spartan6.Examples.ToggleEquivalence

toggleNodes : Nodes 1 1 2
toggleNodes =
  (noNodes
   ▻ invertNode (storedWire fzero))
  ▻ muxNode (externalWire fzero)
            (localWire fzero)
            (literalWire low)

checkedToggle : CheckedNetlist 1 1 1 2
checkedToggle =
  checkedNetlist
    (low ∷ [])
    toggleNodes
    (storedWire fzero ∷ [])
    (localWire fzero ∷ [])

checked-toggle-compiles-to-specification :
  compileNetlist checkedToggle ≡ toggleSpecification
checked-toggle-compiles-to-specification = refl

checked-toggle-correct :
  BehaviorallyEquivalent (compileNetlist checkedToggle) toggleSpecification
checked-toggle-correct = reflexive toggleSpecification

checked-toggle-all-runs-agree : ∀ stimuli
  → run (compileNetlist checkedToggle)
        (initial (compileNetlist checkedToggle))
        stimuli
  ≡ run toggleSpecification (initial toggleSpecification) stimuli
checked-toggle-all-runs-agree =
  initial-run-agreement checked-toggle-correct