+# NLnet LIP6 VLSI Project Grant
+
+* Code: 2021-08-049
+* Approved: 09 Nov 2021
+* Toplevel bugreport: <https://bugs.libre-soc.org/show_bug.cgi?id=748>
+
## Project name
LIP6 VLSI Tools
Industry prevent and prohibit discussion and general improvements beneficial
to users.
-The expected outcome is to improve Coriolis2, HITAS/TAGLE and extend the
+The expected outcome is to improve Coriolis2, HITAS/YAGLE and extend the
whole toolchain so that it is faster, able to handle larger ASIC designs,
and can perform Logical Validation. Also to be improved and tested is
support for lower geometries (starting with 130nm)
To improve the speed of the GUI front-end, to make it possible to
handle larger ASIC designs, to add LVS capability, improve the internal
data format (to better handle mixed case module and signal names), integrate
-the Static Timing Analysis tool (HITAS, TAGLE), to complete the conversion
+the Static Timing Analysis tool (HITAS) and YAGLE gate-level extraction tool, to complete the conversion
to python 3,
to try smaller geometry ASICs (beginning with 130nm), and potentially
investigate using multi-processing to speed up completion.
with the Libre-SOC Team to promote milestones and developments.
# Extra info to be submitted
+
+# Questions 01 Oct 2020
+
+**What rates were used, and what main tasks are there**
+
+we estimate the rates based on LIP6 University hiring an additional engineer in France, at commercial rates, to be around EUR 3000 to 4000 a month.
+
+* training a new Engineer on coriolis2 c++/python internals: estimated
+ 2 months
+* porting to python3 estimated 2 months (some libraries have to be removed and rewritten) including re-running several designs and checking they are still the same.
+* porting and updating of older (Alliance) layout extractor tools
+ (solstice, equinox) to newer (c++/python) coriolis2 as pure
+ netlist extractor: 2 months
+* adding limited electrical information extraction (wire resistance
+ and capacitance) to the new layout extractor: 4-6 weeks
+* researching Logical Equivalence algorithms and Academic papers to ensure good knowledge before proceeding: 4 to 5 weeks.
+* implementation of Logical Equivalence checker: 10 to 14 weeks.
+ this is **not** the same as an **extraction** tool (above). the LEQ tool
+ **uses** (checks) the extracted database.
+* validation of Logical Equivalence checker against simulations and other (proprietary) checkers: 5 to 7 weeks
+* Identifying locations in 150,00 lines of code which can be parallelised by "divide and conquer", and those which can be "threaded": 3 weeks
+* separation of code into separate processes ("divide and conquer"): 2 months
+* adding "mutex" (exclusion) protection around code which can be "threaded": 2 months
+* debugging and stabilising of both of the above: 2 months.
+* alternative file formats and data structures which support case-sensitive net names: 2 months
+* HITAS/YAGLE integration into coriolis2, updating license and documentation: 2 months
+
+**You mention you will be able to perform Logical Validation.
+Can you expand a bit on that, what assurances could that bring?**
+
+Short summary:
+
+there are two main ways to check that the HDL matches (is "equivalent") with the transistor layout, which has many changes made:
+
+1) simulation. for large designs this requires supercomputers for months and sometimes years to complete the simulation. realistically, only a
+very small number of cycles can be run (several days to run one "clock" cycle).
+
+2) Formal Mathematical "Logical equivalence". this performs boolean logic analysis and takes only hours (or days for very large designs).
+
+it is extremely important for a professional VLSI toolchain to have this capability.
+
+Longer version:
+
+As I assume you are not familiar with making ASIC, I will try to
+explain with sufficient details while not being too long.
+
+* The Place & Route (P&R) step of making an ASIC takes in input,
+ you can think of it as a "specification", a netlist.
+* A netlist is, or can be understood as:
+ 1. A specialized kind of electrical schematic with (in digital
+ cases) all components being 1 bit memories or boolean functions
+ (AND, OR, NOR, ...).
+ 2. A gigantic automaton, or set of big boolean equations.
+ The fact that all the components are either memories or logical
+ functions enable that.
+* Checking that the P&R has worked correctly amount to re-create
+ a netlist *from* the layout generated by the router. And, then,
+ perform a comparison of the *specification* netlist and the
+ one coming from the layout. Of course, they must be identical...
+ This is a "simple" graph comparison.
+* BUT, during the P&R, to meet electrical constraints like timing or
+ good power supply, the specification netlist *is modified*.
+ For example, the clock is split into a clock-tree to ensure
+ synchronicity all over the design or some very long wire is
+ broken into smaller ones. In some cases, more drastic operations
+ can be performed, like completely changing the way the boolean
+ computations are done.
+* So, after extraction, we end up with two *different* netlists,
+ which *should* implement the same automaton, hence the concept
+ of "logical equivalence" (LEQ).
+* Currently, with Alliance/Coriolis, we check that the *modificated*
+ netlist is identical to the one extracted from the layout.
+ But we don't know with mathematical certainty that the
+ *modificated* one is equivalent (not equal) to the specification
+ one.
+ Of course we have made some other tests to check that (pattern
+ simulation) but it's not foolproof (to have good coverage the
+ number of pattern grows in 2^N where N is the number of memory
+ *bits* in the circuit...).
projects / libreriscv.git / blobdiff