{-# OPTIONS --safe --cubical #-}
module Spartan6.Netlist.Carry4Builder where
open import Spartan6.Prelude
import Spartan6.Architecture.Primitive as Architecture
import Spartan6.Netlist.Checked as Checked
import Spartan6.Netlist.BuilderCore as Generic
import Spartan6.Netlist.Raw as Raw
import Spartan6.Primitive.Carry4 as Carry
import Spartan6.Validation.Diagnostic as Diagnostic
import Spartan6.Validation.Parameter as Parameter
import Spartan6.Validation.Raw as Validation
singleton : Diagnostic.Diagnostic → Diagnostic.Diagnostics
singleton item = item ∷ᴸ []ᴸ
issue : Diagnostic.DiagnosticCode
→ String → String → String → String
→ Diagnostic.Diagnostic
issue code subject expected observed detail =
Diagnostic.diagnostic
code Diagnostic.reject subject expected observed detail
record Carry4Ports : Type₀ where
constructor carry4Ports
field
carryCI : Raw.RawPort
carryCYINIT : Raw.RawPort
carryDI : Raw.RawPort
carryS : Raw.RawPort
carryO : Raw.RawPort
carryCO : Raw.RawPort
open Carry4Ports public
parseCarry4Ports : List Raw.RawPort → Maybe Carry4Ports
parseCarry4Ports
(ci ∷ᴸ cyinit ∷ᴸ di ∷ᴸ select ∷ᴸ output
∷ᴸ carry-output ∷ᴸ []ᴸ) =
just (carry4Ports ci cyinit di select output carry-output)
parseCarry4Ports ports = nothing
parseFourConnections : List Raw.Connection
→ Maybe (Vec Raw.Connection 4)
parseFourConnections
(c0 ∷ᴸ c1 ∷ᴸ c2 ∷ᴸ c3 ∷ᴸ []ᴸ) =
just (c0 ∷ c1 ∷ c2 ∷ c3 ∷ [])
parseFourConnections connections = nothing
resolveConnections : ∀ {inputCount registerCount localCount count}
→ String
→ Generic.Bindings inputCount registerCount localCount
→ Vec Raw.Connection count
→ Diagnostic.CheckResult
(Vec
(Checked.Wire inputCount registerCount localCount)
count)
resolveConnections subject bindings [] = Diagnostic.accepted []
resolveConnections subject bindings (connection ∷ connections)
with Generic.resolveOneConnection subject bindings connection
... | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
... | Diagnostic.accepted wire
with resolveConnections subject bindings connections
... | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
... | Diagnostic.accepted wires = Diagnostic.accepted (wire ∷ wires)
resolveFourPort : ∀ {inputCount registerCount localCount}
→ String
→ Generic.Bindings inputCount registerCount localCount
→ Raw.RawPort
→ Diagnostic.CheckResult
(Vec (Checked.Wire inputCount registerCount localCount) 4)
resolveFourPort subject bindings port
with parseFourConnections (Raw.rawPortConnections port)
... | nothing =
Diagnostic.rejected
(singleton
(issue Diagnostic.widthMismatch subject
"exactly four bit-ascending connections"
"a differently sized connection list"
"CARRY4 DI, S, O, and CO are four-bit vectors."))
... | just connections = resolveConnections subject bindings connections
outputConnectionNets : ∀ {count}
→ String
→ Vec Raw.Connection count
→ Diagnostic.CheckResult (Vec Raw.NetId count)
outputConnectionNets subject [] = Diagnostic.accepted []
outputConnectionNets subject (Raw.net net-id ∷ connections)
with outputConnectionNets subject connections
... | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
... | Diagnostic.accepted net-ids =
Diagnostic.accepted (net-id ∷ net-ids)
outputConnectionNets subject (Raw.constant bit ∷ connections) =
Diagnostic.rejected
(singleton
(issue Diagnostic.directionMismatch subject
"four raw nets driven by CARRY4"
"a constant output binding"
"A checked local node drives each retained CARRY4 output bit."))
outputConnectionNets subject (Raw.disconnected ∷ connections) =
Diagnostic.rejected
(singleton
(issue Diagnostic.unsupportedMode subject
"four retained raw output nets"
"an explicitly discarded output bit"
"This provenance slice binds every O and CO bit."))
outputFourPort : String → Raw.RawPort
→ Diagnostic.CheckResult (Vec Raw.NetId 4)
outputFourPort subject port
with parseFourConnections (Raw.rawPortConnections port)
... | nothing =
Diagnostic.rejected
(singleton
(issue Diagnostic.widthMismatch subject
"exactly four bit-ascending output connections"
"a differently sized connection list"
"CARRY4 O and CO are four-bit vectors."))
... | just connections = outputConnectionNets subject connections
data CarryEntrySource : Type₀ where
ciSource : CarryEntrySource
cyinitSource : CarryEntrySource
data ResolvedCarryEntry {inputCount registerCount : ℕ}
(current : Generic.Builder inputCount registerCount)
(ci cyinit : Raw.RawPort)
: Type₀ where
entryFromCI : ∀ {connection wire}
→ Raw.rawPortConnections ci ≡ connection ∷ᴸ []ᴸ
→ Raw.rawPortConnections cyinit
≡ Raw.constant low ∷ᴸ []ᴸ
→ Generic.resolveOneConnection
"CARRY4.CI" (Generic.builderBindings current) connection
≡ Diagnostic.accepted wire
→ ResolvedCarryEntry current ci cyinit
entryFromCYINIT : ∀ {connection wire}
→ Raw.rawPortConnections ci
≡ Raw.constant low ∷ᴸ []ᴸ
→ Raw.rawPortConnections cyinit ≡ connection ∷ᴸ []ᴸ
→ Generic.resolveOneConnection
"CARRY4.CYINIT" (Generic.builderBindings current) connection
≡ Diagnostic.accepted wire
→ ResolvedCarryEntry current ci cyinit
resolvedEntrySource : ∀ {inputCount registerCount current ci cyinit}
→ ResolvedCarryEntry
{inputCount = inputCount} {registerCount = registerCount}
current ci cyinit
→ CarryEntrySource
resolvedEntrySource (entryFromCI ci-path low-path resolved) = ciSource
resolvedEntrySource (entryFromCYINIT low-path cyinit-path resolved) =
cyinitSource
resolvedEntryWire : ∀ {inputCount registerCount current ci cyinit}
→ ResolvedCarryEntry
{inputCount = inputCount} {registerCount = registerCount}
current ci cyinit
→ Checked.Wire
inputCount registerCount (Generic.builderLocalCount current)
resolvedEntryWire (entryFromCI {wire = wire} ci-path low-path resolved) =
wire
resolvedEntryWire
(entryFromCYINIT {wire = wire} low-path cyinit-path resolved) =
wire
entryConditionDiagnostics : Diagnostic.Diagnostics
entryConditionDiagnostics =
singleton
(issue Diagnostic.unsupportedMode "CARRY4 entry"
"CYINIT literally low while CI is selected, or CI literally low while CYINIT is selected"
"two simultaneous/non-literal entry sources"
"UG615 does not specify combining CI and CYINIT; the non-selected raw source must be tied low. When both are low, CI is selected using the proved equal-value semantics branch.")
selectCarryEntryConnections : ∀ {inputCount registerCount}
→ (current : Generic.Builder inputCount registerCount)
→ (ci cyinit : Raw.RawPort)
→ (ci-connections cyinit-connections : List Raw.Connection)
→ Raw.rawPortConnections ci ≡ ci-connections
→ Raw.rawPortConnections cyinit ≡ cyinit-connections
→ Diagnostic.CheckResult (ResolvedCarryEntry current ci cyinit)
selectCarryEntryConnections current ci cyinit
(ci-connection ∷ᴸ []ᴸ)
(Raw.constant false ∷ᴸ []ᴸ)
ci-path cyinit-path
with Generic.resolveOneConnection
"CARRY4.CI" (Generic.builderBindings current) ci-connection UsingEq
... | Diagnostic.rejected diagnostics , resolved-path =
Diagnostic.rejected diagnostics
... | Diagnostic.accepted wire , resolved-path =
Diagnostic.accepted
(entryFromCI ci-path cyinit-path resolved-path)
selectCarryEntryConnections current ci cyinit
(Raw.constant false ∷ᴸ []ᴸ)
(cyinit-connection ∷ᴸ []ᴸ)
ci-path cyinit-path
with Generic.resolveOneConnection
"CARRY4.CYINIT"
(Generic.builderBindings current) cyinit-connection UsingEq
... | Diagnostic.rejected diagnostics , resolved-path =
Diagnostic.rejected diagnostics
... | Diagnostic.accepted wire , resolved-path =
Diagnostic.accepted
(entryFromCYINIT ci-path cyinit-path resolved-path)
selectCarryEntryConnections current ci cyinit
ci-connections cyinit-connections ci-path cyinit-path =
Diagnostic.rejected entryConditionDiagnostics
selectCarryEntry : ∀ {inputCount registerCount}
→ (current : Generic.Builder inputCount registerCount)
→ (ci cyinit : Raw.RawPort)
→ Diagnostic.CheckResult (ResolvedCarryEntry current ci cyinit)
selectCarryEntry current ci cyinit =
selectCarryEntryConnections current ci cyinit
(Raw.rawPortConnections ci)
(Raw.rawPortConnections cyinit)
refl refl
liftLocalTwice : ∀ {inputCount registerCount localCount}
→ Checked.Wire inputCount registerCount localCount
→ Checked.Wire inputCount registerCount (suc (suc localCount))
liftLocalTwice wire =
Generic.liftLocalWire (Generic.liftLocalWire wire)
addCarryStage : ∀ {inputCount registerCount}
→ (current : Generic.Builder inputCount registerCount)
→ Checked.Wire
inputCount registerCount (Generic.builderLocalCount current)
→ Checked.Wire
inputCount registerCount (Generic.builderLocalCount current)
→ Checked.Wire
inputCount registerCount (Generic.builderLocalCount current)
→ Raw.NetId
→ Raw.NetId
→ Generic.Builder inputCount registerCount
addCarryStage current incoming di select o-net co-net =
Generic.extendBuilder after-xor co-net
(Checked.muxNode
(Generic.liftLocalWire select)
(Generic.liftLocalWire di)
(Generic.liftLocalWire incoming))
where
after-xor : Generic.Builder _ _
after-xor =
Generic.extendBuilder current o-net
(Checked.xorNode select incoming)
buildCarryStages :
∀ {inputCount registerCount count}
→ (current : Generic.Builder inputCount registerCount)
→ Checked.Wire
inputCount registerCount (Generic.builderLocalCount current)
→ Vec
(Checked.Wire
inputCount registerCount (Generic.builderLocalCount current))
count
→ Vec
(Checked.Wire
inputCount registerCount (Generic.builderLocalCount current))
count
→ Vec Raw.NetId count
→ Vec Raw.NetId count
→ Generic.Builder inputCount registerCount
buildCarryStages current incoming [] [] [] [] = current
buildCarryStages
(Generic.builder local-count nodes bindings)
incoming (di ∷ dis) (select ∷ selects)
(o-net ∷ o-nets) (co-net ∷ co-nets) =
buildCarryStages
next
(Checked.localWire fzero)
(map liftLocalTwice dis)
(map liftLocalTwice selects)
o-nets co-nets
where
next : Generic.Builder _ _
next =
addCarryStage
(Generic.builder local-count nodes bindings)
incoming di select o-net co-net
buildCarry4 : ∀ {inputCount registerCount}
→ (current : Generic.Builder inputCount registerCount)
→ Checked.Wire
inputCount registerCount (Generic.builderLocalCount current)
→ Vec
(Checked.Wire
inputCount registerCount (Generic.builderLocalCount current))
4
→ Vec
(Checked.Wire
inputCount registerCount (Generic.builderLocalCount current))
4
→ Vec Raw.NetId 4
→ Vec Raw.NetId 4
→ Generic.Builder inputCount registerCount
buildCarry4 = buildCarryStages
eightMore : ℕ → ℕ
eightMore count =
suc (suc (suc (suc (suc (suc (suc (suc count)))))))
buildCarry4-adds-eight :
∀ {inputCount registerCount}
(current : Generic.Builder inputCount registerCount)
entry di select o-nets co-nets
→ Generic.builderLocalCount
(buildCarry4 current entry di select o-nets co-nets)
≡ eightMore (Generic.builderLocalCount current)
buildCarry4-adds-eight
(Generic.builder local-count nodes bindings)
entry
(di0 ∷ di1 ∷ di2 ∷ di3 ∷ [])
(s0 ∷ s1 ∷ s2 ∷ s3 ∷ [])
(o0 ∷ o1 ∷ o2 ∷ o3 ∷ [])
(co0 ∷ co1 ∷ co2 ∷ co3 ∷ []) = refl
both-low-entry-semantics : ∀ di select
→ Carry.evalCarry4 (Carry.fromCI low) di select
≡ Carry.evalCarry4 (Carry.fromCYINIT low) di select
both-low-entry-semantics di select =
Carry.CI-CYINIT-same-value low di select
record Carry4Build
{inputCount registerCount : ℕ}
(item : Raw.RawInstance)
(initial : Generic.Builder inputCount registerCount)
: Type₀ where
field
carryKind :
Raw.rawInstanceKind item
≡ Raw.knownPrimitive Architecture.CARRY4
parameterlessAccepted :
Parameter.normaliseCoreParameters Architecture.CARRY4
(Raw.rawInstanceName item)
(Raw.rawInstanceParameters item)
(Raw.rawInstanceInitialBit item)
≡ Diagnostic.accepted Parameter.carry4Parameters
canonicalPortsAccepted :
Validation.orderedPortDiagnostics
(Architecture.inputPortSpecifications Architecture.CARRY4)
(Architecture.outputPortSpecifications Architecture.CARRY4)
(Raw.rawInstancePorts item)
≡ []ᴸ
parsedPorts : Carry4Ports
portsParsed :
parseCarry4Ports (Raw.rawInstancePorts item)
≡ just parsedPorts
resolvedEntry :
ResolvedCarryEntry
initial (carryCI parsedPorts) (carryCYINIT parsedPorts)
entryAccepted :
selectCarryEntry
initial (carryCI parsedPorts) (carryCYINIT parsedPorts)
≡ Diagnostic.accepted resolvedEntry
diWires :
Vec
(Checked.Wire inputCount registerCount
(Generic.builderLocalCount initial))
4
diAccepted :
resolveFourPort
"CARRY4.DI" (Generic.builderBindings initial)
(carryDI parsedPorts)
≡ Diagnostic.accepted diWires
selectWires :
Vec
(Checked.Wire inputCount registerCount
(Generic.builderLocalCount initial))
4
selectAccepted :
resolveFourPort
"CARRY4.S" (Generic.builderBindings initial)
(carryS parsedPorts)
≡ Diagnostic.accepted selectWires
oNets : Vec Raw.NetId 4
oNetsAccepted :
outputFourPort "CARRY4.O" (carryO parsedPorts)
≡ Diagnostic.accepted oNets
coNets : Vec Raw.NetId 4
coNetsAccepted :
outputFourPort "CARRY4.CO" (carryCO parsedPorts)
≡ Diagnostic.accepted coNets
carryBuilder : Generic.Builder inputCount registerCount
carryBuilderBuilt :
carryBuilder
≡ buildCarry4
initial (resolvedEntryWire resolvedEntry)
diWires selectWires oNets coNets
open Carry4Build public
wrongKindDiagnostics : Raw.RawInstance → Diagnostic.Diagnostics
wrongKindDiagnostics item =
singleton
(issue Diagnostic.unsupportedMode
(Raw.rawInstanceName item)
"an explicitly selected CARRY4 instance"
"another raw primitive kind"
"The isolated CARRY4 builder never assigns carry semantics to another primitive.")
internalPortDiagnostics : Raw.RawInstance → Diagnostic.Diagnostics
internalPortDiagnostics item =
singleton
(issue Diagnostic.widthMismatch
(Raw.rawInstanceName item)
"canonical CI, CYINIT, DI, S, O, and CO ports"
"a port list not decoded after canonical validation"
"This total branch preserves the untrusted raw boundary.")
processCARRY4 : ∀ {inputCount registerCount}
→ (item : Raw.RawInstance)
→ (initial : Generic.Builder inputCount registerCount)
→ Diagnostic.CheckResult (Carry4Build item initial)
processCARRY4
item@(Raw.rawInstance name
(Raw.knownPrimitive Architecture.CARRY4)
raw-ports parameters initial-bit)
initial
with Parameter.normaliseCoreParameters Architecture.CARRY4
name parameters initial-bit UsingEq
... | Diagnostic.rejected diagnostics , parameter-path =
Diagnostic.rejected diagnostics
... | Diagnostic.accepted Parameter.carry4Parameters , parameter-path
with Validation.orderedPortDiagnostics
(Architecture.inputPortSpecifications Architecture.CARRY4)
(Architecture.outputPortSpecifications Architecture.CARRY4)
raw-ports UsingEq
... | problem ∷ᴸ problems , canonical-ports-path =
Diagnostic.rejected (problem ∷ᴸ problems)
... | []ᴸ , canonical-ports-path
with parseCarry4Ports raw-ports UsingEq
... | nothing , ports-path =
Diagnostic.rejected (internalPortDiagnostics item)
... | just ports , ports-path
with selectCarryEntry
initial (carryCI ports) (carryCYINIT ports) UsingEq
... | Diagnostic.rejected diagnostics , entry-path =
Diagnostic.rejected diagnostics
... | Diagnostic.accepted entry , entry-path
with resolveFourPort
"CARRY4.DI" (Generic.builderBindings initial)
(carryDI ports) UsingEq
... | Diagnostic.rejected diagnostics , di-path =
Diagnostic.rejected diagnostics
... | Diagnostic.accepted di-wires , di-path
with resolveFourPort
"CARRY4.S" (Generic.builderBindings initial)
(carryS ports) UsingEq
... | Diagnostic.rejected diagnostics , select-path =
Diagnostic.rejected diagnostics
... | Diagnostic.accepted select-wires , select-path
with outputFourPort "CARRY4.O" (carryO ports) UsingEq
... | Diagnostic.rejected diagnostics , o-path =
Diagnostic.rejected diagnostics
... | Diagnostic.accepted o-nets , o-path
with outputFourPort "CARRY4.CO" (carryCO ports) UsingEq
... | Diagnostic.rejected diagnostics , co-path =
Diagnostic.rejected diagnostics
... | Diagnostic.accepted co-nets , co-path =
Diagnostic.accepted
record
{ carryKind = refl
; parameterlessAccepted = parameter-path
; canonicalPortsAccepted = canonical-ports-path
; parsedPorts = ports
; portsParsed = ports-path
; resolvedEntry = entry
; entryAccepted = entry-path
; diWires = di-wires
; diAccepted = di-path
; selectWires = select-wires
; selectAccepted = select-path
; oNets = o-nets
; oNetsAccepted = o-path
; coNets = co-nets
; coNetsAccepted = co-path
; carryBuilder =
buildCarry4 initial (resolvedEntryWire entry)
di-wires select-wires o-nets co-nets
; carryBuilderBuilt = refl
}
processCARRY4 item initial =
Diagnostic.rejected (wrongKindDiagnostics item)
carry-build-adds-eight :
∀ {inputCount registerCount item initial}
→ (built :
Carry4Build
{inputCount = inputCount} {registerCount = registerCount}
item initial)
→ Generic.builderLocalCount (carryBuilder built)
≡ eightMore (Generic.builderLocalCount initial)
carry-build-adds-eight built =
cong Generic.builderLocalCount (carryBuilderBuilt built)
∙ buildCarry4-adds-eight
_ _ (diWires built) (selectWires built)
(oNets built) (coNets built)
carry-build-entry-provenance :
∀ {inputCount registerCount item initial}
→ Carry4Build
{inputCount = inputCount} {registerCount = registerCount}
item initial
→ CarryEntrySource
carry-build-entry-provenance built =
resolvedEntrySource (resolvedEntry built)