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

FloorSet: The First Million-Scale Dataset for SoC Design Planning.

FloorSet is aimed at advancing machine learning for floorplanning physical layouts of systems-on-a-chip (SoCs) and its sub-systems. It features 2 million synthetic benchmark circuits that capture real design constraints and objectives, all carefully sampled from actual design distributions.

FloorSet addresses key challenges of training-data availability and reproducibility in the chip-design world, driving fundamental research in large-scale constrained optimization problems.

Links:
📄 https://arxiv.org/abs/2405.05480
💾 https://github.com/IntelLabs/FloorSet

#floorplan #SoC #MLaimed #CAE #opensource
@fpgasic