diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index fb4b396..a282e94 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -100,6 +100,10 @@ jobs: run: cabal run gatework -- --netlist fixtures/delay.net --duration 12 --output /tmp/delay.vcd --set a=0 --at 2 a=1 --at 6 a=0 - name: Compare the gate delay demo with the golden file run: diff fixtures/delay.golden.vcd /tmp/delay.vcd + - name: Run the asymmetric delay demo + run: cabal run gatework -- --netlist fixtures/asymdelay.net --duration 15 --output /tmp/asymdelay.vcd --set a=0 --at 1 a=1 --at 6 a=0 --at 11 a=1 + - name: Compare the asymmetric delay demo with the golden file + run: diff fixtures/asymdelay.golden.vcd /tmp/asymdelay.vcd - name: Confirm a missing library file stops the run run: | if cabal run gatework -- --netlist fixtures/libadder.net --library fixtures/missing.net --duration 0 --output /tmp/none.vcd 2>/tmp/none.log; then diff --git a/CHANGELOG.md b/CHANGELOG.md index 07b1bb4..a27db66 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -5,6 +5,25 @@ All notable changes to Gatework appear in this file. The format follows the Keep a Changelog convention. This project uses semantic versioning. +## [0.14.0.0] - 2026-08-04 + +### Added + +- Declare separate rise and fall delays with the `rise=N` and `fall=N` fields. +- A rising output transition fires after the rise delay. +- Any other transition fires after the fall delay. +- The `delay=N` field sets both delays to the same value. +- The `delay=N` field cannot combine with `rise=` or `fall=`. +- Reject negative, non-integer, repeated, and unknown delay fields. +- Add an asymmetric delay demo fixture and a golden waveform. +- Add deterministic tests and a QuickCheck property for asymmetric delays. + +### Changed + +- The scheduler picks the delay from the new output value. +- Bump the package version to 0.14.0.0. +- Update the golden VCD files to the new version string. + ## [0.13.0.0] - 2026-08-03 ### Added diff --git a/README.md b/README.md index a013828..ab6fc3b 100644 --- a/README.md +++ b/README.md @@ -51,6 +51,9 @@ You can do these tasks: - Declare a gate output delay with the `delay=N` field. - Watch a gate transition fire after its declared delay. - Let gate delays accumulate through a chain of gates. +- Declare separate rise and fall delays with the `rise=N` and `fall=N` fields. +- Watch a rising output fire after its rise delay. +- Watch a falling output fire after its fall delay. ## Architecture @@ -84,6 +87,8 @@ The scheduler processes only changed signals. The scheduler tracks one committed contribution per gate driver. The scheduler resolves several gate drivers into one wire value. A delayed gate commits its new value after its delay elapses. +A rising output uses the rise delay. +A falling output uses the fall delay. A gate delay accumulates through a chain of gates. A rising clock edge samples attached flip-flops together. An asserted reset forces flip-flop outputs to their initial values. @@ -515,6 +520,45 @@ The signal `x` rises at time 8. The signal `y` falls at time 11. The initial state settles at time zero without delay. +## Asymmetric delay demo + +Run one inverter with different rise and fall delays. + +```powershell +cabal run gatework -- --netlist fixtures/asymdelay.net --duration 15 --output asymdelay.vcd --set a=0 --at 1 a=1 --at 6 a=0 --at 11 a=1 +``` + +The command writes this output: + +```text +Wrote asymdelay.vcd +Signals: 2 +Duration: 15 time units +Assertions: 7 passed +``` + +The gate uses the `rise=4` and `fall=1` fields. +A rising output waits four time units. +A falling output waits one time unit. +The input changes stay farther apart than the longest delay. + +| Time | a | y | +| --- | --- | --- | +| 0 | 0 | 1 | +| 1 | 1 | 1 | +| 2 | 1 | 0 | +| 6 | 0 | 0 | +| 10 | 0 | 1 | +| 11 | 1 | 1 | +| 12 | 1 | 0 | + +The input `a` rises at time 1. +The output `y` falls at time 2, one unit later. +The input `a` falls at time 6. +The output `y` rises at time 10, four units later. +The input `a` rises at time 11. +The output `y` falls at time 12. + ## Bus demo Run four-bit bus operations with gates and a register. @@ -759,6 +803,35 @@ The value `b0101` means `a[3]=0`, `a[2]=1`, `a[1]=0`, and `a[0]=1`. The value `b1111` means every bit of `x` is high. The register output `q` changes together on the clock edge. +The file `fixtures/asymdelay.golden.vcd` holds the asymmetric delay demo waveform. +Its timeline shows the output fall one unit after the input rise. +The output rise comes four units after the input fall: + +```text +#0 +0! +0" +1" +#1 +1! +#2 +0" +#6 +0! +#10 +1" +#11 +1! +#12 +0" +``` + +Here `!` is the input `a` and `"` is the output `y`. +The input rises at time 1 and time 11. +The output falls one unit later at time 2 and time 12. +The input falls at time 6. +The output rises four units later at time 10. + ## Netlist format Use one declaration per line. @@ -814,11 +887,23 @@ A chain of gates adds the delays together. The example output `y` changes two units after `a`. The output `z` changes three units after `y`. -The initial state settles at time zero without delay. -Events at time zero ignore the gate delay. +A gate can use separate rise and fall delays. +The `rise=N` field delays a transition to high. +The `fall=N` field delays every other transition. +Omitted delays default to zero. + +```text +gate NOT slow (a) -> y rise=4 fall=1 +``` + +The `delay=N` field sets both delays to the same value. +The `delay=` field cannot combine with `rise=` or `fall=`. A delay field cannot repeat on one gate. An unknown gate field is an error. +The initial state settles at time zero without delay. +Events at time zero ignore the gate delay. + ### Multiple drivers One wire can have many gate drivers. @@ -1041,6 +1126,7 @@ Deterministic tests also cover whole-bus input values, their bit order, their er Deterministic tests also cover VCD vectors, their header declarations, their grouped values, four-state vector values, and module-internal bus vectors. Deterministic tests also cover gate delay parsing and invalid delay fields. Deterministic tests also cover delayed transitions, delay accumulation, zero-delay behavior, multi-driver delays, and the initial settle. +Deterministic tests also cover rise and fall delay parsing, conflict rules, direction-specific transitions, and the asymmetric delay demo. QuickCheck properties cover gate algebra, full adder correctness, scheduled input sampling, reset sampling, register width, and assertion soundness. QuickCheck properties also compare the hierarchical adder and counter with their flat versions. QuickCheck properties also cover the four-state model and the tri-state buffer truth table. @@ -1048,6 +1134,7 @@ QuickCheck properties also compare a bus circuit with a bitwise reference model. QuickCheck properties also compare the shared bus with a per-time resolution model. QuickCheck properties also compare a library adder with its flat version. QuickCheck properties also compare a delayed gate with a per-time reference model. +QuickCheck properties also compare an asymmetric delayed gate with a per-time reference model. QuickCheck properties also compare the counter report with the simulated waveform. QuickCheck properties also compare whole-bus input values with per-bit reference values. QuickCheck properties also compare every VCD vector value with the per-bit waveform. @@ -1071,6 +1158,7 @@ The library adder property compares a library netlist with the flat adder. The counter report property compares each report cell with the simulated value. The VCD vector property compares each vector value with the per-bit values at that time. The delayed-gate property compares each output sample with the reference input time. +The asymmetric-delay property compares each output sample with the directional reference. ## Test status @@ -1083,6 +1171,7 @@ CI runs the report demo and compares it with the report golden file. CI runs the bus demo with whole-bus input values. CI runs the four-state vector demo and compares it with its golden file. CI runs the gate delay demo and compares it with its golden file. +CI runs the asymmetric delay demo and compares it with its golden file. CI confirms that a missing library file stops the run. CI confirms that an invalid gate delay stops the run. @@ -1099,6 +1188,10 @@ A gate cannot drive a flip-flop output. Combinational loops stop with an event-limit error. A gate without a delay field uses zero delay. A gate delay applies to both rising and falling transitions. +A transition to high uses the rise delay. +Every other transition uses the fall delay. +The `delay=` field sets both delays to one value. +The `delay=` field cannot combine with `rise=` or `fall=`. The initial state settles at time zero without delay. Events at time zero ignore the gate delay. A delayed transition uses the input value at its fire time. @@ -1134,6 +1227,7 @@ The report prints every signal in the stable signal order. ## Roadmap +Release 0.14.0.0 completed separate rise and fall gate delays. Release 0.13.0.0 completed configurable gate delays. Release 0.12.0.0 completed multi-bit values in the VCD timeline. Release 0.11.0.0 completed whole-bus input values on the command line. @@ -1149,9 +1243,8 @@ Release 0.2.0.0 completed scheduled input transitions. Remaining work: -1. Add separate rise and fall delay fields. -2. Add a clock-to-output delay field for flip-flops. -3. Add a buffer gate to the gate library. +1. Add a clock-to-output delay field for flip-flops. +2. Add a buffer gate to the gate library. ## License diff --git a/fixtures/adder.golden.vcd b/fixtures/adder.golden.vcd index 29b3f4b..f268c3a 100644 --- a/fixtures/adder.golden.vcd +++ b/fixtures/adder.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.13.0.0 + gatework 0.14.0.0 $end $timescale 1ns $end $scope module gatework $end diff --git a/fixtures/assert.golden.vcd b/fixtures/assert.golden.vcd index 2f9f21f..f5688c9 100644 --- a/fixtures/assert.golden.vcd +++ b/fixtures/assert.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.13.0.0 + gatework 0.14.0.0 $end $comment assert y = 1 at 0 diff --git a/fixtures/asymdelay.golden.vcd b/fixtures/asymdelay.golden.vcd new file mode 100644 index 0000000..5b07e15 --- /dev/null +++ b/fixtures/asymdelay.golden.vcd @@ -0,0 +1,37 @@ +$date + generated deterministically by gatework +$end +$version + gatework 0.14.0.0 +$end +$comment + assert y = 1 at 0 + assert y = 1 at 1 + assert y = 0 at 2 + assert y = 0 at 9 + assert y = 1 at 10 + assert y = 1 at 11 + assert y = 0 at 12 +$end +$timescale 1ns $end +$scope module gatework $end +$var wire 1 ! a $end +$var wire 1 " y $end +$upscope $end +$enddefinitions $end +#0 +0! +0" +1" +#1 +1! +#2 +0" +#6 +0! +#10 +1" +#11 +1! +#12 +0" diff --git a/fixtures/asymdelay.net b/fixtures/asymdelay.net new file mode 100644 index 0000000..5e53870 --- /dev/null +++ b/fixtures/asymdelay.net @@ -0,0 +1,17 @@ +# Asymmetric gate delay demo. +# A rising output transition uses the rise delay. +# A falling output transition uses the fall delay. +# The input changes stay farther apart than the longest delay. +input a +output y +wire y + +gate NOT inv (a) -> y rise=4 fall=1 + +assert y = 1 at 0 +assert y = 1 at 1 +assert y = 0 at 2 +assert y = 0 at 9 +assert y = 1 at 10 +assert y = 1 at 11 +assert y = 0 at 12 diff --git a/fixtures/bus.golden.vcd b/fixtures/bus.golden.vcd index d810549..e0dab35 100644 --- a/fixtures/bus.golden.vcd +++ b/fixtures/bus.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.13.0.0 + gatework 0.14.0.0 $end $comment assert x[0] = 1 at 0 diff --git a/fixtures/counter.golden.vcd b/fixtures/counter.golden.vcd index 6d9cb0c..e05f567 100644 --- a/fixtures/counter.golden.vcd +++ b/fixtures/counter.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.13.0.0 + gatework 0.14.0.0 $end $timescale 1ns $end $scope module gatework $end diff --git a/fixtures/delay.golden.vcd b/fixtures/delay.golden.vcd index 33cd08d..17fd433 100644 --- a/fixtures/delay.golden.vcd +++ b/fixtures/delay.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.13.0.0 + gatework 0.14.0.0 $end $comment assert x = 1 at 0 diff --git a/fixtures/gates.golden.vcd b/fixtures/gates.golden.vcd index 99f113b..9307225 100644 --- a/fixtures/gates.golden.vcd +++ b/fixtures/gates.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.13.0.0 + gatework 0.14.0.0 $end $comment assert nand_out = 1 at 0 diff --git a/fixtures/haddader.golden.vcd b/fixtures/haddader.golden.vcd index 2720487..5f5e4aa 100644 --- a/fixtures/haddader.golden.vcd +++ b/fixtures/haddader.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.13.0.0 + gatework 0.14.0.0 $end $timescale 1ns $end $scope module gatework $end diff --git a/fixtures/hcounter.golden.vcd b/fixtures/hcounter.golden.vcd index ea1e1aa..d4aa37a 100644 --- a/fixtures/hcounter.golden.vcd +++ b/fixtures/hcounter.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.13.0.0 + gatework 0.14.0.0 $end $timescale 1ns $end $scope module gatework $end diff --git a/fixtures/libadder.golden.vcd b/fixtures/libadder.golden.vcd index 2720487..5f5e4aa 100644 --- a/fixtures/libadder.golden.vcd +++ b/fixtures/libadder.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.13.0.0 + gatework 0.14.0.0 $end $timescale 1ns $end $scope module gatework $end diff --git a/fixtures/reg2.golden.vcd b/fixtures/reg2.golden.vcd index c71c484..9afa6ed 100644 --- a/fixtures/reg2.golden.vcd +++ b/fixtures/reg2.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.13.0.0 + gatework 0.14.0.0 $end $timescale 1ns $end $scope module gatework $end diff --git a/fixtures/register.golden.vcd b/fixtures/register.golden.vcd index 32ebddd..2f04c02 100644 --- a/fixtures/register.golden.vcd +++ b/fixtures/register.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.13.0.0 + gatework 0.14.0.0 $end $timescale 1ns $end $scope module gatework $end diff --git a/fixtures/reset.golden.vcd b/fixtures/reset.golden.vcd index c631710..1694a8a 100644 --- a/fixtures/reset.golden.vcd +++ b/fixtures/reset.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.13.0.0 + gatework 0.14.0.0 $end $timescale 1ns $end $scope module gatework $end diff --git a/fixtures/shared.golden.vcd b/fixtures/shared.golden.vcd index 00b4158..8e05581 100644 --- a/fixtures/shared.golden.vcd +++ b/fixtures/shared.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.13.0.0 + gatework 0.14.0.0 $end $comment assert y = z at 0 diff --git a/fixtures/tristate.golden.vcd b/fixtures/tristate.golden.vcd index aacab25..e8d7098 100644 --- a/fixtures/tristate.golden.vcd +++ b/fixtures/tristate.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.13.0.0 + gatework 0.14.0.0 $end $comment assert y = z at 0 diff --git a/fixtures/unknown.golden.vcd b/fixtures/unknown.golden.vcd index ab2cba6..436149a 100644 --- a/fixtures/unknown.golden.vcd +++ b/fixtures/unknown.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.13.0.0 + gatework 0.14.0.0 $end $comment assert q = x at 0 diff --git a/fixtures/vector4.golden.vcd b/fixtures/vector4.golden.vcd index f3f20ee..e29fb26 100644 --- a/fixtures/vector4.golden.vcd +++ b/fixtures/vector4.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.13.0.0 + gatework 0.14.0.0 $end $comment assert x[0] = 1 at 0 diff --git a/gatework.cabal b/gatework.cabal index fec7630..235f3d3 100644 --- a/gatework.cabal +++ b/gatework.cabal @@ -1,6 +1,6 @@ cabal-version: 3.0 name: gatework -version: 0.13.0.0 +version: 0.14.0.0 synopsis: Event-driven digital logic simulation in Haskell description: Gatework parses typed netlists, runs combinational gates and D @@ -16,6 +16,7 @@ description: The command-line tool also sets a whole bus with one bit string. Buses render as multi-bit vectors in the VCD timeline. A gate can declare a delay with the delay=N field. + A gate can declare separate rise and fall delays. The scheduler delays each gate transition by the declared amount. GTKWave and other waveform viewers can open the output. homepage: https://github.com/DanielCuevas1208/gatework diff --git a/src/Gatework/Netlist.hs b/src/Gatework/Netlist.hs index fe208e0..0d603c5 100644 --- a/src/Gatework/Netlist.hs +++ b/src/Gatework/Netlist.hs @@ -53,7 +53,8 @@ data Gate = Gate , gateName :: String , gateInputs :: [String] , gateOutput :: String - , gateDelay :: Int + , gateRiseDelay :: Int + , gateFallDelay :: Int } deriving (Eq, Show) @@ -113,7 +114,7 @@ data RawDeclaration | RawOutput String Int | RawWire String Int | RawClock Clock - | RawGate GateType String [Ref] Ref Int + | RawGate GateType String [Ref] Ref Int Int | RawDff String Ref [Ref] [Ref] (Maybe String) (Maybe String) (Maybe Ref) | RawAssert Ref Logic Time | RawInstance String String [Ref] [Ref] @@ -314,8 +315,8 @@ parseLine (lineNumber, line) = case words line of outputRef <- parseRef lineNumber output unless (length inputRefs == gateArity gate) $ Left (lineError lineNumber ("gate " ++ name ++ " expects " ++ show (gateArity gate) ++ " inputs")) - delay <- parseGateFields lineNumber fields - pure (RawGate gate gateName' inputRefs outputRef delay) + (riseDelay, fallDelay) <- parseGateFields lineNumber fields + pure (RawGate gate gateName' inputRefs outputRef riseDelay fallDelay) ("dff" : name : fields) -> do dffName' <- parseIdentifier lineNumber name parsedFields <- mapM (parseField lineNumber) fields @@ -425,21 +426,56 @@ parseField lineNumber field = case break (== '=') field of | key `elem` ["clock", "d", "q", "init", "rst", "width"] && not (null value) -> Right (key, value) _ -> Left (lineError lineNumber ("invalid dff field: " ++ field)) -parseGateFields :: Int -> [String] -> Either String Int +data DelayField = DelayField | RiseField | FallField + deriving (Eq, Show) + +parseGateFields :: Int -> [String] -> Either String (Int, Int) parseGateFields lineNumber fields = do - values <- mapM parseOne fields - case [value | Just value <- values] of - [] -> Right 0 - [value] -> Right value + parsed <- mapM parseOne fields + let delays = [number | (DelayField, number) <- parsed] + rises = [number | (RiseField, number) <- parsed] + falls = [number | (FallField, number) <- parsed] + delay <- case delays of + [] -> Right Nothing + [number] -> Right (Just number) _ -> Left (lineError lineNumber "gate delay cannot repeat") + rise <- case rises of + [] -> Right 0 + [number] -> Right number + _ -> Left (lineError lineNumber "gate rise delay cannot repeat") + fall <- case falls of + [] -> Right 0 + [number] -> Right number + _ -> Left (lineError lineNumber "gate fall delay cannot repeat") + case delay of + Just number | null rises && null falls -> Right (number, number) + Just _ -> Left (lineError lineNumber "gate delay cannot combine with rise or fall") + Nothing -> Right (rise, fall) where parseOne field = case break (== '=') field of - ("delay", '=' : value) - | not (null value) -> Just <$> parseDelayValue value + (key, '=' : value) + | key `elem` ["delay", "rise", "fall"] + , not (null value) -> + (,) <$> parseKey key <*> parseDelayValue key value _ -> Left (lineError lineNumber ("invalid gate field: " ++ field)) - parseDelayValue value = case reads value of + parseKey key = case key of + "delay" -> Right DelayField + "rise" -> Right RiseField + "fall" -> Right FallField + _ -> Left (lineError lineNumber ("invalid gate field: " ++ key)) + parseDelayValue key value = case reads value of [(number, "")] | number >= 0 -> Right number - _ -> Left (lineError lineNumber ("gate delay must be a non-negative integer: " ++ value)) + _ -> + Left + ( lineError + lineNumber + ( delayLabel key ++ " must be a non-negative integer: " ++ value + ) + ) + delayLabel key = case key of + "rise" -> "gate rise delay" + "fall" -> "gate fall delay" + _ -> "gate delay" parseNonNegative :: Int -> String -> String -> Either String Int parseNonNegative lineNumber key token = case reads token of @@ -522,16 +558,17 @@ resolveDeclaration signatureModules widths declaration = case declaration of RawOutput name width -> Right (map OutputDeclaration (bitNames name width)) RawWire name width -> Right (map WireDeclaration (bitNames name width)) RawClock clock -> Right [ClockDeclaration clock] - RawGate gateKind name inputRefs outputRef delay -> - resolveGate widths gateKind name inputRefs outputRef delay + RawGate gateKind name inputRefs outputRef riseDelay fallDelay -> + resolveGate widths gateKind name inputRefs outputRef riseDelay fallDelay RawDff name clockRef dataRefs outRefs initText widthText resetRef -> resolveDff widths name clockRef dataRefs outRefs initText widthText resetRef RawAssert signalRef value time -> resolveAssertion widths signalRef value time RawInstance name targetModule inputRefs outputRefs -> resolveInstance signatureModules widths name targetModule inputRefs outputRefs -resolveGate :: Map String Int -> GateType -> String -> [Ref] -> Ref -> Int -> Either String [Declaration] -resolveGate widths gateKind name inputRefs outputRef delay = do +resolveGate :: Map String Int -> GateType -> String -> [Ref] -> Ref -> Int -> Int + -> Either String [Declaration] +resolveGate widths gateKind name inputRefs outputRef riseDelay fallDelay = do inputBits <- mapM (resolveRef widths) inputRefs outputBits <- resolveRef widths outputRef let width = length outputBits @@ -539,7 +576,14 @@ resolveGate widths gateKind name inputRefs outputRef delay = do Left ("gate " ++ name ++ " mixes bus widths") pure [ GateDeclaration - (Gate gateKind (componentName name width index) (map (!! index) inputBits) (outputBits !! index) delay) + ( Gate + gateKind + (componentName name width index) + (map (!! index) inputBits) + (outputBits !! index) + riseDelay + fallDelay + ) | index <- [0 .. width - 1] ] diff --git a/src/Gatework/Simulator.hs b/src/Gatework/Simulator.hs index 0ea6b9f..b36ced0 100644 --- a/src/Gatework/Simulator.hs +++ b/src/Gatework/Simulator.hs @@ -93,15 +93,22 @@ commitsForChanged byInput drivers state changedSignals = , evaluateGate state gate /= currentContribution drivers gate ] -scheduleCommits :: Time -> EventQueue -> [Gate] -> ([Pending], EventQueue) -scheduleCommits time queue commits = foldl' step ([], queue) commits +scheduleCommits :: Time -> EventQueue -> [Gate] -> WireState -> ([Pending], EventQueue) +scheduleCommits time queue commits state = foldl' step ([], queue) commits where - step (immediate, currentQueue) gate - | gateDelay gate == 0 || time == 0 = (immediate ++ [GateCommit gate], currentQueue) - | otherwise = - ( immediate - , Map.insertWith (++) (time + fromIntegral (gateDelay gate)) [GateCommit gate] currentQueue - ) + step (immediate, currentQueue) gate = + let delay = delayForOutput state gate + in if delay == 0 || time == 0 + then (immediate ++ [GateCommit gate], currentQueue) + else + ( immediate + , Map.insertWith (++) (time + fromIntegral delay) [GateCommit gate] currentQueue + ) + +delayForOutput :: WireState -> Gate -> Int +delayForOutput state gate = case evaluateGate state gate of + High -> gateRiseDelay gate + _ -> gateFallDelay gate commitContribution :: Map String [(Gate, Logic)] -> Gate -> Logic -> Map String [(Gate, Logic)] commitContribution drivers gate value = @@ -292,7 +299,8 @@ processSignalEvent netlist byInput duration time signal value pending queue stat if oldValue == Low && value == High then [FlipFlopBatch (edgeSamples netlist signal (simWireValues nextState))] else [] - (immediate, scheduledQueue) = scheduleCommits time queue commits + (immediate, scheduledQueue) = + scheduleCommits time queue commits (simWireValues nextState) in settleAtTime netlist byInput duration time (pending ++ flipFlopEvents ++ immediate) scheduledQueue nextState nextChanges (steps + 1) @@ -302,7 +310,8 @@ processFlipFlopBatch :: Netlist -> Map String [Gate] -> Time -> Time processFlipFlopBatch netlist byInput duration time samples pending queue state changes steps = let (nextState, nextChanges, changedOutputs) = foldl' applySample (state, changes, []) samples commits = commitsForChanged byInput (simDrivers nextState) (simWireValues nextState) changedOutputs - (immediate, scheduledQueue) = scheduleCommits time queue commits + (immediate, scheduledQueue) = + scheduleCommits time queue commits (simWireValues nextState) in settleAtTime netlist byInput duration time (pending ++ immediate) scheduledQueue nextState nextChanges (steps + 1) where applySample (currentState, currentChanges, changed) (flipFlop, index, value) = diff --git a/test/Spec.hs b/test/Spec.hs index e5e5c55..3c1f008 100644 --- a/test/Spec.hs +++ b/test/Spec.hs @@ -166,15 +166,20 @@ main = do , testMultiDriverResolution , testMultiDriverSettlesOnSchedule , testParserAcceptsGateDelay + , testParserAcceptsAsymmetricDelay , testParserRejectsNegativeDelay , testParserRejectsInvalidDelay , testParserRejectsUnknownGateField , testParserRejectsRepeatedDelay + , testParserRejectsDelayWithRiseOrFall , testDelayedGateTransitions , testDelayedGateChainAccumulates , testZeroDelayKeepsImmediateBehavior , testDelayedMultiDriverResolution , testDelayedInitialSettle + , testRisingTransitionUsesRiseDelay + , testFallingTransitionUsesFallDelay + , testGoldenAsymDelayVCD , testParserRejectsDuplicateDffOutput , testParserRejectsGateOnDffOutput , testParserRejectsInvalidClockPeriod @@ -337,6 +342,7 @@ main = do , ("bus module matches the flat circuit", quickCheckResult propBusModuleMatchesFlat) , ("shared bus follows the resolution model", quickCheckResult (propSharedBusResolution shared)) , ("delayed gates follow a reference model", quickCheckResult propDelayedGateMatchesReference) + , ("asymmetric delays follow a reference model", quickCheckResult propAsymmetricDelayMatchesReference) , ("library adder matches the flat adder", quickCheckResult (propLibraryAdderMatchesFlat adder libadder)) , ("counter report matches the waveform", quickCheckResult (propCounterReportMatchesWaveform counter)) , ("whole-bus values match per-bit values", quickCheckResult propWholeBusMatchesBitwise) @@ -455,28 +461,53 @@ testParserAcceptsGateDelay = case Left _ -> check "parser accepts a gate delay" False Right netlist -> check "parser accepts a gate delay" $ case netlistGates netlist of - [gate] -> gateDelay gate == 2 + [gate] -> gateRiseDelay gate == 2 && gateFallDelay gate == 2 + _ -> False + +testParserAcceptsAsymmetricDelay :: IO Bool +testParserAcceptsAsymmetricDelay = case + parseNetlist (unlines + [ "input a" + , "wire x" + , "gate NOT first (a) -> x rise=2 fall=3" + ]) of + Left _ -> check "parser accepts rise and fall delays" False + Right netlist -> check "parser accepts rise and fall delays" $ + case netlistGates netlist of + [gate] -> gateRiseDelay gate == 2 && gateFallDelay gate == 3 _ -> False testParserRejectsNegativeDelay :: IO Bool testParserRejectsNegativeDelay = - check "parser rejects a negative gate delay" $ isLeft $ - parseNetlist "input a\nwire x\ngate NOT first (a) -> x delay=-1" + check "parser rejects a negative gate delay" $ + isLeft (parseNetlist "input a\nwire x\ngate NOT first (a) -> x delay=-1") + && isLeft (parseNetlist "input a\nwire x\ngate NOT first (a) -> x rise=-1") + && isLeft (parseNetlist "input a\nwire x\ngate NOT first (a) -> x fall=-2") testParserRejectsInvalidDelay :: IO Bool testParserRejectsInvalidDelay = - check "parser rejects a non-integer gate delay" $ isLeft $ - parseNetlist "input a\nwire x\ngate NOT first (a) -> x delay=fast" + check "parser rejects a non-integer gate delay" $ + isLeft (parseNetlist "input a\nwire x\ngate NOT first (a) -> x delay=fast") + && isLeft (parseNetlist "input a\nwire x\ngate NOT first (a) -> x rise=fast") + && isLeft (parseNetlist "input a\nwire x\ngate NOT first (a) -> x fall=fast") testParserRejectsUnknownGateField :: IO Bool testParserRejectsUnknownGateField = check "parser rejects an unknown gate field" $ isLeft $ - parseNetlist "input a\nwire x\ngate NOT first (a) -> x delay=2 rise=1" + parseNetlist "input a\nwire x\ngate NOT first (a) -> x delay=2 hold=1" testParserRejectsRepeatedDelay :: IO Bool testParserRejectsRepeatedDelay = - check "parser rejects a repeated gate delay" $ isLeft $ - parseNetlist "input a\nwire x\ngate NOT first (a) -> x delay=1 delay=2" + check "parser rejects a repeated gate delay" $ + isLeft (parseNetlist "input a\nwire x\ngate NOT first (a) -> x delay=1 delay=2") + && isLeft (parseNetlist "input a\nwire x\ngate NOT first (a) -> x rise=1 rise=2") + && isLeft (parseNetlist "input a\nwire x\ngate NOT first (a) -> x fall=1 fall=2") + +testParserRejectsDelayWithRiseOrFall :: IO Bool +testParserRejectsDelayWithRiseOrFall = + check "parser rejects delay combined with rise or fall" $ + isLeft (parseNetlist "input a\nwire x\ngate NOT first (a) -> x delay=2 rise=1") + && isLeft (parseNetlist "input a\nwire x\ngate NOT first (a) -> x delay=2 fall=1") testDelayedGateTransitions :: IO Bool testDelayedGateTransitions = case @@ -572,6 +603,57 @@ testDelayedInitialSettle = case && valueAt simulation "y" 0 == Low Left _ -> False +testRisingTransitionUsesRiseDelay :: IO Bool +testRisingTransitionUsesRiseDelay = case + parseNetlist (unlines + [ "input a" + , "output y" + , "wire y" + , "gate NOT inv (a) -> y rise=4 fall=1" + ]) of + Left _ -> check "a rising output uses the rise delay" False + Right netlist -> check "a rising output uses the rise delay" $ case + simulateWithScheduledInputs netlist [("a", Low)] + [(1, "a", High), (6, "a", Low)] 12 of + Right simulation -> + valueAt simulation "y" 0 == High + && valueAt simulation "y" 2 == Low + && valueAt simulation "y" 9 == Low + && valueAt simulation "y" 10 == High + Left _ -> False + +testFallingTransitionUsesFallDelay :: IO Bool +testFallingTransitionUsesFallDelay = case + parseNetlist (unlines + [ "input a" + , "output y" + , "wire y" + , "gate NOT inv (a) -> y rise=1 fall=5" + ]) of + Left _ -> check "a falling output uses the fall delay" False + Right netlist -> check "a falling output uses the fall delay" $ case + simulateWithScheduledInputs netlist [("a", Low)] + [(1, "a", High), (7, "a", Low)] 14 of + Right simulation -> + valueAt simulation "y" 0 == High + && valueAt simulation "y" 5 == High + && valueAt simulation "y" 6 == Low + && valueAt simulation "y" 8 == High + Left _ -> False + +testGoldenAsymDelayVCD :: IO Bool +testGoldenAsymDelayVCD = do + source <- readFile "fixtures/asymdelay.net" + golden <- readFile "fixtures/asymdelay.golden.vcd" + let actual = do + netlist <- parseNetlist source + overrides <- resolveInputAssignments netlist [("a", "0")] + simulation <- + simulateWithScheduledInputs netlist overrides + [(1, "a", High), (6, "a", Low), (11, "a", High)] 15 + pure (renderVCD simulation) + check "asymdelay VCD matches golden file" (actual == Right golden) + testParserRejectsDuplicateDffOutput :: IO Bool testParserRejectsDuplicateDffOutput = check "parser rejects two flip-flops on one output" $ isLeft $ @@ -2538,6 +2620,55 @@ propDelayedGateMatchesReference = rest <- go time (remaining - 1) pure (time : rest) +propAsymmetricDelayMatchesReference :: Property +propAsymmetricDelayMatchesReference = + forAll (choose (1 :: Int, 4)) $ \rise -> + forAll (choose (1 :: Int, 4)) $ \fall -> + forAll (choose (0 :: Int, 4)) $ \count -> + forAll (spacedChanges (max rise fall + 1) count) $ \changes -> + forAll (choose (0 :: Int, 45)) $ \query -> + let source = unlines + [ "input a" + , "output y" + , "wire y" + , "gate NOT inv (a) -> y rise=" ++ show rise ++ " fall=" ++ show fall + ] + in case parseNetlist source of + Left _ -> property False + Right netlist -> + case simulateWithScheduledInputs netlist [("a", Low)] + [ (fromIntegral time, "a", value) | (time, value) <- changes ] 45 of + Left _ -> property False + Right simulation -> + property + ( all + (\queryTime -> + valueAt simulation "y" (fromIntegral queryTime) + == expectedAsymValue changes rise fall queryTime) + [0 .. query] + ) + where + logical = elements [Low, High] + spacedChanges gap count = go 0 count + where + go _ 0 = pure [] + go current remaining = do + delta <- choose (gap, gap + 6) + let time = current + delta + value <- logical + rest <- go time (remaining - 1) + pure ((time, value) : rest) + expectedAsymValue changes rise fall queryTime = go (reverse changes) + where + go [] = invertTwo Low + go ((time, value) : rest) + | queryTime >= time + commitDelay target = target + | otherwise = go rest + where + target = invertTwo value + commitDelay High = rise + commitDelay _ = fall + propNandInvertsAnd :: Logical -> Logical -> Bool propNandInvertsAnd (Logical left) (Logical right) = evalGate Nand [left, right] == not1 (and2 left right)