6 Commits

Author	SHA1	Message	Date
Jannis Harder	a855d62b42	verific: Improve logic generated for SVA value change expressions ... 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	2022-05-09 15:04:01 +02:00
Miodrag Milanovic	600079e281	Fix running sva tests	2022-05-09 09:01:57 +02:00
Clifford Wolf	5c6247dfa6	Add support for SVA sequence concatenation ranges via verific ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-02-18 16:35:06 +01:00
Clifford Wolf	baddb017fe	Remove PSL example from tests/sva/	2017-10-20 13:16:24 +02:00
Clifford Wolf	4cf890dac1	Add simple VHDL+PSL example	2017-07-28 17:39:43 +02:00
Clifford Wolf	b24f737759	Improve SVA tests, add Makefile and scripts	2017-07-27 11:42:05 +02:00