Shimmers (Synthesize Hardware In Modular Macro Expansions and Runtime in Swift) is a functional framework for creating circuits. You write regular Swift code, and Shimmers turn it into hardware generators with Macros automatically. Shimmers also reasons about the design during synthesis, which enables inline formal verifications, and unbounded while-loop unrolling.
Since learning about HDLs, I have been thinking about how to make an HDL that’s easy to use.
I begin with the realization that every combinational circuit is a function. Moreover, a combinational circuit can fully describe a sequential circuit as the function that changes the states. Thus, it must be possible to create a language that describes circuits purely functionally. The circuit will be represented by a sequence of function calls that can themselves call other functions. By introducing limited mutability, these functions can be used to describe the change of states.
There are many immediate benefits of designing circuits totally functionally. First, using functions eliminates an entire class of design mistakes by enforcing the directed acyclic nature of combinational portions of the circuit. Existing toolings can discover these mistakes, but these mistakes are simply impossible to write. Second, a functional language is easy to read. It purposefully avoids the wiring mess in other HDLs. It’s thus easy to reason about what a function does as a human.
There are also many indirect benefits. First, the length of the function call is an approximation of the critical path of the circuit. This allows designers to develop intuitions about the complexity of the design, leading to better design in general. Second, Functional code is very easy to reason about by a computer, too. There is extensive research into how to perform all sorts of analysis on it. This allows more advanced tooling to be developed to ensure design correctness. Third, functional codes are highly composable. This benefit is not immediately obvious, but it will be discussed in depth.
To realize such an HDL, I first tried creating my own syntax and compiler. However, my lack of knowledge in type theory deterred me from going that route after a whole year of trying and failing. Instead, I settled on the approach that my instructor for CS 2110 instructor, Austin Adams, took. He was a PHD student working on a Quantum programming language. His language uses the Python frontend, but uses a custom backend to generate quantum code. The idea is that I can take an existing language and use it for my own purpose.
I used Swift to build Shimmers on. Swift had just acquired its Macro system in 2023 through the Swift Syntax project, which allows arbitrary syntax transformations directly at the AST level. Furthermore, Swift’s value type and mutability features are well-suited for creating hardware, as everything is by-value, and pointers and references are abstracted away.
Then, I built Shimmers (Synthesize Hardware In Modular Macro Expansions and Runtime in Swift). Shimmers have three parts that form a complete HDL system.
First, it contains a hidden library to construct hardware generators. This library is similar to Chisel. But unlike Chisel, this library is a mirror of the Swift Standard Library. Common types in Swift have a mapping in this Library. Usually, these types have the suffix Ref. For example, the Int type has the mirror IntRef. The purpose of this strict naming convention is that the Macros can derive the mirror type trivially and purely syntactically. This library also contains the necessary driver code, netlist emitter, and formal tools.
Second, it contains a Macro system that converts regular Swift code into the generators. Since the hardware library is only used by the generated code from the Macro system, most of them are hidden. This approach had the additional advantage that all hardware written in Shimmers can be simulated trivially, as the code you write is just regular Swift code.
Third, Shimmers contains runtime support as extensions to the Swift Standard Library. These extensions enable hardware-specific things to be done with the standard types. For example, it supports grabbing any bit from the standard Int type, for example. This set of extensions also introduces many hardware-specific types, like NInt<k>, where k is any positive integer, which allows arbitrary-length integers to be represented and simulated. Of course, these new runtime types will have their hardware generator mirrors, like NIntRef<k>.
In this front, Shimmers is truly unique. Shimmers is not a new HDL, as the code you write is just Swift. Shimmers is not strictly an embedded language either, as you don’t manipulate generators directly.
As described earlier, combinational circuits are just functional code. Below is an ALU in Shimmers. Notice how this is simply a regular Swift function with macro annotations. Even without knowing about Swift, the following code should be self-explanatory.
Code in Shimmers does not have to be purely functional. Mutating variables in local scopes are allowed. As long as this mutable variable does not escape the function, the function has no side effects. Mutating variables in the caller is also allowed through the inout parameters. This is valid too, as some callers must have a mutable local variable.
Notice that simulating this code is trivial, as it’s just running the written Swift code as-is. Shimmers (and any Swift Macro in general) cannot modify the AST of the source. This makes it possible to simply run the execute function by providing it with concrete values.
You are not limited to the existing data types in Shimmers. You can create new ones, too. Notice the instruction type used earlier. It could be reasonably built like this:
Methods can be defined on the Instruction type. In this way, the called value itself is passed as an implicit argument, and the function is still a combinational one. Notice that there is a computed variable named isValid. This is a getter function that behaves like a variable. By this logic, the execute function can be rewritten as a method of the instruction. Also note that the function has a guard statement of early return. This will skip the function if isValid is false. Pretty cool, right?
As a teaser, Shimmers also supports enums with payloads. So you can write the instruction as one big enum, and use the switch statement as your instruction decoder.
You can learn more about constructing hardware in Shimmers here.
Sequential circuits in Shimmers are simply built with mutable functions. Mutable functions are simply methods of a value type that change the self in some way. Since Swift is strict about mutability, a mutating function must be marked with the mutating keyword. For example, a processor can be built by putting the states inside a struct and using a top-level function to change them.
Note that not all mutating functions are sequential, since a mutating function can also be called on a variable within some function’s local scope. For example, the += operator is a mutable function. Thus, the difference between a sequential over a combinational function is purely in whether Shimmers generate registers. This is why isSequential is a property of the TopLevel macro, not a separate macro. This means that a faster version of this processor can simply be built by doing two cycles of work in one cycle.
Magical, isn’t it? Though there are many reasons why this is unsound. The most important reason is that we just doubled the critical path and doubled the memory port. But if it’s running with an atrociously slow clock, you might as well improve the performance like this.
But most importantly, we just doubled the design in function without changing the internal wires at all. If this is a processor in Verilog, for example, I need to change every aspect of the processor to accomplish the same behavior. But since Shimmers is functional, we get this power for free.
Pipelining is even easier. Suppose each pipeline stage is its own struct with mutating functions. A simple pipeline design is just about advancing the pipelines in reverse.
Stalling can also be easily managed. A pipeline stall occurs when a later stage cannot be advanced, which forces the earlier stages to stop. Functionally, in Shimmers, a pipeline stall can just be accomplished by returning early after a stage, after a stall is known. This is natural, as the early return on a later stage won’t execute the earlier stages.
Value forwarding can be done too. Just have the later stage return an extra value that is directly fed into the previous stage’s advance function.
This is the true power that comes with Functional design in Shimmers. To learn more about designing sequential circuits in Shimmers, read Shimmers documentation here.
One of the most important innovations in Shimmers is that it performs formal verification during synthesis on the partial netlist. This allows early discovery of design problems, and also some cool language features.
First, Shimmers honors the safety provided by Swift. Since Shimmers aims to mirror the runtime behavior of Swift in hardware, it translates the safety features of Swift to formal proofs during hardware generation. When generating designs in Shimmers, synthesis will only complete successfully if these operations are proven to be impossible. For example, the first function may not pass synthesis depending on its usage, as the addition may overflow. But the second function will always pass synthesis.
Second, Shimmers allows the user to place explicit formal assertions to ensure their design behaves as expected. These macros allow you to establish design preconditions and prove design correctness. For example, suppose I have a design that performs division combinationally. In this divider, I place two assertion macros to ensure design correctness.
The first assert macro ensures that no user of this function can pass in the number zero as the operand for b. The second assert macro ensures that the opaque division code is always correct. There are other formal macros in Shimmers. To learn more about them, visit the documentation on Formal Methods.
Lastly, Shimmers uses formal verification internally to unroll loops. For example, the following code computes the smallest doubling of a number greater than 10. For example, 1 gives 16, 2 gives 16, 3 gives 12, 4 gives 16, 5 gives 15, 6 gives 12, etc.
Synthesis in another language will simply give up in this scenario, but this code in Shimmers is synthesizable. This is because Shimmers will keep unrolling the loop until the loop is proven to definitely stop. For example, this loop will only go on five times, as it takes the smallest allowed number, one, five doublings to reach 16.
This may also seem like magic, but because Shimmers performs formal verification on the partial netlist during synthesis, this could be done. You can go nuts, by the way. The following code is a naive bubble sort that Shimmers can successfully unroll.
You can learn more about the formal capabilities of Shimmers here.
Shimmers is still a very young language. I wish to perfect it to a point where people can start designing real-world hardware, and there are still a few challenges in the way. First of all, the foreign module interface is nonexistent. It is currently impossible to wrap another design in Shimmers as a submodule. Second, the debugging facility needs to be perfected in such a way that the user can get some information out of error messages. Currently, this is a very difficult task, and macros have no access to semantic information. But as Swift Syntax matures, there may eventually be workarounds. Furthermore, I need to add support for more of the Swift standard library, as well as create new APIs that are only relevant to hardware designers. Perhaps after that, I can design a few RISC-V processors in it and submit them for fabrication.
