Meeting with Zach and Jonathan

[gussmith23]

cc @zsisco

Questions about the verilog->racket importer:

• Should the state track all possible states? Not just the last state?
  • this is specifically useful e.g. in verification, where you might want to make an assertion about the value this state had multiple timesteps ago.
• Are x's and z's squashable in Yosys? e.g. in match statements.

Bigger research ideas:

• Using the IRs of Lakeroad as a standard IR.
• There's an analog of the hardware compilation problem that Lakeroad is attacking in hardware verification.
  • Lakeroad (and previous works) basically say: removing all high-level structural information from Verilog as the first step in compilation is a bad idea. For one thing, it makes compilation really hard, because you have to compile a massive expression expressed in a low-level IR like and-inverter graphs. You have no high-level structural information (e.g. this is a memory, this is a multiplier) to guide compilation.
  • The analogous problem in verification: verification starts with the same step (I think), i.e. it removes all high-level structural information from a Verilog design. Thus, when verifying a multiplier, you have to verify it from the ground up, from the lowest-level bitvector expressions. However, if your multiplier was made with adders and shifters, and you had previously verified that your adders and shifters implement a certain function (expressed at a higher level than their low-level bitvector implementations), then we should be able to swap in that high-level expression, in place of the low-level, much larger expression.
  • The research problem is then, how do you do verification, taking advantage of hierarchical information?