Implement formal verification of PartitionedEq based on GateGenerator

Calculate the expected value, test and assert

Split-out the gate generator from the proof

This reduces repetition among partition proofs.

Compare the expected output for all partition sizes

Optimize for the case where the partition points are equally spaced,
so the possible partition sizes are just multiple of the smaller one.
Otherwise, all combinations of start and end points would have to be
considered.

Generate shifted down outputs

Align the start of any selected partition to zero, so it can easily be
checked with the expected value.
For partitioned operations with inputs, it is also necessary to generate
shifted down versions of each input.

Generate the bit pattern of gates corresponding to a partition

Use Assume to constraint the pattern to conform to the given offset
and width. For each bit it is:
1) one if on the partition boundary
2) zero if it's inside the partition
3) don't care, otherwise

Work only with nibbles on the ascending cascade

Fill the second nibble of the pattern

It should encode the length of the partition.
The first nibble encodes the position within the partition.

Restart the pattern at partition boundaries

Start work on improving formal verification of PartitionedSignal

The goal is to have a generic approach, decoupled from the actual
implementation of each partitioned operation.

partsig: redirect bool to any for now, and use a == Const(-1) for any

comment PartitionedSignal lt/le

disable faulty bit_width reduction logic in DivPipeCore

fix mismatched comb process delays

add process tracing

remove FPPipeContext (moved to nmutil), name-substitute on import
see https://bugs.libre-soc.org/show_bug.cgi?id=431

working on fixing DivPipeCore's test cases

this is as part of fixing the problems caused by Luke reducing the bit-width used without a corresponding change in the fract-width when DivPipeCore only supports UDivMod

clean up DivPipeCoreConfig API

whoops missed set up of temp variable bw

only pass in lhs bit_width * 2 for UDivRem

add arguments to MulPipe_8_16_32_64

fix test_mul_pipe.py unit test

continue reducing length of signals in div core

attempt to get simulation for div test_core.py running

reduce compare lengths to *2 rather than *3

whoops set pass_flag[0] always true
rather than pass_flag[-1] always false

add feedback_width argument to runfp for testing

allow arrangement for feedback loops to be possible on ReservationStations in unit test

cut top trial comparison

remove use of Array, replace with treereduce

cut root_times_radicand if not doing Sqrt

add "supported" option to div core

fix imports (allows test command to be run from non-top-level directory)

move mulAddRecFN.py and nmigen_div_experiment.py to unused dir

add DivPipeOp in fpdiv/op.py

Fix handling of FPPipeContext.ports()

Allow partsig to take in a PartitionPoints directly

Add in FPPipeContext to the cordic pipeline

Use clz.py from nmutil

track down error in CORDIC pipe_data, "yield from" used instead of just "yield"

whoops cant output .il at the moment

add progress counter

allow rtlil file to be created in cordic

Add renormalize.py (oops!)

remove extraneous whitespace

Remove print statements from clz.py

Add asserts to fp pipe test

Sorta working FP renormalization in cordic

Extend clz to work with odd widths

Extend CLZ to work over even, non powers of 2

Add proof for clz.py

Add count leading zeros module (should probably go somewhere else)

Have sin_cos pipeline use bigfloat calculated atan table

Add cordic stages to fp cordic pipeline

Add stage to convert input float to fixed point number

Begin adding floating point cordic pipeline

Allow cordic to work with 64 bit floats

move ripple.py to nmutil

add libmpfr-dev to .gitlab-ci.yml

Change tabs to spaces in .gitlab-ci.yml

Add libgmp-dev to .gitlab-ci.yml

Use python bigfloat to calculate atan tables

Revert "Use higher precision arithmetic when calculating the atan2 table"

This reverts commit 7aea44d471226db693ee99fd272504248d57375b.

Use higher precision arithmetic when calculating the atan2 table

change test_fpsin to use 32 bit floats

Run the cordic for the proper number of iterations

Working (ish) fpsin iterative cordic

Assert that fpsin_cos converts floats to fixed correctly

Begin working on multi cycle float cordic

Add experiment testing the effects of adding extra bits to cordic

add rtlil conversion and fix yield from in Cordic Data

run tests in parallel

building sfpy works

add not yet working .gitlab-ci.yml

Combine a selectable number of rounds into one pipeline stage

Cleanup

Combine initial stage with first cordic stage

Add actual tests to test_pipeline.py

Register each pipeline stage

Add test for sin_cos_pipe (kinda working)

Add test for sin_cos_pipe (not working still)

Connect up pipeline stages

Begin work on pipelined cordic

Cleanup

Working sin/cos cordic

sin/cos cordic partially working

Add test for sin_cos.py

Begin adding cordic

yet another nuisance

annoying, see https://github.com/nmigen/nmigen/issues/302
shift can no longer be signed, even if the amount is guaranteed signed

Apply Luke's suggestions/FIXME's

more fun comments

shuffle and comments

update comments on test partitioned signal

tiny code-shuffle on GatedBitReverse

Add shift right to test_partsig and partsig

Rename bitrev signal to shift_right (more descriptive)

Shift left now working

Remove element mux calculation from PartialResult

Add bit reversal to part_shift_dynamic

Shift Right not working yet