Refactor to Typecheck Chirrtl Correctly #10
Labels
enhancement
New feature or request
v0.1
Issues that affect version v0.1 of secure-firrtl
v0.2
Issues that affect version v0.2 of secure-firrtl
v0.1 typechecks at the Chirrtl level but suffers from a number of soundness bugs due. One of the primary reasons for this is misinterpreting the "last connect semantics" of FIRRTL. Furthermore, label generation modifies the circuit but isn't executed when generating verilog.
v0.2 typechecks at the MidChirrtl level which is after the ExpandWhens pass, which elaborates the last connect semantics. However, this makes typechecking memories difficult since the memory reads and writes are no longer directly associated within a single statement. Furthermore, this elaborates everything into muxes and generates a large number of intermediate computations. This results in security over approximations causing safe circuits to fail to typecheck. It also induces significant overhead in both compilation and solver phases due to the verbose elaboration.
The goal of this issue is to fix the bugs in v0.1 by taking an approach closer to v0.2 that doesn't modify the circuit while still working at the Chirrtl level. This will result in both sound and efficient typechecking.
The text was updated successfully, but these errors were encountered: