Run Formal

After generating the framework, run formal verification from the generated output folder.

Recommended working directory

Move into the generated framework directory before running Makefile targets.

cd ./formal

If you used another output path, replace ./formal with your selected output directory.

Run Makefile commands

The generated Makefile creates one target per module using this format:

<module>_top

Run formal for a specific module with:

make <module>_top

Example

If your module is alu, run:

make alu_top

This command launches the formal flow configured in the generated framework.