(no commit message)
authorlkcl <lkcl@web>
Fri, 1 Oct 2021 12:36:48 +0000 (13:36 +0100)
committerIkiWiki <ikiwiki.info>
Fri, 1 Oct 2021 12:36:48 +0000 (13:36 +0100)
nlnet_2021_lip6_vlsi.mdwn

index 8f94f052341a060f50007d0d5b19663321bda956..873e8a248f870f6945c8adbacad5368ad10396e8 100644 (file)
@@ -91,3 +91,66 @@ write Academic papers and present at conferences.  In addition, they work
 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 an 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.
+* 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.
+* 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
+* 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
+
+**You mention you will be able to perform Logical Validation.
+Can you expand a bit on that, what assurances could that bring?**
+
+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 modificated*.
+  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...).