Skip to content

Commit 6902ce6

Browse files
committed
[formal] Adjust paths to new fusesoc structure
1 parent ffb3d59 commit 6902ce6

File tree

2 files changed

+2
-2
lines changed

2 files changed

+2
-2
lines changed

dv/formal/build_all.ys

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@
55

66
# Parse and lower the Ibex and specification RTL. LOWRISC_SAIL_SRC is replaced in Makefile.
77
read_slang --top top -DSYNTHESIS -DYOSYS \
8-
-F build/fusesoc/default-vcs/lowrisc_ibex_ibex_formal_0.1.scr \
8+
-F build/fusesoc/lowrisc_ibex_ibex_formal_0.1/default-vcs/lowrisc_ibex_ibex_formal_0.1.scr \
99
build/ibexspec.sv spec/stub.sv spec/spec_api.sv check/peek/alt_lsu.sv check/top.sv \
1010
-I LOWRISC_SAIL_SRC/lib/sv/ --single-unit --no-proc
1111
setattr -set keep 1 n:\\* # Keep all named wires. FIXME: Is this still necessary?

dv/formal/verify.tcl

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ set_prove_cache_mode coi
1616
set_prove_per_property_time_limit 10s
1717

1818
# Load all Ibex RTL, using the filelist generated by fusesoc
19-
analyze -sv12 +define+SYNTHESIS -f_relative_to_file_location build/fusesoc/default-vcs/lowrisc_ibex_ibex_formal_0.1.scr
19+
analyze -sv12 +define+SYNTHESIS -f_relative_to_file_location build/fusesoc/lowrisc_ibex_ibex_formal_0.1/default-vcs/lowrisc_ibex_ibex_formal_0.1.scr
2020

2121
set sail_lib_dir $env(LOWRISC_SAIL_SRC)/lib/sv
2222
analyze -sv12 -incdir $sail_lib_dir build/ibexspec.sv

0 commit comments

Comments
 (0)