From c2402054f233733066c1c0a702adbc4a529f1ca8 Mon Sep 17 00:00:00 2001 From: Ryan Slawson Date: Thu, 17 Oct 2024 16:48:40 +0200 Subject: [PATCH] Removed unnecessary bound and included an explanation for another. --- .../src/Bittide/Instances/Hitl/IlaPlot.hs | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/bittide-instances/src/Bittide/Instances/Hitl/IlaPlot.hs b/bittide-instances/src/Bittide/Instances/Hitl/IlaPlot.hs index e7e3dc252..a93e9afb6 100644 --- a/bittide-instances/src/Bittide/Instances/Hitl/IlaPlot.hs +++ b/bittide-instances/src/Bittide/Instances/Hitl/IlaPlot.hs @@ -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 ->