[Libre-soc-bugs] [Bug 901] Formal proof for PriorityPicker and MultiPriorityPicker and BetterMultiPriorityPicker

[bugzilla-daemon at libre-soc.org]

https://bugs.libre-soc.org/show_bug.cgi?id=901

Jacob Lifshay <programmerjake at gmail.com> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
            Summary|Formal proof for            |Formal proof for
                   |PriorityPicker and          |PriorityPicker and
                   |MultiPriorityPicker         |MultiPriorityPicker and
                   |                            |BetterMultiPriorityPicker
             Status|IN_PROGRESS                 |RESOLVED
         Resolution|---                         |FIXED

--- Comment #2 from Jacob Lifshay <programmerjake at gmail.com> ---
I added the formal proof for MultiPriorityPicker.

While I was reading the implementation, I thought of a more efficient
implementation with O(log N) latency instead of the > O(N) latency that
MultiPriorityPicker has, so I wrote BetterMultiPriorityPicker:

it uses a parallel prefix sum of the input bits to compute which level each
input bit should be sent to, rather than needing a O(N) stack of
PriorityPickers.

Testing with width=16, levels=16:

The new algorithm uses a bit less gates and has about 1/4 the latency:

> yosys <<<$'read_rtlil sim_test_out/nmutil.formal.test_picker.TestBetterMultiPriorityPicker.test_16_levels_16_idxs_f_mi_f/0.il\nflatten\nsynth\nltp -noff'

Number of cells:               1171
Longest topological path in top (length=21):

> yosys <<<$'read_rtlil sim_test_out/nmutil.formal.test_picker.TestMultiPriorityPicker.test_16_levels_16_idxs_f_mi_f/0.il\nflatten\nsynth\nltp -noff'

Number of cells:               1469
Longest topological path in top (length=85):

-- 
You are receiving this mail because:
You are on the CC list for the bug.