Help! How to use dtfold ? #2400
-
|
Sorry folks, but I can't work it out from the example+description in the manual at https://hackage.haskell.org/package/clash-prelude-1.6.4/docs/Clash-Sized-Vector.html#v:dtfold . Can anyone help? I am trying to implement a vector mux: for which the obvious, clean, sane simple implementation unfortunately synthesizes using many tens of thousands of logic units, say 60 thousands. My vector is 256 wide and each wire ("x") is some hundreds of bits wide. Yes, that sane implementation is This is a candidate to get the complexity down from 2^n to n log2 n in the classical way by recursive halving. The basic idea is ... do v !! i using the top bit of index i to select the first or the second of the two halves v1,v2 of v=v1++v2, and then recursively use the remaining bits of index i to select from inside the half-vector. Perfect for dtfold? Everything I try elicits incomprehensible (to me) type complaints about needing KnownNat l !-(. I must use vector v :: Vec (2^n) x to construct a function f :: Index (2^n) -> x So for dtfold I need to specify how, given two such functions f1,f2 constructed from the two halves v1,v2 with v1++v2=v, I make function f for v: (give me the lowbits function, say lowbits i = unpack i' where (_::BitVector 1,i') = split i) This is the combinator among the parameters to the dtfold function, though one needs to also say what level "n" it is at. Call it The other argument to dtfold is the base of the recursion/induction, applied to vectors length 1, i.e. the elements of the original vector v. Like this: (that index i is in the Index 1 type, which makes it necessarily 0, so we know what it is and ignore it). These components plus some mysterious type formula that I will call foo for now are put together by dtfold : so I should get and as far as I can make out from the manual that foo thing is given by and I want (???) Proxy @(IIndex x) where I have written Proxy @foo. The above definition of (!!!) gives the single error There is no "l" (letter "ell") anywhere in my definitions. I have declared KnownNat n of every n::Nat that I have introduced in these definitions. What is going on? Is this my mistake or a mistake in dtfold somewhere? The dtfold function wants its argument "combi" to have a universally quantified type that takes a natural as first argument, and combi is defined so that is so. What am I supposed to do here? Thanks for any light in the darkness. PTB |
Beta Was this translation helpful? Give feedback.
Replies: 6 comments 21 replies
-
|
Thanks for opening this discussion! I opened the documentation for Could you try explicitly applying (!!!) :: forall n . KnownNat n => Vec (2^n) x -> Index (2^n) -> x
v !!! i = dtfold (Proxy @foo) bse (combi @n) v i |
Beta Was this translation helpful? Give feedback.
-
|
The result of an @n on combi is a slightly different you-can't-do-that-there error :-( To me, it looks like the combi argument to dtfold needs to have a type that is valid for all possible naturlals l (or n), without the condition that is a KnownNat. But I can't write such a thing because split, splice and anything else I try using in combi (for lowbits) end up requiring a KnownNat. Any clue there? Is there some deeper interface I can get to somehow that will work to define lowbits without requiring the KnownNat l (or n). On the face of it split would do because it only requires KnownNat of the second result, and I can use BitVector 1 for that in lowbits i = unpack i1 where (i1,i2::BitVector 1) = split (shiftL (pack i) 1) But no, it lies and says KnownNat is required, leading to the complaint for (!!!) that KnownNat l is needed for the combi arg to dtfold. |
Beta Was this translation helpful? Give feedback.
-
|
It doesn't lie. The fact that is complains about a missing Luckily1 in this case we have an module TestDtfold where
import Clash.Prelude
import Data.Singletons (Apply, TyFun, Proxy(Proxy))
topEntity :: Vec 8 Int -> Index 8 -> Int
topEntity = (!!!)
lowbits :: (BitPack a, BitPack b, BitSize a ~ BitSize b + 1) => a -> b
lowbits i = unpack i' where (_::BitVector 1,i') = split i
combi :: SNat j -> (Index (2^j) -> x) -> (Index (2^j) -> x) -> (Index (2^(j+1)) -> x)
combi SNat f1 f2
= \i -> let i' = lowbits i in if msb i == 0 then f1 i' else f2 i'
bse :: x -> (Index (2^0) -> x)
bse x = \i -> x
data IIndex (x::Type) (f :: TyFun Nat Type) :: Type
type instance Apply (IIndex x) n = Index (2^n) -> x
(!!!) :: forall n x . KnownNat n => Vec (2^n) x -> Index (2^n) -> x
v !!! i = dtfold (Proxy @(IIndex x)) bse combi v iFootnotes
|
Beta Was this translation helpful? Give feedback.
-
|
What christiaanb said |
Beta Was this translation helpful? Give feedback.
-
|
Note that I would expect any and all synthesis tools to already do this by default. I tested with yosys for ECP5 and it does use a tree like structure. Not that it's not possible to do it structurally using For this it synthesizes to this circuit for target ECP5 (For some reason it renders incorrectly when opening the link directly. Please save the svg and view it that way) :
|
Beta Was this translation helpful? Give feedback.
-
|
Thanks! (nice diagram!) I'm running yosys for xilinx. The vector is 256 wide, the vector elements are 633 bits wide. Used in the muxN of a 256-vector of signals, fmapping the (!!) timewise along the signals, as exhibited in the post at head of thread, that is 66231 LCs. Can you confirm? (I'd still like to know how to use dtfold! It may be useful! For one thing I could save yosys optimization time even if it does manage to come out with that tree structure -- which is a feat of improbable reverse engineering that i am utterly amazed by) Ironically, I like this message from yosys: |
Beta Was this translation helpful? Give feedback.
-
|
That circuit is too large to visualize. Definitely synthesizes to a tree structure using With the size you used |
Beta Was this translation helpful? Give feedback.
-
|
Synthesizing with a few different configs This seems to be best it could theoretically do? If you increase the depth by 1 you double the logic cells since you now have two subtrees of the same size as the first one. If you double the element size you also double the logic cells since you need to select that many bits. So Logic cell usage is |
Beta Was this translation helpful? Give feedback.
-
|
@rowanG077 yes, thank you, that is very thorough of you. Yes, it also takes several hours (3h) here to synthesize with those 600+ bits wide wires and 256-dim vector, on this AMD 2.2GHz multicore machine. taking 4.5GB ram. You are correct ... the number of LCs is proportional to the width of the wires. I have split width wise and run two halves in parallel for the same behavior and about the same complexity, other than some duplicated circuit overhead. But no, I don't see that the number of logical primitives should be exponential in the depth. Isn't the depth the number of bits in the indexing, i.e. the exponent in the dimension of the vector of streams. So 2^depth is the number of streams N and you are saying N * W primitive logical components where W is the width of the streams. The classical number from recursive halving is N * depth * W. From your table: My datum was: |
Beta Was this translation helpful? Give feedback.
-
|
You can approximate the structure with a perfect binary tree. Each node is logic cell. A perfect binary tree of depth and |
Beta Was this translation helpful? Give feedback.
-
|
The structure also breaks out each bit of the index to drive in a different layer of the tree. That ends up as an extra multiplier in the complexity by the number of bits / aka depth of the tree. This is "intuitively" - I haven't tried drawing out the diagram and actually checking the intuition because it is so much part of learned and practiced lore that the complexity is n * log2 n! Maybe you're right! That the "constant of proportionality" is increasing with scale in your table argues against, however. Capital overheads should diminish in proportion with scale. Increasing points to a missed contributing factor. Management costs :-! PS. I generated another line of that table, for greater depth D: The last column number is still rising, so does not look to be bounding. The penultimate column number is still falling, so is apparently bounding. Falling is what I expect as capital overheads become proportionately less with increasing scale. |
Beta Was this translation helpful? Give feedback.
-
|
Try this: Pattern matching on the |
Beta Was this translation helpful? Give feedback.
-
|
@christiaanb Yes, that works! No "KnownNat n" in the definition of the combinator but pattern match on SNat as first argument instead. That seems like a technique! |
Beta Was this translation helpful? Give feedback.
-
|
With dtfold implementing !!, the results after synthesis with yosys for xilinx are the same as when using the standard !!. So yosys seems to automatically make a tree structure for xilinx too ... (256-way 633-bit wide multiplexer) Does anyone have any better ideas? This is very costly for such trivial functionality. Is it possible to use three-valued logic somehow? I could power down all but one of the incoming vector of streams very cheaply with a demuxer driven from the stream of incoming indices, and just join all the wires without any gating .... Thanks for all the inputs! |
Beta Was this translation helpful? Give feedback.
-
|
I am told "Quite a few of the FPGA designs come with significant amounts of onboard cache as they are used to develop specialized accelerators.". So it would be possible to write primitives that map to them., either in clash or yosys or both. I know how to do neither! (yes, I have seen the tutorial :-). a simple pull-through cache would have type: Plus a reset line of course! And some configuration parameters like n=log2 #lines (each an x). Internally n bits of the address will designate the line and the rest of the address bits will form a tag for each line, so one will need at least 2^n * (|x| + |a| - n) bits of internal space. There might be some extra bits for dirty/uptodate etc. flags so one can invalidate a line or age it, etc. Another parameter might specify if it is one-way, two-way, 4-way associative etc. Two way means doubled storage inside, with two lines stored for each |a| - n bits of address and the older of the two being replaced on write. Another parameter might specify which bits of address are indexing. Usually middle bits. I'll look out specs for a cache that can be written from the front too (as well as from the back; the above can only be asked for read from the front). Or tell me if you know! I just make this stuff up ... Are there any plans to target mapping to these components? |
Beta Was this translation helpful? Give feedback.
-
|
BlockRAM is the cache they mention. You will have to build your specific cache out of the blockRAM primitive. |
Beta Was this translation helpful? Give feedback.
-
|
Yes, they seem to be talking about "ultraram" (too) but as "replacement for external sdram" so one could deduce the working cycle will be roughly commensurate with sdram and some people have said it is as fast as 3 ns to me. "The fastest will be block ram (either Xilinx or Intel). It will be more than 1 cycle (except as lower speed for the most part). However, you can pipeline it such that you achieve it. Some FPGAs have embedded DRAM for this L1 type use, much faster than DRAM external on the board ..." - make what you will of that. There are fast caches on board these high-end FPGA platforms and the promotional literature seems to highlight them but I can't see how they are directly accessible to the FPGA design. Still, if they cache memory calls through the platform, then there may be no need to cache data to/from memory at all within the FPGA design. One can remove those caches from the design. In the meantime I have checked and one can make up for the lack of a 1-cycle reset line on blockRamU (and friends) in Clash by adding a filtering bitmap that records dirtied (i.e. written to) elements in the ram. Reading from an element said by the bitmap to be undirtied now returns 0 without consulting the ram. To effectively reset, just clear the filtering bitmap so every element is seen as undirtied again and 0 is returned for it. |
Beta Was this translation helpful? Give feedback.
-
|
ultraRAM is xilinx specific. UltraRAM is basically blockRAM + some restrictions that standard Xilinx blockRAM doesn't have. I expect ultraRAM be inferred from the Clash blockRAM primitive. https://docs.xilinx.com/r/en-US/am007-versal-memory/Block-RAM-and-UltraRAM-Differences blockRAM and ultraRAM are all documented by Xilinx. I'm not sure what you mean that they aren't accessible. |
Beta Was this translation helpful? Give feedback.
-
|
(My thanks to everyone who has participated here, by the way). However .... it appears not quite so easy to use blockRAM for cache. This cache has two write ports and two read ports and blockRAM has one write port and one read port. Two read ports can be simulated by running two blockRAMs in parallel, writing the same thing to both of them. But, but, but ... ... I can't write two times at once. OK, you say, so use trueDualPortBlockRAM instead. Yes, that has two ports but they are not duplex, so I cannot read at the same time as two writes are happening. Alright, that's only going to cause the cache to drop some read requests, so the requester will go to memory instead for those. And provided two writes are not happening at once I can read at two different places at once, by the same trick of putting two trueDualPortBlockRAMs in parallel. But then the read response is delayed one clock in block rams in general. That is, with a register implementation for caches, a read request gets immediately the value from one cycle ago, before the current write happened. Using a block ram a read request will produce nothing immediately, and one cycle later the value comes out, and I can't tell from the documentation if that will reflect the current write or not. Hopefully, being late, the response will at least take it into account. I might be able to resolve most of these difficulties with external logic, but not all, I (don't) think. |
Beta Was this translation helpful? Give feedback.
Try this:
Pattern matching on the
SNat(of typeSNat n) introduces theKnownNat nconstraint for anything in scope of the pattern match. As a result, you no longer need theKnownNat nconstraint in the type signature ofcombi, since anything inside the definition ofcombiwill now get theKnownNat nout of theSNat.