Proposal: BTOR2 Primitives for Cider

[sampsyo]

This proposal is actually for a project that is already in progress. I'm writing it down to capture the plans we made when launching it and to crystallize what still needs to be done. The context for this is that @obhalerao has expressed interest in making this his MEng project in the spring semester.

Overview

The problem is that supporting primitives in Cider is tricky and brittle. You basically have to take the Verilog and rewrite it in Rust. This is already annoying for even simple things like std_reg and seq_mem_d1, and it's untenable for more complex primitives.

The idea, due to @ekiwi, is to let Cider execute the Verilog definitions of primitives themselves, via the BTOR2 intermediate representation. BTOR2 is an IL meant for model checking, but it contains a subset that is also perfectly suitable for executing bit-vector computations translated from Verilog. And yosys can translate Verilog to BTOR2; see #1757 by @NgaiJustin for the steps to do this for our standard primitives library.

Unfortunately, the reference BTOR2 implementation does not really contain an interpreter; the closest thing it has is a "witness checker" that runs the programs but doesn't let you just provide the inputs and obtain the outputs. So the plan in this little project is to write such an interpreter and integrate it with Cider so it runs whenever a primitive needs to be evaluated.

Progress So Far

Check out this CS 6120 blog post for a synopsis. @NgaiJustin took on the initial steps for his MEng project, and he teamed up with @obhalerao and @SanjitBasker to repurpose the effort as their 6120 course project.

As you can see from the blog post, we already have a working interpreter! That effort reuses the C parser for the BTOR2 language and consists of a new interpreter written in Rust. The interpreter is complete enough to run a bunch of Calyx primitives, compiled from Verilog by yosys. Cool!

What Remains

The rest of this effort, in my view, consists of:

1. Integrate the new interpreter into Cider, so the latter can use it to execute primitive semantics.
2. Do the "scaffolding" work required to automatically generate the BTOR2 code required for a given Calyx program for use by Cider.
3. Make the interpreter faster, as much as possible based on measurements from real executions of Calyx programs.
4. Replace the C parser with a homegrown parser.

I have put these in order of importance, and I think we should address them in approximately this order as well. (I am least certain about the ordering of 1 & 2 and of 3 & 4; those could both be swapped.)

I'll expand on each phase a little more below, but surely there is more detail to be added with time.

Integrate into Cider

This is sort of the obvious one: we need to hack Cider so it can call into the new BTOR2 interpreter. This probably means extending the interpreter's library-level interface so it's useful for what Cider demands of primitive evaluations.

I think this could have two significant sub-phases:

• combinational primitives
• sequential primitives

…because the Cider-level interfacing will look sufficiently different for the two styles. I think we should make this work for, like, one of each type as an initial milestone—surely covering a larger number of primitives will bring up more integration headaches, but we can take those one at a time after the MVP works.

Here's one tricky thing about this part: I really think it is not worth attempting this for OG Cider and we should only attempt to do this to the in-progress Cider 2.0. So here I would love some input from @EclecticGriffin: is this feasible? Is there any way in which we can set someone loose on attempting to do this in Cider 2.0 as it currently stands, even if it's not mature enough to run a real Calyx program yet? Optimistically, can we use this effort to help push forward the Cider 2.0 internals required for invoking primitives in the first place?

Generation Scaffolding

BTOR2 (unlike Verilog) is monomorphic, i.e., it does not have parameters. So to generate an executable BTOR2 program from a Verilog primitive implementation, we have to monomorphize it: at yosys invocation time, we supply all the Verilog parameters.

So we need a way to generate all the BTOR2 implementations that a given Calyx program we want to Ciderify might want to use. That process might look something like this:

1. Use a new Calyx pass/backend, which we would write, to look through a given Calyx program and record all the primitive instantiations it uses in a JSON file.
2. Use a pretty simple script to march through that JSON file and generate monomorphized BTOR2 implementations, based on our existing machinery from Automate SystemVerilog to BTOR conversion for Calyx Primitives #1757. This machinery will need to use name-mangling to generate filenames (or some other names) that Cider can then look up when it encounters the same primitive instantiations.
3. Teach Cider to look for those generated BTOR2 files when it starts up.
4. Make fud (or fud2) automate the end-to-end process. That is, when you do fud2 whatever.futil -s sim.data=something.json --to dat --through interp, it should do items 1 and 2 above automatically and then inform Cider of those locations when it launches the interpreter.

It occurs to me that step 1 above is quite similar to something @ayakayorihiro is encountering right now w/r/t generating monomorphized FIRRTL primitive implementations. So perhaps we just need one Calyx backend/pass shared between both of these efforts…

Optimizations

One "fun" part of the project could entail optimizing the BTOR2 interpreter. It is critical that this effort is data-driven, i.e., we profile entire Cider executions to find the primitives that are taking too much time and focus our efforts on optimizing those. Based on that, perhaps we can construct a benchmark that is independent of Cider but is representative of its primitive-related bottlenecks.

An incomplete list of optimizations we could try include:

• Flatten more interpreter data structures.
• Preprocess the BTOR2 to prune out unnecessary computations that don't feed into the outputs we're using.
• Fancy interpreter techniques, e.g., jump threading.
• Parallelize execution, to whatever extent there is parallelism available in the BTOR2 DFGs.
• In the extreme, try JITing to native code.

Rust Parser

Hopefully this is self-explanatory: we cleverly saved some work by reusing the C parser for BTOR2 from the reference implementation; someday, it would be nice if the interpreter were an all-Rust affair. And the grammar for BTOR2 is extremely simple, so hopefully this isn't that hard to do, even if it's a hand-rolled parser. Perhaps this could join up with @ekiwi's efforts in Patron?

[ekiwi]

Integrate into Cider

This point could be explored without having a working interpreter. Essentially, one could try to re-organize the current rust implementations of primitives such that calling into them looks more like calling into a hypothetical interpreter. Imho, one of the most interesting things to explore in this context would be how state is shared between Cider and the primitive executor. Can they both use the same, potentially statically allocated, memory region?

sequential primitives

I wonder if it would be possible to always execute the interpreter to completion, i.e. execute as many steps as we need in order for the computation to be done, without yielding back to Cider. This would make sequential primitives look like combinatorial primitives. Maybe @EclecticGriffin has some insights into whether this is at all feasible.

[sampsyo]

Yep, agreed on all counts!