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

module Spartan6.Netlist.Raw where

open import Spartan6.Prelude
open import Spartan6.Architecture.Primitive using (PrimitiveKind)

-- Raw netlists are an untrusted, format-independent ingestion boundary.
-- Strings preserve source names and diagnostic context only.  They are not
-- identities used by the checked model or by proofs about admitted designs.

NetId : Type₀
NetId = ℕ

data PortDirection : Type₀ where
  inputPort         : PortDirection
  outputPort        : PortDirection
  bidirectionalPort : PortDirection

data RawPrimitiveKind : Type₀ where
  knownPrimitive   : PrimitiveKind → RawPrimitiveKind
  unknownPrimitive : String → RawPrimitiveKind

data Connection : Type₀ where
  net          : NetId → Connection
  constant     : Bit → Connection
  disconnected : Connection

record RawPort : Type₀ where
  constructor rawPort
  field
    rawPortName        : String
    rawPortDirection   : PortDirection
    rawPortWidth       : ℕ
    rawPortConnections : List Connection

open RawPort public

record RawParameter : Type₀ where
  constructor rawParameter
  field
    rawParameterName  : String
    rawParameterValue : String

open RawParameter public

record RawInstance : Type₀ where
  constructor rawInstance
  field
    rawInstanceName       : String
    rawInstanceKind       : RawPrimitiveKind
    rawInstancePorts      : List RawPort
    rawInstanceParameters : List RawParameter
    rawInstanceInitialBit : Maybe Bit

open RawInstance public

record RawTopPort : Type₀ where
  constructor rawTopPort
  field
    rawTopPortName        : String
    rawTopPortDirection   : PortDirection
    rawTopPortWidth       : ℕ
    rawTopPortConnections : List Connection

open RawTopPort public

record RawDesign : Type₀ where
  constructor rawDesign
  field
    rawTargetProfile : Maybe String
    rawTopPorts      : List RawTopPort
    rawInstances     : List RawInstance

open RawDesign public