mirror of
https://github.com/YosysHQ/yosys
synced 2026-05-30 13:56:33 +00:00
Add check_mem command
Comes with a set of tests which (currently) pass with `read_verilog` but fail with `verific` based on #5878. Add `--check-sv`, an alternative to `--prove-sv` with generator defined yosys commands. Helpful for when you want to run the same set of commands on a bunch of sv files.
This commit is contained in:
parent
27ae62f492
commit
a7c8651b76
7 changed files with 210 additions and 4 deletions
47
tests/check_mem/bad_il.ys
Normal file
47
tests/check_mem/bad_il.ys
Normal file
|
|
@ -0,0 +1,47 @@
|
|||
read_rtlil << EOF
|
||||
module \top
|
||||
wire input 1 \clk
|
||||
wire output 1 \o
|
||||
memory size 2 offset 1 \my_array
|
||||
cell $meminit \bad_init
|
||||
parameter \WORDS 1
|
||||
parameter \MEMID "\\my_array"
|
||||
parameter \ABITS 32
|
||||
parameter \WIDTH 1
|
||||
parameter \PRIORITY 1
|
||||
connect \ADDR 0
|
||||
connect \DATA 1'0
|
||||
end
|
||||
cell $memwr \bad_wr
|
||||
parameter \MEMID "\\my_array"
|
||||
parameter \CLK_ENABLE 1
|
||||
parameter \CLK_POLARITY 1
|
||||
parameter \PRIORITY 1
|
||||
parameter \ABITS 2
|
||||
parameter \WIDTH 1
|
||||
connect \EN 1'1
|
||||
connect \CLK \clk
|
||||
connect \ADDR 2'00
|
||||
connect \DATA 1'0
|
||||
end
|
||||
cell $memrd \bad_rd
|
||||
parameter \MEMID "\\my_array"
|
||||
parameter \CLK_ENABLE 0
|
||||
parameter \CLK_POLARITY 1
|
||||
parameter \TRANSPARENT 0
|
||||
parameter \ABITS 2
|
||||
parameter \WIDTH 1
|
||||
connect \CLK 1'x
|
||||
connect \EN 1'x
|
||||
connect \ADDR 2'11
|
||||
connect \DATA \o
|
||||
end
|
||||
end
|
||||
EOF
|
||||
|
||||
logger -expect warning "initializes address 0" 1
|
||||
logger -expect warning "writes address 0" 1
|
||||
logger -expect warning "reads address 3" 1
|
||||
check_mem
|
||||
logger -check-expected
|
||||
design -reset
|
||||
Loading…
Add table
Add a link
Reference in a new issue