ieee754fpu.git
3 months agoReverse order of operations in implies()
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.

3 months agoDo not register carry-out on the PartitionedAdder
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.

3 months agoFix PartitionedSignal.neg and its test case
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.

3 months agoAllow the proof driver to check operations with integer output
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.

4 months agoUse RipleLSB in PartitionedXOR, and invert outputs ls180-24jan2020
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.

4 months agoadd first cut at formal proof for PartitionedXOR
Luke Kenneth Casson Leighton [Sat, 16 Jan 2021 19:07:41 +0000 (19:07 +0000)]
add first cut at formal proof for PartitionedXOR

4 months agoadd PartitionedXOR to PartitionedSignal (xor operator)
Luke Kenneth Casson Leighton [Sat, 16 Jan 2021 19:02:25 +0000 (19:02 +0000)]
add PartitionedXOR to PartitionedSignal (xor operator)

4 months agoCheck PartitionedSignal.any().
Cesar Strauss [Sat, 16 Jan 2021 19:00:28 +0000 (16:00 -0300)]
Check PartitionedSignal.any().

4 months agoadd first cut (untested) of PartitionedXOR
Luke Kenneth Casson Leighton [Sat, 16 Jan 2021 18:51:34 +0000 (18:51 +0000)]
add first cut (untested) of PartitionedXOR

4 months agoconvert EQCombiner to general-purpose, create XORCombiner
Luke Kenneth Casson Leighton [Sat, 16 Jan 2021 18:45:10 +0000 (18:45 +0000)]
convert EQCombiner to general-purpose, create XORCombiner

4 months agoadd partitioned signal any() operator
Luke Kenneth Casson Leighton [Sat, 16 Jan 2021 18:40:50 +0000 (18:40 +0000)]
add partitioned signal any() operator

4 months agoAllow a variable number of operands in the proof driver
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.

4 months agoApparently PartitionedEqGtGe is already conformant
Cesar Strauss [Mon, 11 Jan 2021 19:28:38 +0000 (16:28 -0300)]
Apparently PartitionedEqGtGe is already conformant

4 months agoImplement checks for all the rest of the comparison operarions
Cesar Strauss [Sun, 10 Jan 2021 22:02:01 +0000 (19:02 -0300)]
Implement checks for all the rest of the comparison operarions

4 months agoGenerate and check expected values for all possible partition sizes
Cesar Strauss [Sun, 10 Jan 2021 21:42:58 +0000 (18:42 -0300)]
Generate and check expected values for all possible partition sizes

4 months agoGenerate shifted down input and outputs
Cesar Strauss [Sun, 10 Jan 2021 21:33:10 +0000 (18:33 -0300)]
Generate shifted down input and outputs

4 months agoUse styles in write_gtkw to simplify the trace description
Cesar Strauss [Sun, 10 Jan 2021 21:18:17 +0000 (18:18 -0300)]
Use styles in write_gtkw to simplify the trace description

4 months agoAdd the Gate Generator to the ComparisonOpDriver
Cesar Strauss [Sun, 10 Jan 2021 20:56:29 +0000 (17:56 -0300)]
Add the Gate Generator to the ComparisonOpDriver

4 months agoFactor-out the code to make equally spaced partition points
Cesar Strauss [Sun, 10 Jan 2021 20:28:23 +0000 (17:28 -0300)]
Factor-out the code to make equally spaced partition points

4 months agoStart proof for PartitionedSignal equals operator
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.

4 months agoUpdate Simulator interface to current nMigen
Cesar Strauss [Sun, 10 Jan 2021 18:32:48 +0000 (15:32 -0300)]
Update Simulator interface to current nMigen

4 months agoUse len(sig) instead of sig.shape()[0]
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.

4 months agoUse the correct class name
Cesar Strauss [Sat, 9 Jan 2021 17:29:53 +0000 (14:29 -0300)]
Use the correct class name

4 months agoCheck all possible opcodes for PartitionedEqGtGe
Cesar Strauss [Sat, 9 Jan 2021 17:23:03 +0000 (14:23 -0300)]
Check all possible opcodes for PartitionedEqGtGe

4 months agoFormal verification of PartitionedEqGtGe (EQ only)
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.

4 months agoPost-process PartitionedEq to ripple the LSB
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.

4 months agoImplement formal verification of PartitionedEq based on GateGenerator
Cesar Strauss [Sat, 9 Jan 2021 13:56:28 +0000 (10:56 -0300)]
Implement formal verification of PartitionedEq based on GateGenerator

4 months agoCalculate the expected value, test and assert
Cesar Strauss [Fri, 8 Jan 2021 21:35:10 +0000 (18:35 -0300)]
Calculate the expected value, test and assert

4 months agoSplit-out the gate generator from the proof
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.

4 months agoCompare the expected output for all partition sizes
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.

4 months agoGenerate shifted down outputs
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.

4 months agoGenerate the bit pattern of gates corresponding to a partition
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

4 months agoWork only with nibbles on the ascending cascade
Cesar Strauss [Mon, 4 Jan 2021 21:38:51 +0000 (18:38 -0300)]
Work only with nibbles on the ascending cascade

4 months agoFill the second nibble of the pattern
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.

4 months agoRestart the pattern at partition boundaries
Cesar Strauss [Mon, 4 Jan 2021 20:26:35 +0000 (17:26 -0300)]
Restart the pattern at partition boundaries

4 months agoStart work on improving formal verification of PartitionedSignal
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.

4 months agopartsig: redirect bool to any for now, and use a == Const(-1) for any
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

4 months agocomment PartitionedSignal lt/le
Luke Kenneth Casson Leighton [Sun, 27 Dec 2020 00:09:57 +0000 (00:09 +0000)]
comment PartitionedSignal lt/le

9 months agodisable faulty bit_width reduction logic in DivPipeCore
Jacob Lifshay [Mon, 20 Jul 2020 03:19:22 +0000 (20:19 -0700)]
disable faulty bit_width reduction logic in DivPipeCore

9 months agofix mismatched comb process delays
Jacob Lifshay [Mon, 20 Jul 2020 03:15:25 +0000 (20:15 -0700)]
fix mismatched comb process delays

9 months agoadd process tracing
Jacob Lifshay [Mon, 20 Jul 2020 03:15:01 +0000 (20:15 -0700)]
add process tracing

10 months agoremove FPPipeContext (moved to nmutil), name-substitute on import
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

10 months agoworking on fixing DivPipeCore's test cases
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

10 months agoclean up DivPipeCoreConfig API
Jacob Lifshay [Mon, 13 Jul 2020 02:45:11 +0000 (19:45 -0700)]
clean up DivPipeCoreConfig API

10 months agowhoops missed set up of temp variable bw
Luke Kenneth Casson Leighton [Fri, 10 Jul 2020 12:02:22 +0000 (13:02 +0100)]
whoops missed set up of temp variable bw

10 months agoonly pass in lhs bit_width * 2 for UDivRem
Luke Kenneth Casson Leighton [Fri, 10 Jul 2020 10:34:19 +0000 (11:34 +0100)]
only pass in lhs bit_width * 2 for UDivRem

10 months agoadd arguments to MulPipe_8_16_32_64
Luke Kenneth Casson Leighton [Mon, 6 Jul 2020 14:07:36 +0000 (15:07 +0100)]
add arguments to MulPipe_8_16_32_64

10 months agofix test_mul_pipe.py unit test
Luke Kenneth Casson Leighton [Mon, 6 Jul 2020 14:07:13 +0000 (15:07 +0100)]
fix test_mul_pipe.py unit test

10 months agocontinue reducing length of signals in div core
Luke Kenneth Casson Leighton [Sat, 4 Jul 2020 10:05:48 +0000 (11:05 +0100)]
continue reducing length of signals in div core

10 months agoattempt to get simulation for div test_core.py running
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

10 months agoreduce compare lengths to *2 rather than *3
Luke Kenneth Casson Leighton [Sat, 4 Jul 2020 10:00:03 +0000 (11:00 +0100)]
reduce compare lengths to *2 rather than *3

10 months agowhoops set pass_flag[0] always true
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

10 months agoadd feedback_width argument to runfp for testing
Luke Kenneth Casson Leighton [Sat, 4 Jul 2020 09:25:39 +0000 (10:25 +0100)]
add feedback_width argument to runfp for testing

10 months agoallow arrangement for feedback loops to be possible on ReservationStations in unit...
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

10 months agocut top trial comparison
Luke Kenneth Casson Leighton [Fri, 3 Jul 2020 04:26:17 +0000 (05:26 +0100)]
cut top trial comparison

10 months agoremove use of Array, replace with treereduce
Luke Kenneth Casson Leighton [Fri, 3 Jul 2020 03:45:04 +0000 (04:45 +0100)]
remove use of Array, replace with treereduce

10 months agocut root_times_radicand if not doing Sqrt
Luke Kenneth Casson Leighton [Fri, 3 Jul 2020 03:32:30 +0000 (04:32 +0100)]
cut root_times_radicand if not doing Sqrt

10 months agoadd "supported" option to div core
Luke Kenneth Casson Leighton [Fri, 3 Jul 2020 03:09:36 +0000 (04:09 +0100)]
add "supported" option to div core

11 months agofix imports (allows test command to be run from non-top-level directory)
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)

11 months agomove mulAddRecFN.py and nmigen_div_experiment.py to unused dir
Jacob Lifshay [Thu, 4 Jun 2020 00:26:04 +0000 (17:26 -0700)]
move mulAddRecFN.py and nmigen_div_experiment.py to unused dir

11 months agoadd DivPipeOp in fpdiv/op.py
Jacob Lifshay [Fri, 22 May 2020 22:32:06 +0000 (15:32 -0700)]
add DivPipeOp in fpdiv/op.py

12 months agoFix handling of FPPipeContext.ports()
Michael Nolan [Sat, 16 May 2020 15:16:29 +0000 (11:16 -0400)]
Fix handling of FPPipeContext.ports()

12 months agoAllow partsig to take in a PartitionPoints directly
Michael Nolan [Fri, 8 May 2020 17:01:38 +0000 (13:01 -0400)]
Allow partsig to take in a PartitionPoints directly

12 months agoAdd in FPPipeContext to the cordic pipeline
Michael Nolan [Tue, 5 May 2020 18:08:58 +0000 (14:08 -0400)]
Add in FPPipeContext to the cordic pipeline

12 months agoUse clz.py from nmutil
Michael Nolan [Tue, 5 May 2020 15:16:21 +0000 (11:16 -0400)]
Use clz.py from nmutil

12 months agotrack down error in CORDIC pipe_data, "yield from" used instead of just "yield"
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"

12 months agowhoops cant output .il at the moment
Luke Kenneth Casson Leighton [Tue, 5 May 2020 14:52:35 +0000 (15:52 +0100)]
whoops cant output .il at the moment

12 months agoadd progress counter
Luke Kenneth Casson Leighton [Tue, 5 May 2020 14:51:52 +0000 (15:51 +0100)]
add progress counter

12 months agoallow rtlil file to be created in cordic
Luke Kenneth Casson Leighton [Tue, 5 May 2020 14:48:14 +0000 (15:48 +0100)]
allow rtlil file to be created in cordic

12 months agoAdd renormalize.py (oops!)
Michael Nolan [Tue, 5 May 2020 14:21:02 +0000 (10:21 -0400)]
Add renormalize.py (oops!)

12 months agoremove extraneous whitespace
Luke Kenneth Casson Leighton [Tue, 5 May 2020 14:01:30 +0000 (15:01 +0100)]
remove extraneous whitespace

12 months agoRemove print statements from clz.py
Michael Nolan [Mon, 4 May 2020 22:00:09 +0000 (18:00 -0400)]
Remove print statements from clz.py

12 months agoAdd asserts to fp pipe test
Michael Nolan [Mon, 4 May 2020 21:59:55 +0000 (17:59 -0400)]
Add asserts to fp pipe test

12 months agoSorta working FP renormalization in cordic
Michael Nolan [Mon, 4 May 2020 20:52:41 +0000 (16:52 -0400)]
Sorta working FP renormalization in cordic

12 months agoExtend clz to work with odd widths
Michael Nolan [Mon, 4 May 2020 20:01:20 +0000 (16:01 -0400)]
Extend clz to work with odd widths

12 months agoExtend CLZ to work over even, non powers of 2
Michael Nolan [Mon, 4 May 2020 19:56:24 +0000 (15:56 -0400)]
Extend CLZ to work over even, non powers of 2

12 months agoAdd proof for clz.py
Michael Nolan [Mon, 4 May 2020 19:34:03 +0000 (15:34 -0400)]
Add proof for clz.py

12 months agoAdd count leading zeros module (should probably go somewhere else)
Michael Nolan [Mon, 4 May 2020 18:54:26 +0000 (14:54 -0400)]
Add count leading zeros module (should probably go somewhere else)

12 months agoHave sin_cos pipeline use bigfloat calculated atan table
Michael Nolan [Mon, 4 May 2020 17:40:10 +0000 (13:40 -0400)]
Have sin_cos pipeline use bigfloat calculated atan table

12 months agoAdd cordic stages to fp cordic pipeline
Michael Nolan [Tue, 28 Apr 2020 17:55:53 +0000 (13:55 -0400)]
Add cordic stages to fp cordic pipeline

12 months agoAdd stage to convert input float to fixed point number
Michael Nolan [Tue, 28 Apr 2020 17:44:53 +0000 (13:44 -0400)]
Add stage to convert input float to fixed point number

12 months agoBegin adding floating point cordic pipeline
Michael Nolan [Tue, 28 Apr 2020 17:21:20 +0000 (13:21 -0400)]
Begin adding floating point cordic pipeline

12 months agoAllow cordic to work with 64 bit floats
Michael Nolan [Fri, 17 Apr 2020 15:21:57 +0000 (11:21 -0400)]
Allow cordic to work with 64 bit floats

12 months agomove ripple.py to nmutil
Luke Kenneth Casson Leighton [Fri, 1 May 2020 13:29:20 +0000 (14:29 +0100)]
move ripple.py to nmutil

13 months agoadd libmpfr-dev to .gitlab-ci.yml
Jacob Lifshay [Fri, 17 Apr 2020 21:32:50 +0000 (14:32 -0700)]
add libmpfr-dev to .gitlab-ci.yml

13 months agoChange tabs to spaces in .gitlab-ci.yml
Michael Nolan [Fri, 17 Apr 2020 20:29:09 +0000 (16:29 -0400)]
Change tabs to spaces in .gitlab-ci.yml

13 months agoAdd libgmp-dev to .gitlab-ci.yml
Michael Nolan [Fri, 17 Apr 2020 18:40:10 +0000 (14:40 -0400)]
Add libgmp-dev to .gitlab-ci.yml

13 months agoUse python bigfloat to calculate atan tables
Michael Nolan [Fri, 17 Apr 2020 17:46:05 +0000 (13:46 -0400)]
Use python bigfloat to calculate atan tables

13 months agoRevert "Use higher precision arithmetic when calculating the atan2 table"
Michael Nolan [Fri, 17 Apr 2020 15:22:24 +0000 (11:22 -0400)]
Revert "Use higher precision arithmetic when calculating the atan2 table"

This reverts commit 7aea44d471226db693ee99fd272504248d57375b.

13 months agoUse higher precision arithmetic when calculating the atan2 table
Michael Nolan [Fri, 17 Apr 2020 14:44:34 +0000 (10:44 -0400)]
Use higher precision arithmetic when calculating the atan2 table

13 months agochange test_fpsin to use 32 bit floats
Michael Nolan [Thu, 16 Apr 2020 21:02:09 +0000 (17:02 -0400)]
change test_fpsin to use 32 bit floats

13 months agoRun the cordic for the proper number of iterations
Michael Nolan [Thu, 16 Apr 2020 19:18:07 +0000 (15:18 -0400)]
Run the cordic for the proper number of iterations

13 months agoWorking (ish) fpsin iterative cordic
Michael Nolan [Thu, 16 Apr 2020 18:57:56 +0000 (14:57 -0400)]
Working (ish) fpsin iterative cordic

13 months agoAssert that fpsin_cos converts floats to fixed correctly
Michael Nolan [Thu, 16 Apr 2020 17:14:43 +0000 (13:14 -0400)]
Assert that fpsin_cos converts floats to fixed correctly

13 months agoBegin working on multi cycle float cordic
Michael Nolan [Thu, 16 Apr 2020 15:17:36 +0000 (11:17 -0400)]
Begin working on multi cycle float cordic

13 months agoAdd experiment testing the effects of adding extra bits to cordic
Michael Nolan [Tue, 14 Apr 2020 13:46:23 +0000 (09:46 -0400)]
Add experiment testing the effects of adding extra bits to cordic

13 months agoadd rtlil conversion and fix yield from in Cordic Data
Luke Kenneth Casson Leighton [Mon, 13 Apr 2020 17:22:56 +0000 (18:22 +0100)]
add rtlil conversion and fix yield from in Cordic Data

13 months agorun tests in parallel
Jacob Lifshay [Fri, 3 Apr 2020 07:07:25 +0000 (00:07 -0700)]
run tests in parallel

13 months agobuilding sfpy works
Jacob Lifshay [Fri, 3 Apr 2020 05:52:16 +0000 (22:52 -0700)]
building sfpy works

13 months agoadd not yet working .gitlab-ci.yml
Jacob Lifshay [Fri, 3 Apr 2020 05:27:49 +0000 (22:27 -0700)]
add not yet working .gitlab-ci.yml