需求变成可观测义务
目标: 为什么需要响应身份? 作答时请说明需求、判据、观测事件、故障模式,以及该证据仍不能支持的一项结论。
有用需求说明触发、采样输入、允许延迟、预期响应、复位与取消行为,以及能推翻它的观测。 功能验证追问实现是否在重要情形下满足书面行为契约。一次测试通过,只对其命名的设计版本、参数、假设、激励、判据、采样规则与已检查观测构成证据;不能悄悄转化为时序收敛、CDC 正确、物理可靠、安全、性能容量或制造硅片的证明。因此每课都从说明一个义务以及能够推翻它的观测开始。
验证契约是:在边沿 t 采样到 in_valid&&in_ready 时,除非复位取消,必须在 t+2 到 t+4 边沿之间恰好传输一个匹配响应。 保留的不变量是:复位外每个观测边沿都有“接受计数=完成计数+活动义务数”。 运行前,把需求标识映射到激励分区、独立期望结果、断言、覆盖与故障产物。记录时钟与复位语义、事务身份、合法与非法输入、延迟范围、反压、顺序、取消与参数边界。保留已知故障“只检查某次 out_valid 出现,会让错误请求身份或重复响应通过。”作为变更目标,使证据必须检测可信缺陷,而不只是观察到活动。
复位外每个观测边沿都有“接受计数=完成计数+活动义务数”。 该不变量只在声明的观测边界与假设下检查;被禁用、不可达或未观测的前件不能算作有意义的成功。
接受时创建一个义务记录。 在推导第 1 步,指出需求、采样值、事务身份、独立期望值,以及闭合义务的精确比较或性质。
在每个声明观测边沿增加年龄,并在响应时比较身份/数据。 在推导第 2 步,指出需求、采样值、事务身份、独立期望值,以及闭合义务的精确比较或性质。
重复、缺失、过早、过晚或不匹配完成时失败;只按复位规则取消。 在推导第 3 步,指出需求、采样值、事务身份、独立期望值,以及闭合义务的精确比较或性质。
追踪 t0 接受 A、t2 接受 B,响应 A 在 t3、B 在 t6。 揭示结果前先预测完整事件或事务追踪,在适用时包括复位、空闲、接受、延迟、停顿、响应与超时。
- A 的窗口为 t2..t4,t3 响应合法。 在追踪第 1 步,记录采样前状态、采样输入、监视事件、判据更新、已检查输出、断言状态,以及该观测属于架构接口还是仅属于测试台内部。
- B 的窗口为 t4..t6,t6 响应合法。 在追踪第 2 步,记录采样前状态、采样输入、监视事件、判据更新、已检查输出、断言状态,以及该观测属于架构接口还是仅属于测试台内部。
- 身份匹配各自恰好闭合一次义务,守恒回到零活动义务。 在追踪第 3 步,记录采样前状态、采样输入、监视事件、判据更新、已检查输出、断言状态,以及该观测属于架构接口还是仅属于测试台内部。
结果: 两个义务都在各自窗口内恰好完成一次。 只有在基线通过、命名故障使预期检查或性质在第一个责任边界失败、且恢复后基线从干净环境重跑通过时,才接受该结果。