Oh hi Rachit, long time no see. I sadly didn't have time to submit something to LATTE this year as I've been spending all my time building infrastructure for SUS.
I think improving the safety of hardware design is a noble goal, and certainly there is much that can be improved over Verilog & VHDL's incredibly brittle baseline.
Though for dynamic latency safety, my intuition tells me the problem space is undecidable. Sure one could prove the correctness of various kinds of dynamic latency pipelines, and as research progresses you'll include more and more such constructs, but it'll always remain possible to construct a correct but unprovable dynamic pipeline.
Given that, shouldn't we take a leaf out of Rust's book, and instead give the user tools to build abstractions which internally contain unprovable but correct black magic, yet on their interface provide a safe, static latency count.
Take for instance SUS' SlowState. It abstracts over an internal state, and the user provides a pipeline to update this internal state. Now, if we were to update the state twice, before the change has had time to propagate through the pipeline, that would be an error. SlowState prevents you from doing so by statically measuring the length of the update pipeline, and only allowing updates once it has cleared.
Implementing SlowState requires some unsafe, but it can provide a safe interface upholding its requirement.
I was really happy to see that blue spec was fully open sourced in recent years. Does anyone have experience with a non trivial project with it? Does it have any traction anymore in real silicon development.
Same here, looking for an excuse to use it. It takes some time to get oriented. The BSV fronted makes it easier though. Have been dabbling in it as a hobby on the side.
While there have been tape-outs by universities, I think the learning curve would discourage traditional hardware companies focused on TTM. While bluespec has higher level abstractions, it also provides access to low level HW optimization features like multiple/gated clocks, integrate verilog etc. so I don't see any hindrances.
One needs to be familiar with both using SW abstractions and HW design, which iss a small subset that limits it's usage.
I learned logic design in a class where we wired up 74LS TTL, a couple of years before they switched to programmable logic, so my knowledge of this sort of thing comes from looking over the shoulders of folks who actually do it, but it seems really cool. In particular, I love the idea that you can shoehorn all sorts of temporal constraints into a type system.
I fear that progress in this field might be handicapped by the fact that the folks who know a lot of type theory have little idea of how hardware works, and rarely care, and most of the folks who know how hardware works don't know a lot about types beyond possible bad experiences with VHDL. Luckily there's a non-zero set of people in the overlap, though.
For discrete designs rather than integrated chip design there are some less formal type systems already build in to KiCad, for example using net classes, footprint categories, and pin counts to limit parameter selection. I suspect other design tools are similar.
Strong type systems require zero exception domains, but unfortunately physics isn't a zero exception domain in the way software is: there's always an oddball requirement which has to cater to differences in supply chain, production process or partner, final assembly, testing, operating environment, etc.
In my experience what you tend to see emerge in thornier domains are multiple overlapping systems of relaxed formality that get the job done while retaining a comprehensibility through reduced cognitive load. That is, "useful approximations". In discrete design we can view the standard set of formalisms (symbols, footprints, netlists, etc.) as relaxed type system examples.
Each have issues. Each differ somewhat over time and package. Yet they are still how things are usually designed after decades of evolution, and I don't see that changing for manual discrete designs beyond relative triviality any time soon.
In fact, on zeitgeist I'd wager the problems people are seeing trying to march beyond the status quo in to AI designed schematics, board layouts and firmware are analogous to those issues your prospective type system is going to have problems exhaustively formalizing.
I have no experience designing custom silicon, the apparently intended domain here, but I am skeptical enough to wager it isn't free of the thorny problems we see in discrete electronics: that is, physics doesn't let you select arbitrarily without vengeance, so treating your system as a simple system of lego bricks (albeit 'guaranteed type-compatibile') is never going to yield reliable results. Specific decisions probably require multi-disciplinary insights across thermal models, EMI/radiation, timing and power, not just "the plug fits". Further complicating change is social friction and time friction. I'd wager the stronger designers are deeply invested in current tooling (hell, they probably wrote it) and not time-rich enough to try something new because "academia". Their projects are expensive and often set to difficult schedules.
Good luck changing the world! Perhaps building enhanced type systems specifically targeting the AI design domain would be the best approach, because uptake will be quicker than humans? Maybe consider joining one of the AI-designs-my-board startups.
Oh hi Rachit, long time no see. I sadly didn't have time to submit something to LATTE this year as I've been spending all my time building infrastructure for SUS.
I think improving the safety of hardware design is a noble goal, and certainly there is much that can be improved over Verilog & VHDL's incredibly brittle baseline.
Though for dynamic latency safety, my intuition tells me the problem space is undecidable. Sure one could prove the correctness of various kinds of dynamic latency pipelines, and as research progresses you'll include more and more such constructs, but it'll always remain possible to construct a correct but unprovable dynamic pipeline.
Given that, shouldn't we take a leaf out of Rust's book, and instead give the user tools to build abstractions which internally contain unprovable but correct black magic, yet on their interface provide a safe, static latency count.
Take for instance SUS' SlowState. It abstracts over an internal state, and the user provides a pipeline to update this internal state. Now, if we were to update the state twice, before the change has had time to propagate through the pipeline, that would be an error. SlowState prevents you from doing so by statically measuring the length of the update pipeline, and only allowing updates once it has cleared. Implementing SlowState requires some unsafe, but it can provide a safe interface upholding its requirement.
I was really happy to see that blue spec was fully open sourced in recent years. Does anyone have experience with a non trivial project with it? Does it have any traction anymore in real silicon development.
Same here, looking for an excuse to use it. It takes some time to get oriented. The BSV fronted makes it easier though. Have been dabbling in it as a hobby on the side.
While there have been tape-outs by universities, I think the learning curve would discourage traditional hardware companies focused on TTM. While bluespec has higher level abstractions, it also provides access to low level HW optimization features like multiple/gated clocks, integrate verilog etc. so I don't see any hindrances.
One needs to be familiar with both using SW abstractions and HW design, which iss a small subset that limits it's usage.
I learned logic design in a class where we wired up 74LS TTL, a couple of years before they switched to programmable logic, so my knowledge of this sort of thing comes from looking over the shoulders of folks who actually do it, but it seems really cool. In particular, I love the idea that you can shoehorn all sorts of temporal constraints into a type system.
I fear that progress in this field might be handicapped by the fact that the folks who know a lot of type theory have little idea of how hardware works, and rarely care, and most of the folks who know how hardware works don't know a lot about types beyond possible bad experiences with VHDL. Luckily there's a non-zero set of people in the overlap, though.
For discrete designs rather than integrated chip design there are some less formal type systems already build in to KiCad, for example using net classes, footprint categories, and pin counts to limit parameter selection. I suspect other design tools are similar.
Strong type systems require zero exception domains, but unfortunately physics isn't a zero exception domain in the way software is: there's always an oddball requirement which has to cater to differences in supply chain, production process or partner, final assembly, testing, operating environment, etc.
In my experience what you tend to see emerge in thornier domains are multiple overlapping systems of relaxed formality that get the job done while retaining a comprehensibility through reduced cognitive load. That is, "useful approximations". In discrete design we can view the standard set of formalisms (symbols, footprints, netlists, etc.) as relaxed type system examples.
Each have issues. Each differ somewhat over time and package. Yet they are still how things are usually designed after decades of evolution, and I don't see that changing for manual discrete designs beyond relative triviality any time soon.
In fact, on zeitgeist I'd wager the problems people are seeing trying to march beyond the status quo in to AI designed schematics, board layouts and firmware are analogous to those issues your prospective type system is going to have problems exhaustively formalizing.
I have no experience designing custom silicon, the apparently intended domain here, but I am skeptical enough to wager it isn't free of the thorny problems we see in discrete electronics: that is, physics doesn't let you select arbitrarily without vengeance, so treating your system as a simple system of lego bricks (albeit 'guaranteed type-compatibile') is never going to yield reliable results. Specific decisions probably require multi-disciplinary insights across thermal models, EMI/radiation, timing and power, not just "the plug fits". Further complicating change is social friction and time friction. I'd wager the stronger designers are deeply invested in current tooling (hell, they probably wrote it) and not time-rich enough to try something new because "academia". Their projects are expensive and often set to difficult schedules.
Good luck changing the world! Perhaps building enhanced type systems specifically targeting the AI design domain would be the best approach, because uptake will be quicker than humans? Maybe consider joining one of the AI-designs-my-board startups.