YOSYS - SYMBIOTIC EDA EDITION 

 

Yosys is a framework for RTL synthesis and provides a basic set of synthesis algorithms for various application domains:

​

• Process. synthesize and analyze HDL designs

  • Flexible, controlled using scripts​​​

  • Over 150 commands for a wide range of tasks

• Industry-grade HDL front-ends for the following standards

  • Verilog 1995, 2000, 2005​

  • SystemVerilog 2005, 2009, 2012

  • VHDL 1987, 1993, 2000, 2008

• SVA Support

  • Sequence and Properties​

  • Immediate and Concurrent Assertions/Assuptions/Cover

  • Safety, and Liveness, and Cover Properties

• Highly extensible

  • Yosys C++ and Python APIs​

  • JSON import/export format

  • Standard exchange formats: (structual) Verilog, BLIF, EDIF, etc.

​

​

SYMBIYOSYS - SYMBIOTIC EDA EDITION 

​

SymbiYosys extends the functionality of Yosys to formal verification of digital circuits.

​

• Standard features

  • Unbounded and bounded verification of safety properties

  • Unbounded verification of liveness properties

  • Reachability-check and bounds-detection for cover properties

• Advanced features

  • Additional attributes for management of unconstrained signals

  • Synchronous, asynchronous, and multi-clock designs, resets and latches

• SymbiYosys integrates with state-of-the-art SMT solvers and HW model checkers

  • SMT: Yices, Boolector, Z3

  • AIGER: Avy, ABC, super_prover

  • BTOR2: Boolector btormc

​

​​​

MCY - Mutation Cover with Yosys

​

MCY is a framework for strong formal-enhanced mutation cover for verification of test benches.

​

• Formal-enhanced mutation cover​

  • No false positives, because we check actual test-bench results

  • No false negative, because mutations are formally checked for relevance

  • Formal counter-examples for uncovered mutations

• Works with any test-bench that works on post-synthesis results

  • Works with any HDL simulator from any Vendor

  • Including FPGA-based prototype/emulation platforms

​

​

VERIFICATION IP​

​

Symbiotic EDA Suite ships with a library of Formal Verification IP.

​

• Bus-Interface Verification IP

  • Support for AXI, AXI-Lite, Wishbone

​

​

LICENSE OPTIONS

​

Symbiotic EDA Suite is available in different license options. Please contact office@symbioticeda.com for additional information.

​

• Symbiotic-CE  (Cloud Edition)

  • AWS Cloud Server with Symbiotic EDA Suite pre-installed

  • Pay by the hour (buy directly from AWS AMI store)

  • Setup instructions can be downloaded here.

• Symbiotic-OE  (Online Edition)

  • Use Symbiotic EDA Suite on as many machines as you like

  • Pay per CPU hour (package includes 100 hours per month, additional hours can be purchased as-needed)

• Symbiotic-WE  (Workgroup Edition)

  • Unlimited use on 20 node-locked licenses, plus 200 hours per month online licenses

  • Premium Support

• Symbiotic-EE  (Enterprise Edition)

  • Unlimited use for up to 200 users in your organization

  • Premium Support and Developer Support

​

​

FREE ACADEMIC / TRAINING / OSHW LICENSES

​

For academic users, training providers, and members of the open hardware community we provide free licenses. Please contact office@symbioticeda.com for additional information.

​

• SERP  (Symbiotic EDA Research Partner)

  • For university researchers and open source hardware developers

• SEET  (Symbiotic EDA Education and Training)

  • For use in university courses and other education/training settings​​