Speaker
Description
Yosys is a well-known open source framework for design synthesis and verification. This talk presents an overview of the Yosys-based tools, with a focus on issues relevant to applications of FPGAs in space. Thanks to its extensibility and open interfaces, Yosys is an excellent basis for building both generic and highly customized EDA tools. Examples of such tools by YosysHQ include formal verification of safety properties with SBY, mutation coverage and fault injection with MCY, the new formal sequential equivalence checking tool EQY, and upcoming deep formal cover trace generator SCY. The same interfaces enable third party developers to create their own applications such as the Linty tools (https://www.linty-services.com/) detecting bugs and enforcing coding standards.
SBY (Symbiyosys) is an open source tool for formal verification of SVA properties, such as safety properties, cover properties, and liveness properties, and the generation of formal witness traces.
MCY (Mutation Cover with Yosys) is an open source framework for mutation coverage with a formal verification twist. A main issue with coverage is false negatives: code that appears covered, but even though it is executed, its consequences are not propagated to output ports, or the test bench does not check the output. Mutation coverage solves this issue by introducing a change to the design and making sure that the testbench fails on the modified design. However, this adds a new issue: False positives. False positives are mutations that are not considered covered, simply because they do not actually change the behavior of the design under test. MCY employs formal methods to filter out such false positives, thus providing a significantly more useful coverage metric than most other coverage tools.
Instead of testing a testbench, the same functionality can also be used to test a design's fault tolerance: By setting up the formal test to flag any unexpected change in outputs, it will exhaustively check whether a single-bit mutation can cause an error.
EQY (EQuivalence checking with Yosys) is a brand new open source framework for formal equivalence checking, with focus on verification of post-synthesis netlists generated by other tools. It employs a two-step process in which first candidates for equivalent points in the gold and gate netlists are identified, and then those equivalent points are used to split the large equivalent checking problem into many smaller ones, that each can be solved in relatively short time.
SCY (Sequence of Covers with Yosys) is an upcoming open source framework for producing deep formal cover traces for large designs. With SCY a user can specify a sequence of cover statements that is then eagerly solved by the framework one at a time, using the final state of one such cover trace as the initial state for the next coverage property. With that it becomes possible to generate deep formal traces showing complex bus interactions on an entire SoC. With SCY we also add support for data-flow properties to our formal tools, as those properties are especially useful for encoding properties dealing with complex system buses.
