Skip to content

Commit

Permalink
Removed unnecessary bound and included an explanation for another.
Browse files Browse the repository at this point in the history
  • Loading branch information
rslawson committed Oct 22, 2024
1 parent 67d2191 commit c240205
Showing 1 changed file with 11 additions and 1 deletion.
12 changes: 11 additions & 1 deletion bittide-instances/src/Bittide/Instances/Hitl/IlaPlot.hs
Original file line number Diff line number Diff line change
Expand Up @@ -475,7 +475,17 @@ callistoClockControlWithIla ::
(HasCallStack) =>
(KnownDomain dyn, KnownDomain sys, HasSynchronousReset sys) =>
(KnownNat n, KnownNat m) =>
(1 <= n, 1 <= m, n + m <= 32, 6 + n * (m + 4) <= 1024) =>
{- Reasoning for the '6 + n * (m + 4) <= 1024' bound:
In short, it's the upper bound on the data stored in 'PlotData n m'.
The details:
- 6 bits for 'dSpeedChange' plus 'dRfStateChange'
- 4 bits for the two 'Maybe Bool's
- 'm' bits for the 'RelDataCount m'
- 'n * (4 + m)' bits for 'dEBData'
-}
(1 <= n, 1 <= m, 6 + n * (m + 4) <= 1024) =>
(CompressedBufferSize <= m) =>
Clock dyn ->
Clock sys ->
Expand Down

0 comments on commit c240205

Please sign in to comment.