https://open-source-silicon.dev logo
Channels
aa
abcc
activity
adiabatonauts
analog-design
announce
announcements
b2aws
b2aws-tutorial
bag
basebands
beagleboard
bluetooth
board-respin
cadence-genus
cadence-innovus
cadence-spectre
cadence-virtuoso
caravan
caravel
caravel-board
chilechipmakers
chip-yard
chipignite
chipignite2206q_stanford_bringup
chisel
coalition-for-digital-environmental-sustainability
community_denmark_dtu
containers
courses
design-review
design-services
dffram
digital-design
digital-electronics-learners
discord-mods
dynamic-power-estimation
efabless
electric
events
fasoc
fault
foss-asic-tools
fossee-iitb-esim
fossee-iitb-google-sky130
fpga
funding
fuserisc
general
generative-ai-silicon-challenge
genius-vlsi
gf180
gf180mcu
hardware-beginners
help-
ieee-sscs-cac-23
ieee-sscs-dc-21q3
ieee-sscs-dc-22
ieee-sscs-dc-23
ihp-sg13g2
images
infiniband
j-core
japan-region
junk
klayout
latam_vlsi
layouteditor
lvs
lvs-analysis
magic
magical
maker-projects
maker-zone
microwatt
mpw-2-silicon
mpw-one-clean-short
mpw-one-silicon
neuro-mem
nydesign
open_pdks
open-pdk
openadiabaticlogic
openfpga
openhighqualityresonators
openlane
openlane_cloudrunner
openlane-development
openocd
openpositarithmetic
openpower
openram
openroad
opentitan
osu
pa-test-chip
paracells
pd-openlane-and-sky130
picosoc
pll
popy_neel
power
private-shuttle
rad-lab-silicon
radio
rdircd
reram
researchers
rf-mmw-design
rios
riscv
sdram
serdes
shuttle
shuttle-precheck
shuttle-status
silicon-photonics
silicon-validation
silicon-validation-private
sky130
sky130-ci
sky130-pv-workshop
sky65
sky90
skywater
sram
stdcelllib
strive
swerv
system-verilog-learners
tapeout-job
tapeout-pakistan
team-awesome
timing-closure
toysram
travis-ci
uvm-learners
vendor-synopsys
venn
verification-be
verification-fe
verilog-learners
vh2v
vhdl
vhdl-learners
vliw
vlsi_verilog_using_opensource_eda
vlsi_verilog_using_opensoure_eda
vlsi-learners-group
vlsi101
waveform-viewers
xls
xschem
xyce
zettascale
Powered by
Title
a

Art Scott

02/03/2021, 4:26 PM
https://www.springerprofessional.de/safety-first-about-the-detection-of-arithmetic-overflows-in-hard/18822316 Authors: Fritjof Bornebusch, Christoph Lüth, Robert Wille, Rolf Drechsler Abstract This work proposes an alternative hardware design approach that allows the detection of arithmetic overflows at the specification level. The established hardware design approach describes infinite integer types at that level while the model describes finite types. This opens a semantic gap between both levels, which means that arithmetic overflows cannot be detected at the specification level. To address this problem the CompCert integer library is utilized that describes finite integer types as dependent types using the proof assistant Coq. Properties that argue about these finite types can be specified and verified at the specification level. This closes the semantic gap the established hardware design approach suffers from.