ieee754fpu.git
3 years 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.

3 years 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.

3 years 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

3 years 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

3 years 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.

3 years 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.

3 years 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.

3 years 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

3 years 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

3 years 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.

3 years 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

3 years 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.

3 years 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

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

4 years 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

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

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

4 years 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

4 years 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

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

4 years 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

4 years 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

4 years 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

4 years 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

4 years 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

4 years 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

4 years 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

4 years 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

4 years 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

4 years 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

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

4 years 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

4 years 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

4 years 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

4 years 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)

4 years 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

4 years 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

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

4 years 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

4 years 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

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

4 years 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"

4 years 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

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

4 years 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

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

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

4 years 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

4 years 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

4 years 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

4 years 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

4 years 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

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

4 years 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)

4 years 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

4 years 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

4 years 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

4 years 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

4 years 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

4 years 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

4 years 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

4 years 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

4 years 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

4 years 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

4 years 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.

4 years 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

4 years 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

4 years 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

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

4 years 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

4 years 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

4 years 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

4 years 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

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

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

4 years 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

4 years agoCombine a selectable number of rounds into one pipeline stage
Michael Nolan [Thu, 2 Apr 2020 17:01:46 +0000 (13:01 -0400)]
Combine a selectable number of rounds into one pipeline stage

4 years agoCleanup
Michael Nolan [Wed, 1 Apr 2020 17:29:01 +0000 (13:29 -0400)]
Cleanup

4 years agoCombine initial stage with first cordic stage
Michael Nolan [Wed, 1 Apr 2020 17:26:09 +0000 (13:26 -0400)]
Combine initial stage with first cordic stage

4 years agoAdd actual tests to test_pipeline.py
Michael Nolan [Wed, 1 Apr 2020 17:17:40 +0000 (13:17 -0400)]
Add actual tests to test_pipeline.py

4 years agoRegister each pipeline stage
Michael Nolan [Wed, 1 Apr 2020 17:17:27 +0000 (13:17 -0400)]
Register each pipeline stage

4 years agoAdd test for sin_cos_pipe (kinda working)
Michael Nolan [Wed, 1 Apr 2020 16:08:45 +0000 (12:08 -0400)]
Add test for sin_cos_pipe (kinda working)

4 years agoAdd test for sin_cos_pipe (not working still)
Michael Nolan [Wed, 1 Apr 2020 16:08:45 +0000 (12:08 -0400)]
Add test for sin_cos_pipe (not working still)

4 years agoConnect up pipeline stages
Michael Nolan [Wed, 1 Apr 2020 15:30:35 +0000 (11:30 -0400)]
Connect up pipeline stages

4 years agoBegin work on pipelined cordic
Michael Nolan [Wed, 1 Apr 2020 15:13:45 +0000 (11:13 -0400)]
Begin work on pipelined cordic

4 years agoCleanup
Michael Nolan [Tue, 31 Mar 2020 20:55:00 +0000 (16:55 -0400)]
Cleanup

4 years agoWorking sin/cos cordic
Michael Nolan [Tue, 31 Mar 2020 20:44:27 +0000 (16:44 -0400)]
Working sin/cos cordic

4 years agosin/cos cordic partially working
Michael Nolan [Tue, 31 Mar 2020 20:35:50 +0000 (16:35 -0400)]
sin/cos cordic partially working

4 years agoAdd test for sin_cos.py
Michael Nolan [Tue, 31 Mar 2020 19:47:52 +0000 (15:47 -0400)]
Add test for sin_cos.py

4 years agoBegin adding cordic
Michael Nolan [Tue, 31 Mar 2020 19:19:02 +0000 (15:19 -0400)]
Begin adding cordic

4 years agoyet another nuisance
Luke Kenneth Casson Leighton [Mon, 2 Mar 2020 15:53:49 +0000 (15:53 +0000)]
yet another nuisance

4 years agoannoying, see https://github.com/nmigen/nmigen/issues/302
Luke Kenneth Casson Leighton [Mon, 2 Mar 2020 15:42:16 +0000 (15:42 +0000)]
annoying, see https://github.com/nmigen/nmigen/issues/302
shift can no longer be signed, even if the amount is guaranteed signed

4 years agoApply Luke's suggestions/FIXME's
Michael Nolan [Thu, 27 Feb 2020 00:30:24 +0000 (19:30 -0500)]
Apply Luke's suggestions/FIXME's

4 years agomore fun comments
Luke Kenneth Casson Leighton [Wed, 26 Feb 2020 17:52:06 +0000 (17:52 +0000)]
more fun comments

4 years agoshuffle and comments
Luke Kenneth Casson Leighton [Wed, 26 Feb 2020 17:44:15 +0000 (17:44 +0000)]
shuffle and comments

4 years agoupdate comments on test partitioned signal
Luke Kenneth Casson Leighton [Wed, 26 Feb 2020 17:35:54 +0000 (17:35 +0000)]
update comments on test partitioned signal

4 years agotiny code-shuffle on GatedBitReverse
Luke Kenneth Casson Leighton [Wed, 26 Feb 2020 17:31:01 +0000 (17:31 +0000)]
tiny code-shuffle on GatedBitReverse

4 years agoAdd shift right to test_partsig and partsig
Michael Nolan [Wed, 26 Feb 2020 16:56:24 +0000 (11:56 -0500)]
Add shift right to test_partsig and partsig

4 years agoRename bitrev signal to shift_right (more descriptive)
Michael Nolan [Wed, 26 Feb 2020 16:46:23 +0000 (11:46 -0500)]
Rename bitrev signal to shift_right (more descriptive)

4 years agoShift left now working
Michael Nolan [Wed, 26 Feb 2020 16:37:21 +0000 (11:37 -0500)]
Shift left now working