Spartan6.Import.YosysTests

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

module Spartan6.Import.YosysTests where

open import Spartan6.Prelude

import FF.Json.Native as Native
import Spartan6.Import.Json as Import
import Spartan6.Import.Yosys as Yosys
import Spartan6.Import.YosysCorpus as Corpus
import Spartan6.Netlist.Raw as Raw
import Spartan6.Validation.Diagnostic as Diagnostic
import Spartan6.Validation.Raw as Validation

jsonBits : List Import.JsonValue → Import.JsonValue
jsonBits = Native.jarray

decoded-toggle-is-structurally-valid :
  Validation.StructurallyValid Corpus.toggleRawDesign
decoded-toggle-is-structurally-valid = refl

duplicateModulesDocument : Import.JsonValue
duplicateModulesDocument =
  Native.jobject
    ( ("modules" , Native.jobject []ᴸ)
    ∷ᴸ ("modules" , Native.jobject []ᴸ)
    ∷ᴸ []ᴸ )

duplicate-modules-is-path-aware :
  Yosys.decodeSelectedModule "top" duplicateModulesDocument
  ≡ Diagnostic.rejected
      (Import.malformedAt
        (Import.fieldAt Import.root "modules")
        "a unique object field"
        "a duplicate field"
        "Duplicate JSON object fields are rejected; source order never assigns precedence.")
duplicate-modules-is-path-aware = refl

malformedModulesDocument : Import.JsonValue
malformedModulesDocument =
  Native.jobject (("modules" , Native.jbool true) ∷ᴸ []ᴸ)

malformed-modules-shape-is-explicit :
  Yosys.decodeSelectedModule "top" malformedModulesDocument
  ≡ Diagnostic.rejected
      (Import.malformedAt
        (Import.fieldAt Import.root "modules")
        "an object" "boolean"
        "This Yosys schema position requires a JSON object.")
malformed-modules-shape-is-explicit = refl

missing-modules-field-is-explicit :
  Yosys.decodeSelectedModule "top" (Native.jobject []ᴸ)
  ≡ Diagnostic.rejected
      (Import.malformedAt
        (Import.fieldAt Import.root "modules")
        "one required field" "a missing field"
        "The selected Yosys schema requires this field.")
missing-modules-field-is-explicit = refl

xPath : Import.JsonPath
xPath = Import.indexAt (Import.fieldAt Import.root "bits") 0

x-connection-is-rejected :
  Yosys.decodeConnection xPath (Native.jstring "x")
  ≡ Diagnostic.rejected
      (Yosys.parameterProblem Diagnostic.malformedImport xPath
        "a natural net id or defined constant string 0/1"
        "x"
        "Constants x and z, uppercase variants, and other strings have no two-valued Raw.Connection representation.")
x-connection-is-rejected = refl

z-connection-is-rejected :
  Yosys.decodeConnection xPath (Native.jstring "z")
  ≡ Diagnostic.rejected
      (Yosys.parameterProblem Diagnostic.malformedImport xPath
        "a natural net id or defined constant string 0/1"
        "z"
        "Constants x and z, uppercase variants, and other strings have no two-valued Raw.Connection representation.")
z-connection-is-rejected = refl

two-bit-width-is-rejected :
  Yosys.decodeFixedConnections 1
    (Import.fieldAt Import.root "I")
    (jsonBits (Native.jnumber 2 ∷ᴸ Native.jnumber 3 ∷ᴸ []ᴸ))
  ≡ Diagnostic.rejected
      (Yosys.widthProblem (Import.fieldAt Import.root "I") 1 2)
two-bit-width-is-rejected = refl

wrong-direction-is-rejected :
  Yosys.decodeKnownDirection Raw.inputPort "input"
    (Import.fieldAt Import.root "I")
    (Native.jstring "output")
  ≡ Diagnostic.rejected
      (Yosys.directionProblem
        (Import.fieldAt Import.root "I") "input" "output")
wrong-direction-is-rejected = refl

lut-binary-parameter-converts-to-canonical-hex :
  Yosys.decodeLUTInit 4 1
    (Import.fieldAt Import.root "INIT")
    (Native.jstring "0110")
  ≡ Diagnostic.accepted "6"
lut-binary-parameter-converts-to-canonical-hex = refl

lut-natural-parameter-is-numeric :
  Yosys.decodeLUTInit 4 1
    (Import.fieldAt Import.root "INIT")
    (Native.jnumber 10)
  ≡ Diagnostic.accepted "A"
lut-natural-parameter-is-numeric = refl

lut6-natural-parameter-retains-leading-zeroes :
  Yosys.decodeLUTInit 64 16
    (Import.fieldAt Import.root "INIT")
    (Native.jnumber 1)
  ≡ Diagnostic.accepted "0000000000000001"
lut6-natural-parameter-retains-leading-zeroes = refl

lut-natural-overflow-is-rejected :
  Yosys.decodeLUTInit 4 1
    (Import.fieldAt Import.root "INIT")
    (Native.jnumber 16)
  ≡ Diagnostic.rejected
      (Yosys.parameterProblem Diagnostic.malformedInitialisation
        (Import.fieldAt Import.root "INIT")
        "a natural number smaller than 2^4" "16"
        "Numeric LUT INIT is interpreted numerically and must fit the complete truth-table width.")
lut-natural-overflow-is-rejected = refl

lut-boolean-parameter-is-rejected :
  Yosys.decodeLUTInit 4 1
    (Import.fieldAt Import.root "INIT")
    (Native.jbool true)
  ≡ Diagnostic.rejected
      (Yosys.parameterProblem Diagnostic.illegalParameter
        (Import.fieldAt Import.root "INIT")
        "a fixed-width binary string or natural number" "boolean"
        "Other JSON forms cannot encode a LUT truth table.")
lut-boolean-parameter-is-rejected = refl

duplicate-init-parameter-is-rejected :
  Yosys.decodeLUTParameters 4 1
    (Import.fieldAt Import.root "parameters")
    (Native.jobject
      ( ("INIT" , Native.jstring "0000")
      ∷ᴸ ("INIT" , Native.jstring "1111")
      ∷ᴸ []ᴸ ))
  ≡ Diagnostic.rejected
      (Import.malformedAt
        (Import.fieldAt
          (Import.fieldAt Import.root "parameters") "INIT")
        "a unique object field" "a duplicate field"
        "Duplicate JSON object fields are rejected; source order never assigns precedence.")
duplicate-init-parameter-is-rejected = refl

register-x-parameter-is-rejected :
  Yosys.decodeRegisterInit
    (Import.fieldAt Import.root "INIT")
    (Native.jstring "x")
  ≡ Diagnostic.rejected
      (Yosys.parameterProblem Diagnostic.malformedInitialisation
        (Import.fieldAt Import.root "INIT")
        "defined scalar bit 0 or 1" "x"
        "Register INIT does not admit x, z, wider strings, or alternate spellings.")
register-x-parameter-is-rejected = refl

parameterless-object-is-exact :
  Yosys.decodeParameterless
    (Import.fieldAt Import.root "parameters")
    (Native.jobject (("EXTRA" , Native.jstring "0") ∷ᴸ []ᴸ))
  ≡ Diagnostic.rejected
      (Yosys.parameterProblem Diagnostic.illegalParameter
        (Import.fieldAt Import.root "parameters")
        "an empty parameter object"
        "one or more parameter fields"
        "The selected digital primitive mode is parameterless.")
parameterless-object-is-exact = refl

unknown-scalars-are-preserved-in-order :
  Yosys.decodeUnknownParameters
    (Import.fieldAt Import.root "parameters")
    (Native.jobject
      ( ("MODE" , Native.jstring "opaque")
      ∷ᴸ ("N" , Native.jnumber 12)
      ∷ᴸ []ᴸ ))
  ≡ Diagnostic.accepted
      ( Raw.rawParameter "MODE" "opaque"
      ∷ᴸ Raw.rawParameter "N" "12"
      ∷ᴸ []ᴸ )
unknown-scalars-are-preserved-in-order = refl

unknown-kind-remains-structurally-rejected :
  Validation.structureDiagnostics Corpus.unknownRawDesign
  ≡ Validation.singleton
      (Validation.issue Diagnostic.unknownPrimitive
        "$abc$1406$auto$blifparse.cc:557:parse_blif$1407"
        "a primitive kind in the selected architecture profile"
        "INV"
        "Unknown kinds are rejected rather than approximated.")
unknown-kind-remains-structurally-rejected = refl

unknown-port-without-direction-is-rejected :
  Yosys.decodeUnknownPorts
    (Import.fieldAt Import.root "connections")
    (Native.jobject
      (("I" , jsonBits (Native.jnumber 2 ∷ᴸ []ᴸ)) ∷ᴸ []ᴸ))
    (Import.fieldAt Import.root "port_directions")
    (Native.jobject []ᴸ)
  ≡ Diagnostic.rejected
      (Yosys.missingDirectionProblem
        (Import.fieldAt Import.root "port_directions") "I")
unknown-port-without-direction-is-rejected = refl