2 weeks agosplit out front of div into separate stage, still too long combinatorial master
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

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

2 weeks 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 weeks 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.


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 weeks 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
There needs to be an independent Mux for each write lane, since we may not be
writing on all lanes, necessarily.

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

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

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

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

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

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

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

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

3 weeks agonotes added to - absolute paranoia is needed on
Luke Kenneth Casson Leighton [Thu, 28 Apr 2022 08:21:42 +0000 (09:21 +0100)]
notes added to - 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.

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

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

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

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

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

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

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

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

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

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

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

3 weeks agofix goofed file name
Jacob Lifshay [Tue, 26 Apr 2022 02:00:01 +0000 (19:00 -0700)]
fix goofed file name

3 weeks agoworking on
Jacob Lifshay [Mon, 25 Apr 2022 08:44:31 +0000 (01:44 -0700)]
working on

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

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

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

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

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

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

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

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

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

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

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

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

4 weeks agoMerge ssh://
Tobias Platen [Sat, 16 Apr 2022 20:23:14 +0000 (22:23 +0200)]
Merge ssh://

4 weeks agopart one of issuer_fix: add parameter to
Tobias Platen [Sat, 16 Apr 2022 20:21:34 +0000 (22:21 +0200)]
part one of issuer_fix: add parameter to

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

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

4 weeks 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!

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

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

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

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

4 weeks agoblegh.
Luke Kenneth Casson Leighton [Sat, 16 Apr 2022 12:33:33 +0000 (13:33 +0100)]
* 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

5 weeks 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.

5 weeks 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.

5 weeks 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.

5 weeks agoadd option Spec to XICS ICP/ICS to be able to activate (in a horrible
Luke Kenneth Casson Leighton [Thu, 14 Apr 2022 13:13:23 +0000 (14:13 +0100)]
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

5 weeks agomove IRQLine out because that makes soc dependent on LambdaSOC
Luke Kenneth Casson Leighton [Thu, 14 Apr 2022 13:12:36 +0000 (14:12 +0100)]
move IRQLine out because that makes soc dependent on LambdaSOC

5 weeks ago80 char limit, remove creation of stall from ack/cyc, it has to be
Luke Kenneth Casson Leighton [Thu, 14 Apr 2022 11:47:24 +0000 (12:47 +0100)]
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

5 weeks agowb_async: Allow different feature fields for master/slave busses
Raptor Engineering Development Team [Thu, 14 Apr 2022 00:57:20 +0000 (19:57 -0500)]
wb_async: Allow different feature fields for master/slave busses

5 weeks agoAdd separate memory clock register to SYSCON
Raptor Engineering Development Team [Thu, 14 Apr 2022 00:56:47 +0000 (19:56 -0500)]
Add separate memory clock register to SYSCON

5 weeks add microwatt_old and microwatt_debug options
Tobias Platen [Tue, 12 Apr 2022 18:37:00 +0000 (20:37 +0200)] add microwatt_old and microwatt_debug options

5 weeks agoSeparate core and nest clocks in Microwatt SYSCON
Raptor Engineering Development Team [Mon, 11 Apr 2022 19:31:02 +0000 (14:31 -0500)]
Separate core and nest clocks in Microwatt SYSCON

5 weeks agoAdd initial wrapper for Wishbone asynchronous bridge module
Raptor Engineering Development Team [Mon, 11 Apr 2022 19:30:39 +0000 (14:30 -0500)]
Add initial wrapper for Wishbone asynchronous bridge module

5 weeks agoBegin a formal proof of the LVT-based 1W/1R wrapper
Cesar Strauss [Sun, 10 Apr 2022 15:21:14 +0000 (12:21 -0300)]
Begin a formal proof of the LVT-based 1W/1R wrapper

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

5 weeks agoImplement 1W/1R with a transparent (or not) read port.
Cesar Strauss [Sun, 10 Apr 2022 12:24:19 +0000 (09:24 -0300)]
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).

5 weeks agoImplement a true 1W/1R memory from 1RW blocks
Cesar Strauss [Sat, 9 Apr 2022 21:15:52 +0000 (18:15 -0300)]
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.

5 weeks agoadd a new make target for setting coldboot firmware at 0xfff0_0000
Luke Kenneth Casson Leighton [Sat, 9 Apr 2022 12:36:12 +0000 (13:36 +0100)]
add a new make target for setting coldboot firmware at 0xfff0_0000
put reset values of pc and msr into Issuer explicitly on reset

6 weeks agosyntax error
Luke Kenneth Casson Leighton [Fri, 8 Apr 2022 20:10:19 +0000 (21:10 +0100)]
syntax error

6 weeks agoadd dram to SysCon
Luke Kenneth Casson Leighton [Fri, 8 Apr 2022 20:10:00 +0000 (21:10 +0100)]
add dram to SysCon

6 weeks agoadd SPI offset to microwatt syscon
Luke Kenneth Casson Leighton [Fri, 8 Apr 2022 17:41:30 +0000 (18:41 +0100)]
add SPI offset to microwatt syscon

6 weeks agoonly add clock-settings on ECP5 due to special SPI clock handling
Luke Kenneth Casson Leighton [Wed, 6 Apr 2022 11:29:03 +0000 (12:29 +0100)]
only add clock-settings on ECP5 due to special SPI clock handling
(Tercel QSPI)

6 weeks agoadd tempfile to uart16550 wrapper which defines DATA_BUS_WIDTH_8
Luke Kenneth Casson Leighton [Mon, 4 Apr 2022 21:32:32 +0000 (22:32 +0100)]
add tempfile to uart16550 wrapper which defines DATA_BUS_WIDTH_8

6 weeks agodisable sphinx verilg-diagrams for now
Luke Kenneth Casson Leighton [Mon, 4 Apr 2022 20:41:51 +0000 (21:41 +0100)]
disable sphinx verilg-diagrams for now

6 weeks agoallow direction-setting on each of dq0-3 in Tercel QSPI
Luke Kenneth Casson Leighton [Mon, 4 Apr 2022 19:13:41 +0000 (20:13 +0100)]
allow direction-setting on each of dq0-3 in Tercel QSPI

6 weeks agocant stand the practice of putting docstrings *after* the code they
Luke Kenneth Casson Leighton [Sun, 3 Apr 2022 23:52:27 +0000 (00:52 +0100)]
cant stand the practice of putting docstrings *after* the code they
document.  a trick to get them to go on one line: semi-colons

6 weeks agoExtend the proof to a non-transparent port
Cesar Strauss [Sun, 3 Apr 2022 22:12:15 +0000 (19:12 -0300)]
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.

6 weeks agoRun formal proof on both types (even/odd) of phased SRAMs
Cesar Strauss [Sun, 3 Apr 2022 19:31:13 +0000 (16:31 -0300)]
Run formal proof on both types (even/odd) of phased SRAMs

6 weeks agoComplete the formal proof of the pseudo dual port SRAM
Cesar Strauss [Sun, 3 Apr 2022 19:10:16 +0000 (16:10 -0300)]
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.

6 weeks agoImplement a debug port on the pseudo 1W/1R SRAM
Cesar Strauss [Sun, 3 Apr 2022 18:50:43 +0000 (15:50 -0300)]
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.

6 weeks agoFormal proof of the phased write dual port memory wrapper
Cesar Strauss [Sun, 3 Apr 2022 18:24:16 +0000 (15:24 -0300)]
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.

6 weeks agocorrect default to zero string not zero int
Luke Kenneth Casson Leighton [Sun, 3 Apr 2022 16:00:18 +0000 (17:00 +0100)]
correct default to zero string not zero int

6 weeks agoadd alternative pc_reset argument to
Luke Kenneth Casson Leighton [Sun, 3 Apr 2022 10:30:44 +0000 (11:30 +0100)]
add alternative pc_reset argument to
which propagates right the way down to
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

6 weeks agofix some of instantiation errors in
Luke Kenneth Casson Leighton [Sun, 3 Apr 2022 10:29:33 +0000 (11:29 +0100)]
fix some of instantiation errors in

6 weeks agoFix opencores EthMAC module wiring
Raptor Engineering Development Team [Sat, 2 Apr 2022 21:52:49 +0000 (16:52 -0500)]
Fix opencores EthMAC module wiring

6 weeks agoImplement transparent read ports on the phased write SRAM
Cesar Strauss [Sat, 2 Apr 2022 20:46:29 +0000 (17:46 -0300)]
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.

6 weeks agoImplement and test a "phased write port" memory
Cesar Strauss [Fri, 1 Apr 2022 09:47:01 +0000 (06:47 -0300)]
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.

7 weeks agoinvert cs_n pin in Tercel
Luke Kenneth Casson Leighton [Thu, 31 Mar 2022 13:44:24 +0000 (14:44 +0100)]
invert cs_n pin in Tercel

7 weeks agonope, default features in Tercel WB Buses need to not set err yet
Luke Kenneth Casson Leighton [Wed, 30 Mar 2022 09:27:44 +0000 (10:27 +0100)]
nope, default features in Tercel WB Buses need to not set err yet

7 weeks agoadd bus.err to list of default Wishbone signals in Tercel
Luke Kenneth Casson Leighton [Tue, 29 Mar 2022 19:43:10 +0000 (20:43 +0100)]
add bus.err to list of default Wishbone signals in Tercel

7 weeks agobyte-reverse Tercel read/write data and config bus. urr...
Luke Kenneth Casson Leighton [Tue, 29 Mar 2022 18:54:40 +0000 (19:54 +0100)]
byte-reverse Tercel read/write data and config bus. urr...

7 weeks agoset clock freq Constant length to 32-bit in Tercel.
Luke Kenneth Casson Leighton [Tue, 29 Mar 2022 18:18:07 +0000 (19:18 +0100)]
set clock freq Constant length to 32-bit in Tercel.
this really needs to come from SYSCON

7 weeks agoself.specials does not exist, Instances must be added as submodules
Luke Kenneth Casson Leighton [Tue, 29 Mar 2022 14:28:52 +0000 (15:28 +0100)]
self.specials does not exist, Instances must be added as submodules

7 weeks agomore sorting out wishbone names in Tercel
Luke Kenneth Casson Leighton [Tue, 29 Mar 2022 13:33:49 +0000 (14:33 +0100)]
more sorting out wishbone names in Tercel

7 weeks agofix names of Instance signals in Tercel
Luke Kenneth Casson Leighton [Tue, 29 Mar 2022 13:15:00 +0000 (14:15 +0100)]
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

7 weeks agosort out variable names in Tercel
Luke Kenneth Casson Leighton [Tue, 29 Mar 2022 13:10:30 +0000 (14:10 +0100)]
sort out variable names in Tercel

7 weeks agoself.comb does not exist, comb is a local temp-var (comb = m.d.comb)
Luke Kenneth Casson Leighton [Tue, 29 Mar 2022 12:51:49 +0000 (13:51 +0100)]
self.comb does not exist, comb is a local temp-var (comb = m.d.comb)

7 weeks agowhitespace cleanup (80 char limit)
Luke Kenneth Casson Leighton [Tue, 29 Mar 2022 12:11:47 +0000 (13:11 +0100)]
whitespace cleanup (80 char limit)

7 weeks agoAdd initial integration for OpenCores 10/100 Ethernet MAC
Raptor Engineering Development Team [Tue, 29 Mar 2022 01:11:17 +0000 (20:11 -0500)]
Add initial integration for OpenCores 10/100 Ethernet MAC

7 weeks agoFinish the SRAM formal proof by implementing induction
Cesar Strauss [Sun, 27 Mar 2022 17:23:39 +0000 (14:23 -0300)]
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.

7 weeks agoAdd formal verification of the single port memory block
Cesar Strauss [Sat, 26 Mar 2022 21:09:12 +0000 (18:09 -0300)]
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.

7 weeks agorename PLRU modules to avoid conflict in microwatt
Luke Kenneth Casson Leighton [Sat, 26 Mar 2022 20:18:53 +0000 (20:18 +0000)]
rename PLRU modules to avoid conflict in microwatt

2 months agowhitespace cleanup (80 char limit, pep8)
Luke Kenneth Casson Leighton [Fri, 18 Mar 2022 10:45:59 +0000 (10:45 +0000)]
whitespace cleanup (80 char limit, pep8)

2 months agoturn CompALU/CompLDST latches synchronous
Luke Kenneth Casson Leighton [Fri, 18 Mar 2022 10:00:13 +0000 (10:00 +0000)]
turn CompALU/CompLDST latches synchronous
to cut down combinatorial loops