soc.git
14 months agomake installing cocotb work
Jacob Lifshay [Mon, 11 Sep 2023 21:39:22 +0000 (14:39 -0700)]
make installing cocotb work

14 months agoskip madd* tests since they're not implemented
Jacob Lifshay [Mon, 11 Sep 2023 21:32:10 +0000 (14:32 -0700)]
skip madd* tests since they're not implemented

14 months agoMASK was moved into ISACallerHelper class
Jacob Lifshay [Mon, 11 Sep 2023 20:30:26 +0000 (13:30 -0700)]
MASK was moved into ISACallerHelper class

14 months agoset parent pspec to class with XLEN = 64
Jacob Lifshay [Mon, 11 Sep 2023 20:29:51 +0000 (13:29 -0700)]
set parent pspec to class with XLEN = 64

14 months agoset 'soc' filter to filter out v3.1 insns
Jacob Lifshay [Mon, 11 Sep 2023 20:28:46 +0000 (13:28 -0700)]
set 'soc' filter to filter out v3.1 insns

14 months agofix ALU test by setting 'soc' filter to filter out addex
Jacob Lifshay [Mon, 11 Sep 2023 20:27:43 +0000 (13:27 -0700)]
fix ALU test by setting 'soc' filter to filter out addex

14 months agomark src/soc/experiment/test/test_compldst_multi.py as broken
Jacob Lifshay [Mon, 11 Sep 2023 20:26:32 +0000 (13:26 -0700)]
mark src/soc/experiment/test/test_compldst_multi.py as broken

14 months agomark test_pi2ls.py as broken
Jacob Lifshay [Mon, 11 Sep 2023 20:24:55 +0000 (13:24 -0700)]
mark test_pi2ls.py as broken

I tried to fix it, but a whole bunch needs changing so I gave up for now

14 months agoadd cocotb to gitlab-ci
Jacob Lifshay [Mon, 11 Sep 2023 20:23:56 +0000 (13:23 -0700)]
add cocotb to gitlab-ci

14 months agoadd pytest-output-to-files's output dir to gitignore
Jacob Lifshay [Mon, 11 Sep 2023 16:54:57 +0000 (09:54 -0700)]
add pytest-output-to-files's output dir to gitignore

14 months agomake CI work
Jacob Lifshay [Wed, 16 Aug 2023 02:10:31 +0000 (19:10 -0700)]
make CI work

16 months agoMakefile: Added rule for generating mw-compatible core with SVP64
Andrey Miroshnikov [Thu, 27 Jul 2023 11:35:00 +0000 (11:35 +0000)]
Makefile: Added rule for generating mw-compatible core with SVP64
issue_verilog.py: Added argument for mw+svp64.

It's intended to be an unintrusive change for testing. No default behaviour
has been changed.

22 months agoHandle newer nMigen adding a "bench" hierarchy root in VCD files
Cesar Strauss [Sun, 1 Jan 2023 12:30:41 +0000 (09:30 -0300)]
Handle newer nMigen adding a "bench" hierarchy root in VCD files

2 years agoKeep the valid signal from the formal engine ALU stable, until read
Cesar Strauss [Tue, 15 Nov 2022 11:52:58 +0000 (08:52 -0300)]
Keep the valid signal from the formal engine ALU stable, until read

2 years agoCheck that exactly one ALU write is made, per instruction
Cesar Strauss [Fri, 28 Oct 2022 13:15:34 +0000 (10:15 -0300)]
Check that exactly one ALU write is made, per instruction

2 years agoCheck cover and bmc in separate sub-tests
Cesar Strauss [Fri, 28 Oct 2022 12:56:41 +0000 (09:56 -0300)]
Check cover and bmc in separate sub-tests

This allows generating a bmc trace even if cover failed.

2 years agoReset req_l latch on system reset
Cesar Strauss [Wed, 26 Oct 2022 22:02:21 +0000 (19:02 -0300)]
Reset req_l latch on system reset

Even if the holding register of SRLatch is really reset-less, it is still
reset at startup, because the latch reset port has reset=1. But, this only
works if the latch reset port is driven by the sync domain. In case of
req_l, it's driven by the comb domain, so the latch is not reset on system
reset.

Generate a pulse on system reset, and combine it with the latch reset.

2 years agoReset src_l latch on issue_i
Cesar Strauss [Sun, 16 Oct 2022 13:01:37 +0000 (10:01 -0300)]
Reset src_l latch on issue_i

When the input operand is masked, there will be no go_i pulse to
reset the src_l latch, so we force it to reset on issue_i, as well.

2 years agoonly NLnet sponsor
Luke Kenneth Casson Leighton [Mon, 24 Oct 2022 21:05:54 +0000 (22:05 +0100)]
only NLnet sponsor

2 years agoMove test to expose bug in MultiCompUnit
Cesar Strauss [Sun, 16 Oct 2022 11:52:41 +0000 (08:52 -0300)]
Move test to expose bug in MultiCompUnit

A bug was discovered in MultiCompUnit, which occurs only when an
instruction with zero_a or imm_ok is immediately followed by one with
a masked input port. If we move one test out of the way, we get exactly
that.

2 years agoCheck invariant for instruction operands
Cesar Strauss [Wed, 12 Oct 2022 13:32:49 +0000 (10:32 -0300)]
Check invariant for instruction operands

For every instruction issued, at any point in time, each operand
was either:
1) Already read
2) Not read yet, but the read is pending (rel_o high)
3) Masked

2 years agoIf the ALU is idle, do not assert valid
Cesar Strauss [Wed, 12 Oct 2022 12:41:42 +0000 (09:41 -0300)]
If the ALU is idle, do not assert valid

2 years agoCount zero_a and imm_data.ok as masked read transactions
Cesar Strauss [Sun, 9 Oct 2022 21:01:36 +0000 (18:01 -0300)]
Count zero_a and imm_data.ok as masked read transactions

2 years agoDon't issue while busy
Cesar Strauss [Sun, 9 Oct 2022 10:08:13 +0000 (07:08 -0300)]
Don't issue while busy

Otherwise, the formal engine, in some cases, will happily assert issue_i
while busy_o is high. MultiCompUnit can't handle that.

2 years agoAdd count of masked reads
Cesar Strauss [Sat, 8 Oct 2022 21:57:57 +0000 (18:57 -0300)]
Add count of masked reads

2 years agoAdd ALU read transaction counter
Cesar Strauss [Sat, 8 Oct 2022 21:08:48 +0000 (18:08 -0300)]
Add ALU read transaction counter

2 years agoAdd ALU write transaction counter
Cesar Strauss [Sat, 8 Oct 2022 21:05:32 +0000 (18:05 -0300)]
Add ALU write transaction counter

2 years agoAdd write transaction counter
Cesar Strauss [Sat, 8 Oct 2022 20:36:39 +0000 (17:36 -0300)]
Add write transaction counter

2 years agoFix duplicate line (copy & paste error)
Cesar Strauss [Wed, 5 Oct 2022 22:11:09 +0000 (19:11 -0300)]
Fix duplicate line (copy & paste error)

2 years agoAdd counter for operand reads
Cesar Strauss [Sat, 1 Oct 2022 22:08:00 +0000 (19:08 -0300)]
Add counter for operand reads

2 years agoAvoid toggling go_i when rel_o is low
Cesar Strauss [Sat, 1 Oct 2022 22:06:23 +0000 (19:06 -0300)]
Avoid toggling go_i when rel_o is low

This must be enforced on the scoreboard, in its proof.

2 years agoLeave shadow / die proof for last
Cesar Strauss [Sat, 1 Oct 2022 22:00:55 +0000 (19:00 -0300)]
Leave shadow / die proof for last

2 years agoStart of formal proof of MultiCompUnit
Cesar Strauss [Sat, 1 Oct 2022 14:48:19 +0000 (11:48 -0300)]
Start of formal proof of MultiCompUnit

Create a "random" ALU, controlled by the formal engine.
Add an "issue" transaction counter and ask the fomal engine to
give an example.

2 years agochange goldschmidt_div_sqrt to use nmutil.plain_data rather than dataclasses
Jacob Lifshay [Tue, 16 Aug 2022 06:43:13 +0000 (23:43 -0700)]
change goldschmidt_div_sqrt to use nmutil.plain_data rather than dataclasses

2 years agogrr not a yield function
Luke Kenneth Casson Leighton [Sun, 14 Aug 2022 21:09:13 +0000 (22:09 +0100)]
grr not a yield function

2 years agoadd get_fpregs stub function to HDLstate
Luke Kenneth Casson Leighton [Sun, 14 Aug 2022 18:50:46 +0000 (19:50 +0100)]
add get_fpregs stub function to HDLstate

2 years agoupdate pinmux submodule, rename to "fabric"
Luke Kenneth Casson Leighton [Wed, 6 Jul 2022 13:22:54 +0000 (14:22 +0100)]
update pinmux submodule, rename to "fabric"

2 years agoadd fabric compatibility mode
Luke Kenneth Casson Leighton [Wed, 6 Jul 2022 08:11:47 +0000 (09:11 +0100)]
add fabric compatibility mode

2 years agoMulOutputData was only 64-bit output not 128-bit
Luke Kenneth Casson Leighton [Tue, 5 Jul 2022 13:20:11 +0000 (14:20 +0100)]
MulOutputData was only 64-bit output not 128-bit
meaning that mulhd is truncated (always zero)
https://bugs.libre-soc.org/show_bug.cgi?id=855

2 years agoadd signal for resetting trap internal state (kaivb cache)
Luke Kenneth Casson Leighton [Mon, 4 Jul 2022 15:12:46 +0000 (16:12 +0100)]
add signal for resetting trap internal state (kaivb cache)

2 years agoset msr_o.data not msr_o Record in trap main_stage.py
Luke Kenneth Casson Leighton [Mon, 4 Jul 2022 15:07:29 +0000 (16:07 +0100)]
set msr_o.data not msr_o Record in trap main_stage.py

2 years agoadapt TRAP function in main state pipeline to put KAIVB
Luke Kenneth Casson Leighton [Sun, 26 Jun 2022 11:57:33 +0000 (12:57 +0100)]
adapt TRAP function in main state pipeline to put KAIVB
into top bits

2 years agostore KAIVB SPR 850 in TRAP Pipeline
Luke Kenneth Casson Leighton [Sun, 26 Jun 2022 11:38:52 +0000 (12:38 +0100)]
store KAIVB SPR 850 in TRAP Pipeline
by redirecting OP_MTSPR and OP_MFSPR to it
https://bugs.libre-soc.org/show_bug.cgi?id=859

2 years agoreduce icache/dcache TLB sizes
Luke Kenneth Casson Leighton [Sun, 26 Jun 2022 11:11:42 +0000 (12:11 +0100)]
reduce icache/dcache TLB sizes

2 years agoupdate trap test_pipe_caller.py to use up-to-date test method
Luke Kenneth Casson Leighton [Sun, 26 Jun 2022 11:11:14 +0000 (12:11 +0100)]
update trap test_pipe_caller.py to use up-to-date test method

2 years agomissing module argument to TestRunner execute
Luke Kenneth Casson Leighton [Sun, 26 Jun 2022 11:10:35 +0000 (12:10 +0100)]
missing module argument to TestRunner execute

2 years agoconvert trap test_pipe_caller.py to consistent format
Luke Kenneth Casson Leighton [Fri, 17 Jun 2022 14:13:11 +0000 (15:13 +0100)]
convert trap test_pipe_caller.py to consistent format
(like alu test_pipe_caller.py)

2 years agoChange usage of WB sel for individual control
Andrey Miroshnikov [Mon, 23 May 2022 22:17:07 +0000 (22:17 +0000)]
Change usage of WB sel for individual control

2 years agosplit out front of div into separate stage, still too long combinatorial
Luke Kenneth Casson Leighton [Sun, 1 May 2022 17:56:27 +0000 (18:56 +0100)]
split out front of div into separate stage, still too long combinatorial
blocks

2 years agoadd missing module
Luke Kenneth Casson Leighton [Sat, 30 Apr 2022 21:20:02 +0000 (22:20 +0100)]
add missing module

2 years agosplit off CR0/XER production in DIV Function Unit into separate stage
Luke Kenneth Casson Leighton [Sat, 30 Apr 2022 21:17:58 +0000 (22:17 +0100)]
split off CR0/XER production in DIV Function Unit into separate stage
due to massive combinatorial chains

2 years agoclear out DEC in core.cur_state.dec due to spurious interrupt.
Luke Kenneth Casson Leighton [Sat, 30 Apr 2022 12:52:00 +0000 (13:52 +0100)]
clear out DEC in core.cur_state.dec due to spurious interrupt.

this is slightly complicated.  the STATE regfile contains pc, msr, svstate,
dec, and tb, being a reflection of CoreState.  reading from STATE regfile
is on a one-clock delay. the DEC/TB FSM needs to decrement DEC and increment
TB, by reading from the STATE regfile and then writing a new value.

of course, the SPR pipeline has to get a word in edgeways as well.

but...

the complication comes in that it is the PowerDecoder2 which receives
a *cached* copy of DEC, and this cached copy is what has (up until now)
been out-of-date with what is in the STATE regfile.

the hack-job-solution is to zero-out the cached copy when the SPR pipeline
writes a new value to DEC.  the DEC/TB FSM will then rewrite a correct
value into it.

given that PowerDecoder2 only uses the MSB of DEC (and the EE bit of MSR)
to determine whether to fire an interrupt, this should be perfectly fine.

2 years agoImplement transparent read port option on the XOR wrapper SRAM
Cesar Strauss [Sat, 30 Apr 2022 11:08:27 +0000 (08:08 -0300)]
Implement transparent read port option on the XOR wrapper SRAM

Add a bypass path when simultaneously reading and writing to the same
address.
There needs to be an independent Mux for each write lane, since we may not be
writing on all lanes, necessarily.

2 years agofix waay-too-precise error requirements
Jacob Lifshay [Fri, 29 Apr 2022 18:56:49 +0000 (11:56 -0700)]
fix waay-too-precise error requirements

reduces 128x64->64-bit divider to 220k cells rather than 700k cells

2 years agoadd option to set small cache sizes in
Luke Kenneth Casson Leighton [Fri, 29 Apr 2022 09:32:24 +0000 (10:32 +0100)]
add option to set small cache sizes in
issuer_verilog.py

2 years agoadd comment
Jacob Lifshay [Fri, 29 Apr 2022 06:05:08 +0000 (23:05 -0700)]
add comment

2 years agofix so HDL works for 5, 8, 16, 32, and 64-bits.
Jacob Lifshay [Fri, 29 Apr 2022 06:04:05 +0000 (23:04 -0700)]
fix so HDL works for 5, 8, 16, 32, and 64-bits.

2 years agoHDL works for io_width=5
Jacob Lifshay [Fri, 29 Apr 2022 05:40:32 +0000 (22:40 -0700)]
HDL works for io_width=5

2 years agoTest simultaneous transparent reads and partial writes
Cesar Strauss [Thu, 28 Apr 2022 22:37:20 +0000 (19:37 -0300)]
Test simultaneous transparent reads and partial writes

Should catch some corner cases.

2 years agoadd docs for clz
Jacob Lifshay [Thu, 28 Apr 2022 09:26:09 +0000 (02:26 -0700)]
add docs for clz

2 years agoadd WIP HDL version of goldschmidt division -- it's currently broken
Jacob Lifshay [Thu, 28 Apr 2022 09:19:01 +0000 (02:19 -0700)]
add WIP HDL version of goldschmidt division -- it's currently broken

2 years agonotes added to setup.py - absolute paranoia is needed on
Luke Kenneth Casson Leighton [Thu, 28 Apr 2022 08:21:42 +0000 (09:21 +0100)]
notes added to setup.py - absolute paranoia is needed on
what dependencies the HDL has.  dropping USD 16 million on 7nm Mask Charges
you absolutely cannot have arbitrary software downloaded off the internet
from external sources.

2 years agomove GoldschmidtDivState
Jacob Lifshay [Thu, 28 Apr 2022 05:52:41 +0000 (22:52 -0700)]
move GoldschmidtDivState

2 years agoadd FIXME comments
Jacob Lifshay [Thu, 28 Apr 2022 05:50:42 +0000 (22:50 -0700)]
add FIXME comments

2 years agoadd the goldschmidt sqrt/rsqrt algorithm, still need code to calculate good parameters
Jacob Lifshay [Thu, 28 Apr 2022 05:39:08 +0000 (22:39 -0700)]
add the goldschmidt sqrt/rsqrt algorithm, still need code to calculate good parameters

2 years agoswitch cached-property dependency to using libre-soc's git repo
Jacob Lifshay [Wed, 27 Apr 2022 23:21:46 +0000 (16:21 -0700)]
switch cached-property dependency to using libre-soc's git repo

2 years agoimproved goldschmidt division algorithm parameter optimization algorithm
Jacob Lifshay [Wed, 27 Apr 2022 06:50:37 +0000 (23:50 -0700)]
improved goldschmidt division algorithm parameter optimization algorithm

2 years agosplit out non-derived params into separate class without all the accuracy checking...
Jacob Lifshay [Wed, 27 Apr 2022 04:57:40 +0000 (21:57 -0700)]
split out non-derived params into separate class without all the accuracy checking stuff.

2 years agosplit out n_hat as separate property
Jacob Lifshay [Wed, 27 Apr 2022 04:52:08 +0000 (21:52 -0700)]
split out n_hat as separate property

2 years agoadd default_cost_fn
Jacob Lifshay [Wed, 27 Apr 2022 04:41:05 +0000 (21:41 -0700)]
add default_cost_fn

2 years agomove GoldschmidtDivParams.get to bottom of class
Jacob Lifshay [Wed, 27 Apr 2022 04:36:23 +0000 (21:36 -0700)]
move GoldschmidtDivParams.get to bottom of class

2 years agorename _goldschmidt_div_ops to GoldschmidtDivState.__make_ops
Jacob Lifshay [Wed, 27 Apr 2022 04:27:29 +0000 (21:27 -0700)]
rename _goldschmidt_div_ops to GoldschmidtDivState.__make_ops

2 years agogoldschmidt division works! still needs better parameter selection tho...
Jacob Lifshay [Tue, 26 Apr 2022 03:56:30 +0000 (20:56 -0700)]
goldschmidt division works! still needs better parameter selection tho...

2 years agofix goofed __init__.py file name
Jacob Lifshay [Tue, 26 Apr 2022 02:00:01 +0000 (19:00 -0700)]
fix goofed __init__.py file name

2 years agoworking on goldschmidt_div_sqrt.py
Jacob Lifshay [Mon, 25 Apr 2022 08:44:31 +0000 (01:44 -0700)]
working on goldschmidt_div_sqrt.py

2 years agoadd cached_property dependency
Jacob Lifshay [Mon, 25 Apr 2022 08:44:13 +0000 (01:44 -0700)]
add cached_property dependency

2 years agoworking on goldschmidt division algorithm
Jacob Lifshay [Sat, 23 Apr 2022 02:28:37 +0000 (19:28 -0700)]
working on goldschmidt division algorithm

2 years agowhitespace
Luke Kenneth Casson Leighton [Fri, 22 Apr 2022 13:13:21 +0000 (14:13 +0100)]
whitespace

2 years agoadd WIP goldschmidt division algorithm
Jacob Lifshay [Fri, 22 Apr 2022 07:58:17 +0000 (00:58 -0700)]
add WIP goldschmidt division algorithm

2 years agoImplement a 1W/1R register file, XOR style
Cesar Strauss [Sun, 17 Apr 2022 22:27:58 +0000 (19:27 -0300)]
Implement a 1W/1R register file, XOR style

Test case seems to be working.
Total 6x 1RW SRAMs were used, but no DFF RAM was needed.
Still needs a bypass for a transparent read option.

2 years agoFormal proof of pseudo 1W/2R SRAM
Cesar Strauss [Sun, 17 Apr 2022 20:19:32 +0000 (17:19 -0300)]
Formal proof of pseudo 1W/2R SRAM

Mostly taken from the proof of the 1W/1R SRAM. Sorry for all the
duplication, they are all variations of the same theme.

2 years agoAdd transparent option for the full read port
Cesar Strauss [Sun, 17 Apr 2022 18:44:23 +0000 (15:44 -0300)]
Add transparent option for the full read port

2 years agoImplement a pseudo 1W/2R memory
Cesar Strauss [Sun, 17 Apr 2022 18:13:52 +0000 (15:13 -0300)]
Implement a pseudo 1W/2R memory

This is intended for a XOR-based 6x1RW implementation of a 1R/1W
register file.
It costs 3 x 1RW memory blocks.

2 years agoreduce dcache/icache number of ways, to fit into ECP5 45k resource
Luke Kenneth Casson Leighton [Sat, 16 Apr 2022 22:03:27 +0000 (23:03 +0100)]
reduce dcache/icache number of ways, to fit into ECP5 45k resource

2 years agopart two of issuer_fix: read pspec.microwatt_old and pspec.microwatt_debug
Tobias Platen [Sat, 16 Apr 2022 20:50:29 +0000 (22:50 +0200)]
part two of issuer_fix: read pspec.microwatt_old and pspec.microwatt_debug

2 years agoCheck non-transparent 1W/1R SRAM wrapper
Cesar Strauss [Sat, 16 Apr 2022 20:44:30 +0000 (17:44 -0300)]
Check non-transparent 1W/1R SRAM wrapper

Add special case for the non-transparent case, where a simultaneous write
returns the old value of the holding register.
This completes the proof for this 1W/1R SRAM wrapper

2 years agoEnable read port for non-transparent memories
Cesar Strauss [Sat, 16 Apr 2022 20:36:04 +0000 (17:36 -0300)]
Enable read port for non-transparent memories

For some reason, the reset value (=1) of the port enable is not recognized
by the formal engine, even if the simulation is fine with it.

2 years agoMerge ssh://git.libre-riscv.org:922/soc
Tobias Platen [Sat, 16 Apr 2022 20:23:14 +0000 (22:23 +0200)]
Merge ssh://git.libre-riscv.org:922/soc

2 years agopart one of issuer_fix: add parameter to issuer_verilog.py
Tobias Platen [Sat, 16 Apr 2022 20:21:34 +0000 (22:21 +0200)]
part one of issuer_fix: add parameter to issuer_verilog.py

2 years agoAdd port declarations to the SRAM wrappers
Cesar Strauss [Sat, 16 Apr 2022 17:33:04 +0000 (14:33 -0300)]
Add port declarations to the SRAM wrappers

2 years agoChange write lane signal from one-hot to binary
Cesar Strauss [Sat, 16 Apr 2022 17:25:14 +0000 (14:25 -0300)]
Change write lane signal from one-hot to binary

It's simpler to write, and actually runs faster, somehow...

2 years agowhoops, WBASyncBridge ack signal not wired up!
Luke Kenneth Casson Leighton [Sat, 16 Apr 2022 16:21:05 +0000 (17:21 +0100)]
whoops, WBASyncBridge ack signal not wired up!

2 years agoselect width is data_width // data granularity.
Luke Kenneth Casson Leighton [Sat, 16 Apr 2022 15:26:33 +0000 (16:26 +0100)]
select width is data_width // data granularity.
(common mistake to make, confused the hell out of me too)

2 years agoSynchronize LVT state, completing the induction proof
Cesar Strauss [Sat, 16 Apr 2022 14:33:08 +0000 (11:33 -0300)]
Synchronize LVT state, completing the induction proof

2 years agoSync proof state with downstream memories
Cesar Strauss [Sat, 16 Apr 2022 14:29:05 +0000 (11:29 -0300)]
Sync proof state with downstream memories

2 years agoput the old microwatt compatibility back
Luke Kenneth Casson Leighton [Sat, 16 Apr 2022 13:51:47 +0000 (14:51 +0100)]
put the old microwatt compatibility back
PLEASE DO NOT CHANGE THIS WITHOUT CONSULTATION

2 years agoblegh.
Luke Kenneth Casson Leighton [Sat, 16 Apr 2022 12:33:33 +0000 (13:33 +0100)]
blegh.
* add in a new PRE_IDLE state into issue FSM (to allow pc_at_reset to
  get a word in edgeways)
* set nia to pc_at_reset on core_rst (not 0x0)
* add in a terrible hack where the STATE regfile entry for PC is
  shifted down by one.

absolutely no frickin idea why that is needed

2 years agoComplete moving the induction support into the DUT
Cesar Strauss [Fri, 15 Apr 2022 19:43:56 +0000 (16:43 -0300)]
Complete moving the induction support into the DUT

That way, we pass the state down, to be checked by single code at
the lowest level, instead of having to check all variations of the
lower level states, at the top level.
Had to increment the proof depth, for some reason.

2 years agoFix incorrect signal widths
Cesar Strauss [Fri, 15 Apr 2022 19:36:05 +0000 (16:36 -0300)]
Fix incorrect signal widths

dbg_data is the width of a write lane (granularity) and dbg_wrote is a
single bit.

2 years agoMove part of formal proof to the implementation
Cesar Strauss [Fri, 15 Apr 2022 16:55:00 +0000 (13:55 -0300)]
Move part of formal proof to the implementation

For induction, some state has to be synchronized with the
device under test. Make the device itself responsible for checking
this, to avoid exposing its internal workings, and making the proof
more generic.
This is done for PhasedDualPortRegfile, the rest will follow.