Formal Methods have been proved to be a highly efficient method to develop and debug digital circuits. Up to now mostly companies with deep pockets could afford those tools. Since 2018, Symbiotic EDA is providing those efficient class of design tools to the rest of the chip industry.

Training

For experienced digital circuit designers with no prior knowledge of formal methods, Symbiotic EDA offers a 16 hour on -premise or online training, which provides a practical hands on learning experience.

The Symbiotic EDA Suite is a collection of software packages with a variety of functionality useful for the experienced designer of digital circuits. It improves productivity, speeds up design writing and refactoring, and makes discovering bugs easier, thereby increasing confidence in the designs functionality. Formal methods are used to verify existing and new digital logic designs and can be used to supplement simulation.

The Symbiotic EDA Suite is delivered as a single, all-in-one, easy to install, binary package tested on various Linux distributions.

Yosys Symbiotic EDA edition

… is a framework for RTL synthesis and provides a basic set of synthesis algorithms for various applications domains.

  • Process, Synthesize and analyze HDL designs
  • Industry-grade  HDL front ends for the following standards
    • Verilog 1995, 2000, 2005
    • SystemVerilog 2005, 2009, 2012
    • VHDL 1987, 1993, 2000, 2008
  • SVA Support
    • Sequences and Properties
    • Immediate and Concurrent Assertions/Assumptions/Cover
  • Highly extensible Enterprise Edition
    • Sequences and Properties
    • JSON import/export format

SymbiYosys

… extends the functionality of Yosys to do formal verification of digital circuits.

  • Standard features
    • Verification of safety properties
    • Unbounded verification of liveness properties
    • Reachability-chech and bounds-detection for cover properties
  • Advanced features
    • Facilitates management of unconstrained signals
    • Support synchronous, asynchronous and bounds-detection for cover properties
  • state of the art SMT solvers and HW model checkers
    • SMT: Yices, Boolector
    • AIGER: Avy, ABC, Super_Prover

License options:

Online license Edition

Workgroup Edition

Enterprise Edition

Research Partner License Program

Education and Training License Program