clashCompilerError leads to synthesis failure, even though it should be on a branch not taken

[gergoerdi]

As usual, I have a reproducer that is reduced beyond usefulness but still not minimal. In the following code, the ascii function uses clashCompilerError when given a non-ASCII Char. I use it in the definition of symbolValASCII:

symbolVecASCII :: forall s -> SymbolVec s => Vec (SymbolLength s) Word8
symbolVecASCII s = fmap ascii $ symbolVec' (Proxy @(UnconsSymbol s))

but that leads to an error at synthesis time:

src/Sudoku.hs:85:1: error:
    
    Clash.Netlist.BlackBox(410): Could not create blackbox template using BBFN<Clash.Primitives.Magic.clashCompileErrorBBF> for "Clash.Magic.clashCompileError". Function reported: 
    
     clashCompileError: Not an ASCII code point
    
    The source location of the error is not exact, only indicative, as it is acquired 
    after optimizations. The actual location of the error can be in a function that is 
    inlined. To prevent inlining of those functions, annotate them with a NOINLINE pragma.
   |
85 | topEntity clk rst = withClockResetEnable clk rst enableGen $
   | ^^^^^^^^^

An alternate definition that uses an alternate typeclass method that puts ASCII characters into symbolVecASCII' does work, so the problem is ensuring ascii is pushed down deep enough at synthesis time.

{-# LANGUAGE RequiredTypeArguments #-}
{-# LANGUAGE BlockArguments, LambdaCase #-}
{-# LANGUAGE UndecidableInstances #-}
module Sudoku where

import Clash.Prelude
import Clash.Annotations.TH

import Clash.Class.Counter
import Protocols
import qualified Protocols.Df as Df
import Data.Word
import Data.Maybe
import Data.Proxy
import Data.Char (ord)

ascii :: Char -> Word8
ascii c
    | code <= 0x7f = fromIntegral code
    | otherwise = clashCompileError "Not an ASCII code point"
  where
    code = ord c

class (KnownNat (SymbolLength' s)) => SymbolVec' (s :: Maybe (Char, Symbol)) where
    type SymbolLength' s :: Nat

    symbolVec' :: Proxy s -> Vec (SymbolLength' s) Char
    symbolVecASCII' :: Proxy s -> Vec (SymbolLength' s) Word8

instance SymbolVec' Nothing where
    type SymbolLength' Nothing = 0

    symbolVec' _ = Nil
    symbolVecASCII' _ = Nil

instance (SymbolVec s, KnownChar c) => SymbolVec' (Just '(c, s)) where
    type SymbolLength' (Just '(c, s)) = 1 + SymbolLength s

    symbolVec' _ = charVal (Proxy @c) :> symbolVec s
    symbolVecASCII' _ = ascii (charVal (Proxy @c)) :> symbolVecASCII' (Proxy @(UnconsSymbol s))

type SymbolLength s = SymbolLength' (UnconsSymbol s)
type SymbolVec s = SymbolVec' (UnconsSymbol s)

symbolVec :: forall s -> SymbolVec s => Vec (SymbolLength s) Char
symbolVec s = symbolVec' (Proxy @(UnconsSymbol s))

symbolVecASCII :: forall s -> SymbolVec s => Vec (SymbolLength s) Word8
-- symbolVecASCII s = symbolVecASCII' (Proxy @(UnconsSymbol s))
symbolVecASCII s = fmap ascii $ symbolVec' (Proxy @(UnconsSymbol s))

compander'
    :: (HiddenClockResetEnable dom, NFDataX s)
    => s
    -> (s -> (s, Maybe o))
    -> Circuit (Df dom i) (Df dom o)
compander' s0 step = Df.compander s0 \s x -> case step s of
    (s', y) -> (s', y, True)

countSuccChecked :: (Counter a) => a -> Maybe a
countSuccChecked = countSucc . Just

type Format str = (SymbolVec str, KnownNat (SymbolLength str), 1 <= SymbolLength str)

start :: forall str -> (Format str) => Index (SymbolLength str)
start _ = 0

transition :: forall str -> (Format str) => Index (SymbolLength str) -> (Maybe (Index (SymbolLength str)), Maybe Word8)
transition str = \i -> (countSuccChecked i, Just (s !! i))
  where
    s = symbolVecASCII str

board
    :: (HiddenClockResetEnable dom)
    => Circuit (Df dom Word8) (Df dom Word8)
board = compander' (Just 0) \case
    Nothing -> (Nothing, Nothing)
    Just s -> transition "FOO" s

topEntity
    :: "CLK"   ::: Clock System
    -> "RESET" ::: Reset System
    -> "RX"    ::: Signal System (Df.Data Word8)
    -> "TX"    ::: Signal System (Df.Data Word8)
topEntity clk rst = withClockResetEnable clk rst enableGen $
    \rx -> let (_, tx) = toSignals board (rx, pure $ Ack True) in tx

makeTopEntity 'topEntity

[gergoerdi]

If I replace clashCompileError with vanilla error, then it goes through but we can see in the generated Verilog that ascii wasn't applied, since we get 21-bit wide constants for our characters:

  assign c$vec = {21'd70,   21'd79,   21'd79};

Compare with what we get when using symbolVecASCII', i.e. the version that builds a vector of ascii values instead of an fmap ascii of the Char vector:

  assign c$vecFlat = {8'd70,   8'd79,   8'd79};

[gergoerdi]

Hah, much simpler reproducer:

{-# LANGUAGE RequiredTypeArguments #-}
{-# LANGUAGE UndecidableInstances #-}
module Sudoku where

import Clash.Prelude
import Clash.Annotations.TH

import Data.Word
import Data.Maybe
import Data.Proxy
import Data.Char (ord)

ascii :: Char -> Word8
ascii c
    | code <= 0x7f = fromIntegral code
    | otherwise = clashCompileError "Not an ASCII code point"
  where
    code = ord c

class (KnownNat (SymbolLength' s)) => SymbolVec' (s :: Maybe (Char, Symbol)) where
    type SymbolLength' s :: Nat

    symbolVec' :: Proxy s -> Vec (SymbolLength' s) Char
    symbolVecASCII' :: Proxy s -> Vec (SymbolLength' s) Word8

instance SymbolVec' Nothing where
    type SymbolLength' Nothing = 0

    symbolVec' _ = Nil
    symbolVecASCII' _ = Nil

instance (SymbolVec s, KnownChar c) => SymbolVec' (Just '(c, s)) where
    type SymbolLength' (Just '(c, s)) = 1 + SymbolLength s

    symbolVec' _ = charVal (Proxy @c) :> symbolVec s
    symbolVecASCII' _ = ascii (charVal (Proxy @c)) :> symbolVecASCII' (Proxy @(UnconsSymbol s))

type SymbolLength s = SymbolLength' (UnconsSymbol s)
type SymbolVec s = SymbolVec' (UnconsSymbol s)

symbolVec :: forall s -> SymbolVec s => Vec (SymbolLength s) Char
symbolVec s = symbolVec' (Proxy @(UnconsSymbol s))

symbolVecASCII :: forall s -> SymbolVec s => Vec (SymbolLength s) Word8
symbolVecASCII s = symbolVecASCII' (Proxy @(UnconsSymbol s))

topEntity
    :: "RX"    ::: Index 6
    -> "TX"    ::: Word8
topEntity = \i -> s !! i
  where
    s = fmap ascii $ symbolVec "FOOBAR"
    -- s = symbolVecASCII "FOOBAR"

makeTopEntity 'topEntity

This fails, but with s = symbolVecASCII "FOOBAR" it works.

[gergoerdi]

Forget all the typeclass and type-directed constants noise:

module Sudoku where

import Clash.Prelude
import Clash.Annotations.TH

import Data.Word
import Data.Char (ord)

ascii :: Char -> Word8
ascii c
    | code <= 0x7f = fromIntegral code
    | otherwise = clashCompileError "Not an ASCII code point"
  where
    code = ord c

topEntity :: "X" ::: Index 2 -> "Y" ::: Word8
topEntity = \i -> s !! i
  where
    -- -- This alternate definition of `s` works
    -- s = ascii 'F' :>
    --     ascii 'O' :>
    --     Nil

    s = fmap ascii $
        'F' :>
        'O' :>
        Nil

makeTopEntity 'topEntity

[gergoerdi]

@christiaanb suggested trying out the -fclash-compiler-ultra flag, and indeed that makes the reduced versions go through. I'll have to check what happens if I try using it with my full circuit.

[gergoerdi]

@christiaanb from the Clash slack:

I recommend not enabling it for your full circuit. It can make Clash take incredibly long to compile.

So it would be nice to have some alternative that scales. For example, I'd be happy to mark either the definition of ascii, or the definition of symbolVec, or the application of fmap ascii, or anything else, with some explicit marker to get Clash to reduce this during synthesis.

(Chalk this up to another example why explicit staging a la https://andraskovacs.github.io/pdfs/2ltt_icfp24.pdf would be The Way to do Clash, just like #1536 :( )

[DigitalBrains1]

More generally, if I wanted this to happen during synthesis, I'd use Template Haskell. But another option I sometimes use is smap, that is quite good at "try your best to do this at compile time instead of just generating HDL functions for the Haskell functions". I do consider it a bit of a hack... The following works:

    s =
      smap (\_ c -> ascii c) $
        'F' :>
        'O' :>
        Nil

I think this would have been a nice topic on https://clash-lang.discourse.group/ :-). I don't consider the current behaviour a bug; it's a missed optimisation opportunity, where it could do constant propagation at compile-time more. I respect it if you say "Clash should be able to do this and it's still a bug", though.

[gergoerdi]

I respect it if you say "Clash should be able to do this and it's still a bug", though.

Well I do think it should be able to do that (the distinction between ascii 'F' :> ascii 'O' :> Nil and fmap ascii ('F' :> 'O' :> Nil) is quite opaque to me), but perhaps stronger, I also think that it is weird that the clashCompileError ends up firing.

[DigitalBrains1]

It just renders the ascii function into HDL. So it renders both branches, and then applies the function to a constant. If you replace it by error and then simulate or synthesise the resulting HDL, the error case is never taken. But because clashCompileError aborts compilation when it is rendered into HDL, you can't reach that point. I intended clashCompileError to be used in branches based purely on type-level information, which is information with which Clash should almost always eliminate branches based on it.

the distinction between ascii 'F' :> ascii 'O' :> Nil and fmap ascii ('F' :> 'O' :> Nil) is quite opaque to me

Yeah I consider them fully equivalent. It's just that one by chance happens to do more at Haskell compile time and the other happens to do more at HDL compile time.

[edit]
I feel perhaps "branches based purely on type-level information" is too strict an explanation. I'm oversimplifying. But I definitely didn't intend it to be based on term-level arguments of the function the branch is in! Maybe compare some constants, but not arguments.
[/edit]

[gergoerdi]

But another option I sometimes use is smap, that is quite good at "try your best to do this at compile time instead of just generating HDL functions for the Haskell functions". I do consider it a bit of a hack...

Interesting! Indeed using smap . const instead of (f)map seems to work for my full circuit. Unfortunately, as you say this is just a lucky accident -- I have other places that don't involve vectors that have the same problem and smap doesn't (directly?) point towards a solution for proper staging.

[DigitalBrains1]

I'd use Template Haskell. Talking about "proper staging" though X-(

[gergoerdi]

I intended clashCompileError to be used in branches based purely on type-level information, which is information with which Clash should almost always eliminate branches based on it.

I'm actually kinda grateful that ascii fails like this, since it gives me a guarantee that when synthesis succeeds, it will have pushed the ascii applications down and so the HDL is in terms of 8-bit signals instead of 23-bit ones.

[DigitalBrains1]

Yes, that's also a feature of clashCompileError! It checks your assumptions about constant propagation.

I do wonder whether it actually hurts that the HDL is expressed in terms of 23-bit constants. Synthesis tools do a fair bit of constant propagation (although sometimes I'm surprised when someone reports "this could have been less LUTs" and they didn't).

[gergoerdi]

BTW it might be hard to see in these mangled versions, but I am applying ascii on arguments that are completely determined by types! That's the whole point -- the vector is built from a (Known)Symbol.

[DigitalBrains1]

I'm afraid they turn into regular Char too soon then, at which point Clash will render the Char into HDL and then go on happily treating everything as regular terms again. An alternative might be a custom primitive that gets a type-level string as its argument and returns an Unsigned 8 or an appropriately-sized Vec _ (Unsigned 8); the Haskell would remain the same but the primitive function would render the stuff directly into appropriate HDL.

[edit]
Adding SChar to Clash would definitely make sense to me.

You could do ascii :: SChar c -> Unsigned 8 as a primitive and do the rest as regular functions.
[/edit]

[gergoerdi]

But that's pretty much what I'm doing -- I have asciiVal (to mirror charVal) of type forall ch -> KnownChar ch => Word8 and that works reliably.

The problems come when I start to explore ways of generalizing most of my stream formatter for arbitrary input-output types. I would like Symbols and Chars to be useful as formatter specifiers both for Char and Word8 output types, and the Word8 version should ideally be implemented as a transformation of the Char version, instead of having a separate shadow hierarchy of turning Symbols directly into Word8s.

[rowanG077]

What does CONST do in the templating language? The tutorial claims "Clash will try to reduce this to a literal, even if it would otherwise consider it too expensive.". Would this same functionality be something that could help here as a function in Clash.Magic?

[gergoerdi]

I do wonder whether it actually hurts that the HDL is expressed in terms of 23-bit constants. Synthesis tools do a fair bit of constant propagation (although sometimes I'm surprised when someone reports "this could have been less LUTs" and they didn't).

Well what do you know, I now tried it via Char like this:

    Df.map (chr . fromIntegral) |>
    format (Loop (OutputFormat n m)) |>
    Df.map (fromIntegral . ord)

and indeed by the end of synthesis, I get the same parts count as before!

So maybe for my particular problem, I should just drop Word8s completely from my perspective and really stick to just Chars!

[DigitalBrains1]

Would this same functionality be something that could help here as a function in Clash.Magic?

I do feel that would be possible, to add a primitive in Clash.Magic that does the more generic equivalent of a primitive with ~CONST (written in the DSL instead of the templating language). It would still fail if it couldn't reduce it to a constant, though.

and the Word8 version should ideally be implemented as a transformation of the Char version, instead of having a separate shadow hierarchy of turning Symbols directly into Word8s.

That sounds like it would indeed need such a magic function as Rowan suggests. Otherwise I'd expect it to just end up as Chars in HDL.

[edit]
Wait... I might be making it unnecessarily complex... perhaps just a primitive whose template is just ~CONST[0] would already work?
[/edit]

[rowanG077]

Yeah I expect a primitive that just does ~CONST[0] would work.

[DigitalBrains1]

Doesn't work out of the box...

Sudoku.hs

{-# LANGUAGE TemplateHaskellQuotes #-}

module Sudoku where

import Clash.Prelude
import Clash.Annotations.Primitive
import Clash.Annotations.TH

import Data.Word
import Data.Char (ord)

import Data.String.Interpolate (__i)

ascii :: Char -> Word8
ascii c
    | code <= 0x7f = fromIntegral code
    | otherwise = undefined -- clashCompileError "Not an ASCII code point"
  where
    code = ord c

makeConst :: a -> a
makeConst = id
{-# OPAQUE makeConst #-}
{-# ANN makeConst (
   let
     primName = 'makeConst
   in InlineYamlPrimitive [minBound ..] [__i|
      BlackBox:
        name: #{primName}
        kind: Expression
        template: ~CONST[0]
   |]) #-}

topEntity :: "X" ::: Index 2 -> "Y" ::: Word8
topEntity = \i -> s !! i
  where
    -- s =
    --   smap (\_ c -> ascii c) $
    --     'F' :>
    --     'O' :>
    --     Nil

    -- -- This alternate definition of `s` works
    -- s = ascii 'F' :>
    --     ascii 'O' :>
    --     Nil

    s = fmap (makeConst . ascii) $
        'F' :>
        'O' :>
        Nil

makeTopEntity 'topEntity

gives

Sudoku.hs:35:1: error:
    
    Clash.Netlist.BlackBox(219): Couldn't instantiate blackbox for Sudoku.makeConst. Verification procedure reported:
    
    Argument 0 should be literal, as blackbox used ~CONST[0], but was:
    
    Identifier (RawIdentifier "c$app_arg" Nothing []) Nothing
    
    The source location of the error is not exact, only indicative, as it is acquired 
    after optimizations. The actual location of the error can be in a function that is 
    inlined. To prevent inlining of those functions, annotate them with a NOINLINE pragma.
   |
35 | topEntity = \i -> s !! i
   | ^^^^^^^^^

[DigitalBrains1]

Perhaps we should add an equivalent of smap that works on values instead of vectors, and errors if it couldn't compile-time reduce.

[edit]
I doubt that would work. I'm really not familiar enough with the inner workings here, but my gut tells me it doesn't work.

smap f x is all internal to smap. It gets a function and a value and applies the function to the value. In fmap (makeConst . f) x in the generated Core, the makeConst is in the wrong position to do the reduction. It needs to widen its net to where it is applied instead of working locally to make anything constant. Likewise, I don't expect fmap (smap f) x to actually have smap do constant reduction; it's just in the special case of smap f x as the exact expression (f and x are allowed to vary) that it will do its work.

Or something of that order. Again, I'm not familiar enough with the inner workings.

But we could add a variant of smap that doesn't get the SNat argument to at least make the code less surprising. It'd still only work fully applied, though.
[/edit]

[christiaanb]

Try:

topEntity :: "X" ::: Index 2 -> "Y" ::: Word8
topEntity = \i -> s !! i
  where
    -- s =
    --   smap (\_ c -> ascii c) $
    --     'F' :>
    --     'O' :>
    --     Nil

    -- -- This alternate definition of `s` works
    -- s = ascii 'F' :>
    --     ascii 'O' :>
    --     Nil

    s = makeConst $ fmap ascii $
        'F' :>
        'O' :>
        Nil

[DigitalBrains1]

D'oh! Of course! Yeah, that actually works!