Главная    Ex Libris    Книги    Журналы    Статьи    Серии    Каталог    Wanted    Загрузка    ХудЛит    Справка    Поиск по индексам    Поиск    Форум   
blank
Авторизация

       
blank
Поиск по указателям

blank
blank
blank
Красота
blank
Warren A. Jr. Hunt — Fm8501: A Verified Microprocessor
Warren A. Jr. Hunt — Fm8501: A Verified Microprocessor

Читать книгу
бесплатно

Скачать книгу с нашего сайта нельзя

Обсудите книгу на научном форуме



Нашли опечатку?
Выделите ее мышкой и нажмите Ctrl+Enter


Название: Fm8501: A Verified Microprocessor

Автор: Warren A. Jr. Hunt

Аннотация:

The FM 8501 microprocessor was invented as a generic microprocessor somewhat similar to a PDP-11. The principal idea of the FM 8501 effort was to see if it was possible to express the user-level specification and the design implementation using a formal logic, the Boyer-Moore logic; this approach permitted a complete mechanically checked proof that the FM 8501 implementation fully implemented its specification. The implementation model for the FM 8501 was inadequate for industrial hardware design but the effort was an important step in the evolution to the design verification methodology now employed by the author. The original version of this monograph was submitted as a dissertation at the University of Texas at Austin under the advisorship of R. Boyer and J. Moore.


Язык: en

Рубрика: Computer science/

Статус предметного указателя: Готов указатель с номерами страниц

ed2k: ed2k stats

Издание: 1

Год издания: 1994

Количество страниц: 338

Добавлена в каталог: 24.02.2011

Операции: Положить на полку | Скопировать ссылку для форума | Скопировать ID
blank
Предметный указатель
a-b-oracle      284
a-reg      231
a-reg-after-a-b      283
a-reg-after-a-b-is-a-value-for-alu-after-oprd-a-pre-decrement      300
a-value-for-alu-after-oprd-a-pre-decrement      295
abstract      308
abstract-list      308
Add      161
add-0      180
add-1-1      180
add-with-carry-of-negatives-is-negative      161
add-with-carry-of-non-negatives-is-non-negative      162
addl-difference-subl      188
addr-out      229
addr-out-after-a-b      283
addr-out-after-a-b-is-v-nth-of-reg-file-after-oprd-b-pre-decrement nt      302
all-onesp      158
all-onesp-of-compl      164
all-zerosp      158
alu-c-flag      269 270
alu-correct-twos-complement      208
alu-n-flag      269 270
alu-oracle      277
alu-post-inc-oracle      286
alu-v-flag      269 270
alu-z-flag      269 270
assoc-of-append      212
associativity-of-add      161
associativity-of-plus      147
associativity-of-times      148
b-and      156
b-bv-nzerop      214
b-bv-zerop      214
b-bv-zerop-equal-v-zerop      214
b-cc-set      218
b-direct-reg-a      218
b-direct-reg-b      218
b-dout-incdec      223
b-en-no-store      223
b-equv      156
b-force-inc      223
b-if      189
b-if-works      225
b-indirect-reg-a      218
b-indirect-reg-a-dec      219
b-indirect-reg-a-inc      219
b-indirect-reg-b      218
b-indirect-reg-b-dec      218
b-indirect-reg-b-inc      218
b-ir-mem-ref      223
b-move-op      218
b-nand      156
b-nor      156
b-not      156
b-oprd-mem-ref      226
b-oprd-mem-ref-ifs      226
b-oprd-mem-ref-with-ifs      226
b-oprda-oprdb      223
b-or      156
b-pc-regnum      223
b-postinc      223
b-predec      223
b-rd      223
b-reg      231
b-reg-after-a-b      283
b-reg-after-a-b-is-b-value-for-alu-after-oprd-b-pre-decrement      300
b-seq      223
b-store-alu-result      220 221
b-store-alu-result-ifs      221
b-store-alu-result-with-ifs      220
b-value-for-alu-after-oprd-b-pre-decrement      295
b-we-a-reg      223
b-we-addr-out      223
b-we-alu-result      223
b-we-b-reg      223
b-we-ir      223
b-wr      223
b-xor      156
big-machine      234 236
big-machine-append      237
big-machine-induction      306
big-machine-is-soft-machine      311
bit-interpretation-of-even-and-odd      199
bit-vector-interpretation-of-n-flag      315
bit-vector-interpretation-of-z-flag      315
bitn      157
bitn-compl      180
bitn-equiv-lessp      196
bitn-implies-compl-not-all-onesp      164
bitn-means-negativep      165
bitn-on-implies-non-0      167
bitn-v-append      187
bitv      157
bitvp-v-append      187
boolp      156 217
boolp-alu-c-flag      269
boolp-alu-n-flag      269
boolp-alu-v-flag      269
boolp-alu-z-flag      269
boolp-b-not      181
boolp-bit      157
btmp      158
bv- incrementer-t runcates      1
bv-adder      169 170
bv-adder-as-shifter      195 196
bv-adder-carry-out      169
bv-adder-carry-out-used-as-asl      196
bv-adder-non-btm      170
bv-adder-output      169
bv-adder-output-used-as-asl      195
bv-adder-overflowp      169
bv-alu-cv      191 212
bv-alu-cv-correct-boolean      197
bv-alu-cv-correct-natural-number      201
bv-alu-cv-results      296 315
bv-alu-cv-with-ifs      193 212
bv-alu-op-code      220
bv-and      160
bv-and-is-v-and      192
bv-append      186
bv-asr      186
bv-asr-divides-by-two      188
bv-asr-divides-by-two-bridge      204
bv-cv      189
bv-cv-if      189 191
bv-cv-if-reduce      192
bv-cv-if-works      189
bv-decrementer-truncates-to-machine-size      239
bv-decrementer-truncates-to-machine-size-help      239
bv-equal      215
bv-equal-is-equal      215
bv-if      189
bv-if-works      189
bv-lsr      186
bv-lsr-divides-by-two-lemma      187
bv-next      223
bv-not      159
bv-not-is-compl      177
bv-op-code      218
bv-oprd-a      219
bv-oprd-b      218
bv-or      159
bv-or-is-v-or      192
bv-reg-select      226
bv-reg-select-ifs      226
bv-reg-select-with-ifs      226
bv-ror      186
bv-subtracter-carry-out      177
bv-subtracter-output      177
bv-subtracter-overflowp      177
bv-to-nat      163
bv-to-nat-of-bv-adder      170
bv-to-nat-of-compl      164
bv-to-nat-of-incr      164
bv-to-nat-of-trunc      164
bv-to-nat-of-twos-compl      187
bv-to-nat-to-bv      167
bv-to-nat-to-tc      167
bv-to-nat-to-tc-lemma      2 164
bv-to-nat-to-tc-lemmal      164
bv-to-nat-v-append      187
bv-to-tc      163
bv-to-tc-compl-0      181
bv-to-tc-to-bv      167
bv-to-tc-to-bv-of-zero-is-zero      204
bv-to-tc-to-nat      167
bv-xor      160
bv-xor-is-v-xor      192
c-flag      229
c-flag-ifs      229
c-flag-with-ifs      229
car-if      283
Carry      157
cdr-if      283
commutativity-2-of-add      161
commutativity-2-of-plus      147
commutativity-2-of-times      148
commutativity-of-add      161
commutativity-of-plus      147
commutativity-of-times      148
compl      157
compl-not-btm      181
current-instruction      294
data-out-ifs      228
data-out-with-ifs      228
default-visual-mem-value      232
difference-2      151
difference-2-x-x      187
difference-addl      151
difference-crockl      151
difference-difference      151
difference-elim      151
difference-plus      151
difference-plus-cancellation      151
difference-x-x      151
difference-x-x-1      187
dist ribut ivity-of-t imes-over-plus      148
dtack      227
dtack-after-a-b      284
embed-in-nat-to-bv      168
embed-in-tc-to-bv      168
equal-bools      148
equal-difference-0      180
equal-lessp-hack      179
equal-times-0      148
every-member-sizep      217
every-member-sizep-implies-bit vp      225
every-member-sizep-implies-bitvp-machine-size      225
every-member-sizep-implies-size-nt h-machine-size      217
every-member-sizep-implies-size-nth      217
every-member-sizep-implies-size-nth-0      217
every-member-sizep-update-nth      252 259
every-member-sizep-update-nth-machine-size      258
EXP      150
exp-2-never-0      150
exp-by-0      150
exp-of-0      150
exp-of-1      150
exp-plus      150
exp-times      150
fetch-ir-oracle      249
fetch-oprd-a-addr-out      252
fetch-oprd-a-oracle      258
fetch-oprd-a-reg-file      252
fetch-oprd-b-addr-out      261
fetch-oprd-b-oracle      267
fetch-oprd-b-reg-file      261
fix-bool      212
fix-bv      157
hard-c-flag-is-soft-c-flag      300
hard-n-flag-is-soft-n-flag      302
hard-real-mem-is-soft-real-mem      303
hard-reg-file-is-soft- reg-file      304
hard-v-flag-is-soft-v-flag      301
hard-z-flag-is-soft-z-flag      301
i      195
i-by      2 155
i-by-2      154
i-reg      231
i-reg-ifs      231
i-reg-with-ifs      231
incr      157
incr-compl-nat-to-bv-0      167
incr-f-noop      158
integer-interpretation-of-z-flag      315
length-0      212
length-update-nth      213
length-update-v-nth      213
lessp-crockl      149
lessp-difference      151
lessp-remainder      152
lessp-times      148
list-of-n-plus-l-dtack-off-reset-on      242
list-of-n-plus-l-dtack-reset-off      246
listp-reg-file      241
listp-update-nth      213
listp-update-v-nth      213
lower-bound-on-negative-bv-to-nat      165
machine- size      239
machine-size      216
make-micro-rom      222
make-micro-word      222
MAR      226
mar-on-reset      241
mem-store-flag      278 279
micro-rom      223
micro-store      222
MOD      2 187
n-flag      230 231
n-flag-equals-negativep      214 215
n-flag-ifs      231
n-flag-with-ifs      231
nat-bv-adder-output-seen-as-bit-vector      171 172
nat-bv-subtracter-output-seen-as-bit-vector      178 179
nat-interpret at ion-of-bv-adder- carry-out      172
nat-interpretation-of-bv-adder-output      171
nat-interpretation-of-bv-subtracter-carry-out      179
nat-interpretation-of-bv-subtracter-output      178
nat-interpretation-of-inc-bit-vector      199
nat-interpretation-of-inc-carry-out      199 200
nat-of-zero-is-tc-of-zero      205 207
nat-to-bv      163
nat-to-bv-ignores-remainder      195
nat-to-bv-of      2
nat-to-bv-to-nat      167
nat-to-bv-to-nat-hidden-to-accomodate-hands-off      199
nat-to-bv-to-nat-wrong-size      195
nat-to-tc      163
no-store      227 228
no-store-ifs      227
no-store-with-ifs      227
NTH      213
nth-update-nth      291
nxsz      216
open-big-machine-on-listp      235
open-big-machine-on-nlistp      235
opposite-signs- implies-t c-in-rangep      162
opposite-signs-implies-tc-in-rangep-commuted      162
Oracle      305
oracle-reset      313
1 2
blank
Реклама
blank
blank
HR
@Mail.ru
       © Электронная библиотека попечительского совета мехмата МГУ, 2004-2019
Электронная библиотека мехмата МГУ | Valid HTML 4.01! | Valid CSS! О проекте