فهرست مقاله
در یک رابطِ وضعیت، خواندنِ عددِ یازده و نوشتنِ همان عدد الزاماً دو سوی یک حافظهٔ معمولی نیستند. ممکن است هر بیتِ یک در فرمانِ نوشتن، پرچمی را پاک کند. اگر فقط قصدِ تأییدِ یک رخداد را داشته باشیم، بازگرداندنِ همهٔ بیت‌های دیده‌شده می‌تواند اثرِ بزرگ‌تری از درخواست ایجاد کند. در این درس با یک رجیسترِ چهارپرچمیِ ساختگی، تفاوتِ «وضعیتِ مشاهده‌شده» و «فرمانِ قابلِ اجرا» را با پایتون می‌آزماییم؛ هیچ میکروکنترلر، وقفه یا درگاهِ سخت‌افزاری اجرا نمی‌شود.
۱. خواندنِ وضعیت و نوشتنِ فرمان یک قرارداد ندارند
در قراردادِ Write One to Clear یا W1C، نوشتنِ یک، بیتِ متناظر را صفر می‌کند و نوشتنِ صفر، آن بیت را تغییر نمی‌دهد. بنابراین یکِ خوانده‌شده یعنی پرچم روشن است؛ یکِ نوشته‌شده یعنی همان پرچم را پاک کن. این تفاوت به معنای کم‌ارزش یا پرارزش بودنِ عدد نیست؛ به قراردادِ عملیات مربوط است. بیت‌ها بی‌واحدند و جایگاهِ مستقل را نشان می‌دهند، نه میلی‌ولت، تعدادِ رخداد یا اولویتِ بیشتر.
تعریفِ کاملِ عنصرِ register در Open-CMSIS-SVD، معنای oneToClear را در modifiedWriteValues از ذخیره‌سازیِ عادی جدا می‌کند. همان بخش برای اثرِ خواندن، readAction مستقلی دارد. در مدلِ ما هر چهار بیت فقط W1C هستند و خواندن اثری ندارد. رجیسترِ مخلوط با بیتِ عادی، رزروشده یا پاک‌شونده با خواندن، مشمولِ این مدل نیست؛ نامِ W1C جایِ خواندنِ مشخصاتِ دقیقِ دستگاه را نمی‌گیرد.
برای بیانِ دامنهٔ فرمان، requested ماسکِ پرچم‌هایی است که می‌خواهیم تأیید کنیم. تابع، مجوزِ کاربر یا صحتِ رسیدگی به رخداد را بررسی نمی‌کند؛ فقط اثرِ همان ماسک را محاسبه می‌کند. در درسِ پرچم‌های IntFlag در سایتِ شخصی مسئله، پذیرشِ نمایش و بیتِ ناشناخته بود. اینجا همهٔ ماسک‌های چهار‌بیتی شناخته‌شده‌اند، ولی معنای نوشتن همچنان باید جدا تعریف شود.
۲. چرا خواندن، OR و نوشتن پرچمِ دیگری را پاک می‌کند؟
وضعیتِ خوانده‌شده را در نمایشِ دودویی 1011 و ماسکِ درخواستی را 0001 بگیریم. فقط پرچمِ کم‌ارزش باید پاک شود. نوشتنِ مستقیمِ 0001، وضعیت را به 1010 می‌رساند؛ دو پرچمِ دیگر روشن می‌مانند. این همان مرزِ اثرِ مطلوبِ فرمان است. نوشتنِ صفر روی جایگاهِ دیگر، به معنیِ درخواستِ پاک‌کردنِ آن نیست.
اگر مقدارِ خوانده‌شده را با ماسک OR کنیم، فرمانِ نوشته‌شده 1011 می‌شود. در حافظهٔ معمولی شاید انتظارِ حفظِ بیت‌های دیگر داشته باشیم، اما در این رابط، هر سه یک فرمانِ پاک‌کردن‌اند. نتیجه صفر است و بیت‌های 1010 بیرون از درخواست هم پاک شده‌اند. برنامه این مسیر را با نامِ read_or_write فقط برای نشان‌دادنِ خطا نگه می‌دارد؛ آن را به‌عنوان روشِ تأیید معرفی نمی‌کند.
پرسشِ کاملِ پرچم‌های وقفه در AVR-LibC همین تفاوت را با نمونهٔ نوشتنِ مستقیمِ TIFR و عبارتِ نادرستِ OR توضیح می‌دهد. متن دربارهٔ «بسیاری» از پرچم‌هاست و استثناهای زیرسامانه‌ها را هم یادآوری می‌کند. از این مثال، دستورِ عمومی برای هر قطعه یا پیاده‌سازیِ یک راه‌انداز نتیجه نمی‌گیریم؛ برنامهٔ این درس حتی کدِ C آن منبع را اجرا نمی‌کند.
۳. ترتیبِ رویداد و تأیید؛ پرچم شمارنده نیست
ترتیبِ ساختگیِ ما چهار مرحله دارد: خواندنِ وضعیت، رخدادِ داده‌شده پیش از نوشتن، یک نوشتن، و رخدادِ داده‌شده پس از آن. رخداد، ماسکِ بیت‌هایی است که روشن می‌شوند. این مرحله‌ها زمانِ واقعی ندارند و رفتارِ دو عملِ فیزیکیِ هم‌زمان را حدس نمی‌زنند. مشخصاتِ تقدمِ هم‌زمانِ رخداد و پاک‌کردن در سخت‌افزار، بیرون از قرارداد است.
در مثالِ قبلی اگر میانِ خواندن و نوشتن، پرچمِ تازهٔ 0100 روشن شود، وضعیتِ پیش از نوشتن 1111 است. فرمانِ مستقیمِ 0001 نتیجهٔ 1110 می‌دهد. مسیرِ نادرست هنوز مقدارِ قدیمیِ 1011 را می‌نویسد و نتیجهٔ 0100 می‌دهد؛ پرچمِ تازه در این شاهد باقی می‌ماند، ولی دو پرچمِ قبلیِ خارج از درخواست پاک می‌شوند. پس نباید ادعا کنیم هر رخدادِ بینِ دو مرحله در مسیرِ نادرست حتماً از بین می‌رود.
محدودیتِ مهم‌تر، تکرارِ همان بیت است. اگر وضعیت 0001 باشد و پیش از تأیید، همان رخداد دوباره برسد، وضعیت همچنان 0001 است. حتی نوشتنِ مستقیمِ درست آن را صفر می‌کند؛ از یک بیت نمی‌توان فهمید یک رخداد داشتیم یا دو رخداد. اگر همان رخداد پس از نوشتن برسد، وضعیت دوباره 0001 می‌شود. تفاوتِ ترتیب واقعی است، ولی مدل راهی برای بازیابیِ شمارشِ ازدست‌رفته نمی‌سازد.
در پنجرهٔ ضدبازپخش با بیت‌مپ، نرم‌افزار حافظهٔ شاخص‌های پذیرفته‌شده را مدیریت می‌کرد. اینجا نه شاخصِ شبکه داریم و نه تأییدِ اصالت؛ عملیاتِ پاک‌کردن از قراردادِ رابط می‌آید. هر دو درس نشان می‌دهند شباهتِ نمایشِ بیتی، دلیلِ یکسان بودنِ معنای تغییرِ حالت نیست.
۴. کدِ کامل و مرجعِ مستقلِ مجموعهٔ پرچم‌ها
فایل را با نامِ w1c_status_write.py ذخیره و با python w1c_status_write.py اجرا کنید. فقط کتابخانهٔ استاندارد لازم است؛ نسخهٔ واقعیِ اجرا در خروجی ثبت می‌شود. ماسک‌ها باید int دقیق بین صفر و پانزده باشند؛ bool، زیرکلاسِ عدد، رشته و عددِ اعشاری تبدیل نمی‌شوند. رابطِ دسته‌ای، tuple دقیق با حداکثر هشت فرمانِ set یا write می‌گیرد و همهٔ ورودی را پیش از محاسبه بررسی می‌کند. این سقف، ظرفیتِ سخت‌افزار یا نرخِ پردازش نیست.
"""Bounded synthetic W1C status semantics, not a hardware or interrupt driver.
All four bits are W1C; reads have no side effects. Events are supplied masks.
Read, event-before-write, write and event-after-write form an explicit order.
No simultaneous event/write priority, reserved bits, bus or atomicity modeled.
"""
from itertools import product
import json
import platform
import sys
WIDTH = 4
FULL = (1 << WIDTH) - 1
MAX_OPERATIONS = 8
STRATEGIES = ('direct', 'read_or_write')
def checked_mask(value, name):
if type(value) is not int or not 0 <= value <= FULL:
raise ValueError(name + ' must be an exact int mask0..15')
return value
def set_flags(status, events):
"""Set supplied pending bits. A flag does not count repeated occurrences."""
checked_mask(status, 'status')
checked_mask(events, 'events')
return status | events
def w1c_write(status, written):
"""A written1 clears; a written0 leaves the corresponding bit unchanged."""
checked_mask(status, 'status')
checked_mask(written, 'written')
return status & (FULL ^ written)
def acknowledge(initial, requested, *, between=0, after=0, strategy='direct'):
"""Serial fixture, with events explicitly before/after the single write.
read_or_write is an intentionally wrong comparison, never a recommended
acknowledgement operation. Both paths use the same chosen W1C semantics.
"""
for name, value in (('initial', initial), ('requested', requested),
('between', between), ('after', after)):
checked_mask(value, name)
if type(strategy) is not str or strategy not in STRATEGIES:
raise ValueError('strategy must be direct or read_or_write')
read_snapshot = initial # Our chosen register has no readAction side effect.
written = requested if strategy == 'direct' else read_snapshot | requested
at_write = set_flags(read_snapshot, between)
after_write = w1c_write(at_write, written)
final = set_flags(after_write, after)
return {'strategy': strategy, 'read_snapshot': read_snapshot,
'requested': requested, 'event_between_read_and_write': between,
'written': written, 'status_before_write': at_write,
'status_after_write': after_write, 'event_after_write': after,
'final_status': final,
'cleared_outside_requested': at_write & written & (FULL ^ requested)}
def run_operations(initial, operations):
"""At most8 supplied set/write commands; full validation before evaluation."""
checked_mask(initial, 'initial')
if type(operations) is not tuple or len(operations) > MAX_OPERATIONS:
raise ValueError('operations must be an exact tuple of length0..8')
for item in operations:
if type(item) is not tuple or len(item) != 2:
raise ValueError('each operation must be an exact(kind, mask) tuple')
kind, mask = item
if type(kind) is not str or kind not in ('set', 'write'):
raise ValueError('only exact set/write operation names accepted')
checked_mask(mask, 'operation mask')
state, steps = initial, []
for kind, mask in operations:
before = state
state = set_flags(state, mask) if kind == 'set' else w1c_write(state, mask)
steps.append({'operation': kind, 'mask': mask, 'before': before, 'after': state})
return {'initial': initial, 'steps': steps, 'final_status': state}
def digit_positions(mask):
"""Internal small valid-fixture oracle representation, not public validation."""
return {position for position, digit in enumerate(reversed(format(mask, '04b')))
if digit == '1'}
def position_value(positions):
return sum(2 ** position for position in positions)
def set_reference(initial, requested, between, after, strategy):
"""Independent set union/difference reference; no main bitwise/API calls."""
observed = digit_positions(initial)
target = digit_positions(requested)
pending = observed.union(digit_positions(between))
command = target if strategy == 'direct' else observed.union(target)
cleared = pending.intersection(command)
remaining = pending.difference(command)
return {'strategy': strategy, 'read_snapshot': initial,
'requested': requested, 'event_between_read_and_write': between,
'written': position_value(command), 'status_before_write': position_value(pending),
'status_after_write': position_value(remaining), 'event_after_write': after,
'final_status': position_value(remaining.union(digit_positions(after))),
'cleared_outside_requested': position_value(cleared.difference(target))}
def rejects(function, *args, **kwargs):
try:
function(*args, **kwargs)
except ValueError:
return True
return False
def run_example():
direct = acknowledge(0b1011, 0b0001)
wrong = acknowledge(0b1011, 0b0001, strategy='read_or_write')
new_other = acknowledge(0b1011, 0b0001, between=0b0100)
wrong_new_other = acknowledge(0b1011, 0b0001, between=0b0100,
strategy='read_or_write')
same_before = acknowledge(0b0001, 0b0001, between=0b0001)
same_after = acknowledge(0b0001, 0b0001, after=0b0001)
set_then_write = run_operations(0, (('set', 1), ('write', 1)))
write_then_set = run_operations(0, (('write', 1), ('set', 1)))
single_set = run_operations(0, (('set', 1),))
repeated_set = run_operations(0, (('set', 1), ('set', 1)))
oracle_profiles, oracle_comparisons, oracle_ok = 0, 0, True
for initial, requested, between, after in product(range(16), repeat=4):
oracle_profiles += 1
for strategy in STRATEGIES:
actual = acknowledge(initial, requested, between=between, after=after,
strategy=strategy)
expected = set_reference(initial, requested, between, after, strategy)
oracle_ok &= actual == expected
oracle_comparisons += 1
class IntChild(int):
pass
class TupleChild(tuple):
pass
class StringChild(str):
pass
invalid = (True, False, 1.0, float('nan'), float('inf'), '1', b'1', None,
[], {}, (1,), IntChild(1), -1, 16, 10 ** 100)
mask_rejections = 0
invalid_ok = True
for value in invalid:
calls = ((w1c_write, (value, 0), {}), (w1c_write, (0, value), {}),
(set_flags, (value, 0), {}), (set_flags, (0, value), {}),
(acknowledge, (value, 0), {}), (acknowledge, (0, value), {}),
(acknowledge, (0, 0), {'between': value}),
(acknowledge, (0, 0), {'after': value}))
for function, args, kwargs in calls:
invalid_ok &= rejects(function, *args, **kwargs)
mask_rejections += 1
bad_batches = ([('set', 1)], TupleChild((('set', 1),)), (['set', 1],),
(('set',),), (('set', 1, 2),), (('unknown', 1),),
((StringChild('set'), 1),), (('set', True),),
(('set', 1), ('write', 16)), (('set', 1),) * 9)
untouched = []
def supplied_generator():
untouched.append('consumed')
yield ('set', 1)
generator = supplied_generator()
batches_ok = (all(rejects(run_operations, 0, items) for items in bad_batches)
and rejects(run_operations, 0, generator) and not untouched)
strategies_ok = all(rejects(acknowledge, 1, 1, strategy=value)
for value in ('', 'DIRECT', None, True, StringChild('direct')))
fixture = (('set', 3), ('write', 1), ('set', 8))
first = run_operations(0, fixture)
first['steps'][0]['after'] = -1
first['steps'].append({'fake': True})
fresh = run_operations(0, fixture)
checks = {
'manual_direct_mask_retains_other_flags_but_read_OR_write_clears_them': (
direct['written'] == 1 and direct['final_status'] == 10
and direct['cleared_outside_requested'] == 0
and wrong['written'] == 11 and wrong['final_status'] == 0
and wrong['cleared_outside_requested'] == 10),
'zero_write_has_no_effect_in_pure_W1C_contract': (
w1c_write(11, 0) == 11 and acknowledge(11, 0)['final_status'] == 11),
'all_one_write_clears_current_flags': (
w1c_write(11, 15) == 0 and w1c_write(15, 15) == 0),
'writing_one_to_unset_flags_does_not_set_them': (
w1c_write(0, 15) == 0 and w1c_write(1, 8) == 1),
'read_snapshot_is_separate_from_written_command_and_not_changed_by_later_events': (
new_other['read_snapshot'] == 11 and new_other['written'] == 1
and new_other['status_before_write'] == 15),
'direct_ack_has_no_clearing_outside_requested_positions': (
acknowledge(15, 5)['final_status'] == 10
and acknowledge(15, 5)['cleared_outside_requested'] == 0),
'different_new_flag_between_read_and_write_survives_direct_ack': (
new_other['final_status'] == 14
and wrong_new_other['final_status'] == 4
and wrong_new_other['written'] == 11),
'same_bit_event_before_ack_is_collapsed_and_cleared_even_with_direct_mask': (
same_before['status_before_write'] == 1 and same_before['final_status'] == 0),
'event_after_write_remains_pending_including_requested_position': (
same_after['status_after_write'] == 0 and same_after['final_status'] == 1),
'event_then_ack_and_ack_then_event_have_different_final_states': (
set_then_write['final_status'] == 0 and write_then_set['final_status'] == 1),
'one_pending_bit_does_not_preserve_event_multiplicity': (
single_set['final_status'] == repeated_set['final_status'] == 1
and len(single_set['steps']) == 1 and len(repeated_set['steps']) == 2),
'complete_65536_profiles_two_strategies_match_independent_set_reference_ONE_family': (
bool(oracle_ok) and oracle_profiles == 16 ** 4
and oracle_comparisons == 2 * 16 ** 4),
'strict_mask_strategy_operation_shapes_and_caps_rejected_before_simulation': (
bool(invalid_ok) and mask_rejections == 120 and batches_ok and strategies_ok),
'empty_full_cap_fresh_outputs_and_immutable_supplied_operations': (
run_operations(3, ()) == {'initial': 3, 'steps': [], 'final_status': 3}
and len(run_operations(15, (('write', 0),) * 8)['steps']) == 8
and fresh['final_status'] == 10 and len(fresh['steps']) == 3
and fresh['steps'][0]['after'] == 3
and fixture == (('set', 3), ('write', 1), ('set', 8))
and acknowledge(0, 0)['final_status'] == 0),
}
assert len(checks) == 14 and all(type(v) is bool and v for v in checks.values()), checks
return {'python': platform.python_version(), 'implementation': platform.python_implementation(),
'scope': 'Synthetic four-bit pure W1C register, explicit serial event order; no hardware, ISR, bus, atomicity, clock or device validation',
'contract': {'width_bits': WIDTH, 'mask_range': [0, FULL],
'read_side_effect': 'none in chosen model',
'write_semantics': 'written1 clears, written0 leaves unchanged',
'event_semantics': 'set supplied bits, multiplicity is not retained',
'order': ['read', 'supplied_event_between', 'single_write', 'supplied_event_after'],
'units': 'dimensionless bit positions and logical order',
'max_supplied_operations': MAX_OPERATIONS},
'manual_no_events': {'initial_binary': '1011', 'requested_binary': '0001',
'direct': direct, 'deliberately_wrong_read_OR_write': wrong},
'new_other_flag_between': {'event_binary': '0100', 'direct': new_other,
'deliberately_wrong_read_OR_write': wrong_new_other},
'same_bit_recurrence': {'before_write': same_before, 'after_write': same_after},
'information_loss': {'one_set_final': single_set['final_status'],
'two_sets_final': repeated_set['final_status'],
'flag_is_event_counter': False},
'independent_finite_family': {'initial_requested_between_after_profiles': oracle_profiles,
'strategies_per_profile': 2, 'whole_trace_comparisons_inside_ONE_group': oracle_comparisons,
'reference': 'binary digit sets, union and difference; no main API or bitwise AND/XOR'},
'invalid_cases_inside_ONE_group': {'mask_call_rejections': mask_rejections,
'bad_batch_profiles': len(bad_batches), 'invalid_strategy_profiles': 5,
'generator_consumed': bool(untouched)},
'checks': checks,
'limitations': ['No mixed W1C/RW/clear-on-read/reserved-bit device registers modeled.',
'Same-bit recurrence before clearing is lost by a single flag; direct mask does not solve multiplicity.',
'Simultaneous physical event/write priority and hardware atomicity are unspecified, not inferred.',
'Finite comparison is evidence for this bounded model, not a hardware or safety proof.']}
if __name__ == '__main__':
sys.stdout.buffer.write((json.dumps(run_example(), ensure_ascii=True, indent=2) + '\n').encode('utf-8'))
روشِ اصلی، عملیاتِ بیتی دارد. مرجع، رشتهٔ دودوییِ ماسکِ معتبر را به مجموعهٔ جایگاه‌های روشن تبدیل می‌کند؛ رخداد با اجتماع و نوشتن با تفاضلِ مجموعه‌ها محاسبه می‌شود. مرجع از تابعِ اصلی یا ماسکِ AND و XOR آن استفاده نمی‌کند. مقایسهٔ مستقل، تمامِ ردیفِ اثر را شامل می‌شود: مقدارِ خوانده‌شده، فرمان، حالتِ پیش و پس از نوشتن، نتیجهٔ نهایی و بیت‌های پاک‌شده بیرون از درخواست.
خانوادهٔ محدود، همهٔ شانزده انتخاب برای وضعیتِ اولیه، درخواست و دو ماسکِ رخداد را ترکیب می‌کند؛ ۶۵۵۳۶ پروفایل و دو راهبرد داریم. همهٔ این مقایسه‌ها یک گروه‌اند، نه هزاران آزمونِ مستقلِ نام‌دار. چهارده گروه، علاوه بر این خانواده، شاهدِ دستی، صفر و همهٔ یک‌ها، ترتیبِ رخداد، تکرار، ورودیِ نامعتبر، کرانِ دسته و استقلالِ نتیجه‌ها را بررسی می‌کنند. خروجیِ کاملِ ثبت‌شده در ادامه می‌آید.
{
"python": "3.14.5",
"implementation": "CPython",
"scope": "Synthetic four-bit pure W1C register, explicit serial event order; no hardware, ISR, bus, atomicity, clock or device validation",
"contract": {
"width_bits": 4,
"mask_range": [
0,
15
],
"read_side_effect": "none in chosen model",
"write_semantics": "written1 clears, written0 leaves unchanged",
"event_semantics": "set supplied bits, multiplicity is not retained",
"order": [
"read",
"supplied_event_between",
"single_write",
"supplied_event_after"
],
"units": "dimensionless bit positions and logical order",
"max_supplied_operations": 8
},
"manual_no_events": {
"initial_binary": "1011",
"requested_binary": "0001",
"direct": {
"strategy": "direct",
"read_snapshot": 11,
"requested": 1,
"event_between_read_and_write": 0,
"written": 1,
"status_before_write": 11,
"status_after_write": 10,
"event_after_write": 0,
"final_status": 10,
"cleared_outside_requested": 0
},
"deliberately_wrong_read_OR_write": {
"strategy": "read_or_write",
"read_snapshot": 11,
"requested": 1,
"event_between_read_and_write": 0,
"written": 11,
"status_before_write": 11,
"status_after_write": 0,
"event_after_write": 0,
"final_status": 0,
"cleared_outside_requested": 10
}
},
"new_other_flag_between": {
"event_binary": "0100",
"direct": {
"strategy": "direct",
"read_snapshot": 11,
"requested": 1,
"event_between_read_and_write": 4,
"written": 1,
"status_before_write": 15,
"status_after_write": 14,
"event_after_write": 0,
"final_status": 14,
"cleared_outside_requested": 0
},
"deliberately_wrong_read_OR_write": {
"strategy": "read_or_write",
"read_snapshot": 11,
"requested": 1,
"event_between_read_and_write": 4,
"written": 11,
"status_before_write": 15,
"status_after_write": 4,
"event_after_write": 0,
"final_status": 4,
"cleared_outside_requested": 10
}
},
"same_bit_recurrence": {
"before_write": {
"strategy": "direct",
"read_snapshot": 1,
"requested": 1,
"event_between_read_and_write": 1,
"written": 1,
"status_before_write": 1,
"status_after_write": 0,
"event_after_write": 0,
"final_status": 0,
"cleared_outside_requested": 0
},
"after_write": {
"strategy": "direct",
"read_snapshot": 1,
"requested": 1,
"event_between_read_and_write": 0,
"written": 1,
"status_before_write": 1,
"status_after_write": 0,
"event_after_write": 1,
"final_status": 1,
"cleared_outside_requested": 0
}
},
"information_loss": {
"one_set_final": 1,
"two_sets_final": 1,
"flag_is_event_counter": false
},
"independent_finite_family": {
"initial_requested_between_after_profiles": 65536,
"strategies_per_profile": 2,
"whole_trace_comparisons_inside_ONE_group": 131072,
"reference": "binary digit sets, union and difference; no main API or bitwise AND/XOR"
},
"invalid_cases_inside_ONE_group": {
"mask_call_rejections": 120,
"bad_batch_profiles": 10,
"invalid_strategy_profiles": 5,
"generator_consumed": false
},
"checks": {
"manual_direct_mask_retains_other_flags_but_read_OR_write_clears_them": true,
"zero_write_has_no_effect_in_pure_W1C_contract": true,
"all_one_write_clears_current_flags": true,
"writing_one_to_unset_flags_does_not_set_them": true,
"read_snapshot_is_separate_from_written_command_and_not_changed_by_later_events": true,
"direct_ack_has_no_clearing_outside_requested_positions": true,
"different_new_flag_between_read_and_write_survives_direct_ack": true,
"same_bit_event_before_ack_is_collapsed_and_cleared_even_with_direct_mask": true,
"event_after_write_remains_pending_including_requested_position": true,
"event_then_ack_and_ack_then_event_have_different_final_states": true,
"one_pending_bit_does_not_preserve_event_multiplicity": true,
"complete_65536_profiles_two_strategies_match_independent_set_reference_ONE_family": true,
"strict_mask_strategy_operation_shapes_and_caps_rejected_before_simulation": true,
"empty_full_cap_fresh_outputs_and_immutable_supplied_operations": true
},
"limitations": [
"No mixed W1C/RW/clear-on-read/reserved-bit device registers modeled.",
"Same-bit recurrence before clearing is lost by a single flag; direct mask does not solve multiplicity.",
"Simultaneous physical event/write priority and hardware atomicity are unspecified, not inferred.",
"Finite comparison is evidence for this bounded model, not a hardware or safety proof."
]
}۵. چهار پرسش دربارهٔ حدودِ اثرِ نوشتن
پرسش اول: چرا مقدارِ مشاهده‌شده را همان‌طور به رابط برنگردانیم؟
پاسخ: چون در W1C یکِ نوشته‌شده فرمانِ پاک‌کردن است. برای وضعیتِ 1011 و درخواستِ 0001، بازنویسیِ 1011 دو پرچمِ دیگر را هم هدف می‌گیرد. مشاهدهٔ همهٔ پرچم‌ها، درخواستِ رسیدگی به همهٔ آن‌ها نیست.
پرسش دوم: نوشتنِ صفر همیشه بی‌اثر است؟
پاسخ: فقط در قراردادِ انتخابیِ ما، بله. در رجیسترِ عادی ممکن است مقدار را صفر کند و در قالب‌های دیگر، معنای دیگری داشته باشد. CMSIS-SVD چند نوعِ اثرِ نوشتن و خواندن را جدا توصیف می‌کند؛ مدل فقط یکی را برگزیده است.
پرسش سوم: آیا تأییدِ مستقیم، رخدادِ دوبارهٔ همان بیت را حفظ می‌کند؟
پاسخ: اگر پیش از پاک‌کردن برسد، نه؛ بیتِ ازقبل‌روشن تغییرِ قابلِ مشاهده‌ای نمی‌کند. اگر پس از نوشتن برسد، در این ترتیب روشن می‌ماند. برای شمارش، به قرارداد و سازوکارِ دیگری نیاز است؛ از یک پرچم شمارنده نمی‌سازیم.
پرسش چهارم: تطبیقِ کاملِ خانواده، اجرای اتمیِ یک دستگاه را ثابت می‌کند؟
پاسخ: خیر؛ فقط مدلِ چهار‌بیتی و ترتیبِ صریح را سنجیده‌ایم. باس، وقفه، دسترسیِ هم‌زمان، بیتِ رزروشده و اولویتِ رخدادِ هم‌زمان اجرا نشده‌اند. موفقیتِ مرجع، مشخصاتِ دستگاه یا درستیِ خودِ فرض‌ها را تأیید نمی‌کند.
دو دامنهٔ فنیِ منابع در ۲۹ مهر ۱۴۰۵ کامل خوانده شدند. FAQ نسخهٔ AVR-LibC 2.3.0 را نشان می‌دهد؛ صفحهٔ دوم شاخهٔ mainِ Open-CMSIS-SVD است و شمارهٔ ثابتِ انتشار در HTML ذخیره‌شده‌اش مشخص نیست. تاریخِ نخستین انتشارشان را معلوم فرض نمی‌کنیم. این یک آموزشِ تألیفیِ قراردادِ عملیات است، نه خبرِ تازه، آزمونِ دستگاه یا تضمینِ ایمنی.
منابع و مطالعهٔ بیشتر
- AVR-LibC2.3.0؛ پرسشِ کاملِ پرچم‌های وقفه و نوشتنِ مستقیمِ یک
- Open-CMSIS-SVD؛ عنصرِ register و معنای oneToClear/readAction
بررسی منابع: ۲۹ مهر ۱۴۰۵. تحلیل‌ها و پیشنهادهای اجرایی، جمع‌بندی نویسنده‌اند.
