T. Meissner
db5a7c3c56
Update Link to Tabby CAD suite
10 months ago
T. Meissner
cfb36987a2
Link GHA shield badge to GHA workflow
10 months ago
T. Meissner
2f06350a33
Fix GHA shield badge
10 months ago
Colin Marquardt
3d29afb13d
Modernize Test GHA workflow ( #3 )
10 months ago
T. Meissner
6a319686ac
fifo: Fix SERE to also match cycles w/o ren after last write
3 years ago
T. Meissner
4a58b1789c
fifo: Add example for GHDL property replication
* By replacing the goto operator with non-literal parameter
by counting the read enabled with simple VHDL counters we
can now replicate the properties instead of writing them
all out.
* Decrease the data width to decrease run-time of unbounded proofs
3 years ago
T. Meissner
c8c8062dca
Add data flow checks in fifo units
4 years ago
T. Meissner
c355c14409
Correct full & empty flag deassertion, fixes #2
4 years ago
T. Meissner
3d57fff226
Replace reset checks by async VHDL asserts; Add assumptions about inputs
4 years ago
T. Meissner
641fa3a6b4
Add fwft-fifo info to readme
4 years ago
T. Meissner
e9b4035e8d
Add fwft-fifo & use that for vai-fifo; minor fixes
4 years ago
T. Meissner
763c2f03c7
Fix badge URL; minor further changes
4 years ago
T. Meissner
2bc122eb5d
Add infos about recommended docker images
4 years ago
T. Meissner
93e98010f7
Merge pull request #1 from umarcor/ci/gha
ci: add GitHub Actions workflow 'Test'
4 years ago
umarcor
37619d21ab
ci: add GitHub Actions workflow 'Test'
4 years ago
T. Meissner
f4029a24ec
Add simple top levem Makefile & test list
4 years ago
T. Meissner
667601fd5e
Use chformal to remove unreachable cover cells
4 years ago
T. Meissner
db4cdea24a
Name assume & restrict directives
4 years ago
T. Meissner
4adea23c43
Fix chformal selection parameter; add reset restrict to top-level
4 years ago
T. Meissner
23cc189011
Add (non-functional yet) VAI-FIFO
4 years ago
T. Meissner
f2e4f71292
Add infos about fifo model to README
4 years ago
T. Meissner
705171911a
Add simple FIFO model incl. formal tests
4 years ago
T. Meissner
903931b2d9
Removing verific related dlatchsr from master branch
5 years ago
T. Meissner
f2f433b165
Use PSL functions instead of workarounds; add forgotten always to asserts in alu
5 years ago
T. Meissner
3da2f2df9e
Update README to renamed branches
5 years ago
T. Meissner
1ef9d692c8
Minor updates to README file
5 years ago
T. Meissner
d94585cad8
Making counter design work with GHDL synthesis
* Remove unused SVA properties file
* Makefile optimizations
* Use prep auto-top option to prevent error with not founded top-level module
when using generics
* Add some simple PSL assertions
5 years ago
T. Meissner
bc59bfd47c
Symplifing Makefile targets
5 years ago
T. Meissner
3e621b02e9
Add alu checks
* Add asserts for correct behaviour of Overflow flag
* Switch to smtbmc engine in prove mode (much faster than abc)
5 years ago
T. Meissner
d420b00310
Making alu design work with GHDL synthesis
* Remove unused SVA properties file
* Makefile optimizations
* Use prep auto-top option to prevent error with not founded top-level module
* Rewrite assignments of Dout_o & Overflow_o as GHDL synthesis don't
support concatenation on left side of assignments
* Add some simple PSL assertions
5 years ago
T. Meissner
996bec1d87
Add short informations about the ghdl-synth branch
5 years ago
T. Meissner
6c3a6db83b
Remove unused SVA properties file; Makefile optimizations; use prep auto-top option to prevent error with not founded top-level module
5 years ago
T. Meissner
bd5fcbcb7a
GHDL supports memory with resets, finally
5 years ago
T. Meissner
e71b70d34e
Add Assumptions about job req VAI interface
5 years ago
T. Meissner
8cf0be6e4c
Add many new asserts & covers
5 years ago
T. Meissner
367343cff5
Add make targets and SymbiYosys tasks for cover, bmc & prove
5 years ago
T. Meissner
195765a2aa
Adapt to use GHDL as plugin for Yosys VHDL synthesis
5 years ago
T. Meissner
c6cc9203d3
Add png versions of read/write waveform examples
6 years ago
T. Meissner
8586d8a265
Add frame diagrams for write/read req/acks
6 years ago
T. Meissner
2a090443ef
Add waveforms of read/write examples
6 years ago
T. Meissner
38ae7057c2
Incomment proof with abc pdr
6 years ago
T. Meissner
9cb4b7d291
Replace integer coded FSM states by symbolic state names
6 years ago
T. Meissner
8edb03c011
Add a bunch of new properties; name all assert directives
6 years ago
T. Meissner
ac767bb9d3
Use SVA defaults for clock & reset; minor RTL optimizations for bettrer readability
6 years ago
T. Meissner
b8a39e9106
Update link to git repo
6 years ago
T. Meissner
60e2c0f301
Add some more signals to trace
6 years ago
T. Meissner
b48e99c1f0
Simplify signal generation
6 years ago
T. Meissner
4e30f44cb0
Fix req cai handling; add more properties
6 years ago
T. Meissner
1deb6e9789
Add vai_reg to README; using SVA default clocking
6 years ago
T. Meissner
63fc34f66a
Add DoutValid_o to condition for state change in putput states
6 years ago