add PartitionedRepl into PartitionedSignal.__Repl__
uses same auto-module-creation as PCat, PMux and PAssign

shuffle order of functions (whitespace) to same order as ast.Value

add PartitionedRepl first version, no unit test just demo

whoops accidentally removed bugreport link

add signed/unsigned functions and preliminary unit test

pull in unit test code for PartitionedSignal.matches to be adapted

bit of a reorder / reorg, to match up with current ast.Value function order
this makes it easier to ensure that all functions are there, easier to
read / find.

disable mul and rmul in PartitionedSignal for now

rewrite complex comprehensions as for loops

Fix broken code caused by attempted removal of type annotations.

This partially reverts commit 0cdf4be4df5c0fbae476442c1a91b0e8140e2104.

add TODO comments
https://bugs.libre-soc.org/show_bug.cgi?id=718

add a PartitionedSignal.any() test and extend range of values tested
in horizontal logic operators

make note about failing PartitionedAll
https://bugs.libre-soc.org/show_bug.cgi?id=176#c17

revert to using self == Const(-1) for now in PartitionedSignal.all()

bit more sophisticated on the partsig horizontal test, use subTest to report
function name and input value

add PartitionedSignal.all() and unit test, currently failing

add PartitionedAll operator, based on PartitionedBase

add bool PartitionedSignal test

removing unnecessary type information which makes the code
completely unreadable, longer and more complex

add PartitionedSignalTester

split out logical ops into PartitionedBase

add PartitionedBool class (based on PartitionedXOR)
could very likely be combined but hey

add quick use/self-test to PartitionedXOR

add PartitionedSignal XOR partsig test

partsig unit test tidyup

test names to go under a different fileset

add scalar test of PartitionedSignal.__Assign__
completes all 12 permutations needed

add six combinations of PartitionedSignal.__Assign__ test:
* input width less, equal or greater to output width
* output signed or unsigned

rework partsig TestAssign to cope with different types of input,
scalar/partitioned, lengths equal/greater/less, signed/unsigned

fix PartitionedAssign, PAssign, and PartitionedSignal.__Assign__

preliminary unit test showed wiring was incorrect, as was the return
result from PAssign, which has to return Statements

correct test_partsig name, remove redundant code

remove PartitionedSignal.eq, expectation is to use PartitionedSignal.__Assign__
due to eq being removed, access to the underlying ".sig" is now
done using PartitionedSignal.lower()

whitespace / comments

add use of PartitionedAssign in PartitionedSignal, behind __Assign__
move to separate module due to recursive import issues

add support in PartitionedAssign for scalar signals

add PartitionedAssign class for use in PartitionedSignal

add PartitionedSignal.shape function
(simply returns underlying self.sig.shape())

add PartitionedSignal.__len__ override, redirects to self.sig len

reduce part_mask in partsig tests to 3 (actual number of break points
not actual number of partitions), fix PartitionedSignal.like(),
needed to pass in PartitionPoints(other.partpoints)

add assert to check partition jump point size

unit test for PartitionedSignal.__Cat__
decided also to change the mask to be the number of partition points
(not waste one bit)

move PCat to separate module
(didnt help but hey), solve recursive import by moving import of
PartitionedCat into the PCat function

add PartitionedSignal.__Cat__ override
calls and creates PartitionedCat module

corrections to PartitionedCat after corrections to PartitionedSignal,
using make_partitions2, off-by-one error

add PartitionedSignal.__Mux__ unit test
split out from TestPartitionedSignal to reduce time and make it clear
what is being tested

add PartitionedSignal.__Mux__ using existing PMux function

derive PartitionedSignal from UserValue (temporarily) and add lower()

whitespace

fix chunking to get correct order for PartitionedCat

add first cut at PartitionedSignal "Cat"

Remove comment sign and add correct path for nmigen intersphinx.

Add Makefile modified for sphinx.

Initial addition of sphinx documentation system.

    Add run of sphinx-quickstart and manual modifications of files.

corrections to setup.py for classifier, for pypi upload

update for upload to pypi

Convert add and sub to return PartitionedSignal

Adjust the test suite accordingly.

Revert order of operations in PartitionedSignal.implies()

Now that all bitwise logic operations return PartitionedSignal, the
original order of operations will work.

Clarify comment about operations returning plain Signals

Possibly not all Signal results will be ported to PartitionedSignal. For
instance, comparison operations.

Convert all bitwise logical ops to return PartitionedSignal

Also copy the module in PartotionSignal.like()

Return a PartitionedSignal from the bitwise "not" operation

Adjust the proof to accommodate such operations.

Implement PartitionedSignal.like()

Use z3 solver instead of yices2 when convenient

Add tests for bitwise logical operators

Reverse order of operations in implies()

Put the negation last, since it returns a Signal, and then Signal OR
was being called instead of PartitionedSignal OR.

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.