mirror of
https://github.com/YosysHQ/yosys
synced 2025-10-27 09:49:25 +00:00
a855d62b42
The previously generated logic assumed an unconstrained past value in the initial state and did not handle 'x values. While the current formal verification flow uses 2-valued logic, SVA value change expressions require a past value of 'x during the initial state to behave in the expected way (i.e. to consider both an initial 0 and an initial 1 as $changed and an initial 1 as $rose and an initial 0 as $fell). This patch now generates logic that at the same time a) provides the expected behavior in a 2-valued logic setting, not depending on any dont-care optimizations, and b) properly handles 'x values in yosys simulation
14 lines
385 B
Makefile
14 lines
385 B
Makefile
|
|
TESTS = $(sort $(basename $(wildcard *.sv)) $(basename $(wildcard *.vhd)))
|
|
|
|
all: $(addsuffix .ok,$(TESTS))
|
|
|
|
%.ok:
|
|
bash runtest.sh $@
|
|
|
|
clean:
|
|
rm -rf $(addsuffix .ok,$(TESTS)) $(addsuffix .sby,$(TESTS)) $(TESTS)
|
|
rm -rf $(addsuffix _pass.sby,$(TESTS)) $(addsuffix _pass,$(TESTS))
|
|
rm -rf $(addsuffix _fail.sby,$(TESTS)) $(addsuffix _fail,$(TESTS))
|
|
rm -rf $(addsuffix .fst,$(TESTS))
|
|
|