Examples of using PSL for functional and formal verification of VHDL with GHDL (and SymbiYosys)
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

28 lines
744 B

  1. [tasks]
  2. sere_0 bmc
  3. sere_1 bmc
  4. sere_2 bmc
  5. sere_3 bmc
  6. all bmc
  7. bmc all
  8. [options]
  9. depth 25
  10. bmc: mode bmc
  11. [engines]
  12. bmc: smtbmc z3
  13. [script]
  14. sere_0: ghdl --std=08 -gformal=SERE_0 pkg.vhd sequencer.vhd psl_vunit.vhd psl_vunit.psl -e psl_vunit
  15. sere_1: ghdl --std=08 -gformal=SERE_1 pkg.vhd sequencer.vhd psl_vunit.vhd psl_vunit.psl -e psl_vunit
  16. sere_2: ghdl --std=08 -gformal=SERE_2 pkg.vhd sequencer.vhd psl_vunit.vhd psl_vunit.psl -e psl_vunit
  17. sere_3: ghdl --std=08 -gformal=SERE_3 pkg.vhd sequencer.vhd psl_vunit.vhd psl_vunit.psl -e psl_vunit
  18. all: ghdl --std=08 -gformal=ALL pkg.vhd sequencer.vhd psl_vunit.vhd psl_vunit.psl -e psl_vunit
  19. prep -top psl_vunit
  20. [files]
  21. ../src/pkg.vhd
  22. ../src/sequencer.vhd
  23. ../src/psl_vunit.vhd
  24. ../src/psl_vunit.psl