44 Commits (master)

Author SHA1 Message Date
  T. Meissner f2e4f71292 Add infos about fifo model to README 1 month ago
  T. Meissner 705171911a Add simple FIFO model incl. formal tests 1 month ago
  T. Meissner 903931b2d9 Removing verific related dlatchsr from master branch 3 months ago
  T. Meissner f2f433b165 Use PSL functions instead of workarounds; add forgotten always to asserts in alu 3 months ago
  T. Meissner 3da2f2df9e Update README to renamed branches 3 months ago
  T. Meissner 1ef9d692c8 Minor updates to README file 6 months ago
  T. Meissner d94585cad8 Making counter design work with GHDL synthesis 6 months ago
  T. Meissner bc59bfd47c Symplifing Makefile targets 6 months ago
  T. Meissner 3e621b02e9 Add alu checks 7 months ago
  T. Meissner d420b00310 Making alu design work with GHDL synthesis 7 months ago
  T. Meissner 996bec1d87 Add short informations about the ghdl-synth branch 7 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 7 months ago
  T. Meissner bd5fcbcb7a GHDL supports memory with resets, finally 10 months ago
  T. Meissner e71b70d34e Add Assumptions about job req VAI interface 11 months ago
  T. Meissner 8cf0be6e4c Add many new asserts & covers 11 months ago
  T. Meissner 367343cff5 Add make targets and SymbiYosys tasks for cover, bmc & prove 11 months 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 1 year ago
  T. Meissner 9cb4b7d291 Replace integer coded FSM states by symbolic state names 1 year ago
  T. Meissner 8edb03c011 Add a bunch of new properties; name all assert directives 1 year ago
  T. Meissner ac767bb9d3 Use SVA defaults for clock & reset; minor RTL optimizations for bettrer readability 1 year ago
  T. Meissner b8a39e9106 Update link to git repo 1 year ago
  T. Meissner 60e2c0f301 Add some more signals to trace 1 year ago
  T. Meissner b48e99c1f0 Simplify signal generation 1 year ago
  T. Meissner 4e30f44cb0 Fix req cai handling; add more properties 1 year ago
  T. Meissner 1deb6e9789 Add vai_reg to README; using SVA default clocking 1 year ago
  T. Meissner 63fc34f66a Add DoutValid_o to condition for state change in putput states 1 year ago
  T. Meissner a0f6a0b81d Add simple VAI register file as base to try to formal verify FSM designs 1 year ago
  T. Meissner 307c6b5f44 Add clock constrain using global clocking 1 year ago
  T. Meissner 7aa4aa52a8 Data in/put width now unconstrained 1 year ago
  T. Meissner 5b8d9650e0 Add genric setting counter end value 1 year ago
  T. Meissner 6d230226f2 Add info about git repo 1 year ago
  T. Meissner 12e20b1da2 Some small improvements 1 year ago
  T. Meissner 9d03113704 Make the unbounded prove work 1 year ago
  T. Meissner 445c013e5c Add example for dlatchsr error 1 year ago
  T. Meissner 3c042a168b Remove unused Data_i port from testbench 1 year ago
  T. Meissner dd0642e762 parameterize design; fix minor makefile problemswq 1 year ago
  T. Meissner 9d0198b0b4 Add counter as example for initial reset problems 1 year ago
  T. Meissner fca663d7ac Makefile: add clean target; fixed Reset_n_i port dir in alu_t.sv 1 year ago
  T. Meissner 2f7959db61 Remove gitignore from alu folder; added link to Yosys 1 year ago
  T. Meissner 4feec0fff6 Inital commit 1 year ago