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

module Spartan6.Semantics.Simulation where

open import Spartan6.Prelude
open import Spartan6.Semantics.Design

record Simulation
  {ℓ : Level}
  {inputCount outputCount leftRegisters rightRegisters : ℕ}
  (left : Design inputCount outputCount leftRegisters)
  (right : Design inputCount outputCount rightRegisters)
  (Related : State left → State right → Type ℓ) : Type ℓ where
  field
    initialRelated : Related (initial left) (initial right)
    observationsAgree : ∀ external left-state right-state
                      → Related left-state right-state
                      → observe left external left-state
                      ≡ observe right external right-state
    stepsRelated : ∀ event external left-state right-state
                 → Related left-state right-state
                 → Related (step left event external left-state)
                           (step right event external right-state)

open Simulation public

run-related :
  ∀ {ℓ inputCount outputCount leftRegisters rightRegisters}
    {left : Design inputCount outputCount leftRegisters}
    {right : Design inputCount outputCount rightRegisters}
    {Related : State left → State right → Type ℓ}
  → Simulation left right Related
  → (samples : List (Stimulus inputCount))
  → (left-state : State left)
  → (right-state : State right)
  → Related left-state right-state
  → Related (run left left-state samples) (run right right-state samples)
run-related simulation []ᴸ left-state right-state related = related
run-related {left = left} {right = right}
            simulation (sample ∷ᴸ samples)
            left-state right-state related =
  run-related simulation samples
    (step left
          (stimulusEvent sample)
          (stimulusInputs sample)
          left-state)
    (step right
          (stimulusEvent sample)
          (stimulusInputs sample)
          right-state)
    (stepsRelated simulation
      (stimulusEvent sample)
      (stimulusInputs sample)
      left-state right-state related)

initial-runs-related :
  ∀ {ℓ inputCount outputCount leftRegisters rightRegisters}
    {left : Design inputCount outputCount leftRegisters}
    {right : Design inputCount outputCount rightRegisters}
    {Related : State left → State right → Type ℓ}
  → (simulation : Simulation left right Related)
  → (samples : List (Stimulus inputCount))
  → Related (run left (initial left) samples)
            (run right (initial right) samples)
initial-runs-related simulation samples =
  run-related simulation samples _ _ (initialRelated simulation)

initial-run-observations-agree :
  ∀ {ℓ inputCount outputCount leftRegisters rightRegisters}
    {left : Design inputCount outputCount leftRegisters}
    {right : Design inputCount outputCount rightRegisters}
    {Related : State left → State right → Type ℓ}
  → (simulation : Simulation left right Related)
  → (samples : List (Stimulus inputCount))
  → (observation-input : Vec Bit inputCount)
  → observe left observation-input (run left (initial left) samples)
  ≡ observe right observation-input (run right (initial right) samples)
initial-run-observations-agree simulation samples observation-input =
  observationsAgree simulation observation-input _ _
    (initial-runs-related simulation samples)