See: http://lists.libre-riscv.org/pipermail/libre-riscv-dev/2020-March/004725.html
Experimental, we are likely to not change to using this even if it works due to network effects benefiting nmigen.
if there was ever a compelling reason to do this it would be if there was, like BSV, a 100% guarantee that syntactically-correct HDL was synthesiseable. this however is only the case in BSV because it utilises the formal proof / functional programming aspects of Haskell.
(In reply to Luke Kenneth Casson Leighton from comment #2) > if there was ever a compelling reason to do this it would be if there was, > like BSV, a 100% guarantee that syntactically-correct HDL was > synthesiseable. this however is only the case in BSV because it utilises > the formal proof / functional programming aspects of Haskell. Rust does support type and lifetime-based formal proofs, which is one of the reasons I really like it.
(In reply to Samuel Falvo II from email) > I can see the benefit that algebraic types can offer; however, it's not > clear to me how Rust's borrow-checker would be a benefit for synthesis, or > logic design at all for that matter. Have you run into a situation in the > past where the borrow checker would have proven advantageous to have around? I was thinking lifetimes might be useful for proving that combinatorial logic doesn't have loops. Most of the benefit I can see is not actually the algebraic sum (enum/union) types, but actually Rust's generics, trait system, compile-time function evaluation (const fn -- like C++ constexpr), and const-generics (generics based on values rather than types). > (In reply to Jacob Lifshay from comment #3) > > (In reply to Luke Kenneth Casson Leighton from comment #2) > > > if there was ever a compelling reason to do this it would be if there was, > > > like BSV, a 100% guarantee that syntactically-correct HDL was > > > synthesiseable. this however is only the case in BSV because it utilises > > > the formal proof / functional programming aspects of Haskell. > > > > Rust does support type and lifetime-based formal proofs, which is one of the > > reasons I really like it.
(In reply to Jacob Lifshay from comment #4) > (In reply to Samuel Falvo II from email) > > Most of the benefit I can see is not actually the algebraic sum (enum/union) > types, but actually Rust's generics, trait system, compile-time function > evaluation (const fn -- like C++ constexpr), and const-generics (generics > based on values rather than types). there are a couple of ways to do this. the first is just to have Signals, Muxes, Ifs etc and to create an AST in memory, just like in nmigen. on *top* of that can be considered the addition of data types, such that, just as in BSV, a bool type can *not* be assigned to a 1-bit Signal, nor can one signal of one width be assigned to one of another width, you *must* do an explicit slice. clocks, reset and cross-domain data transfer was particularly irksome in BSV, particularly when trying to assign a dual role GPIO pin to be a clock output for one pinmux selection and a plain GPIO for another. getting this right *without* the tool being an absolute ftickin nuisance that just makes you wish you'd never started down this path needs a careful balance.