search

trailofbits / sv_circuit

Compile processor circuit to ZK-statement
GNU Affero General Public License v3.0
6 stars 2 forks source link

Use `yosys` for circuit flattening #64

Open jleightcap opened 1 year ago

jleightcap commented 1 year ago

For targets that require a fully inlined circuit, yosys itself can perform complete inlining. See: https://yosyshq.readthedocs.io/projects/yosys/en/latest/cmd/flatten.html

For targets with function calls (like the primary IR0+), a non-flattened circuit with @functions at module boundaries could yield more efficient circuits at verification time.

jleightcap commented 1 year ago

Note: the potential performance benefit mentioned is incorrect. The current singular tiny86 @function is optimal. CC @lisaoverall, I'm not sure I understood completely why that is the case.

lisaoverall commented 1 year ago

The current singular tiny86 @function is optimal.

At this point, this is a conjecture by our collaborators based on (I think) I/O performance in how their proof systems handle @function.