Bug 596 - formal correctness proof for nmigen integration of Dynamic Partitioned Signal
Summary: formal correctness proof for nmigen integration of Dynamic Partitioned Signal
Status: CONFIRMED
Alias: None
Product: Libre-SOC's first SoC
Classification: Unclassified
Component: Formal Verification (show other bugs)
Version: unspecified
Hardware: Other Linux
: --- enhancement
Assignee: mail
URL:
Depends on:
Blocks: 196
  Show dependency treegraph
 
Reported: 2021-02-13 12:02 GMT by Luke Kenneth Casson Leighton
Modified: 2022-06-25 09:50 BST (History)
1 user (show)

See Also:
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:


Attachments

Note You need to log in before you can comment on or make changes to this bug.
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