Luke Kenneth Casson Leighton [Wed, 29 Sep 2021 18:10:48 +0000 (19:10 +0100)]
add PartitionedAssign class for use in PartitionedSignal
Luke Kenneth Casson Leighton [Wed, 29 Sep 2021 18:10:23 +0000 (19:10 +0100)]
add PartitionedSignal.shape function
(simply returns underlying self.sig.shape())
Luke Kenneth Casson Leighton [Wed, 29 Sep 2021 17:25:45 +0000 (18:25 +0100)]
add PartitionedSignal.__len__ override, redirects to self.sig len
Luke Kenneth Casson Leighton [Wed, 29 Sep 2021 16:13:45 +0000 (17:13 +0100)]
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)
Luke Kenneth Casson Leighton [Wed, 29 Sep 2021 16:12:51 +0000 (17:12 +0100)]
add assert to check partition jump point size
Luke Kenneth Casson Leighton [Wed, 29 Sep 2021 15:43:50 +0000 (16:43 +0100)]
unit test for PartitionedSignal.__Cat__
decided also to change the mask to be the number of partition points
(not waste one bit)
Luke Kenneth Casson Leighton [Tue, 28 Sep 2021 18:50:41 +0000 (19:50 +0100)]
move PCat to separate module
(didnt help but hey), solve recursive import by moving import of
PartitionedCat into the PCat function
Luke Kenneth Casson Leighton [Tue, 28 Sep 2021 18:41:20 +0000 (19:41 +0100)]
add PartitionedSignal.__Cat__ override
calls and creates PartitionedCat module
Luke Kenneth Casson Leighton [Tue, 28 Sep 2021 18:36:31 +0000 (19:36 +0100)]
corrections to PartitionedCat after corrections to PartitionedSignal,
using make_partitions2, off-by-one error
Luke Kenneth Casson Leighton [Tue, 28 Sep 2021 16:00:40 +0000 (17:00 +0100)]
add PartitionedSignal.__Mux__ unit test
split out from TestPartitionedSignal to reduce time and make it clear
what is being tested
Luke Kenneth Casson Leighton [Tue, 28 Sep 2021 14:17:15 +0000 (15:17 +0100)]
add PartitionedSignal.__Mux__ using existing PMux function
Luke Kenneth Casson Leighton [Mon, 27 Sep 2021 18:29:26 +0000 (19:29 +0100)]
derive PartitionedSignal from UserValue (temporarily) and add lower()
Luke Kenneth Casson Leighton [Mon, 27 Sep 2021 18:28:57 +0000 (19:28 +0100)]
whitespace
Luke Kenneth Casson Leighton [Fri, 24 Sep 2021 19:17:34 +0000 (20:17 +0100)]
fix chunking to get correct order for PartitionedCat
Luke Kenneth Casson Leighton [Fri, 24 Sep 2021 13:59:01 +0000 (14:59 +0100)]
add first cut at PartitionedSignal "Cat"
R Veera Kumar [Sat, 5 Jun 2021 02:31:29 +0000 (08:01 +0530)]
Remove comment sign and add correct path for nmigen intersphinx.
R Veera Kumar [Sat, 5 Jun 2021 02:14:27 +0000 (07:44 +0530)]
Add Makefile modified for sphinx.
R Veera Kumar [Sat, 5 Jun 2021 02:04:00 +0000 (07:34 +0530)]
Initial addition of sphinx documentation system.
Add run of sphinx-quickstart and manual modifications of files.
Luke Kenneth Casson Leighton [Mon, 12 Apr 2021 00:05:34 +0000 (01:05 +0100)]
corrections to setup.py for classifier, for pypi upload
Luke Kenneth Casson Leighton [Mon, 12 Apr 2021 00:03:16 +0000 (01:03 +0100)]
update for upload to pypi
Cesar Strauss [Sat, 23 Jan 2021 22:33:44 +0000 (19:33 -0300)]
Convert add and sub to return PartitionedSignal
Adjust the test suite accordingly.
Cesar Strauss [Sat, 23 Jan 2021 21:16:04 +0000 (18:16 -0300)]
Revert order of operations in PartitionedSignal.implies()
Now that all bitwise logic operations return PartitionedSignal, the
original order of operations will work.
Cesar Strauss [Sat, 23 Jan 2021 21:09:28 +0000 (18:09 -0300)]
Clarify comment about operations returning plain Signals
Possibly not all Signal results will be ported to PartitionedSignal. For
instance, comparison operations.
Cesar Strauss [Sat, 23 Jan 2021 20:58:41 +0000 (17:58 -0300)]
Convert all bitwise logical ops to return PartitionedSignal
Cesar Strauss [Sat, 23 Jan 2021 20:46:29 +0000 (17:46 -0300)]
Also copy the module in PartotionSignal.like()
Cesar Strauss [Sat, 23 Jan 2021 20:39:49 +0000 (17:39 -0300)]
Return a PartitionedSignal from the bitwise "not" operation
Adjust the proof to accommodate such operations.
Cesar Strauss [Sat, 23 Jan 2021 20:31:39 +0000 (17:31 -0300)]
Implement PartitionedSignal.like()
Cesar Strauss [Sat, 23 Jan 2021 09:55:03 +0000 (06:55 -0300)]
Use z3 solver instead of yices2 when convenient
Cesar Strauss [Wed, 20 Jan 2021 10:35:01 +0000 (07:35 -0300)]
Add tests for bitwise logical operators
Cesar Strauss [Wed, 20 Jan 2021 10:29:35 +0000 (07:29 -0300)]
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.
Cesar Strauss [Mon, 18 Jan 2021 08:59:44 +0000 (05:59 -0300)]
Do not register carry-out on the PartitionedAdder
The user of this module can register it if needed.
Cesar Strauss [Sun, 17 Jan 2021 21:45:47 +0000 (18:45 -0300)]
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.
Cesar Strauss [Sun, 17 Jan 2021 17:00:27 +0000 (14:00 -0300)]
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.
Cesar Strauss [Sat, 16 Jan 2021 20:37:35 +0000 (17:37 -0300)]
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.
Luke Kenneth Casson Leighton [Sat, 16 Jan 2021 19:07:41 +0000 (19:07 +0000)]
add first cut at formal proof for PartitionedXOR
Luke Kenneth Casson Leighton [Sat, 16 Jan 2021 19:02:25 +0000 (19:02 +0000)]
add PartitionedXOR to PartitionedSignal (xor operator)
Cesar Strauss [Sat, 16 Jan 2021 19:00:28 +0000 (16:00 -0300)]
Check PartitionedSignal.any().
Luke Kenneth Casson Leighton [Sat, 16 Jan 2021 18:51:34 +0000 (18:51 +0000)]
add first cut (untested) of PartitionedXOR
Luke Kenneth Casson Leighton [Sat, 16 Jan 2021 18:45:10 +0000 (18:45 +0000)]
convert EQCombiner to general-purpose, create XORCombiner
Luke Kenneth Casson Leighton [Sat, 16 Jan 2021 18:40:50 +0000 (18:40 +0000)]
add partitioned signal any() operator
Cesar Strauss [Sat, 16 Jan 2021 17:06:41 +0000 (14:06 -0300)]
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.
Cesar Strauss [Mon, 11 Jan 2021 19:28:38 +0000 (16:28 -0300)]
Apparently PartitionedEqGtGe is already conformant
Cesar Strauss [Sun, 10 Jan 2021 22:02:01 +0000 (19:02 -0300)]
Implement checks for all the rest of the comparison operarions
Cesar Strauss [Sun, 10 Jan 2021 21:42:58 +0000 (18:42 -0300)]
Generate and check expected values for all possible partition sizes
Cesar Strauss [Sun, 10 Jan 2021 21:33:10 +0000 (18:33 -0300)]
Generate shifted down input and outputs
Cesar Strauss [Sun, 10 Jan 2021 21:18:17 +0000 (18:18 -0300)]
Use styles in write_gtkw to simplify the trace description
Cesar Strauss [Sun, 10 Jan 2021 20:56:29 +0000 (17:56 -0300)]
Add the Gate Generator to the ComparisonOpDriver
Cesar Strauss [Sun, 10 Jan 2021 20:28:23 +0000 (17:28 -0300)]
Factor-out the code to make equally spaced partition points
Cesar Strauss [Sun, 10 Jan 2021 19:43:57 +0000 (16:43 -0300)]
Start proof for PartitionedSignal equals operator
The idea is to make use of operator.* to abstract away the operation.
Start with binary comparison operators.
Cesar Strauss [Sun, 10 Jan 2021 18:32:48 +0000 (15:32 -0300)]
Update Simulator interface to current nMigen
Cesar Strauss [Sun, 10 Jan 2021 17:47:26 +0000 (14:47 -0300)]
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.
Cesar Strauss [Sat, 9 Jan 2021 17:29:53 +0000 (14:29 -0300)]
Use the correct class name
Cesar Strauss [Sat, 9 Jan 2021 17:23:03 +0000 (14:23 -0300)]
Check all possible opcodes for PartitionedEqGtGe
Cesar Strauss [Sat, 9 Jan 2021 16:55:25 +0000 (13:55 -0300)]
Formal verification of PartitionedEqGtGe (EQ only)
Fix operation at EQ to begin with.
Code is mostly identical to the PartitionedEq proof.
Cesar Strauss [Sat, 9 Jan 2021 14:41:18 +0000 (11:41 -0300)]
Post-process PartitionedEq to ripple the LSB
This needs to be removed once PartitionedEq is compliant.
Cesar Strauss [Sat, 9 Jan 2021 13:56:28 +0000 (10:56 -0300)]
Implement formal verification of PartitionedEq based on GateGenerator
Cesar Strauss [Fri, 8 Jan 2021 21:35:10 +0000 (18:35 -0300)]
Calculate the expected value, test and assert
Cesar Strauss [Fri, 8 Jan 2021 21:17:02 +0000 (18:17 -0300)]
Split-out the gate generator from the proof
This reduces repetition among partition proofs.
Cesar Strauss [Thu, 7 Jan 2021 22:34:20 +0000 (19:34 -0300)]
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.
Cesar Strauss [Wed, 6 Jan 2021 09:41:24 +0000 (06:41 -0300)]
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.
Cesar Strauss [Tue, 5 Jan 2021 20:32:40 +0000 (17:32 -0300)]
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
Cesar Strauss [Mon, 4 Jan 2021 21:38:51 +0000 (18:38 -0300)]
Work only with nibbles on the ascending cascade
Cesar Strauss [Mon, 4 Jan 2021 21:08:37 +0000 (18:08 -0300)]
Fill the second nibble of the pattern
It should encode the length of the partition.
The first nibble encodes the position within the partition.
Cesar Strauss [Mon, 4 Jan 2021 20:26:35 +0000 (17:26 -0300)]
Restart the pattern at partition boundaries
Cesar Strauss [Mon, 4 Jan 2021 19:56:25 +0000 (16:56 -0300)]
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.
Luke Kenneth Casson Leighton [Mon, 28 Dec 2020 13:34:49 +0000 (13:34 +0000)]
partsig: redirect bool to any for now, and use a == Const(-1) for any
Luke Kenneth Casson Leighton [Sun, 27 Dec 2020 00:09:57 +0000 (00:09 +0000)]
comment PartitionedSignal lt/le
Jacob Lifshay [Mon, 20 Jul 2020 03:19:22 +0000 (20:19 -0700)]
disable faulty bit_width reduction logic in DivPipeCore
Jacob Lifshay [Mon, 20 Jul 2020 03:15:25 +0000 (20:15 -0700)]
fix mismatched comb process delays
Jacob Lifshay [Mon, 20 Jul 2020 03:15:01 +0000 (20:15 -0700)]
add process tracing
Luke Kenneth Casson Leighton [Wed, 15 Jul 2020 13:42:39 +0000 (14:42 +0100)]
remove FPPipeContext (moved to nmutil), name-substitute on import
see https://bugs.libre-soc.org/show_bug.cgi?id=431
Jacob Lifshay [Mon, 13 Jul 2020 03:49:59 +0000 (20:49 -0700)]
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
Jacob Lifshay [Mon, 13 Jul 2020 02:45:11 +0000 (19:45 -0700)]
clean up DivPipeCoreConfig API
Luke Kenneth Casson Leighton [Fri, 10 Jul 2020 12:02:22 +0000 (13:02 +0100)]
whoops missed set up of temp variable bw
Luke Kenneth Casson Leighton [Fri, 10 Jul 2020 10:34:19 +0000 (11:34 +0100)]
only pass in lhs bit_width * 2 for UDivRem
Luke Kenneth Casson Leighton [Mon, 6 Jul 2020 14:07:36 +0000 (15:07 +0100)]
add arguments to MulPipe_8_16_32_64
Luke Kenneth Casson Leighton [Mon, 6 Jul 2020 14:07:13 +0000 (15:07 +0100)]
fix test_mul_pipe.py unit test
Luke Kenneth Casson Leighton [Sat, 4 Jul 2020 10:05:48 +0000 (11:05 +0100)]
continue reducing length of signals in div core
Luke Kenneth Casson Leighton [Sat, 4 Jul 2020 10:00:30 +0000 (11:00 +0100)]
attempt to get simulation for div test_core.py running
Luke Kenneth Casson Leighton [Sat, 4 Jul 2020 10:00:03 +0000 (11:00 +0100)]
reduce compare lengths to *2 rather than *3
Luke Kenneth Casson Leighton [Sat, 4 Jul 2020 09:43:52 +0000 (10:43 +0100)]
whoops set pass_flag[0] always true
rather than pass_flag[-1] always false
Luke Kenneth Casson Leighton [Sat, 4 Jul 2020 09:25:39 +0000 (10:25 +0100)]
add feedback_width argument to runfp for testing
Luke Kenneth Casson Leighton [Fri, 3 Jul 2020 14:42:51 +0000 (15:42 +0100)]
allow arrangement for feedback loops to be possible on ReservationStations in unit test
Luke Kenneth Casson Leighton [Fri, 3 Jul 2020 04:26:17 +0000 (05:26 +0100)]
cut top trial comparison
Luke Kenneth Casson Leighton [Fri, 3 Jul 2020 03:45:04 +0000 (04:45 +0100)]
remove use of Array, replace with treereduce
Luke Kenneth Casson Leighton [Fri, 3 Jul 2020 03:32:30 +0000 (04:32 +0100)]
cut root_times_radicand if not doing Sqrt
Luke Kenneth Casson Leighton [Fri, 3 Jul 2020 03:09:36 +0000 (04:09 +0100)]
add "supported" option to div core
Luke Kenneth Casson Leighton [Tue, 9 Jun 2020 17:44:13 +0000 (18:44 +0100)]
fix imports (allows test command to be run from non-top-level directory)
Jacob Lifshay [Thu, 4 Jun 2020 00:26:04 +0000 (17:26 -0700)]
move mulAddRecFN.py and nmigen_div_experiment.py to unused dir
Jacob Lifshay [Fri, 22 May 2020 22:32:06 +0000 (15:32 -0700)]
add DivPipeOp in fpdiv/op.py
Michael Nolan [Sat, 16 May 2020 15:16:29 +0000 (11:16 -0400)]
Fix handling of FPPipeContext.ports()
Michael Nolan [Fri, 8 May 2020 17:01:38 +0000 (13:01 -0400)]
Allow partsig to take in a PartitionPoints directly
Michael Nolan [Tue, 5 May 2020 18:08:58 +0000 (14:08 -0400)]
Add in FPPipeContext to the cordic pipeline
Michael Nolan [Tue, 5 May 2020 15:16:21 +0000 (11:16 -0400)]
Use clz.py from nmutil
Luke Kenneth Casson Leighton [Tue, 5 May 2020 14:59:23 +0000 (15:59 +0100)]
track down error in CORDIC pipe_data, "yield from" used instead of just "yield"
Luke Kenneth Casson Leighton [Tue, 5 May 2020 14:52:35 +0000 (15:52 +0100)]
whoops cant output .il at the moment
Luke Kenneth Casson Leighton [Tue, 5 May 2020 14:51:52 +0000 (15:51 +0100)]
add progress counter
Luke Kenneth Casson Leighton [Tue, 5 May 2020 14:48:14 +0000 (15:48 +0100)]
allow rtlil file to be created in cordic
Michael Nolan [Tue, 5 May 2020 14:21:02 +0000 (10:21 -0400)]
Add renormalize.py (oops!)
Luke Kenneth Casson Leighton [Tue, 5 May 2020 14:01:30 +0000 (15:01 +0100)]
remove extraneous whitespace