I did my bachelor's project on translation between functional HDLs that were also reversible, i.e. only describing total, bijective functions. The idea of functional HDLs goes back to at least the 1970s, and the coolest language I found was 𝜇FP by Mary Sheeran. It was an algebraic VLSI design language where logical gates as combinators are the only language constructs.
That sounds cool. I don't know anything about HDLs, but can you explain why you might want your functions to be bijective? What does that give you in hardware?
