SymbiFlow is a work-in-progress FOSS Verilog-to-Bitstream (end-to-end) FPGA synthesis flow, currently targeting Xilinx 7-Series, Lattice iCE40 and Lattice ECP5 FPGAs. Think of it as the GCC of FPGAs.

https://symbiflow.github.io/
https://github.com/SymbiFlow

#xilinx #yosys #ice40 #series7 #latticesemi

Formal Verification with SymbiYosys and Yosys-SMTBMC
◦ Presentation Slides
◦ Examples

Investigating and Verifying Hardware Designs with Formal Open Source Tools
◦ Presentation Slides
◦ Examples

References:
==========

Yosys family:
◦ Yosys - a framework for Verilog RTL synthesis. It currently has extensive Verilog-2005 support and provides a basic set of synthesis algorithms for various application domains
◦ SymbiYosys - a front-end driver program for Yosys-based formal hardware verification flows

SAT and SMT solvers:
◦ Z3 Theorem Prover
◦ Yices2 SMT Solver
◦ Boolector
◦ ABC
◦ super_prove
◦ Avy

#Formal #Verification #SymbiYosys #Yosys #solver #publication #opensource

OpenLANE is an automated RTL to GDSII flow based on several components including OpenROAD, Yosys, Magic, Netgen, Fault and custom methodology scripts for design exploration and optimization. The flow performs full ASIC implementation steps from RTL all the way down to GDSII - this capability will be released in the coming weeks with completed SoC design examples that have been sent to SkyWater for fabricaiton.

https://github.com/efabless/openlane

#GDSII #PDK #RTL #OpenROAD #Yosys #Magic #Netgen #SkyWater