tmeissner
/
formal_hw_verification
1
0
Fork 0
Code Issues 0 Pull Requests 0 Releases 6 Wiki Activity

Commit Graph

  • db5a7c3 (HEAD -> master) Update Link to Tabby CAD suite by tmeissner 2024-03-07 10:18:05 +0100
  • cfb3698 Link GHA shield badge to GHA workflow by tmeissner 2024-03-07 10:10:03 +0100
  • 2f06350 Fix GHA shield badge by tmeissner 2024-03-07 10:06:19 +0100
  • 3d29afb Modernize Test GHA workflow (#3) by Colin Marquardt 2024-03-06 20:20:05 +0100
  • 6a31968 fifo: Fix SERE to also match cycles w/o ren after last write by tmeissner 2021-10-05 17:40:03 +0200
  • 4a58b17 fifo: Add example for GHDL property replication by tmeissner 2021-10-05 15:06:00 +0200
  • c8c8062 Add data flow checks in fifo units by tmeissner 2021-03-13 02:03:42 +0100
  • c355c14 Correct full & empty flag deassertion, fixes #2 by tmeissner 2021-03-12 23:56:31 +0100
  • 3d57fff Replace reset checks by async VHDL asserts; Add assumptions about inputs by tmeissner 2021-02-16 23:16:43 +0100
  • 641fa3a Add fwft-fifo info to readme by tmeissner 2021-02-04 01:02:20 +0100
  • e9b4035 Add fwft-fifo & use that for vai-fifo; minor fixes by tmeissner 2021-02-04 00:55:04 +0100
  • 763c2f0 Fix badge URL; minor further changes by tmeissner 2021-01-14 15:24:45 +0100
  • 2bc122e Add infos about recommended docker images by tmeissner 2021-01-14 13:03:19 +0100
  • 93e9801 Merge pull request #1 from umarcor/ci/gha by T. Meissner 2021-01-14 12:06:21 +0100
  • 37619d2 ci: add GitHub Actions workflow 'Test' by umarcor 2021-01-13 23:09:01 +0100
  • f4029a2 Add simple top levem Makefile & test list by tmeissner 2021-01-13 23:26:28 +0100
  • 667601f Use chformal to remove unreachable cover cells by tmeissner 2021-01-06 17:28:48 +0100
  • db4cdea Name assume & restrict directives by tmeissner 2021-01-06 17:02:16 +0100
  • 4adea23 Fix chformal selection parameter; add reset restrict to top-level by tmeissner 2021-01-06 17:01:49 +0100
  • 23cc189 Add (non-functional yet) VAI-FIFO by tmeissner 2021-01-06 16:07:58 +0100
  • f2e4f71 Add infos about fifo model to README by tmeissner 2020-08-10 17:13:24 +0200
  • 7051719 Add simple FIFO model incl. formal tests by tmeissner 2020-08-10 16:58:01 +0200
  • 903931b Removing verific related dlatchsr from master branch by tmeissner 2020-06-08 13:14:15 +0200
  • f2f433b Use PSL functions instead of workarounds; add forgotten always to asserts in alu by tmeissner 2020-06-08 13:12:30 +0200
  • 3da2f2d Update README to renamed branches by tmeissner 2020-06-08 12:38:30 +0200
  • 36d6da1 (verific) Minor updates to README file by tmeissner 2020-03-24 14:39:09 +0100
  • 1ef9d69 Minor updates to README file by tmeissner 2020-03-24 14:39:09 +0100
  • d94585c Making counter design work with GHDL synthesis by tmeissner 2020-03-24 14:32:54 +0100
  • bc59bfd Symplifing Makefile targets by tmeissner 2020-03-21 12:12:27 +0100
  • 3e621b0 Add alu checks by tmeissner 2020-02-24 11:21:44 +0100
  • d420b00 Making alu design work with GHDL synthesis by tmeissner 2020-02-23 15:27:35 +0100
  • 30ef117 Add short informations about the ghdl-synth branch by tmeissner 2020-02-08 12:43:56 +0100
  • 996bec1 Add short informations about the ghdl-synth branch by tmeissner 2020-02-08 01:25:22 +0100
  • 6c3a6db Remove unused SVA properties file; Makefile optimizations; use prep auto-top option to prevent error with not founded top-level module by tmeissner 2020-02-08 01:08:22 +0100
  • bd5fcbc GHDL supports memory with resets, finally by tmeissner 2019-11-06 22:00:03 +0100
  • e71b70d Add Assumptions about job req VAI interface by tmeissner 2019-10-21 18:01:02 +0200
  • 8cf0be6 Add many new asserts & covers by tmeissner 2019-10-21 16:22:05 +0200
  • 367343c Add make targets and SymbiYosys tasks for cover, bmc & prove by tmeissner 2019-10-21 16:21:41 +0200
  • 195765a Adapt to use GHDL as plugin for Yosys VHDL synthesis by tmeissner 2019-09-22 23:10:40 +0200
  • c6cc920 Add png versions of read/write waveform examples by tmeissner 2019-05-23 14:47:20 +0200
  • 8586d8a Add frame diagrams for write/read req/acks by tmeissner 2019-05-23 12:25:59 +0200
  • 2a09044 Add waveforms of read/write examples by tmeissner 2019-05-22 10:13:50 +0200
  • 38ae705 Incomment proof with abc pdr by tmeissner 2019-01-15 23:42:50 +0100
  • 9cb4b7d Replace integer coded FSM states by symbolic state names by tmeissner 2019-01-15 23:42:08 +0100
  • c1ed7d7 (tag: smtbmc_error_2_solution, verific_problem) smtbmc error test case 2 solution (using --nomem) by tmeissner 2019-01-03 23:50:56 +0100
  • eee1d0a (tag: smtbmc_error_2) smtbmc error test case 2 by tmeissner 2019-01-03 23:48:54 +0100
  • b4a8a66 (tag: abc_error_1) abc error test case 1 by tmeissner 2019-01-03 23:45:05 +0100
  • e762dda (tag: smtbmc_error_1, tag: smtbmc_error_0) smtbmc error test case 1 by tmeissner 2019-01-03 23:40:55 +0100
  • 8edb03c Add a bunch of new properties; name all assert directives by tmeissner 2019-01-02 11:30:03 +0100
  • ac767bb Use SVA defaults for clock & reset; minor RTL optimizations for bettrer readability by tmeissner 2019-01-02 11:26:18 +0100
  • b8a39e9 Update link to git repo by tmeissner 2019-01-02 11:25:04 +0100
  • 60e2c0f Add some more signals to trace by tmeissner 2019-01-02 11:04:22 +0100
  • b48e99c Simplify signal generation by tmeissner 2019-01-02 11:03:50 +0100
  • 4e30f44 Fix req cai handling; add more properties by tmeissner 2018-12-31 01:00:50 +0100
  • 1deb6e9 (tag: symbiyosys_error) Add vai_reg to README; using SVA default clocking by tmeissner 2018-12-28 13:57:23 +0100
  • 63fc34f Add DoutValid_o to condition for state change in putput states by tmeissner 2018-12-27 23:43:54 +0100
  • a0f6a0b Add simple VAI register file as base to try to formal verify FSM designs by tmeissner 2018-12-27 22:50:32 +0100
  • 307c6b5 Add clock constrain using global clocking by Torsten Meissner 2018-11-28 16:34:36 +0100
  • 7aa4aa5 Data in/put width now unconstrained by Torsten Meissner 2018-11-28 13:33:52 +0100
  • 5b8d965 Add genric setting counter end value by Torsten Meissner 2018-11-28 11:39:20 +0100
  • 6d23022 Add info about git repo by Torsten Meissner 2018-11-14 12:31:59 +0100
  • 12e20b1 Some small improvements by Torsten Meissner 2018-11-14 12:08:31 +0100
  • 9d03113 Make the unbounded prove work by Torsten Meissner 2018-11-14 11:40:35 +0100
  • 445c013 Add example for dlatchsr error by Torsten Meissner 2018-11-13 15:43:36 +0100
  • 3c042a1 Remove unused Data_i port from testbench by Torsten Meissner 2018-11-13 13:13:30 +0100
  • dd0642e parameterize design; fix minor makefile problemswq by Torsten Meissner 2018-11-13 12:30:12 +0100
  • 9d0198b Add counter as example for initial reset problems by tmeissner 2018-11-13 00:23:19 +0100
  • fca663d Makefile: add clean target; fixed Reset_n_i port dir in alu_t.sv by tmeissner 2018-11-13 00:22:05 +0100
  • 2f7959d Remove gitignore from alu folder; added link to Yosys by tmeissner 2018-11-11 19:32:41 +0100
  • 4feec0f Inital commit by tmeissner 2018-11-11 19:15:03 +0100