module FinFnsBool where
import Clash.Prelude
tf
:: (Bool -> Bool)
-> Bool
-> (Bool -> Bool, Bool)
tf f b = (not . f, f b)
tfun
:: SystemClockResetEnable
=> Signal System Bool
-> Signal System Bool
tfun = mealy tf not
topEntity
:: Clock System
-> Reset System
-> Enable System
-> Signal System Bool
-> Signal System Bool
topEntity = exposeClockResetEnable tfun
I was told on slack that clash tries to rewrite all functions with its definitions till it can be straightforwardly be converted to vectors (or something along those lines).
Is that the problem here?
Bool -> Bool cannot be reduced because it needs an argument and hence cannot be the state type of mealy?
I guess the compiler doesn’t try to represent Bool -> Bool as a 2x2 matrix?
Even though Bool is known to be a finite type (with an NFDataX instance).
If we change not to complement, we get another error:
Not in normal form: no Letrec: [...]
Which isn’t very clear either.
But it hints that clash encounters, or is left with, something in a form that it wasn’t expecting.
The internally the state s of a mealy is stored in a register.
And in your case this state is of type Bool -> Bool.
But this is just something that isn’t supported by clash, storing functions in registers.
Clash has no mechanisms to generate HDL for that.
While in principle you could store truth tables, the 2x2 matrix you mentioned.
This isn’t something that is implemented in clash.
And I suspect it would be quite tricky to get working in general.
Looking at this I’m thinking maybe we should remove the NFDataX (a -> b) instance.
Unless there is a good reason to have that instance, which I can’t see right now.
None was provided when it was introduced.
And your problem seems like a good reason not to have the instance.
I was thinking that each function usage would be rewritten with their definitions till all function calls become expressions.
ie, till everything boils down to a bunch of finite values which can directly be converted to their bitvector representation.
The fundamental problem here is that unlike in Haskell, in Verilog functions aren’t considered values.
When clash generates a register in Verilog it uses a template which looks something like:
// register begin
always @(posedge clk or posedge rst) begin : result_1_register
if ( rst) begin
result_1 <= XXX;
end else begin
result_1 <= YYY;
end
end
// register end
These XXX and YYY have to be some have to be valid Verilog values, or expressions which evaluate to values.
And not in Haskell is something like:
not = \x -> case x of
True -> False
False -> True
Clash has no mechanism to translate that into a valid Verilog value.
It’s only when the function is applied to an argument that clash could(*) generate something like:
x ? 1'b0 : 1'b1
But that is only the translation of the case part of not:
case x of
True -> False
False -> True
But clash has no way to translate the \x -> part to a Verilog value.
* In reality clash uses a template to translatenot x into an expression with the Verilog not operator: ~ x.
But the same basic problem remain, you (or clash) are not allowed to simply put ~ in place of XXX or YYY.
To continue from @leonschoorl’s excellent answer, @Julin can you think what hardware \f -> not . f should compile to? What does that look like as a circuit? you’ve made f “larger”, and every time you iterate using mealy, f gets even larger. Circuits can’t grow at runtime. For your specific example, you can get away with having your state be a Bool and call not on it in every cycle, applying xor s b as the output.
tf s b = (not s, xor s b)
tfun = mealy tf True
This feels quite related to the algebra of types that make up ADTs - a function of type Bool → Bool has 2^2 inhabitants, but you only care about two of them - id and not, so you can represent that function using just two values - a bool indicating whether you want to invert the input or not.
Basically, the summary you should take away from this is that clash can only produce outputs which can work on real hardware, and functions don’t exist on real hardware. We can’t pass them around like we do in FP (but was can use them to make circuits - clash gives us an excellent meta language for describing circuits). If you think you need to create functions at runtime, then you’re probably doing something wrong. I’ll also note that the solution I suggest is also what I’d use in Haskell without the ‘needs to work on hardware’ constraint - repeated application of not here makes f’s runtime grow linearly with the number of iterations, so this actually ends up being an O(N^2) algorithm!