<Cedar5.2>Top>SignalGenerators.thy>> <> Pulse: circuit[output | amplitude _ 5V, 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 _ 5V, OffLevel _ 0V, 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 _ 5V, OffLevel _ 0V, 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 _ 5V, OffLevel _ 0V, tRise _ 5ns, tDelay _ 0ns] asserts[tRise > 0] = { pg: voltage[output, Gnd] _ StepGen[ OnLevel, OffLevel, tRise, tDelay] }; -- Step