logo.png
LINKS
ABOUT

Symbiotic GmbH 
Alaudagasse 11/107/6 
1100 Vienna 
Austria

ATU73115835

SOCIAL

© 2019 All rights reserved - find out more about our privacy policy

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)

  • 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 researchers and open source hardware developers

  • SEET  (Symbiotic EDA Education and Training)

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

SMART EDA EMPOWERMENT

SYMBIOTIC EDA SUITE

01 / DESIGN

Find bugs early and raise the confidence in your design by using formal checks and formal properties. Apply formal early on in the design process wherever it makes sense for your application.

02 / DEBUG

Use formal cover traces to further your design understanding and answer hard questions about the design under test. Apply formal safety properties to produce shorter and more insightful traces than simulation could ever generate.

03 / VERIFY

Employ formal proofs to ensure correctness of your design, use mutation cover to gain confidence in your simulation-based verification strategy, and speed up writing of test cases by guiding the process with formal cover traces.

REQUEST A DEMO

Tools you are interested in:

Environment you might use our tools:

Subscribe to Our Site!