modern chisel3 support

[sequencer]

Since chisel newbies are not familiar with Chisel2 now, old style will introduce burdens to maintaining in community. This PR removes legacy import Chisel._ usage and give new tester2 based strategy. And also remove Driver which should be deprecated soon.

• [x] sbt and mill sub-project support.
• [x] In suite test passed.
• [] test with rocket-chip.
• [x] LEC with legacy flow.

[aswaterman]

I agree we should LEC before merging.

[sequencer]

Thanks @leahyao and @msyksphinz! all tests has passed, formal verification framework should wait for #51 getting merged.

[azidar]

Any update on this? It would be great to finish it up.

[sequencer]

Sorry @azidar i got a terribly Tonsillitis these days my work need to be delayed. I’ll put it to my next sprint.

[aswaterman]

Hope you recover quickly @sequencer!

[aswaterman]

@sequencer any update on this? I'd like to merge it if it LECs.

[sequencer]

Tonight! I will work on the yosys LEC CI tonight!

[aswaterman]

@sequencer cool! Note I have added AddRecFN and MulRecFN functional units, but they are already written in chisel3.

[sequencer]

Sure, I’ll work on it tonight.

[sequencer]

Hi, Andrew, I added yosys Miter based LEC for all those modules. I don't know what value should be set to DivSqrtRecF64_div and DivSqrtRecF64_sqrt in yosys script equiv_simple -seq ???, since they are sequential circuits, so DivSqrtRecF64MiterSpec didn't pass. I'm not familiar with design currently, maybe you can give some suggests for this? And by the way, LEC is really time consuming with yosys :)

[jackkoenig]

@sequencer rather than committing the reference .fir files, can you just make it possible to generate them all easily? Either 1) organizing the commits so that the code to generate all of the .fir files comes first, followed by the commit changing things to chisel3 (and making the target directory configurable) or 2) putting the logic to do the LEC in a different repo so that it can generate all of the .fir before the change to chisel3 and after (via 2 checkouts of hardfloat at different commits) and then LEC them.

[jackkoenig]

I can help look at the sequential circuits, we can try an inductive proof http://www.clifford.at/yosys/cmd_equiv_induct.html

[sequencer]

rather than committing the reference .fir files, can you just make it possible to generate them all easily?

Yes, I thought a good idea about this. But didn’t implemented, I will work on my this commit this night. Since in most case, we don’t need to use LEC, diff is enough since most file won’t change.

[sequencer]

In these LEC has been running for 300 hours in my server.

MulAddRecFNMiterSpec_MulAddRecF32_mul
MulAddRecFNMiterSpec_MulAddRecF64_mul
MulRecFNMiterSpec_MulRecF32
MulAddRecFNMiterSpec_MulAddRecF32
MulAddRecFNMiterSpec_MulAddRecF64
MulRecFNMiterSpec_MulRecF64

I think they yosys may not be able to handle this.

DivSqrtRecF64_div
DivSqrtRecF64_sqrt

test failed since they have multi cycles.

May @jackkoenig give some suggestions to this?

[sequencer]

LEC has been running for 630h, I think they can not finish this year. But can we get those merged this year? ;P I think FMA test is good enough to check the correctness now.

[jackkoenig]

@sequencer I would kill that lec run, it's unlikely to ever finish.

Can you package this up slightly differently, rather that committing the .fir files, can you provide instructions to show how to generate them and then LEC them, as well as list which ones LEC doesn't complete for?

I'd like to be able to run LEC myself and maybe set up some model checking for the ones that aren't passing/completing with Yosys.

[sequencer]

I would kill that lec run, it's unlikely to ever finish.

Kill after 2800 hours I finally decided to kill this. ;p someone need to solve the np problem.

Can you package this up slightly differently, rather that committing the .fir files, can you provide instructions to show how to generate them and then LEC them, as well as list which ones LEC doesn't complete for?

I'll work on that ;p

[sequencer]

After two years... I still haven't gain accessibility to JG. ask @tianrui-wei for LEC

[jerryz123]

Since most of these have LEC'd properly, we should merge these. @sequencer can you note in the pr description which modules did not finish LEC?

[sequencer]

I ran LEC with yosys and never ends with these modules:

MulAddRecFNMiterSpec_MulAddRecF32_mul
MulAddRecFNMiterSpec_MulAddRecF64_mul
MulRecFNMiterSpec_MulRecF32
MulAddRecFNMiterSpec_MulAddRecF32
MulAddRecFNMiterSpec_MulAddRecF64
MulRecFNMiterSpec_MulRecF64

I wish I can access jasper :(

[sequencer]

Thanks @jerryz123 for merging this!