I've recently started writing my own HDL as an embedded language within Idris. The idea behind it is that you can take advantage of the rich type system and you have the option to prove theorems about your circuits to gain confidence in them. There are also bindings to picosat, so that you can automatically prove some properties. Here's a snippet of how it looks so far (though things are changing rapidly):
lt : BoolOperation op => Vect n v -> Vect n v -> SSA op v v
lt [] [] = constOp False
lt (x :: xs) (y :: ys) = do
nX <- notOp x
t1 <- andOp [nX, y]
t2 <- xnorOp x y
t3 <- lt xs ys
t4 <- andOp [t2, t3]
orOp [t1, t4]
I haven't touched the code since I graduated last year, and I've had various ideas about how I should restructure it since then. The most interesting part of the project is probably the implementation of guarded channels, which turned out to admit useful Functor and Applicative instances.
I hope to start as a PhD student next year working on a new version of the language taking into account what I've learned since then. Most notably, GHC's recursive do-notation sounds like it will be incredibly useful for creating the kind of monadic cyclic graph structures needed for hardware.
That's just combinational logic, how do you implement clocked processes and latches?
In my (admittedly limited) experience with hardware design making correct pure combinational logic isn't generally too difficult, it's keeping track of the state and state transitions that's problematic.
I'm glad you asked. At the moment, only combinational circuits are possible, but I'm working to extend this to synchronous (clocked) circuits.
When you need feedback, there will be a combinator that will look something like this:
feedback : Vect n Bool -> (Vect i v -> Vect n v -> SSA op v (Vect n v, Vect o v)) -> Vect i v -> SSA op v (Vect o v)
This is all up in the air. I'm still working it through.
I'm very keen to end up with something that it nice to use, even at the expense of being difficult to implement.
I may be getting ahead of myself, but I'd like to have functions that do things like: take a combinational circuit and return a synchronous circuit where the logic is evenly separated (in terms of delay) over n clock cycles.
