Mutation Cover with Yosys (MCY) Documentation

MCY is a new tool to help digital designers and project managers understand and improve testbench coverage.

If you have a testbench, and it fails, you know you have a problem. But if it passes, you know nothing if you don’t know what your testbench is actually testing for.

Given a self checking testbench, mcy generates 1000s of mutations by modifying individual signals in a post synthesis netlist. These mutations are then filtered using Formal Verification techniques, keeping only those that can cause an important change in the design’s output.

All mutated designs are run against the testbench to check that the testbench will detect and fail for a relevant mutation. The testbench can then be improved to get 100% complete coverage.

• Getting Started
  • Dependencies
  • Installation
  • Example
• Methodology
• Command Reference
• Configuration File Format
  • [options]
  • [setup]
  • [script]
  • [files]
  • [logic]
  • [report]
  • [test <testname>]
• Writing a test script
  • Exporting the Mutated Source
  • Running the Testbench
  • Reporting the Result
• Writing the equivalence check
  • Creating the miter circuit
  • Setting up the test script for the equivalence check
    • Mutation export
    • Running the equivalence check
    • Reporting equivalence
• Mutation export options
  • The create_mutated.sh script
  • The task mutation list input.txt
  • Writing a custom mutation export script
  • The Yosys mutate command
    • Mutation generation
    • Applying a mutation
• Tutorial