53 Commits (master)
 

Author SHA1 Message Date
  T. Meissner 763c2f03c7 Fix badge URL; minor further changes 6 days ago
  T. Meissner 2bc122eb5d Add infos about recommended docker images 1 week ago
  T. Meissner 93e98010f7
Merge pull request #1 from umarcor/ci/gha 1 week ago
  umarcor 37619d21ab ci: add GitHub Actions workflow 'Test' 1 week ago
  T. Meissner f4029a24ec Add simple top levem Makefile & test list 1 week ago
  T. Meissner 667601fd5e Use chformal to remove unreachable cover cells 2 weeks ago
  T. Meissner db4cdea24a Name assume & restrict directives 2 weeks ago
  T. Meissner 4adea23c43 Fix chformal selection parameter; add reset restrict to top-level 2 weeks ago
  T. Meissner 23cc189011 Add (non-functional yet) VAI-FIFO 2 weeks ago
  T. Meissner f2e4f71292 Add infos about fifo model to README 5 months ago
  T. Meissner 705171911a Add simple FIFO model incl. formal tests 5 months ago
  T. Meissner 903931b2d9 Removing verific related dlatchsr from master branch 7 months ago
  T. Meissner f2f433b165 Use PSL functions instead of workarounds; add forgotten always to asserts in alu 7 months ago
  T. Meissner 3da2f2df9e Update README to renamed branches 7 months ago
  T. Meissner 1ef9d692c8 Minor updates to README file 10 months ago
  T. Meissner d94585cad8 Making counter design work with GHDL synthesis 10 months ago
  T. Meissner bc59bfd47c Symplifing Makefile targets 10 months ago
  T. Meissner 3e621b02e9 Add alu checks 11 months ago
  T. Meissner d420b00310 Making alu design work with GHDL synthesis 11 months ago
  T. Meissner 996bec1d87 Add short informations about the ghdl-synth branch 11 months 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 11 months ago
  T. Meissner bd5fcbcb7a GHDL supports memory with resets, finally 1 year ago
  T. Meissner e71b70d34e Add Assumptions about job req VAI interface 1 year ago
  T. Meissner 8cf0be6e4c Add many new asserts & covers 1 year ago
  T. Meissner 367343cff5 Add make targets and SymbiYosys tasks for cover, bmc & prove 1 year ago
  T. Meissner 195765a2aa Adapt to use GHDL as plugin for Yosys VHDL synthesis 1 year ago
  T. Meissner c6cc9203d3 Add png versions of read/write waveform examples 1 year ago
  T. Meissner 8586d8a265 Add frame diagrams for write/read req/acks 1 year ago
  T. Meissner 2a090443ef Add waveforms of read/write examples 1 year ago
  T. Meissner 38ae7057c2 Incomment proof with abc pdr 2 years ago
  T. Meissner 9cb4b7d291 Replace integer coded FSM states by symbolic state names 2 years ago
  T. Meissner 8edb03c011 Add a bunch of new properties; name all assert directives 2 years ago
  T. Meissner ac767bb9d3 Use SVA defaults for clock & reset; minor RTL optimizations for bettrer readability 2 years ago
  T. Meissner b8a39e9106 Update link to git repo 2 years ago
  T. Meissner 60e2c0f301 Add some more signals to trace 2 years ago
  T. Meissner b48e99c1f0 Simplify signal generation 2 years ago
  T. Meissner 4e30f44cb0 Fix req cai handling; add more properties 2 years ago
  T. Meissner 1deb6e9789 Add vai_reg to README; using SVA default clocking 2 years ago
  T. Meissner 63fc34f66a Add DoutValid_o to condition for state change in putput states 2 years ago
  T. Meissner a0f6a0b81d Add simple VAI register file as base to try to formal verify FSM designs 2 years ago
  T. Meissner 307c6b5f44 Add clock constrain using global clocking 2 years ago
  T. Meissner 7aa4aa52a8 Data in/put width now unconstrained 2 years ago
  T. Meissner 5b8d9650e0 Add genric setting counter end value 2 years ago
  T. Meissner 6d230226f2 Add info about git repo 2 years ago
  T. Meissner 12e20b1da2 Some small improvements 2 years ago
  T. Meissner 9d03113704 Make the unbounded prove work 2 years ago
  T. Meissner 445c013e5c Add example for dlatchsr error 2 years ago
  T. Meissner 3c042a168b Remove unused Data_i port from testbench 2 years ago
  T. Meissner dd0642e762 parameterize design; fix minor makefile problemswq 2 years ago
  T. Meissner 9d0198b0b4 Add counter as example for initial reset problems 2 years ago