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 tree / graph
 
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
Add an attachment (proposed patch, testcase, etc.)

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