Bug 823

Summary: Implementation of the Logical Equivalence Checker (LEQ)
Product: Libre-SOC's second ASIC Reporter: Jean-Paul Chaput <Jean-Paul.Chaput>
Component: source codeAssignee: Jean-Paul Chaput <Jean-Paul.Chaput>
Status: RESOLVED FIXED    
Severity: enhancement CC: libre-soc-bugs, lkcl
Priority: ---    
Version: unspecified   
Hardware: PC   
OS: Linux   
NLnet milestone: NLnet.2021-08-049.coriolis2 total budget (EUR) for completion of task and all subtasks: 9000
budget (EUR) for this task, excluding subtasks' budget: 9000 parent task for budget allocation: 748
child tasks for budget allocation: The table of payments (in EUR) for this task; TOML format:

Description Jean-Paul Chaput 2022-04-29 15:52:47 BST 
This task must not be mistaken with the extractor tool (aka Solstice).

Implementation of LEQ, using the algorithm of Equinox as a starting point and enriching it according to the survey of LEQ algorithms.

One of the main goal is to provide *trans-hierarchical* error messages that are sufficiently understandable by the designer (often one of the main weakness of such tools).