diff options
| author | Clifford Wolf <clifford@clifford.at> | 2017-09-13 18:45:57 +0200 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2017-09-13 18:45:57 +0200 |
| commit | a412d3ea69618960d6cfd900b5b4e99a9161992f (patch) | |
| tree | 097c7d3376f7c55c0651ce61d27db9acfc91aaac /Makefile | |
| parent | 8db3073ff9fc7ac73c9739e893a3cd94713486b9 (diff) | |
| download | picorv32-a412d3ea69618960d6cfd900b5b4e99a9161992f.tar.gz picorv32-a412d3ea69618960d6cfd900b5b4e99a9161992f.zip | |
Add "make test_rvf"
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 33 |
1 files changed, 20 insertions, 13 deletions
@@ -19,6 +19,9 @@ test: testbench.vvp firmware/firmware.hex test_vcd: testbench.vvp firmware/firmware.hex vvp -N $< +vcd +trace +noerror +test_rvf: testbench_rvf.vvp firmware/firmware.hex + vvp -N $< +vcd +trace +noerror + test_wb: testbench_wb.vvp firmware/firmware.hex vvp -N $< @@ -31,18 +34,6 @@ test_ez: testbench_ez.vvp test_ez_vcd: testbench_ez.vvp vvp -N $< +vcd -check: check-yices - -check-%: check.smt2 - yosys-smtbmc -s $(subst check-,,$@) -t 30 --dump-vcd check.vcd check.smt2 - yosys-smtbmc -s $(subst check-,,$@) -t 25 --dump-vcd check.vcd -i check.smt2 - -check.smt2: picorv32.v - yosys -v2 -p 'read_verilog -formal picorv32.v' \ - -p 'prep -top picorv32 -nordff' \ - -p 'assertpmux -noinit; opt -fast' \ - -p 'write_smt2 -wires check.smt2' - test_sp: testbench_sp.vvp firmware/firmware.hex vvp -N $< @@ -56,6 +47,10 @@ testbench.vvp: testbench.v picorv32.v iverilog -o $@ $(subst C,-DCOMPRESSED_ISA,$(COMPRESSED_ISA)) $^ chmod -x $@ +testbench_rvf.vvp: testbench.v picorv32.v rvfimon.v + iverilog -o $@ -D RISCV_FORMAL $(subst C,-DCOMPRESSED_ISA,$(COMPRESSED_ISA)) $^ + chmod -x $@ + testbench_wb.vvp: testbench_wb.v picorv32.v iverilog -o $@ $(subst C,-DCOMPRESSED_ISA,$(COMPRESSED_ISA)) $^ chmod -x $@ @@ -72,6 +67,18 @@ testbench_synth.vvp: testbench.v synth.v iverilog -o $@ -DSYNTH_TEST $^ chmod -x $@ +check: check-yices + +check-%: check.smt2 + yosys-smtbmc -s $(subst check-,,$@) -t 30 --dump-vcd check.vcd check.smt2 + yosys-smtbmc -s $(subst check-,,$@) -t 25 --dump-vcd check.vcd -i check.smt2 + +check.smt2: picorv32.v + yosys -v2 -p 'read_verilog -formal picorv32.v' \ + -p 'prep -top picorv32 -nordff' \ + -p 'assertpmux -noinit; opt -fast' \ + -p 'write_smt2 -wires check.smt2' + synth.v: picorv32.v scripts/yosys/synth_sim.ys yosys -qv3 -l synth.log scripts/yosys/synth_sim.ys @@ -155,6 +162,6 @@ clean: rm -vrf $(FIRMWARE_OBJS) $(TEST_OBJS) check.smt2 check.vcd synth.v synth.log \ firmware/firmware.elf firmware/firmware.bin firmware/firmware.hex firmware/firmware.map \ testbench.vvp testbench_sp.vvp testbench_synth.vvp testbench_ez.vvp \ - testbench_wb.vvp testbench.vcd testbench.trace + testbench_rvf.vvp testbench_wb.vvp testbench.vcd testbench.trace .PHONY: test test_vcd test_sp test_axi test_wb test_wb_vcd test_ez test_ez_vcd test_synth download-tools build-tools toc clean |