File: [Thyme]<Thyme>Cedar5.2>Top>SignalGenerators.thy
Last Edited by: McCreight, March 28, 1985 11:29:10 am PST
Pulse: circuit[output | amplitude ← 5
V, offset ← 0, period ← 10ns, width ← 5ns, tRise ← 2ns, tFall ← 2ns, tDelay ← 0] asserts[width < period, tRise + tFall < width] = {
pg: voltage[output, Gnd] ← PulseGen[amplitude + offset, offset, period, width, tRise, tFall, tDelay]
}; -- Pulse
RectWave: circuit[output | OnLevel ← 5
V, OffLevel ← 0
V, period ← 20ns, width ← 10ns, tRise ← 2ns, tFall ← 2ns, tDelay ← 0ns] asserts[width < period, tRise + tFall < width] = {
pg: voltage[output, Gnd] ← PulseGen[OnLevel, OffLevel, period, width, tRise, tFall, tDelay]
}; -- RectWave
OneShot: circuit[output | OnLevel ← 5
V, OffLevel ← 0
V, width ← 10ns, tRise ← 2ns, tFall ← 2ns, tDelay ← 0ns] asserts[tRise + tFall < width] = {
pg: voltage[output, Gnd] ← OneShotGen[OnLevel, OffLevel, width, tRise, tFall, tDelay]
}; -- OneShot
Step: circuit[output | OnLevel ← 5
V, OffLevel ← 0
V, tRise ← 5ns, tDelay ← 0ns]
asserts[tRise > 0] = {
pg: voltage[output, Gnd] ← StepGen[
OnLevel, OffLevel, tRise, tDelay]
}; -- Step