iCE40/yosys - [no description]

	Commit message (Collapse)	Author	Age	Files	Lines
*	formalff: Fix crash with _NOT_ gates in -hierarchy mode	Jannis Harder	2023-01-25	1	-1/+1
\|
*	sim/formalff: Clock handling for yw cosim	Jannis Harder	2023-01-11	1	-2/+214
\|
*	Merge pull request #3537 from jix/xprop	Jannis Harder	2023-01-11	1	-0/+2
\|\ \| \| \| \|	New xprop pass
\| *	formalff: Fix -ff2anyinit assertion error for fine FFs	Jannis Harder	2022-11-30	1	-0/+2
\| \|
* \|	formalff: Proper error messages on async inputs for the -clk2ff mode	Jannis Harder	2022-12-09	1	-0/+3
\|/
*	formalff: New -setundef option	Jannis Harder	2022-08-16	1	-0/+335
\| \| \| \| \| \| \|	Find FFs with undefined initialization values for which changing the initialization does not change the observable behavior and initialize them. For -ff2anyinit, this reduces the number of generated $anyinit cells that drive wires with private names.
*	formalff: Set new replaced_by_gclk attribute on removed dff's clks	Jannis Harder	2022-08-16	1	-0/+22
\| \| \| \| \| \|	This attribute can be used by formal backends to indicate which clocks were mapped to the global clock. Update the btor and smt2 backend which already handle clock inputs to understand this attribute.
*	Add the $anyinit cell and the formalff pass	Jannis Harder	2022-08-16	1	-0/+192
	These can be used to protect undefined flip-flop initialization values from optimizations that are not sound for formal verification and can help mapping all solver-provided values in witness traces for flows that use different backends simultaneously.