Skip to content

Commit

Permalink
Work around clash-compiler#2376 (#213)
Browse files Browse the repository at this point in the history
  • Loading branch information
martijnbastiaan authored Jan 2, 2023
1 parent e782d9c commit b92ba9b
Show file tree
Hide file tree
Showing 2 changed files with 11 additions and 1 deletion.
1 change: 1 addition & 0 deletions bittide-instances/src/Clash/Shake/Extra.hs
Original file line number Diff line number Diff line change
Expand Up @@ -48,6 +48,7 @@ clashCmd buildDir hdl topName extraArgs =
, hdlToFlag hdl
, "-fclash-clear"
, "-fclash-spec-limit=100"
, "-fclash-debug", "DebugSilent"
] <> extraArgs
)
where
Expand Down
11 changes: 10 additions & 1 deletion bittide/src/Data/Constraint/Nat/Extra.hs
Original file line number Diff line number Diff line change
Expand Up @@ -27,16 +27,19 @@ import Unsafe.Coerce
-- | b <= ceiling(b/a)*a
timesDivRU :: forall a b . (1 <= a) => Dict (b <= (Div (b + (a - 1)) a * a))
timesDivRU = unsafeCoerce (Dict :: Dict ())
{-# NOINLINE timesDivRU #-} -- https://github.com/clash-lang/clash-compiler/issues/2376

-- | Implements logarithmic product rule. Currently hardcoded for specific
-- constants, which we might relax in the future.
clogProductRule :: (1 <= n) => CLog 2 (n * 2) :~: (CLog 2 n + 1)
clogProductRule = unsafeCoerce Refl
{-# NOINLINE clogProductRule #-} -- https://github.com/clash-lang/clash-compiler/issues/2376

-- | Postulates that multiplying some number /a/ by some consant /b/, and
-- | Postulates that multiplying some number /a/ by some constant /b/, and
-- subsequently dividing that result by /b/ equals /a/.
cancelMulDiv :: forall a b . (1 <= b) => Dict (DivRU (a * b) b ~ a)
cancelMulDiv = unsafeCoerce (Dict :: Dict ())
{-# NOINLINE cancelMulDiv #-} -- https://github.com/clash-lang/clash-compiler/issues/2376

-- | Postulates that adding a constant less than the denominator does not
-- change the result (for the given specific context).
Expand All @@ -45,26 +48,32 @@ divWithRemainder ::
(1 <= b, c <= (b - 1)) =>
Dict (Div ((a * b) + c) b ~ a)
divWithRemainder = unsafeCoerce (Dict :: Dict ())
{-# NOINLINE divWithRemainder #-} -- https://github.com/clash-lang/clash-compiler/issues/2376

-- | Postulates that a part is less than or equal to a sum parts, in context
-- of 'Max's left argument.
leMaxLeft :: forall a b c. Dict (a <= Max (a + c) b)
leMaxLeft = unsafeCoerce (Dict :: Dict ())
{-# NOINLINE leMaxLeft #-} -- https://github.com/clash-lang/clash-compiler/issues/2376

-- | Postulates that a part is less than or equal to a sum parts, in context
-- of 'Max's right argument.
leMaxRight :: forall a b c. Dict (b <= Max a (b + c))
leMaxRight = unsafeCoerce (Dict :: Dict ())
{-# NOINLINE leMaxRight #-} -- https://github.com/clash-lang/clash-compiler/issues/2376

-- | if (1 <= a) and (1 <= b) then (1 <= DivRU a b)
strictlyPositiveDivRu :: forall a b . (1 <= a, 1 <= b) => Dict (1 <= DivRU a b)
strictlyPositiveDivRu = unsafeCoerce (Dict :: Dict ())
{-# NOINLINE strictlyPositiveDivRu #-} -- https://github.com/clash-lang/clash-compiler/issues/2376

-- | Euclid's third axiom: /If equals be subtracted from equals, the remainders
-- are equal/.
euclid3 :: forall a b c . (a + b <= c) => Dict (a <= c - b)
euclid3 = unsafeCoerce (Dict :: Dict ())
{-# NOINLINE euclid3 #-} -- https://github.com/clash-lang/clash-compiler/issues/2376

-- | if (2 <= n) holds, then (1 <= CLog 2 n) also holds.
oneLeCLog2n :: forall n . (2 <= n) => Dict (1 <= CLog 2 n)
oneLeCLog2n = unsafeCoerce unsafeCoerce (Dict :: Dict ())
{-# NOINLINE oneLeCLog2n #-} -- https://github.com/clash-lang/clash-compiler/issues/2376

0 comments on commit b92ba9b

Please sign in to comment.