Formal has been making strides in recent years. “FPGA formal equivalence checkingfrom RTL to programming bitstream will become an absolute necessity,” says Marchese. https://semiengineering.com/will-tool-vendors-break-out-in-2019/ …
-
This Tweet is unavailable.
-
What I think is needed to handle that well is some kind of "map file" in which synthesis documents the transformations it did, and mappings from RTL to post-synthesis nets, so that the formal tool can detect the isomorphisms and verify the transformations are correct.
You probably want two equivalent checks. One of RTL vs post synth netlist, and one of that netlist against the bitstream. The latter is the LVS equivalent imo and can be done quite well. Former depends on the design and how crazy you want to get during synthesis.
-
-
Register balancing can be done during P&R though. Doing it at synthesis time misses lots of opportunities for compensating for wire length, IOs that are far apart from each other, etc.
-
Even Vivado only does register balancing when explicitly asked to (there are two switches that control this. One for synthesis and another one for pnr). I don't think any current ice40 flow (neither ours nor from the vendor) does register balancing in pnr.
- Show replies
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.