AppNote 123

This application note provides a guided example of how to use SBY with large and complex designs; looking at how to configure the tools and the limitations therein.

Note

The source code for this application note is provided in:

• Link to github repo https://github.com/YosysHQ-Docs/AppNote-123

Also, Tabby CAD Suite is required for all included examples! Ask us for an evaluation license: https://www.yosyshq.com/contact

In general, the steps for verifying a design are as follows:

1. Create a new folder

2. Copy/clone design source to folder

3. Run sby --init-config-file <name>

4. Add source files to [files] section

5. Update [script] section to read source files and prepare top level

   module

6. Run sby <name>.sby

   1. Remove or ignore any sections of code which raise errors in parsing

   2. Re-run with sby -f <name.sby> to ignore existing folder

7. Setup clock/reset and any other inputs which need to be constrained

8. Remove or convert unwanted properties

9. Cutpoint multipliers, memories, and any other difficult-to-prove logic

10. Add tasks for cover/prove modes

11. Perform any other configuration steps needed

12. Run sby -f <name>.sby [task]

Examples

• Verifying the VeeR core
  • Loading the design
  • Formal setup
  • Changing properties
  • The keep-going flag
  • Tasks and verification IP
• Working with a CV32 core
  • The existing Jasper script
  • Converting to SBY
    • The Yosys script
    • Setup clock and reset
    • Patching the source
  • Running SBY