Source / Read the circuit
ti_reference.py
lessons/adc_digital/models/ti_reference.py
#!/usr/bin/env python3
"""Generate interface schedules, verify RTL trace against sample-time ledger.
No DUT slot/RTL arithmetic reused. Reference values use Fraction oracle.
"""
import argparse
import json
from pathlib import Path
import random
from experiments import corrected
def require(condition, message):
if not condition:
raise AssertionError(message)
def pack(values, bits):
return sum((v & ((1 << bits)-1)) << (i*bits) for i,v in enumerate(values))
def make(output):
output.mkdir(parents=True, exist_ok=True)
names = ['normal','random','missing','late','duplicate','wrong_lane','wrong_epoch',
'wrong_id','sink','four_response','reset','reset_old','reset_request',
'reset_return','reset_release','reset_correct','wrap_guard','version_guard']
for name in names:
rng = random.Random(177)
samples = 512 if name in ('normal','random') else 24
limit = samples*25+100
bank0 = ([0]*4,[65536]*4)
bank1 = ([-128,64,160,-96],[round(65536/a) for a in [.99,1.02,.98,1.01]])
bank2 = ([16,-32,48,-64],[60000,70000,65000,66000])
invalid = ([3000]*4,[65536]*4)
updates = {10:bank1,15:bank2,100:bank2,101:bank2,201:invalid,300:bank1}
returned = {}
raw = [rng.randrange(-2048,2048) for _ in range(samples+5)]
delays = [rng.randrange(1,61) if name=='random' else [18,52,9,31][n%4]
for n in range(samples+5)]
if name in ('normal','random'):
delays[4:7] = [60,35,10] # Legal simultaneous three-lane response.
if name=='missing': delays[0] = None
if name=='late': delays[0] = 61
if name=='four_response': delays[:4] = [90,65,40,15] # Violates <=60 bound.
for n,d in enumerate(delays):
if d is not None:
returned.setdefault(25*n+d,[]).append((n%4,n,raw[n],3))
if name=='duplicate': returned.setdefault(19,[]).append((0,0,raw[0],3))
if name=='wrong_lane': returned[18] = [(1,0,raw[0],3)]
if name=='wrong_epoch': returned[18] = [(0,0,raw[0],2)]
if name=='wrong_id': returned[18] = [(0,8,raw[0],3)]
# Coordinated reset starts a new time axis/epoch at global cycle128.
# Old and new responses are deliberately distinguished in reset_old.
reset_start = {'reset_request':25,'reset_return':18,'reset_release':80,
'reset_correct':82}.get(name,125)
restart = reset_start+3
if name.startswith('reset'):
returned = {t:r for t,r in returned.items() if t<reset_start}
for n in range(samples+5):
t = restart+25*n+[18,52,9,31][n%4]
if t<limit: returned.setdefault(t,[]).append((n%4,n,raw[n],4))
if name=='reset_old': returned[restart+1] = [(0,0,123,3)]
fail = {'missing':(80,4,0), 'late':(61,3,0), 'duplicate':(19,2,0),
'wrong_lane':(18,1,0), 'wrong_epoch':(18,1,0), 'wrong_id':(18,1,8),
'sink':(85,6,0), 'four_response':(80,4,0),
'reset_old':(restart+1,1,0),
'wrap_guard':(25,7,0xfffffffc), 'version_guard':(100,7,4)}.get(name)
pending, active, version = None,bank0,0
outputs, expected_rows = {}, []
events = []
local_origin=0
for t in range(limit):
rst = not (name.startswith('reset') and reset_start<=t<restart)
ep = 4 if name.startswith('reset') and t>=restart else 3
if not rst:
pending,active,version=None,bank0,0
outputs = {k:v for k,v in outputs.items() if k<t}
if name.startswith('reset') and t==restart:
local_origin=restart
local=t-local_origin
halted = fail is not None and t>=fail[0]
acc=rej=apply=0; apply_id=None
if rst and not halted:
if local%25==0:
n=local//25
if n%4==0 and pending is not None:
active=pending; pending=None; version+=1; apply=1; apply_id=n
o,g=active
y,sat=corrected(raw[n],o[n%4],g[n%4])
metadata=(ep<<50)|(version<<34)|(n<<2)|(n%4)
outputs[t+84] = (y,sat,metadata,n)
events.append((t,n))
if t in updates and not name.startswith('reset'):
# If pending existed before this frame edge, commit rejects even if applied.
if t in (15,100) or updates[t]==invalid:
rej=1
else: pending=updates[t]; acc=1
elif t in updates and rst and not name.startswith('reset'): rej=1
# Reset during a pipeline transfer aborts its pending output.
output_value=outputs.get(t) if rst and not halted else None
if output_value and name.startswith('reset') and t>=reset_start and t<restart+84:
output_value=None
req = 0
n=local//25
if rst and not halted and local%25==0: req=1<<(n%4)
entry={'req':req,'output':output_value,'acc':acc,'rej':rej,'apply':apply,'apply_id':apply_id,
'fault':int(halted),'fault_spec':fail,'epoch':ep,'local_tick':local,'in_reset':not rst}
expected_rows.append(entry)
stimulus=output/f'{name}.txt'
with stimulus.open('w') as f:
for t,e in enumerate(expected_rows):
rst=int(not (name.startswith('reset') and reset_start<=t<restart))
cfg=updates.get(t,bank0) if not name.startswith('reset') else bank0
commit=int(t in updates and not name.startswith('reset'))
responses=returned.get(t,[])
rv=0; r=[0]*4; ids=[0]*4; ep=[0]*4
for lane,n,value,epoch in responses:
require(not rv & 1<<lane,'two responses same lane in schedule')
rv |= 1<<lane; r[lane]=value; ids[lane]=n; ep[lane]=epoch
ready=0 if name=='sink' and t==85 else 1
snap=int(t in (500,550))
f.write(f'{rst} {e["epoch"]:x} {commit} {pack(cfg[0],18):x} {pack(cfg[1],18):x} '
f'{rv:x} {pack(r,12):x} {pack(ids,32):x} {pack(ep,16):x} {ready} {snap}\n')
(output/f'{name}.json').write_text(json.dumps({'name':name,'rows':expected_rows,'events':events,
'restart':restart,'reset_start':reset_start,
'responses':returned},indent=2)+'\n')
print('ADC_TI_STIMULI_COMPLETE cases='+str(len(names)))
def verify(expected_path, trace_path):
expected=json.loads(expected_path.read_text())
trace=trace_path.read_text().splitlines()
require(len(trace)==len(expected['rows']),'trace length')
seen=0; previous_snapshot=0; saturation_count=0; fault_events=0; previous_fault=0
for t,(line,e) in enumerate(zip(trace,expected['rows'])):
fields=line.split()
require(len(fields)==16, f'trace shape at {t}')
values=[int(v,16) if i in (1,6,15) else int(v) for i,v in enumerate(fields)]
_,req,sample,valid,data,sat,meta,acc,rej,apply,apply_id,fault,code,fid,ftick,snap=values
require(req==e['req'],f'{expected["name"]} request at {t}: {req} != {e["req"]}')
origin=expected['restart'] if expected['name'].startswith('reset') and t>=expected['restart'] else 0
if req: require(sample==(t-origin)//25,
f'sample identity at {t}')
require(fault==e['fault'],f'{expected["name"]} fault at {t}: {fault} != {e["fault"]}')
fault_events+=int(fault and not previous_fault)
previous_fault=fault
if fault:
fail=e['fault_spec']
require(code==fail[1] and fid==fail[2],f'fault reason/id at {t}')
wanted_tick=fail[0]-(expected['restart'] if expected['name']=='reset_old' else 0)
require(ftick==wanted_tick,f'fault timestamp {ftick} != {wanted_tick}')
require((acc,rej,apply)==(e['acc'],e['rej'],e['apply']),f'config handshake at {t}')
if apply: require(apply_id==e['apply_id'],f'apply id at {t}')
out=e['output']
require(bool(valid)==bool(out),f'{expected["name"]} valid at {t}')
if out:
require((data,sat,meta)==tuple(out[:3]),f'{expected["name"]} value/tag at {t}')
seen+=1
saturation_count+=sat
if t in (500,550) and expected['name'] in ('normal','random'):
requests=sum(k<t for k,_ in expected['events'])
responses=sum(len(v) for k,v in expected['responses'].items() if int(k)<t)
delivered=sum(k+85<t for k,_ in expected['events'])
require(snap==(requests<<128)|(responses<<64)|delivered,f'snapshot counts at {t}')
elif t not in (500,550) and not e['in_reset']:
require(snap==previous_snapshot,f'snapshot was not frozen at {t}')
previous_snapshot=snap
(trace_path.parent/'verification.json').write_text(json.dumps({
'case':expected['name'],'cycles':len(trace),'outputs':seen,
'saturation_outputs':saturation_count,'fault_events':fault_events,
'evidence':'RTL trace compared with independent sample ledger'},indent=2)+'\n')
print(f'PASS TI case={expected["name"]} cycles={len(trace)} outputs={seen}')
if __name__=='__main__':
p=argparse.ArgumentParser()
p.add_argument('--generate',type=Path)
p.add_argument('--expected',type=Path)
p.add_argument('--trace',type=Path)
a=p.parse_args()
if a.generate: make(a.generate)
else: verify(a.expected,a.trace)