P4Synth: 1000x faster function synthesis vs. SAT

(github.com)

1 points | by ashtonsix 4 hours ago ago

2 comments

  • colinb 3 hours ago

    Wholly ignorant passer by here. Is this a thing that’d make (notoriously) slow FPGA synthesis (by which I think I mean the conversion of VHDL or Verilog to something that can be injected into an FPGA) much faster?

    • ashtonsix an hour ago

      No, but it could help people build those synthesis tools much faster.

      P4Synth takes a (mathematical) group of functions/expressions and finds strong candidate implementations for every class in that group. Then, as long we have a fast (expression → class) mapping for that group we can use the generated solutions as a database embedded within the compiler for automated expression replacement (or mapping from expressions to circuits/technology).

      Vivado/Quartus (FPGA) technology mapping and LLVM's InstCombine stage are essentially this. InstCombine's pattern library is partially human-authored, partially generated by search tools; it lists ~30k subexpression replacements like a+a+a → a*3. P4Synth competes with those search tools. For hard function classes, existing methods might take weeks on a supercomputer: P4Synth speeds that up exponentially.

      It only solves a narrow toy problem right now (4-input boolean functions), but I believe the technique could scale with modifications (like A* style prioritisation over signal-set novelty and implementation score).