This website works better with JavaScript.
Home
Help
Sign In
tmeissner
/
formal_hw_verification
Watch
1
Star
0
Fork
0
Code
Issues
0
Pull Requests
0
Releases
6
Wiki
Activity
Compare commits
merge into: tmeissner:master
tmeissner:master
tmeissner:verific
tmeissner:verific_problem
...
pull from: tmeissner:verific_problem
tmeissner:master
tmeissner:verific
tmeissner:verific_problem
4 Commits
master
...
verific_problem
Author
SHA1
Message
Date
T. Meissner
c1ed7d7b64
smtbmc error test case 2 solution (using --nomem)
6 years ago
T. Meissner
eee1d0a142
smtbmc error test case 2
6 years ago
T. Meissner
b4a8a66d5a
abc error test case 1
6 years ago
T. Meissner
e762dda316
smtbmc error test case 1
6 years ago
2 changed files
with
3 additions
and
2 deletions
Split View
Diff Options
Show Stats
+2
-1
vai_reg/symbiyosys.sby
+1
-1
vai_reg/vai_reg.vhd
+ 2
- 1
vai_reg/symbiyosys.sby
View File
@ -3,9 +3,10 @@ depth 30
wait on
mode prove
#mode bmc
#mode cover
[engines]
smtbmc
smtbmc
--nomem
#abc pdr
[script]
+ 1
- 1
vai_reg/vai_reg.vhd
View File
@ -114,7 +114,7 @@ begin
s_register
(
to_integer
(
unsigned
(
a_addr
)
)
)
<
=
Din_i
;
-- Following line results in following error:
-- ERROR: Unsupported cell type $dlatchsr for cell $verific$wide_dlatchrs_8.$verific$i1$172.
s_register
(
0
)
<
=
Din_i
;
--s_register(0) <= Din_i
;
else
s_error
<
=
true
;
end
if
;
Write
Preview
Loading…
Cancel
Save