Do not register carry-out on the PartitionedAdder

The user of this module can register it if needed.

Fix PartitionedSignal.neg and its test case

For some reason, neg(a) was returning (a - 1) instead of (-a).
Implemented it as (0 - a).
For the test case, shifted down the input, negated it and shifted it
back again. Could have done it also by (0 - a), but this way it is more
independent of the implementation.
Added a formal proof.

Allow the proof driver to check operations with integer output

The "part_out" parameter tells the driver whether the output of the
operation is supposed to be arithmetic or boolean.

Added checks for addition and subtraction, without carry.

Use RipleLSB in PartitionedXOR, and invert outputs

The combiner was built to give inverted outputs, since it was designed
for ORing "not equals" signals, instead of ANDing equals signals.

Use 4-bit partitions when checking, 8-bit takes a long time for some
reason.

add first cut at formal proof for PartitionedXOR

add PartitionedXOR to PartitionedSignal (xor operator)

Check PartitionedSignal.any().

add first cut (untested) of PartitionedXOR

convert EQCombiner to general-purpose, create XORCombiner

add partitioned signal any() operator

Allow a variable number of operands in the proof driver

It can now check unary operations, as well as binary.

Check the "all" method by defining an operation that applies it to
its argument.

Apparently PartitionedEqGtGe is already conformant

Implement checks for all the rest of the comparison operarions

Generate and check expected values for all possible partition sizes

Generate shifted down input and outputs

Use styles in write_gtkw to simplify the trace description

Add the Gate Generator to the ComparisonOpDriver

Factor-out the code to make equally spaced partition points

Start proof for PartitionedSignal equals operator

The idea is to make use of operator.* to abstract away the operation.
Start with binary comparison operators.

Update Simulator interface to current nMigen

Use len(sig) instead of sig.shape()[0]

In latest nMigen, Shape is no longer a tuple. On the other hand,
len(sig) worked since the last stable nMigen release, so it should not
break for anyone.

Use the correct class name

Check all possible opcodes for PartitionedEqGtGe

Formal verification of PartitionedEqGtGe (EQ only)

Fix operation at EQ to begin with.
Code is mostly identical to the PartitionedEq proof.

Post-process PartitionedEq to ripple the LSB

This needs to be removed once PartitionedEq is compliant.

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