Formal Verification

Formal Verification is a Linty scan engine that provides additional rules based on formal verification. These advanced rules help you detect bugs and vulnerabilities, improving the reliability and security of your IPs.

BugFinder is available as part of Linty Ultra.

Workflow

  1. Generate and run formal checks directly in VS Code with the Linty Formal Verification extension.

  2. Save these formal checks in your project repository (default location: .linty/formal; this can be updated via the sonar.hdl.formal.paths property).

  3. Integrate these formal checks into your continuous integration workflow. First, activate the formal verification rules tagged as formal in your quality profiles. Then, run a Linty scan.

Custom Formal Checks

You can embed your own formal checks based on SymbiYosys into Linty. To do so, for each check:

  1. Create a rule from the Linty formal check template and activate it in your quality profiles.

  2. Get the ID of the rule you just created.

  3. Add the following line at the top of your formal check .sby file: # Linty check ID: my_rule. Replace my_rule with the ID of the rule you just created (everything after hdlformal).

  4. Store the .sby file in your project repository (default location: .linty/formal; this can be updated via the sonar.hdl.formal.paths property).