Leave shadow / die proof for last

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.

change goldschmidt_div_sqrt to use nmutil.plain_data rather than dataclasses

grr not a yield function

add get_fpregs stub function to HDLstate

update pinmux submodule, rename to "fabric"

add fabric compatibility mode

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

add signal for resetting trap internal state (kaivb cache)

set msr_o.data not msr_o Record in trap main_stage.py

adapt TRAP function in main state pipeline to put KAIVB
into top bits

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

reduce icache/dcache TLB sizes

update trap test_pipe_caller.py to use up-to-date test method

missing module argument to TestRunner execute

convert trap test_pipe_caller.py to consistent format
(like alu test_pipe_caller.py)

Change usage of WB sel for individual control

split out front of div into separate stage, still too long combinatorial
blocks

add missing module

split off CR0/XER production in DIV Function Unit into separate stage
due to massive combinatorial chains

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.

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.

fix waay-too-precise error requirements

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

add option to set small cache sizes in
issuer_verilog.py

add comment

fix so HDL works for 5, 8, 16, 32, and 64-bits.

HDL works for io_width=5

Test simultaneous transparent reads and partial writes

Should catch some corner cases.

add docs for clz

add WIP HDL version of goldschmidt division -- it's currently broken

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.

move GoldschmidtDivState

add FIXME comments

add the goldschmidt sqrt/rsqrt algorithm, still need code to calculate good parameters

switch cached-property dependency to using libre-soc's git repo

improved goldschmidt division algorithm parameter optimization algorithm

split out non-derived params into separate class without all the accuracy checking stuff.

split out n_hat as separate property

add default_cost_fn

move GoldschmidtDivParams.get to bottom of class

rename _goldschmidt_div_ops to GoldschmidtDivState.__make_ops

goldschmidt division works! still needs better parameter selection tho...

fix goofed __init__.py file name

working on goldschmidt_div_sqrt.py

add cached_property dependency

working on goldschmidt division algorithm

whitespace

add WIP goldschmidt division algorithm

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.

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.

Add transparent option for the full read port

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.

reduce dcache/icache number of ways, to fit into ECP5 45k resource

part two of issuer_fix: read pspec.microwatt_old and pspec.microwatt_debug

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

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.

Merge ssh://git.libre-riscv.org:922/soc

part one of issuer_fix: add parameter to issuer_verilog.py

Add port declarations to the SRAM wrappers

Change write lane signal from one-hot to binary

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

whoops, WBASyncBridge ack signal not wired up!

select width is data_width // data granularity.
(common mistake to make, confused the hell out of me too)

Synchronize LVT state, completing the induction proof

Sync proof state with downstream memories

put the old microwatt compatibility back
PLEASE DO NOT CHANGE THIS WITHOUT CONSULTATION

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

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.

Fix incorrect signal widths

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

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.

add option Spec to XICS ICP/ICS to be able to activate (in a horrible
hack way) make_wb_layout to add stall
this is done by spotting "spec.microwatt_compat" adds stall
blegh

move IRQLine out because that makes soc dependent on LambdaSOC

80 char limit, remove creation of stall from ack/cyc, it has to be
done in the parent because that is what knows the usage

wb_async: Allow different feature fields for master/slave busses

Add separate memory clock register to SYSCON

issuer.py: add microwatt_old and microwatt_debug options

Separate core and nest clocks in Microwatt SYSCON

Add initial wrapper for Wishbone asynchronous bridge module

Begin a formal proof of the LVT-based 1W/1R wrapper

Start with a Bounded Model Check, on the transparent case.

Implement 1W/1R with a transparent (or not) read port.

Seems that it's just a matter of the underlying memories being
transparent (or not).

Implement a true 1W/1R memory from 1RW blocks

Uses four phased memories, multiplexers, and FFRAM for the LVT.
Only non-transparent reads, for now.
Test case is included, seems to work.

add a new make target for setting coldboot firmware at 0xfff0_0000
put reset values of pc and msr into Issuer explicitly on reset

syntax error

add dram to SysCon

add SPI offset to microwatt syscon

only add clock-settings on ECP5 due to special SPI clock handling
(Tercel QSPI)

add tempfile to uart16550 wrapper which defines DATA_BUS_WIDTH_8

disable sphinx verilg-diagrams for now

allow direction-setting on each of dq0-3 in Tercel QSPI

cant stand the practice of putting docstrings *after* the code they
document.  a trick to get them to go on one line: semi-colons

Extend the proof to a non-transparent port

For the non-transparent case, have to distinguish the case of a
simultaneous write, where the expected value is the previous
value of the holding register, not the new.

Run formal proof on both types (even/odd) of phased SRAMs

Complete the formal proof of the pseudo dual port SRAM

Have to ensure that the holding register is in sync with the memory
contents, to avoid false positives due to unreachable states.

Since we are adding assertions, we can only strengthen the proof, even
if it does become more complex.

Implement a debug port on the pseudo 1W/1R SRAM

Exposes the debug ports of the underlying memories.
This is needed to assist the induction proof.

Formal proof of the phased write dual port memory wrapper

Similar to the proof of the 1RW memory block, but read and writes are
done on dedicated ports.
For now, only transparent regfile is tested.
To complete the formal verification, an induction proof will follow.

correct default to zero string not zero int

add alternative pc_reset argument to issuer_verilog.py
which propagates right the way down to core.py
next to msr_reset it is now possible to set the pc_reset value.
these actually have to go into the regfile as initial values,
which will be fun for an ASIC

fix some of instantiation errors in opencores_ethmac.py

Fix opencores EthMAC module wiring

Implement transparent read ports on the phased write SRAM

Add a multiplexer to select the write memory instead of the read
memory, in case both port addresses coincide.

Implement and test a "phased write port" memory

It has one read and one write port, but the writes can only happen every
two cycles.
It uses two 1RW memory blocks.
For the moment, it's not transparent: a simultaneous read and write from
the same address returns the old value. Next step is implementing a
transparent read port.