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

module Spartan6.Examples.HandlerCorrectness where

open import Spartan6.Prelude
import Spartan6.Netlist.PrimitiveHandler as Handler
import Spartan6.Primitive.LUT as LUT

lut2Table : LUT.TruthTable 
lut2Table = low ∷ high ∷ high ∷ low ∷ []

lut2-local-correctness :
  Handler.denotation (Handler.lutHandler lut2Table) (high ∷ low ∷ [])
  ≡ high ∷ []
lut2-local-correctness = refl

obufds-local-correctness :
  Handler.denotation Handler.obufdsHandler (high ∷ [])
  ≡ high ∷ low ∷ []
obufds-local-correctness = refl

carry4-local-correctness :
  Handler.denotation Handler.carry4Handler
    (low ∷ low ∷ low ∷ low ∷ low
     ∷ high ∷ high ∷ high ∷ high ∷ [])
  ≡ high ∷ high ∷ high ∷ high
    ∷ low ∷ low ∷ low ∷ low ∷ []
carry4-local-correctness = refl

fdre-next-local-correctness :
  Handler.stateDenotationNext (Handler.fdreHandler low)
    (high ∷ high ∷ low ∷ []) (low ∷ [])
  ≡ high ∷ []
fdre-next-local-correctness = refl