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.

invert cs_n pin in Tercel

nope, default features in Tercel WB Buses need to not set err yet

add bus.err to list of default Wishbone signals in Tercel

byte-reverse Tercel read/write data and config bus. urr...

set clock freq Constant length to 32-bit in Tercel.
this really needs to come from SYSCON

self.specials does not exist, Instances must be added as submodules

more sorting out wishbone names in Tercel

fix names of Instance signals in Tercel
names *start* with o_ for output i_ for input p_ for parameter a_ for attr
not end with them

sort out variable names in Tercel

self.comb does not exist, comb is a local temp-var (comb = m.d.comb)

whitespace cleanup (80 char limit)

Add initial integration for OpenCores 10/100 Ethernet MAC

Finish the SRAM formal proof by implementing induction

Add a combinatorial (no delay) debug read port to the SRAM model,
for turning an unreacheable state (memory and holding register differ)
into an illegal state.
Just two clock cycles are needed for a working proof.

Add formal verification of the single port memory block

We test a single, random memory location.
If any memory location, chosen at random, passes, then the whole memory
is correct.
Note that an induction proof is still missing, since it requires
additional assertions to avoid illegal states.

rename PLRU modules to avoid conflict in microwatt

whitespace cleanup (80 char limit, pep8)

turn CompALU/CompLDST latches synchronous
to cut down combinatorial loops

Add initial Tercel integration

NOTE: Still needs testing on physical hardware,
waiting for Arctic Tern support.

Simulate some read/write/modify operations on the SRAM model

Add a Single R/W Port SRAM model

Begin making unit tests by checking with Yosys.

add extra pipeline stages to ALU FU to make timing

introduce extra register of delay to split combinatorial loops
by making fetch_ic_i_valid sync

Revert "read last row from r.wb.adr not r.req_adr in icache"

This reverts commit 1bcb90676398c8fa0c309c3c7ed3c9ef306c577e.

Revert "store cur_state.pc+4 in separate register to help reduce"

This reverts commit d9b58d594ede33db2b0290d7edf8e062f5e91460.

store cur_state.pc+4 in separate register to help reduce
combinatorial chains

read last row from r.wb.adr not r.req_adr in icache

remove stbs_done in icache.py

remove ld_stbs_done from dcache: not needed

work-in-progress on sdram opencores wrapper

Copy the startup delay from issuer.py to inorder.py

Fixes TestIssuerInternalInOrder hanging at startup.

attempting to introduce an extra few clock cycles delay on power-up
this may help with initialisation of I-Cache SRAM which is combinatorial.
maybe

for lulz make I-Cache possible to set to 32-bit (XLEN=32)

bit_length is 1 more than needed: subtract 1 from XLEN first

fix up shift_rot test_pipe_caller to new regspeckls style

convert shift_rot pipeline to XLEN=32/64

fix up Logical pipeline to produce HDL with XLEN=32
fix Logical test_pipe_caller.py to use new regspeckls style

whoops ALU common output target must be XLEN-bit,
cannot set to length of output (o) using Signal.like

set up dummy parent_pspec to pass XLEN=64 in
ALU test_pipe_spec.py

start on converting MUL and DIV pipelines to XLEN

convert from public static functions/properties for regspecs
to member functions to obtain regspecs
this allows pspec (containing XLEN) to be passed to the regspecs,
which in turn allows them to be dynamically set by issuer_verilog.py
and unit tests

fix ALU with XLEN=32, carry and overflow

use XLEN in Function Units (starting with ALU)

add XLEN to issuer_verilog.py defaults to 64

add XLEN option to regfiles via pspec

add running instructions

add formal proof for shift/rot o.ok

clean up code

add formal proof for OP_RLCR

add formal proof for OP_RLCL

add formal proof for OP_RLC

forgot to pass cix (cache-inhibited) through to LD/ST which was
causing D-Cache to make too many read/writes and overrun wishbone
bus addressing on peripherals.
D-Cache always (for non-cache-inhibited) makes 8 64-bit requests:
if a memory-mapped peripheral has only say 3 32-bit CSRs then the
additional requests beyond the range of the peripheral will cause
a permanent lock-up

speed up shift/rot formal proof by running stuff in parallel

it now runs in about 1m30s in `pytest -n auto <file>.py`

also start work on rewriting proofs to hopefully work better, all
of grev, ternlog, extswsli, shl, and shr are completed.

again reduce combinatorial chains, similar to Trap pipeline,
introduce dummy passthrough stage in Branch pipeline

add syn_ramstyle "block_ram" attributes and reduce i/d-cache sizes again

same as shiftrot, split out separate pipelines for logical
stages in order to meet FPGA timing

put LDST go-store on a 1-clock delay to help with combinatorial chains

name core_stop and terminated_o synchronous to potentially help
cut down on combinatorial chains

nope, it's perfectly fine

Revert "weird exception, oe not found in the shiftrot input record"

This reverts commit 264cc7fd7d7547e1e19424b8f8fd0fbfea29cec5.

weird exception, oe not found in the shiftrot input record

Revert "separate out shiftrot stages due to size of main stage being so large"

This reverts commit 87d6b84e96fb62cda16cc9f335e34fe15ad6cd97.

separate out shiftrot stages due to size of main stage being so large

add blockram style to regfile Memory

use block_ram attribute for FPGA synthesis

reduce number of d-cache lines in microwatt fpga mode