Bug 596

Summary:	formal correctness proof for nmigen integration of Dynamic Partitioned Signal
Product:	Libre-SOC's first SoC	Reporter:	Luke Kenneth Casson Leighton <lkcl>
Component:	Formal Verification	Assignee:	mail
Status:	CONFIRMED ---
Severity:	enhancement	CC:	libre-soc-bugs
Priority:	---
Version:	unspecified
Hardware:	Other
OS:	Linux
See Also:	https://bugs.libre-soc.org/show_bug.cgi?id=196 https://bugs.libre-soc.org/show_bug.cgi?id=115 https://bugs.libre-soc.org/show_bug.cgi?id=565
NLnet milestone:	NLNet.2019.10.032.Formal	total budget (EUR) for completion of task and all subtasks:	0
budget (EUR) for this task, excluding subtasks' budget:	0	parent task for budget allocation:
child tasks for budget allocation:		The table of payments (in EUR) for this task; TOML format:
Bug Depends on:
Bug Blocks:	196

Description Luke Kenneth Casson Leighton 2021-02-13 12:02:07 GMT

on integration with nmigen m.If, m.Switch etc. some formal correctness proofs will be needed that ensure equivalence.

this is different from bug #565 which is about providing a Formal correctness oroof of PartitionedSignal itself, not of PartitionedSignal's interaction with nmigen m.If and m.Switch.

* TODO: m.If
* TODO: m.Elif
* TODO: m.Else
* TODO: m.Switch
* TODO: m.FSM