Command:
Formal Property Verification:
ebmc --systemverilog --top fv_tb top.sv arbiter_sva.sv arbiter.sv --trace
Mutation Coverage with Yosys:
Note: The create_mutated.sh file was modified to use the -attr2comment flag.
mcy init
mcy run -j$(nproc)
Formal Proof Results:
See RESULTS
Mutation Coverage Results:
See MCY_RESULTS
Documentation:
https://www.hackster.io/shashank-v-m/fpga-design-verification-of-fixed-priority-arbiter-3dfc6a