| Summary: | Design Rust-based HDL like nmigen (deferred for later) | ||
|---|---|---|---|
| Product: | Libre-SOC's first SoC | Reporter: | Jacob Lifshay <programmerjake> |
| Component: | Source Code | Assignee: | Jacob Lifshay <programmerjake> |
| Status: | CONFIRMED --- | ||
| Severity: | enhancement | CC: | libre-soc-bugs, lkcl, programmerjake, vivekvpandya |
| Priority: | Low | ||
| Version: | unspecified | ||
| Hardware: | Other | ||
| OS: | Other | ||
| NLnet milestone: | --- | total budget (EUR) for completion of task and all subtasks: | 0 |
| budget (EUR) for this task, excluding subtasks' budget: | 0 | parent task for budget allocation: | |
| child tasks for budget allocation: | The table of payments (in EUR) for this task; TOML format: | ||
|
Description
Jacob Lifshay
2020-03-03 07:37:56 GMT
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. |